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 17676
[Adamek] p. 21Condition 3.1(b)df-cat 17676
[Adamek] p. 22Example 3.3(1)df-setc 18085
[Adamek] p. 24Example 3.3(4.c)0cat 17697  0funcg 49654  df-termc 50042
[Adamek] p. 24Example 3.3(4.d)df-prstc 50119  prsthinc 50033
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50147  df-mndtc 50147
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50143
[Adamek] p. 25Definition 3.5df-oppc 17720
[Adamek] p. 25Example 3.6(1)oduoppcciso 50135
[Adamek] p. 25Example 3.6(2)oppgoppcco 50160  oppgoppchom 50159  oppgoppcid 50161
[Adamek] p. 28Remark 3.9oppciso 17790
[Adamek] p. 28Remark 3.12invf1o 17778  invisoinvl 17799
[Adamek] p. 28Example 3.13idinv 17798  idiso 17797
[Adamek] p. 28Corollary 3.11inveq 17783
[Adamek] p. 28Definition 3.8df-inv 17757  df-iso 17758  dfiso2 17781
[Adamek] p. 28Proposition 3.10sectcan 17764
[Adamek] p. 29Remark 3.16cicer 17815  cicerALT 49615
[Adamek] p. 29Definition 3.15cic 17808  df-cic 17805
[Adamek] p. 29Definition 3.17df-func 17867
[Adamek] p. 29Proposition 3.14(1)invinv 17779
[Adamek] p. 29Proposition 3.14(2)invco 17780  isoco 17786
[Adamek] p. 30Remark 3.19df-func 17867
[Adamek] p. 30Example 3.20(1)idfucl 17890
[Adamek] p. 30Example 3.20(2)diag1 49873
[Adamek] p. 32Proposition 3.21funciso 17883
[Adamek] p. 33Example 3.26(1)discsnterm 50143  discthing 50030
[Adamek] p. 33Example 3.26(2)df-thinc 49987  prsthinc 50033  thincciso 50022  thincciso2 50024  thincciso3 50025  thinccisod 50023
[Adamek] p. 33Example 3.26(3)df-mndtc 50147
[Adamek] p. 33Proposition 3.23cofucl 17897  cofucla 49665
[Adamek] p. 34Remark 3.28(1)cofidfth 49731
[Adamek] p. 34Remark 3.28(2)catciso 18120  catcisoi 49969
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18175
[Adamek] p. 34Definition 3.27(2)df-fth 17916
[Adamek] p. 34Definition 3.27(3)df-full 17915
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18175
[Adamek] p. 35Corollary 3.32ffthiso 17940
[Adamek] p. 35Proposition 3.30(c)cofth 17946
[Adamek] p. 35Proposition 3.30(d)cofull 17945
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18160
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18160
[Adamek] p. 39Remark 3.422oppf 49701
[Adamek] p. 39Definition 3.41df-oppf 49692  funcoppc 17884
[Adamek] p. 39Definition 3.44.df-catc 18108  elcatchom 49966
[Adamek] p. 39Proposition 3.43(c)fthoppc 17934  fthoppf 49733
[Adamek] p. 39Proposition 3.43(d)fulloppc 17933  fulloppf 49732
[Adamek] p. 40Remark 3.48catccat 18117
[Adamek] p. 40Definition 3.470funcg 49654  df-catc 18108
[Adamek] p. 45Exercise 3Gincat 50170
[Adamek] p. 48Remark 4.2(2)cnelsubc 50173  nelsubc3 49640
[Adamek] p. 48Remark 4.2(3)imasubc 49720  imasubc2 49721  imasubc3 49725
[Adamek] p. 48Example 4.3(1.a)0subcat 17847
[Adamek] p. 48Example 4.3(1.b)catsubcat 17848
[Adamek] p. 48Definition 4.1(1)nelsubc3 49640
[Adamek] p. 48Definition 4.1(2)fullsubc 17859
[Adamek] p. 48Definition 4.1(a)df-subc 17821
[Adamek] p. 49Remark 4.4idsubc 49729
[Adamek] p. 49Remark 4.4(1)idemb 49728
[Adamek] p. 49Remark 4.4(2)idfullsubc 49730  ressffth 17949
[Adamek] p. 58Exercise 4Asetc1onsubc 50171
[Adamek] p. 83Definition 6.1df-nat 17955
[Adamek] p. 87Remark 6.14(a)fuccocl 17976
[Adamek] p. 87Remark 6.14(b)fucass 17980
[Adamek] p. 87Definition 6.15df-fuc 17956
[Adamek] p. 88Remark 6.16fuccat 17982
[Adamek] p. 101Definition 7.10funcg 49654  df-inito 17993
[Adamek] p. 101Example 7.2(3)0funcg 49654  df-termc 50042  initc 49660
[Adamek] p. 101Example 7.2 (6)irinitoringc 21504
[Adamek] p. 102Definition 7.4df-termo 17994  oppctermo 49805
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18021
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18025
[Adamek] p. 103Remark 7.8oppczeroo 49806
[Adamek] p. 103Definition 7.7df-zeroo 17995
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21505
[Adamek] p. 103Proposition 7.6termoeu1w 18028
[Adamek] p. 106Definition 7.19df-sect 17756
[Adamek] p. 107Example 7.20(7)thincinv 50038
[Adamek] p. 108Example 7.25(4)thincsect2 50037
[Adamek] p. 110Example 7.33(9)thincmon 50002
[Adamek] p. 110Proposition 7.35sectmon 17791
[Adamek] p. 112Proposition 7.42sectepi 17793
[Adamek] p. 185Section 10.67updjud 9882
[Adamek] p. 193Definition 11.1(1)df-lmd 50214
[Adamek] p. 193Definition 11.3(1)df-lmd 50214
[Adamek] p. 194Definition 11.3(2)df-lmd 50214
[Adamek] p. 202Definition 11.27(1)df-cmd 50215
[Adamek] p. 202Definition 11.27(2)df-cmd 50215
[Adamek] p. 478Item Rngdf-ringc 20668
[AhoHopUll] p. 2Section 1.1df-bigo 49118
[AhoHopUll] p. 12Section 1.3df-blen 49140
[AhoHopUll] p. 318Section 9.1df-concat 14574  df-pfx 14675  df-substr 14645  df-word 14517  lencl 14536  wrd0 14542
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24741  df-nmoo 30887
[AkhiezerGlazman] p. 64Theoremhmopidmch 32295  hmopidmchi 32293
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32343  pjcmul2i 32344
[AkhiezerGlazman] p. 72Theoremcnvunop 32060  unoplin 32062
[AkhiezerGlazman] p. 72Equation 2unopadj 32061  unopadj2 32080
[AkhiezerGlazman] p. 73Theoremelunop2 32155  lnopunii 32154
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32228
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27990
[Alling] p. 184Axiom Bbdayfo 27711
[Alling] p. 184Axiom Oltsso 27710
[Alling] p. 184Axiom SDnodense 27726
[Alling] p. 185Lemma 0nocvxmin 27818
[Alling] p. 185Theoremconway 27842
[Alling] p. 185Axiom FEnoeta 27777
[Alling] p. 186Theorem 4lesrec 27862  lesrecd 27863
[Alling], p. 2Definitionrp-brsslt 43947
[Alling], p. 3Notenla0001 43950  nla0002 43948  nla0003 43949
[Apostol] p. 18Theorem I.1addcan 11357  addcan2d 11377  addcan2i 11367  addcand 11376  addcani 11366
[Apostol] p. 18Theorem I.2negeu 11410
[Apostol] p. 18Theorem I.3negsub 11469  negsubd 11538  negsubi 11499
[Apostol] p. 18Theorem I.4negneg 11471  negnegd 11523  negnegi 11491
[Apostol] p. 18Theorem I.5subdi 11610  subdid 11633  subdii 11626  subdir 11611  subdird 11634  subdiri 11627
[Apostol] p. 18Theorem I.6mul01 11352  mul01d 11372  mul01i 11363  mul02 11351  mul02d 11371  mul02i 11362
[Apostol] p. 18Theorem I.7mulcan 11814  mulcan2d 11811  mulcand 11810  mulcani 11816
[Apostol] p. 18Theorem I.8receu 11822  xreceu 33053
[Apostol] p. 18Theorem I.9divrec 11851  divrecd 11960  divreci 11926  divreczi 11919
[Apostol] p. 18Theorem I.10recrec 11878  recreci 11913
[Apostol] p. 18Theorem I.11mul0or 11817  mul0ord 11825  mul0ori 11824
[Apostol] p. 18Theorem I.12mul2neg 11616  mul2negd 11632  mul2negi 11625  mulneg1 11613  mulneg1d 11630  mulneg1i 11623
[Apostol] p. 18Theorem I.13divadddiv 11896  divadddivd 12001  divadddivi 11943
[Apostol] p. 18Theorem I.14divmuldiv 11881  divmuldivd 11998  divmuldivi 11941  rdivmuldivd 20434
[Apostol] p. 18Theorem I.15divdivdiv 11882  divdivdivd 12004  divdivdivi 11944
[Apostol] p. 20Axiom 7rpaddcl 13007  rpaddcld 13042  rpmulcl 13008  rpmulcld 13043
[Apostol] p. 20Axiom 8rpneg 13017
[Apostol] p. 20Axiom 90nrp 13020
[Apostol] p. 20Theorem I.17lttri 11299
[Apostol] p. 20Theorem I.18ltadd1d 11770  ltadd1dd 11788  ltadd1i 11731
[Apostol] p. 20Theorem I.19ltmul1 12031  ltmul1a 12030  ltmul1i 12100  ltmul1ii 12110  ltmul2 12032  ltmul2d 13069  ltmul2dd 13083  ltmul2i 12103
[Apostol] p. 20Theorem I.20msqgt0 11697  msqgt0d 11744  msqgt0i 11714
[Apostol] p. 20Theorem I.210lt1 11699
[Apostol] p. 20Theorem I.23lt0neg1 11683  lt0neg1d 11746  ltneg 11677  ltnegd 11755  ltnegi 11721
[Apostol] p. 20Theorem I.25lt2add 11662  lt2addd 11800  lt2addi 11739
[Apostol] p. 20Definition of positive numbersdf-rp 12984
[Apostol] p. 21Exercise 4recgt0 12027  recgt0d 12116  recgt0i 12087  recgt0ii 12088
[Apostol] p. 22Definition of integersdf-z 12559
[Apostol] p. 22Definition of positive integersdfnn3 12214
[Apostol] p. 22Definition of rationalsdf-q 12940
[Apostol] p. 24Theorem I.26supeu 9390
[Apostol] p. 26Theorem I.28nnunb 12467
[Apostol] p. 26Theorem I.29arch 12468  archd 45688
[Apostol] p. 28Exercise 2btwnz 12666
[Apostol] p. 28Exercise 3nnrecl 12469
[Apostol] p. 28Exercise 4rebtwnz 12938
[Apostol] p. 28Exercise 5zbtwnre 12937
[Apostol] p. 28Exercise 6qbtwnre 13192
[Apostol] p. 28Exercise 10(a)zeneo 16349  zneo 12646  zneoALTV 48239
[Apostol] p. 29Theorem I.35cxpsqrtth 26765  msqsqrtd 15446  resqrtth 15258  sqrtth 15368  sqrtthi 15374  sqsqrtd 15445
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12203
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12904
[Apostol] p. 361Remarkcrreczi 14231
[Apostol] p. 363Remarkabsgt0i 15403
[Apostol] p. 363Exampleabssubd 15459  abssubi 15407
[ApostolNT] p. 7Remarkfmtno0 48097  fmtno1 48098  fmtno2 48107  fmtno3 48108  fmtno4 48109  fmtno5fac 48139  fmtnofz04prm 48134
[ApostolNT] p. 7Definitiondf-fmtno 48085
[ApostolNT] p. 8Definitiondf-ppi 27134
[ApostolNT] p. 14Definitiondf-dvds 16263
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16279
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16304
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16299
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16292
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16294
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16280
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16281
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16286
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16321
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16323
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16325
[ApostolNT] p. 15Definitiondf-gcd 16505  dfgcd2 16556
[ApostolNT] p. 16Definitionisprm2 16692
[ApostolNT] p. 16Theorem 1.5coprmdvds 16663
[ApostolNT] p. 16Theorem 1.7prminf 16927
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16523
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16557
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16559
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16538
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16530
[ApostolNT] p. 17Theorem 1.8coprm 16722
[ApostolNT] p. 17Theorem 1.9euclemma 16724
[ApostolNT] p. 17Theorem 1.101arith2 16940
[ApostolNT] p. 18Theorem 1.13prmrec 16934
[ApostolNT] p. 19Theorem 1.14divalg 16413
[ApostolNT] p. 20Theorem 1.15eucalg 16597
[ApostolNT] p. 24Definitiondf-mu 27135
[ApostolNT] p. 25Definitiondf-phi 16777
[ApostolNT] p. 25Theorem 2.1musum 27225
[ApostolNT] p. 26Theorem 2.2phisum 16802
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16787
[ApostolNT] p. 28Theorem 2.5(c)phimul 16791
[ApostolNT] p. 32Definitiondf-vma 27132
[ApostolNT] p. 32Theorem 2.9muinv 27227
[ApostolNT] p. 32Theorem 2.10vmasum 27250
[ApostolNT] p. 38Remarkdf-sgm 27136
[ApostolNT] p. 38Definitiondf-sgm 27136
[ApostolNT] p. 75Definitiondf-chp 27133  df-cht 27131
[ApostolNT] p. 104Definitioncongr 16674
[ApostolNT] p. 106Remarkdvdsval3 16266
[ApostolNT] p. 106Definitionmoddvds 16273
[ApostolNT] p. 107Example 2mod2eq0even 16356
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16357
[ApostolNT] p. 107Example 4zmod1congr 13888
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13928
[ApostolNT] p. 107Theorem 5.2(c)modexp 14241
[ApostolNT] p. 108Theorem 5.3modmulconst 16298
[ApostolNT] p. 109Theorem 5.4cncongr1 16677
[ApostolNT] p. 109Theorem 5.6gcdmodi 17086
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16679
[ApostolNT] p. 113Theorem 5.17eulerth 16794
[ApostolNT] p. 113Theorem 5.18vfermltl 16813
[ApostolNT] p. 114Theorem 5.19fermltl 16795
[ApostolNT] p. 116Theorem 5.24wilthimp 27106
[ApostolNT] p. 179Definitiondf-lgs 27329  lgsprme0 27373
[ApostolNT] p. 180Example 11lgs 27374
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27350
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27365
[ApostolNT] p. 181Theorem 9.4m1lgs 27422
[ApostolNT] p. 181Theorem 9.52lgs 27441  2lgsoddprm 27450
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27408
[ApostolNT] p. 185Theorem 9.8lgsquad 27417
[ApostolNT] p. 188Definitiondf-lgs 27329  lgs1 27375
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27366
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27368
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27376
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27377
[Baer] p. 40Property (b)mapdord 42210
[Baer] p. 40Property (c)mapd11 42211
[Baer] p. 40Property (e)mapdin 42234  mapdlsm 42236
[Baer] p. 40Property (f)mapd0 42237
[Baer] p. 40Definition of projectivitydf-mapd 42197  mapd1o 42220
[Baer] p. 41Property (g)mapdat 42239
[Baer] p. 44Part (1)mapdpg 42278
[Baer] p. 45Part (2)hdmap1eq 42373  mapdheq 42300  mapdheq2 42301  mapdheq2biN 42302
[Baer] p. 45Part (3)baerlem3 42285
[Baer] p. 46Part (4)mapdheq4 42304  mapdheq4lem 42303
[Baer] p. 46Part (5)baerlem5a 42286  baerlem5abmN 42290  baerlem5amN 42288  baerlem5b 42287  baerlem5bmN 42289
[Baer] p. 47Part (6)hdmap1l6 42393  hdmap1l6a 42381  hdmap1l6e 42386  hdmap1l6f 42387  hdmap1l6g 42388  hdmap1l6lem1 42379  hdmap1l6lem2 42380  mapdh6N 42319  mapdh6aN 42307  mapdh6eN 42312  mapdh6fN 42313  mapdh6gN 42314  mapdh6lem1N 42305  mapdh6lem2N 42306
[Baer] p. 48Part 9hdmapval 42400
[Baer] p. 48Part 10hdmap10 42412
[Baer] p. 48Part 11hdmapadd 42415
[Baer] p. 48Part (6)hdmap1l6h 42389  mapdh6hN 42315
[Baer] p. 48Part (7)mapdh75cN 42325  mapdh75d 42326  mapdh75e 42324  mapdh75fN 42327  mapdh7cN 42321  mapdh7dN 42322  mapdh7eN 42320  mapdh7fN 42323
[Baer] p. 48Part (8)mapdh8 42360  mapdh8a 42347  mapdh8aa 42348  mapdh8ab 42349  mapdh8ac 42350  mapdh8ad 42351  mapdh8b 42352  mapdh8c 42353  mapdh8d 42355  mapdh8d0N 42354  mapdh8e 42356  mapdh8g 42357  mapdh8i 42358  mapdh8j 42359
[Baer] p. 48Part (9)mapdh9a 42361
[Baer] p. 48Equation 10mapdhvmap 42341
[Baer] p. 49Part 12hdmap11 42420  hdmapeq0 42416  hdmapf1oN 42437  hdmapneg 42418  hdmaprnN 42436  hdmaprnlem1N 42421  hdmaprnlem3N 42422  hdmaprnlem3uN 42423  hdmaprnlem4N 42425  hdmaprnlem6N 42426  hdmaprnlem7N 42427  hdmaprnlem8N 42428  hdmaprnlem9N 42429  hdmapsub 42419
[Baer] p. 49Part 14hdmap14lem1 42440  hdmap14lem10 42449  hdmap14lem1a 42438  hdmap14lem2N 42441  hdmap14lem2a 42439  hdmap14lem3 42442  hdmap14lem8 42447  hdmap14lem9 42448
[Baer] p. 50Part 14hdmap14lem11 42450  hdmap14lem12 42451  hdmap14lem13 42452  hdmap14lem14 42453  hdmap14lem15 42454  hgmapval 42459
[Baer] p. 50Part 15hgmapadd 42466  hgmapmul 42467  hgmaprnlem2N 42469  hgmapvs 42463
[Baer] p. 50Part 16hgmaprnN 42473
[Baer] p. 110Lemma 1hdmapip0com 42489
[Baer] p. 110Line 27hdmapinvlem1 42490
[Baer] p. 110Line 28hdmapinvlem2 42491
[Baer] p. 110Line 30hdmapinvlem3 42492
[Baer] p. 110Part 1.2hdmapglem5 42494  hgmapvv 42498
[Baer] p. 110Proposition 1hdmapinvlem4 42493
[Baer] p. 111Line 10hgmapvvlem1 42495
[Baer] p. 111Line 15hdmapg 42502  hdmapglem7 42501
[Bauer], p. 483Theorem 1.22irrexpq 26766  2irrexpqALT 26835
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2590
[BellMachover] p. 460Notationdf-mo 2560
[BellMachover] p. 460Definitionmo3 2585
[BellMachover] p. 461Axiom Extax-ext 2728
[BellMachover] p. 462Theorem 1.1axextmo 2732
[BellMachover] p. 463Axiom Repaxrep5 5229
[BellMachover] p. 463Scheme Sepax-sep 5240
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37497  sepex 5244
[BellMachover] p. 466Problemaxpow2 5318
[BellMachover] p. 466Axiom Powaxpow3 5319
[BellMachover] p. 466Axiom Unionaxun2 7709
[BellMachover] p. 468Definitiondf-ord 6338
[BellMachover] p. 469Theorem 2.2(i)ordirr 6353
[BellMachover] p. 469Theorem 2.2(iii)onelon 6360
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6355
[BellMachover] p. 471Definition of Ndf-om 7836
[BellMachover] p. 471Problem 2.5(ii)uniordint 7773
[BellMachover] p. 471Definition of Limdf-lim 6340
[BellMachover] p. 472Axiom Infzfinf2 9587
[BellMachover] p. 473Theorem 2.8limom 7851
[BellMachover] p. 477Equation 3.1df-r1 9712
[BellMachover] p. 478Definitionrankval2 9766  rankval2b 35350
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9730  r1ord3g 9727
[BellMachover] p. 480Axiom Regzfreg 9534
[BellMachover] p. 488Axiom ACac5 10424  dfac4 10068
[BellMachover] p. 490Definition of alephalephval3 10056
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39891
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32495
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32537  chirredi 32536
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32525
[Beran] p. 3Definition of joinsshjval3 31496
[Beran] p. 39Theorem 2.3(i)cmcm2 31758  cmcm2i 31735  cmcm2ii 31740  cmt2N 39822
[Beran] p. 40Theorem 2.3(iii)lecm 31759  lecmi 31744  lecmii 31745
[Beran] p. 45Theorem 3.4cmcmlem 31733
[Beran] p. 49Theorem 4.2cm2j 31762  cm2ji 31767  cm2mi 31768
[Beran] p. 95Definitiondf-sh 31349  issh2 31351
[Beran] p. 95Lemma 3.1(S5)his5 31228
[Beran] p. 95Lemma 3.1(S6)his6 31241
[Beran] p. 95Lemma 3.1(S7)his7 31232
[Beran] p. 95Lemma 3.2(S8)ho01i 31970
[Beran] p. 95Lemma 3.2(S9)hoeq1 31972
[Beran] p. 95Lemma 3.2(S10)ho02i 31971
[Beran] p. 95Lemma 3.2(S11)hoeq2 31973
[Beran] p. 95Postulate (S1)ax-his1 31224  his1i 31242
[Beran] p. 95Postulate (S2)ax-his2 31225
[Beran] p. 95Postulate (S3)ax-his3 31226
[Beran] p. 95Postulate (S4)ax-his4 31227
[Beran] p. 96Definition of normdf-hnorm 31110  dfhnorm2 31264  normval 31266
[Beran] p. 96Definition for Cauchy sequencehcau 31326
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31115
[Beran] p. 96Definition of complete subspaceisch3 31383
[Beran] p. 96Definition of convergedf-hlim 31114  hlimi 31330
[Beran] p. 97Theorem 3.3(i)norm-i-i 31275  norm-i 31271
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31279  norm-ii 31280  normlem0 31251  normlem1 31252  normlem2 31253  normlem3 31254  normlem4 31255  normlem5 31256  normlem6 31257  normlem7 31258  normlem7tALT 31261
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31281  norm-iii 31282
[Beran] p. 98Remark 3.4bcs 31323  bcsiALT 31321  bcsiHIL 31322
[Beran] p. 98Remark 3.4(B)normlem9at 31263  normpar 31297  normpari 31296
[Beran] p. 98Remark 3.4(C)normpyc 31288  normpyth 31287  normpythi 31284
[Beran] p. 99Remarklnfn0 32189  lnfn0i 32184  lnop0 32108  lnop0i 32112
[Beran] p. 99Theorem 3.5(i)nmcexi 32168  nmcfnex 32195  nmcfnexi 32193  nmcopex 32171  nmcopexi 32169
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32196  nmcfnlbi 32194  nmcoplb 32172  nmcoplbi 32170
[Beran] p. 99Theorem 3.5(iii)lnfncon 32198  lnfnconi 32197  lnopcon 32177  lnopconi 32176
[Beran] p. 100Lemma 3.6normpar2i 31298
[Beran] p. 101Lemma 3.6norm3adifi 31295  norm3adifii 31290  norm3dif 31292  norm3difi 31289
[Beran] p. 102Theorem 3.7(i)chocunii 31443  pjhth 31535  pjhtheu 31536  pjpjhth 31567  pjpjhthi 31568  pjth 25474
[Beran] p. 102Theorem 3.7(ii)ococ 31548  ococi 31547
[Beran] p. 103Remark 3.8nlelchi 32203
[Beran] p. 104Theorem 3.9riesz3i 32204  riesz4 32206  riesz4i 32205
[Beran] p. 104Theorem 3.10cnlnadj 32221  cnlnadjeu 32220  cnlnadjeui 32219  cnlnadji 32218  cnlnadjlem1 32209  nmopadjlei 32230
[Beran] p. 106Theorem 3.11(i)adjeq0 32233
[Beran] p. 106Theorem 3.11(v)nmopadji 32232
[Beran] p. 106Theorem 3.11(ii)adjmul 32234
[Beran] p. 106Theorem 3.11(iv)adjadj 32078
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32244  nmopcoadji 32243
[Beran] p. 106Theorem 3.11(iii)adjadd 32235
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32245
[Beran] p. 106Theorem 3.11(viii)adjcoi 32242  pjadj2coi 32346  pjadjcoi 32303
[Beran] p. 107Definitiondf-ch 31363  isch2 31365
[Beran] p. 107Remark 3.12choccl 31448  isch3 31383  occl 31446  ocsh 31425  shoccl 31447  shocsh 31426
[Beran] p. 107Remark 3.12(B)ococin 31550
[Beran] p. 108Theorem 3.13chintcl 31474
[Beran] p. 109Property (i)pjadj2 32329  pjadj3 32330  pjadji 31827  pjadjii 31816
[Beran] p. 109Property (ii)pjidmco 32323  pjidmcoi 32319  pjidmi 31815
[Beran] p. 110Definition of projector orderingpjordi 32315
[Beran] p. 111Remarkho0val 31892  pjch1 31812
[Beran] p. 111Definitiondf-hfmul 31876  df-hfsum 31875  df-hodif 31874  df-homul 31873  df-hosum 31872
[Beran] p. 111Lemma 4.4(i)pjo 31813
[Beran] p. 111Lemma 4.4(ii)pjch 31836  pjchi 31574
[Beran] p. 111Lemma 4.4(iii)pjoc2 31581  pjoc2i 31580
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31822
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32307  pjssmii 31823
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32306
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32305
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32310
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32308  pjssge0ii 31824
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32309  pjdifnormii 31825
[Bobzien] p. 116Statement T3stoic3 1790
[Bobzien] p. 117Statement T2stoic2a 1788
[Bobzien] p. 117Statement T4stoic4a 1791
[Bobzien] p. 117Conclusion the contradictorystoic1a 1786
[Bogachev] p. 16Definition 1.5df-oms 34543
[Bogachev] p. 17Lemma 1.5.4omssubadd 34551
[Bogachev] p. 17Example 1.5.2omsmon 34549
[Bogachev] p. 41Definition 1.11.2df-carsg 34553
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34573
[Bogachev] p. 116Definition 2.3.1df-itgm 34604  df-sitm 34582
[Bogachev] p. 118Chapter 2.4.4df-itgm 34604
[Bogachev] p. 118Definition 2.4.1df-sitg 34581
[Bollobas] p. 1Section I.1df-edg 29188  isuhgrop 29210  isusgrop 29302  isuspgrop 29301
[Bollobas] p. 2Section I.1df-isubgr 48431  df-subgr 29408  uhgrspan1 29443  uhgrspansubgr 29431
[Bollobas] p. 3Definitiondf-gric 48451  gricuspgr 48488  isuspgrim 48466
[Bollobas] p. 3Section I.1cusgrsize 29594  df-clnbgr 48389  df-cusgr 29552  df-nbgr 29473  fusgrmaxsize 29604
[Bollobas] p. 4Definitiondf-upwlks 48704  df-wlks 29739
[Bollobas] p. 4Section I.1finsumvtxdg2size 29690  finsumvtxdgeven 29692  fusgr1th 29691  fusgrvtxdgonume 29694  vtxdgoddnumeven 29693
[Bollobas] p. 5Notationdf-pths 29853
[Bollobas] p. 5Definitiondf-crcts 29925  df-cycls 29926  df-trls 29830  df-wlkson 29740
[Bollobas] p. 7Section I.1df-ushgr 29199
[BourbakiAlg1] p. 1Definition 1df-clintop 48770  df-cllaw 48756  df-mgm 18650  df-mgm2 48789
[BourbakiAlg1] p. 4Definition 5df-assintop 48771  df-asslaw 48758  df-sgrp 18729  df-sgrp2 48791
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48790  df-comlaw 48757
[BourbakiAlg1] p. 12Definition 2df-mnd 18745
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33158  mndlactf1o 33162  mndractf1 33160  mndractf1o 33163
[BourbakiAlg1] p. 92Definition 1df-ring 20257
[BourbakiAlg1] p. 93Section I.8.1df-rng 20175
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33884
[BourbakiAlg2] p. 113Chapter 5.assafld 33888  assarrginv 33887
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33929  fldextrspunfld 33927  fldextrspunlem1 33926  fldextrspunlem2 33928  fldextrspunlsp 33925  fldextrspunlsplem 33924
[BourbakiCAlg2], p. 228Proposition 21arithidom 33687  dfufd2 33700
[BourbakiEns] p. Proposition 8fcof1 7260  fcofo 7261
[BourbakiTop1] p. Remarkxnegmnf 13203  xnegpnf 13202
[BourbakiTop1] p. Remark rexneg 13204
[BourbakiTop1] p. Remark 3ust0 24253  ustfilxp 24246
[BourbakiTop1] p. Axiom GT'tgpsubcn 24123
[BourbakiTop1] p. Criterionishmeo 23792
[BourbakiTop1] p. Example 1cstucnd 24316  iducn 24315  snfil 23897
[BourbakiTop1] p. Example 2neifil 23913
[BourbakiTop1] p. Theorem 1cnextcn 24100
[BourbakiTop1] p. Theorem 2ucnextcn 24336
[BourbakiTop1] p. Theorem 3df-hcmp 34208
[BourbakiTop1] p. Paragraph 3infil 23896
[BourbakiTop1] p. Definition 1df-ucn 24308  df-ust 24234  filintn0 23894  filn0 23895  istgp 24110  ucnprima 24314
[BourbakiTop1] p. Definition 2df-cfilu 24319
[BourbakiTop1] p. Definition 3df-cusp 24330  df-usp 24290  df-utop 24264  trust 24262
[BourbakiTop1] p. Definition 6df-pcmp 34107
[BourbakiTop1] p. Property V_issnei2 23149
[BourbakiTop1] p. Theorem 1(d)iscncl 23302
[BourbakiTop1] p. Condition F_Iustssel 24239
[BourbakiTop1] p. Condition U_Iustdiag 24242
[BourbakiTop1] p. Property V_iiinnei 23158
[BourbakiTop1] p. Property V_ivneiptopreu 23166  neissex 23160
[BourbakiTop1] p. Proposition 1neips 23146  neiss 23142  ucncn 24317  ustund 24255  ustuqtop 24279
[BourbakiTop1] p. Proposition 2cnpco 23300  neiptopreu 23166  utop2nei 24283  utop3cls 24284
[BourbakiTop1] p. Proposition 3fmucnd 24324  uspreg 24306  utopreg 24285
[BourbakiTop1] p. Proposition 4imasncld 23724  imasncls 23725  imasnopn 23723
[BourbakiTop1] p. Proposition 9cnpflf2 24033
[BourbakiTop1] p. Condition F_IIustincl 24241
[BourbakiTop1] p. Condition U_IIustinvel 24243
[BourbakiTop1] p. Property V_iiielnei 23144
[BourbakiTop1] p. Proposition 11cnextucn 24335
[BourbakiTop1] p. Condition F_IIbustbasel 24240
[BourbakiTop1] p. Condition U_IIIustexhalf 24244
[BourbakiTop1] p. Definition C'''df-cmp 23420
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23879
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22927
[BourbakiTop2] p. 195Definition 1df-ldlf 34104
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46584
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46586  stoweid 46585
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46523  stoweidlem10 46532  stoweidlem14 46536  stoweidlem15 46537  stoweidlem35 46557  stoweidlem36 46558  stoweidlem37 46559  stoweidlem38 46560  stoweidlem40 46562  stoweidlem41 46563  stoweidlem43 46565  stoweidlem44 46566  stoweidlem46 46568  stoweidlem5 46527  stoweidlem50 46572  stoweidlem52 46574  stoweidlem53 46575  stoweidlem55 46577  stoweidlem56 46578
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46545  stoweidlem24 46546  stoweidlem27 46549  stoweidlem28 46550  stoweidlem30 46552
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46556  stoweidlem59 46581  stoweidlem60 46582
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46567  stoweidlem49 46571  stoweidlem7 46529
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46553  stoweidlem39 46561  stoweidlem42 46564  stoweidlem48 46570  stoweidlem51 46573  stoweidlem54 46576  stoweidlem57 46579  stoweidlem58 46580
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46547
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46539
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46533  stoweidlem13 46535  stoweidlem26 46548  stoweidlem61 46583
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46540
[Bruck] p. 1Section I.1df-clintop 48770  df-mgm 18650  df-mgm2 48789
[Bruck] p. 23Section II.1df-sgrp 18729  df-sgrp2 48791
[Bruck] p. 28Theorem 3.2dfgrp3 19057
[ChoquetDD] p. 2Definition of mappingdf-mpt 5176
[Church] p. 129Section II.24df-ifp 1072  dfifp2 1073
[Clemente] p. 10Definition ITnatded 30544
[Clemente] p. 10Definition I` `m,nnatded 30544
[Clemente] p. 11Definition E=>m,nnatded 30544
[Clemente] p. 11Definition I=>m,nnatded 30544
[Clemente] p. 11Definition E` `(1)natded 30544
[Clemente] p. 11Definition E` `(2)natded 30544
[Clemente] p. 12Definition E` `m,n,pnatded 30544
[Clemente] p. 12Definition I` `n(1)natded 30544
[Clemente] p. 12Definition I` `n(2)natded 30544
[Clemente] p. 13Definition I` `m,n,pnatded 30544
[Clemente] p. 14Proof 5.11natded 30544
[Clemente] p. 14Definition E` `nnatded 30544
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30546  ex-natded5.2 30545
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30549  ex-natded5.3 30548
[Clemente] p. 18Theorem 5.5ex-natded5.5 30551
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30553  ex-natded5.7 30552
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30555  ex-natded5.8 30554
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30557  ex-natded5.13 30556
[Clemente] p. 32Definition I` `nnatded 30544
[Clemente] p. 32Definition E` `m,n,p,anatded 30544
[Clemente] p. 32Definition E` `n,tnatded 30544
[Clemente] p. 32Definition I` `n,tnatded 30544
[Clemente] p. 43Theorem 9.20ex-natded9.20 30558
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30559
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30561  ex-natded9.26 30560
[Cohen] p. 301Remarkrelogoprlem 26626
[Cohen] p. 301Property 2relogmul 26627  relogmuld 26660
[Cohen] p. 301Property 3relogdiv 26628  relogdivd 26661
[Cohen] p. 301Property 4relogexp 26631
[Cohen] p. 301Property 1alog1 26620
[Cohen] p. 301Property 1bloge 26621
[Cohen4] p. 348Observationrelogbcxpb 26822
[Cohen4] p. 349Propertyrelogbf 26826
[Cohen4] p. 352Definitionelogb 26805
[Cohen4] p. 361Property 2relogbmul 26812
[Cohen4] p. 361Property 3logbrec 26817  relogbdiv 26814
[Cohen4] p. 361Property 4relogbreexp 26810
[Cohen4] p. 361Property 6relogbexp 26815
[Cohen4] p. 361Property 1(a)logbid1 26803
[Cohen4] p. 361Property 1(b)logb1 26804
[Cohen4] p. 367Propertylogbchbase 26806
[Cohen4] p. 377Property 2logblt 26819
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34536  sxbrsigalem4 34538
[Cohn] p. 81Section II.5acsdomd 18565  acsinfd 18564  acsinfdimd 18566  acsmap2d 18563  acsmapd 18562
[Cohn] p. 143Example 5.1.1sxbrsiga 34541
[Connell] p. 57Definitiondf-scmat 22524  df-scmatalt 48969
[Conway] p. 4Definitionlesrec 27862  lesrecd 27863
[Conway] p. 5Definitionaddsval 28025  addsval2 28026  df-adds 28023  df-muls 28170  df-negs 28084
[Conway] p. 7Theorem0lt1s 27875
[Conway] p. 12Theorem 12pw2cut2 28525
[Conway] p. 16Theorem 0(i)sltsright 27924
[Conway] p. 16Theorem 0(ii)sltsleft 27923
[Conway] p. 16Theorem 0(iii)lesid 27801
[Conway] p. 17Theorem 3addsass 28068  addsassd 28069  addscom 28029  addscomd 28030  addsrid 28027  addsridd 28028
[Conway] p. 17Definitiondf-0s 27870
[Conway] p. 17Theorem 4(ii)negnegs 28107
[Conway] p. 17Theorem 4(iii)negsid 28104  negsidd 28105
[Conway] p. 18Theorem 5leadds1 28052  leadds1d 28058
[Conway] p. 18Definitiondf-1s 27871
[Conway] p. 18Theorem 6(ii)negscl 28099  negscld 28100
[Conway] p. 18Theorem 6(iii)addscld 28043
[Conway] p. 19Notemulsunif2 28233
[Conway] p. 19Theorem 7addsdi 28218  addsdid 28219  addsdird 28220  mulnegs1d 28223  mulnegs2d 28224  mulsass 28229  mulsassd 28230  mulscom 28202  mulscomd 28203
[Conway] p. 19Theorem 8(i)mulscl 28197  mulscld 28198
[Conway] p. 19Theorem 8(iii)lemulsd 28201  ltmuls 28199  ltmulsd 28200
[Conway] p. 20Theorem 9mulsgt0 28207  mulsgt0d 28208
[Conway] p. 21Theorem 10(iv)precsex 28281
[Conway] p. 23Theorem 11eqcuts3 27867
[Conway] p. 24Definitiondf-reno 28553
[Conway] p. 24Theorem 13(ii)readdscl 28562  remulscl 28565  renegscl 28561
[Conway] p. 27Definitiondf-ons 28315  elons2 28321
[Conway] p. 27Theorem 14ltonsex 28325
[Conway] p. 28Theorem 15oncutlt 28327  onswe 28335
[Conway] p. 29Remarkmadebday 27963  newbday 27965  oldbday 27964
[Conway] p. 29Definitiondf-made 27890  df-new 27892  df-old 27891
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13861
[Crawley] p. 1Definition of posetdf-poset 18321
[Crawley] p. 107Theorem 13.2hlsupr 39958
[Crawley] p. 110Theorem 13.3arglem1N 40762  dalaw 40458
[Crawley] p. 111Theorem 13.4hlathil 42533
[Crawley] p. 111Definition of set Wdf-watsN 40562
[Crawley] p. 111Definition of dilationdf-dilN 40678  df-ldil 40676  isldil 40682
[Crawley] p. 111Definition of translationdf-ltrn 40677  df-trnN 40679  isltrn 40691  ltrnu 40693
[Crawley] p. 112Lemma Acdlema1N 40363  cdlema2N 40364  exatleN 39976
[Crawley] p. 112Lemma B1cvrat 40048  cdlemb 40366  cdlemb2 40613  cdlemb3 41178  idltrn 40722  l1cvat 39627  lhpat 40615  lhpat2 40617  lshpat 39628  ltrnel 40711  ltrnmw 40723
[Crawley] p. 112Lemma Ccdlemc1 40763  cdlemc2 40764  ltrnnidn 40746  trlat 40741  trljat1 40738  trljat2 40739  trljat3 40740  trlne 40757  trlnidat 40745  trlnle 40758
[Crawley] p. 112Definition of automorphismdf-pautN 40563
[Crawley] p. 113Lemma Ccdlemc 40769  cdlemc3 40765  cdlemc4 40766
[Crawley] p. 113Lemma Dcdlemd 40779  cdlemd1 40770  cdlemd2 40771  cdlemd3 40772  cdlemd4 40773  cdlemd5 40774  cdlemd6 40775  cdlemd7 40776  cdlemd8 40777  cdlemd9 40778  cdleme31sde 40957  cdleme31se 40954  cdleme31se2 40955  cdleme31snd 40958  cdleme32a 41013  cdleme32b 41014  cdleme32c 41015  cdleme32d 41016  cdleme32e 41017  cdleme32f 41018  cdleme32fva 41009  cdleme32fva1 41010  cdleme32fvcl 41012  cdleme32le 41019  cdleme48fv 41071  cdleme4gfv 41079  cdleme50eq 41113  cdleme50f 41114  cdleme50f1 41115  cdleme50f1o 41118  cdleme50laut 41119  cdleme50ldil 41120  cdleme50lebi 41112  cdleme50rn 41117  cdleme50rnlem 41116  cdlemeg49le 41083  cdlemeg49lebilem 41111
[Crawley] p. 113Lemma Ecdleme 41132  cdleme00a 40781  cdleme01N 40793  cdleme02N 40794  cdleme0a 40783  cdleme0aa 40782  cdleme0b 40784  cdleme0c 40785  cdleme0cp 40786  cdleme0cq 40787  cdleme0dN 40788  cdleme0e 40789  cdleme0ex1N 40795  cdleme0ex2N 40796  cdleme0fN 40790  cdleme0gN 40791  cdleme0moN 40797  cdleme1 40799  cdleme10 40826  cdleme10tN 40830  cdleme11 40842  cdleme11a 40832  cdleme11c 40833  cdleme11dN 40834  cdleme11e 40835  cdleme11fN 40836  cdleme11g 40837  cdleme11h 40838  cdleme11j 40839  cdleme11k 40840  cdleme11l 40841  cdleme12 40843  cdleme13 40844  cdleme14 40845  cdleme15 40850  cdleme15a 40846  cdleme15b 40847  cdleme15c 40848  cdleme15d 40849  cdleme16 40857  cdleme16aN 40831  cdleme16b 40851  cdleme16c 40852  cdleme16d 40853  cdleme16e 40854  cdleme16f 40855  cdleme16g 40856  cdleme19a 40875  cdleme19b 40876  cdleme19c 40877  cdleme19d 40878  cdleme19e 40879  cdleme19f 40880  cdleme1b 40798  cdleme2 40800  cdleme20aN 40881  cdleme20bN 40882  cdleme20c 40883  cdleme20d 40884  cdleme20e 40885  cdleme20f 40886  cdleme20g 40887  cdleme20h 40888  cdleme20i 40889  cdleme20j 40890  cdleme20k 40891  cdleme20l 40894  cdleme20l1 40892  cdleme20l2 40893  cdleme20m 40895  cdleme20y 40874  cdleme20zN 40873  cdleme21 40909  cdleme21d 40902  cdleme21e 40903  cdleme22a 40912  cdleme22aa 40911  cdleme22b 40913  cdleme22cN 40914  cdleme22d 40915  cdleme22e 40916  cdleme22eALTN 40917  cdleme22f 40918  cdleme22f2 40919  cdleme22g 40920  cdleme23a 40921  cdleme23b 40922  cdleme23c 40923  cdleme26e 40931  cdleme26eALTN 40933  cdleme26ee 40932  cdleme26f 40935  cdleme26f2 40937  cdleme26f2ALTN 40936  cdleme26fALTN 40934  cdleme27N 40941  cdleme27a 40939  cdleme27cl 40938  cdleme28c 40944  cdleme3 40809  cdleme30a 40950  cdleme31fv 40962  cdleme31fv1 40963  cdleme31fv1s 40964  cdleme31fv2 40965  cdleme31id 40966  cdleme31sc 40956  cdleme31sdnN 40959  cdleme31sn 40952  cdleme31sn1 40953  cdleme31sn1c 40960  cdleme31sn2 40961  cdleme31so 40951  cdleme35a 41020  cdleme35b 41022  cdleme35c 41023  cdleme35d 41024  cdleme35e 41025  cdleme35f 41026  cdleme35fnpq 41021  cdleme35g 41027  cdleme35h 41028  cdleme35h2 41029  cdleme35sn2aw 41030  cdleme35sn3a 41031  cdleme36a 41032  cdleme36m 41033  cdleme37m 41034  cdleme38m 41035  cdleme38n 41036  cdleme39a 41037  cdleme39n 41038  cdleme3b 40801  cdleme3c 40802  cdleme3d 40803  cdleme3e 40804  cdleme3fN 40805  cdleme3fa 40808  cdleme3g 40806  cdleme3h 40807  cdleme4 40810  cdleme40m 41039  cdleme40n 41040  cdleme40v 41041  cdleme40w 41042  cdleme41fva11 41049  cdleme41sn3aw 41046  cdleme41sn4aw 41047  cdleme41snaw 41048  cdleme42a 41043  cdleme42b 41050  cdleme42c 41044  cdleme42d 41045  cdleme42e 41051  cdleme42f 41052  cdleme42g 41053  cdleme42h 41054  cdleme42i 41055  cdleme42k 41056  cdleme42ke 41057  cdleme42keg 41058  cdleme42mN 41059  cdleme42mgN 41060  cdleme43aN 41061  cdleme43bN 41062  cdleme43cN 41063  cdleme43dN 41064  cdleme5 40812  cdleme50ex 41131  cdleme50ltrn 41129  cdleme51finvN 41128  cdleme51finvfvN 41127  cdleme51finvtrN 41130  cdleme6 40813  cdleme7 40821  cdleme7a 40815  cdleme7aa 40814  cdleme7b 40816  cdleme7c 40817  cdleme7d 40818  cdleme7e 40819  cdleme7ga 40820  cdleme8 40822  cdleme8tN 40827  cdleme9 40825  cdleme9a 40823  cdleme9b 40824  cdleme9tN 40829  cdleme9taN 40828  cdlemeda 40870  cdlemedb 40869  cdlemednpq 40871  cdlemednuN 40872  cdlemefr27cl 40975  cdlemefr32fva1 40982  cdlemefr32fvaN 40981  cdlemefrs32fva 40972  cdlemefrs32fva1 40973  cdlemefs27cl 40985  cdlemefs32fva1 40995  cdlemefs32fvaN 40994  cdlemesner 40868  cdlemeulpq 40792
[Crawley] p. 114Lemma E4atex 40648  4atexlem7 40647  cdleme0nex 40862  cdleme17a 40858  cdleme17c 40860  cdleme17d 41070  cdleme17d1 40861  cdleme17d2 41067  cdleme18a 40863  cdleme18b 40864  cdleme18c 40865  cdleme18d 40867  cdleme4a 40811
[Crawley] p. 115Lemma Ecdleme21a 40897  cdleme21at 40900  cdleme21b 40898  cdleme21c 40899  cdleme21ct 40901  cdleme21f 40904  cdleme21g 40905  cdleme21h 40906  cdleme21i 40907  cdleme22gb 40866
[Crawley] p. 116Lemma Fcdlemf 41135  cdlemf1 41133  cdlemf2 41134
[Crawley] p. 116Lemma Gcdlemftr1 41139  cdlemg16 41229  cdlemg28 41276  cdlemg28a 41265  cdlemg28b 41275  cdlemg3a 41169  cdlemg42 41301  cdlemg43 41302  cdlemg44 41305  cdlemg44a 41303  cdlemg46 41307  cdlemg47 41308  cdlemg9 41206  ltrnco 41291  ltrncom 41310  tgrpabl 41323  trlco 41299
[Crawley] p. 116Definition of Gdf-tgrp 41315
[Crawley] p. 117Lemma Gcdlemg17 41249  cdlemg17b 41234
[Crawley] p. 117Definition of Edf-edring-rN 41328  df-edring 41329
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41332
[Crawley] p. 118Remarktendopltp 41352
[Crawley] p. 118Lemma Hcdlemh 41389  cdlemh1 41387  cdlemh2 41388
[Crawley] p. 118Lemma Icdlemi 41392  cdlemi1 41390  cdlemi2 41391
[Crawley] p. 118Lemma Jcdlemj1 41393  cdlemj2 41394  cdlemj3 41395  tendocan 41396
[Crawley] p. 118Lemma Kcdlemk 41546  cdlemk1 41403  cdlemk10 41415  cdlemk11 41421  cdlemk11t 41518  cdlemk11ta 41501  cdlemk11tb 41503  cdlemk11tc 41517  cdlemk11u-2N 41461  cdlemk11u 41443  cdlemk12 41422  cdlemk12u-2N 41462  cdlemk12u 41444  cdlemk13-2N 41448  cdlemk13 41424  cdlemk14-2N 41450  cdlemk14 41426  cdlemk15-2N 41451  cdlemk15 41427  cdlemk16-2N 41452  cdlemk16 41429  cdlemk16a 41428  cdlemk17-2N 41453  cdlemk17 41430  cdlemk18-2N 41458  cdlemk18-3N 41472  cdlemk18 41440  cdlemk19-2N 41459  cdlemk19 41441  cdlemk19u 41542  cdlemk1u 41431  cdlemk2 41404  cdlemk20-2N 41464  cdlemk20 41446  cdlemk21-2N 41463  cdlemk21N 41445  cdlemk22-3 41473  cdlemk22 41465  cdlemk23-3 41474  cdlemk24-3 41475  cdlemk25-3 41476  cdlemk26-3 41478  cdlemk26b-3 41477  cdlemk27-3 41479  cdlemk28-3 41480  cdlemk29-3 41483  cdlemk3 41405  cdlemk30 41466  cdlemk31 41468  cdlemk32 41469  cdlemk33N 41481  cdlemk34 41482  cdlemk35 41484  cdlemk36 41485  cdlemk37 41486  cdlemk38 41487  cdlemk39 41488  cdlemk39u 41540  cdlemk4 41406  cdlemk41 41492  cdlemk42 41513  cdlemk42yN 41516  cdlemk43N 41535  cdlemk45 41519  cdlemk46 41520  cdlemk47 41521  cdlemk48 41522  cdlemk49 41523  cdlemk5 41408  cdlemk50 41524  cdlemk51 41525  cdlemk52 41526  cdlemk53 41529  cdlemk54 41530  cdlemk55 41533  cdlemk55u 41538  cdlemk56 41543  cdlemk5a 41407  cdlemk5auN 41432  cdlemk5u 41433  cdlemk6 41409  cdlemk6u 41434  cdlemk7 41420  cdlemk7u-2N 41460  cdlemk7u 41442  cdlemk8 41410  cdlemk9 41411  cdlemk9bN 41412  cdlemki 41413  cdlemkid 41508  cdlemkj-2N 41454  cdlemkj 41435  cdlemksat 41418  cdlemksel 41417  cdlemksv 41416  cdlemksv2 41419  cdlemkuat 41438  cdlemkuel-2N 41456  cdlemkuel-3 41470  cdlemkuel 41437  cdlemkuv-2N 41455  cdlemkuv2-2 41457  cdlemkuv2-3N 41471  cdlemkuv2 41439  cdlemkuvN 41436  cdlemkvcl 41414  cdlemky 41498  cdlemkyyN 41534  tendoex 41547
[Crawley] p. 120Remarkdva1dim 41557
[Crawley] p. 120Lemma Lcdleml1N 41548  cdleml2N 41549  cdleml3N 41550  cdleml4N 41551  cdleml5N 41552  cdleml6 41553  cdleml7 41554  cdleml8 41555  cdleml9 41556  dia1dim 41633
[Crawley] p. 120Lemma Mdia11N 41620  diaf11N 41621  dialss 41618  diaord 41619  dibf11N 41733  djajN 41709
[Crawley] p. 120Definition of isomorphism mapdiaval 41604
[Crawley] p. 121Lemma Mcdlemm10N 41690  dia2dimlem1 41636  dia2dimlem2 41637  dia2dimlem3 41638  dia2dimlem4 41639  dia2dimlem5 41640  diaf1oN 41702  diarnN 41701  dvheveccl 41684  dvhopN 41688
[Crawley] p. 121Lemma Ncdlemn 41784  cdlemn10 41778  cdlemn11 41783  cdlemn11a 41779  cdlemn11b 41780  cdlemn11c 41781  cdlemn11pre 41782  cdlemn2 41767  cdlemn2a 41768  cdlemn3 41769  cdlemn4 41770  cdlemn4a 41771  cdlemn5 41773  cdlemn5pre 41772  cdlemn6 41774  cdlemn7 41775  cdlemn8 41776  cdlemn9 41777  diclspsn 41766
[Crawley] p. 121Definition of phi(q)df-dic 41745
[Crawley] p. 122Lemma Ndih11 41837  dihf11 41839  dihjust 41789  dihjustlem 41788  dihord 41836  dihord1 41790  dihord10 41795  dihord11b 41794  dihord11c 41796  dihord2 41799  dihord2a 41791  dihord2b 41792  dihord2cN 41793  dihord2pre 41797  dihord2pre2 41798  dihordlem6 41785  dihordlem7 41786  dihordlem7b 41787
[Crawley] p. 122Definition of isomorphism mapdihffval 41802  dihfval 41803  dihval 41804
[Diestel] p. 3Definitiondf-gric 48451  df-grim 48448  isuspgrim 48466
[Diestel] p. 3Section 1.1df-cusgr 29552  df-nbgr 29473
[Diestel] p. 3Definition by df-grisom 48447
[Diestel] p. 4Section 1.1df-isubgr 48431  df-subgr 29408  uhgrspan1 29443  uhgrspansubgr 29431
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29694  vtxdgoddnumeven 29693
[Diestel] p. 27Section 1.10df-ushgr 29199
[EGA] p. 80Notation 1.1.1rspecval 34115
[EGA] p. 80Proposition 1.1.2zartop 34127
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34119  zarcls1 34120
[EGA] p. 81Corollary 1.1.8zart0 34130
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34133
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34136
[Eisenberg] p. 67Definition 5.3df-dif 3902
[Eisenberg] p. 82Definition 6.3dfom3 9592
[Eisenberg] p. 125Definition 8.21df-map 8798
[Eisenberg] p. 216Example 13.2(4)omenps 9600
[Eisenberg] p. 310Theorem 19.8cardprc 9928
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10502
[Enderton] p. 18Axiom of Empty Setaxnul 5249
[Enderton] p. 19Definitiondf-tp 4581
[Enderton] p. 26Exercise 5unissb 4893
[Enderton] p. 26Exercise 10pwel 5332
[Enderton] p. 28Exercise 7(b)pwun 5533
[Enderton] p. 30Theorem "Distributive laws"iinin1 5030  iinin2 5029  iinun2 5024  iunin1 5023  iunin1f 32699  iunin2 5022  uniin1 32693  uniin2 32694
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5028  iundif2 5025
[Enderton] p. 32Exercise 20unineq 4235
[Enderton] p. 33Exercise 23iinuni 5049
[Enderton] p. 33Exercise 25iununi 5050
[Enderton] p. 33Exercise 24(a)iinpw 5057
[Enderton] p. 33Exercise 24(b)iunpw 7743  iunpwss 5058
[Enderton] p. 36Definitionopthwiener 5477
[Enderton] p. 38Exercise 6(a)unipw 5411
[Enderton] p. 38Exercise 6(b)pwuni 4898
[Enderton] p. 41Lemma 3Dopeluu 5432  rnex 7880  rnexg 7872
[Enderton] p. 41Exercise 8dmuni 5883  rnuni 6123
[Enderton] p. 42Definition of a functiondffun7 6537  dffun8 6538
[Enderton] p. 43Definition of function valuefunfv2 6944
[Enderton] p. 43Definition of single-rootedfuncnv 6579
[Enderton] p. 44Definition (d)dfima2 6041  dfima3 6042
[Enderton] p. 47Theorem 3Hfvco2 6953
[Enderton] p. 49Axiom of Choice (first form)ac7 10420  ac7g 10421  df-ac 10062  dfac2 10078  dfac2a 10076  dfac2b 10077  dfac3 10067  dfac7 10079
[Enderton] p. 50Theorem 3K(a)imauni 7219
[Enderton] p. 52Definitiondf-map 8798
[Enderton] p. 53Exercise 21coass 6242
[Enderton] p. 53Exercise 27dmco 6231
[Enderton] p. 53Exercise 14(a)funin 6586
[Enderton] p. 53Exercise 22(a)imass2 6081
[Enderton] p. 54Remarkixpf 8891  ixpssmap 8903
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8869
[Enderton] p. 55Axiom of Choice (second form)ac9 10430  ac9s 10440
[Enderton] p. 56Theorem 3Meqvrelref 39141  erref 8687
[Enderton] p. 57Lemma 3Neqvrelthi 39144  erthi 8723
[Enderton] p. 57Definitiondf-ec 8668
[Enderton] p. 58Definitiondf-qs 8672
[Enderton] p. 61Exercise 35df-ec 8668
[Enderton] p. 65Exercise 56(a)dmun 5879
[Enderton] p. 68Definition of successordf-suc 6341
[Enderton] p. 71Definitiondf-tr 5202  dftr4 5207
[Enderton] p. 72Theorem 4Eunisuc 6416  unisucg 6415
[Enderton] p. 73Exercise 6unisuc 6416  unisucg 6415
[Enderton] p. 73Exercise 5(a)truni 5217
[Enderton] p. 73Exercise 5(b)trint 5219  trintALT 45404
[Enderton] p. 79Theorem 4I(A1)nna0 8562
[Enderton] p. 79Theorem 4I(A2)nnasuc 8564  onasuc 8485
[Enderton] p. 79Definition of operation valuedf-ov 7388
[Enderton] p. 80Theorem 4J(A1)nnm0 8563
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8565  onmsuc 8486
[Enderton] p. 81Theorem 4K(1)nnaass 8580
[Enderton] p. 81Theorem 4K(2)nna0r 8567  nnacom 8575
[Enderton] p. 81Theorem 4K(3)nndi 8581
[Enderton] p. 81Theorem 4K(4)nnmass 8582
[Enderton] p. 81Theorem 4K(5)nnmcom 8584
[Enderton] p. 82Exercise 16nnm0r 8568  nnmsucr 8583
[Enderton] p. 88Exercise 23nnaordex 8596
[Enderton] p. 129Definitiondf-en 8917
[Enderton] p. 132Theorem 6B(b)canth 7339
[Enderton] p. 133Exercise 1xpomen 9961
[Enderton] p. 133Exercise 2qnnen 16221
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9164
[Enderton] p. 135Corollary 6Cphp3 9166
[Enderton] p. 136Corollary 6Enneneq 9163
[Enderton] p. 136Corollary 6D(a)pssinf 9195
[Enderton] p. 136Corollary 6D(b)ominf 9197
[Enderton] p. 137Lemma 6Fpssnn 9126
[Enderton] p. 138Corollary 6Gssfi 9130
[Enderton] p. 139Theorem 6H(c)mapen 9102
[Enderton] p. 142Theorem 6I(3)xpdjuen 10126
[Enderton] p. 142Theorem 6I(4)mapdjuen 10127
[Enderton] p. 143Theorem 6Jdju0en 10122  dju1en 10118
[Enderton] p. 144Exercise 13iunfi 9276  unifi 9277  unifi2 9278
[Enderton] p. 144Corollary 6Kundif2 4425  unfi 9128  unfi2 9243
[Enderton] p. 145Figure 38ffoss 7916
[Enderton] p. 145Definitiondf-dom 8918
[Enderton] p. 146Example 1domen 8931  domeng 8932
[Enderton] p. 146Example 3nndomo 9175  nnsdom 9599  nnsdomg 9232
[Enderton] p. 149Theorem 6L(a)djudom2 10130
[Enderton] p. 149Theorem 6L(c)mapdom1 9103  xpdom1 9037  xpdom1g 9035  xpdom2g 9034
[Enderton] p. 149Theorem 6L(d)mapdom2 9109
[Enderton] p. 151Theorem 6Mzorn 10454  zorng 10451
[Enderton] p. 151Theorem 6M(4)ac8 10439  dfac5 10075
[Enderton] p. 159Theorem 6Qunictb 10523
[Enderton] p. 164Exampleinfdif 10154
[Enderton] p. 168Definitiondf-po 5548
[Enderton] p. 192Theorem 7M(a)oneli 6450
[Enderton] p. 192Theorem 7M(b)ontr1 6382
[Enderton] p. 192Theorem 7M(c)onirri 6449
[Enderton] p. 193Corollary 7N(b)0elon 6390
[Enderton] p. 193Corollary 7N(c)onsuci 7808
[Enderton] p. 193Corollary 7N(d)ssonunii 7753
[Enderton] p. 194Remarkonprc 7750
[Enderton] p. 194Exercise 16suc11 6444
[Enderton] p. 197Definitiondf-card 9887
[Enderton] p. 197Theorem 7Pcarden 10498
[Enderton] p. 200Exercise 25tfis 7824
[Enderton] p. 202Lemma 7Tr1tr 9724
[Enderton] p. 202Definitiondf-r1 9712
[Enderton] p. 202Theorem 7Qr1val1 9734
[Enderton] p. 204Theorem 7V(b)rankval4 9815  rankval4b 35351
[Enderton] p. 206Theorem 7X(b)en2lp 9551
[Enderton] p. 207Exercise 30rankpr 9805  rankprb 9799  rankpw 9791  rankpwi 9771  rankuniss 9814
[Enderton] p. 207Exercise 34opthreg 9563
[Enderton] p. 208Exercise 35suc11reg 9564
[Enderton] p. 212Definition of alephalephval3 10056
[Enderton] p. 213Theorem 8A(a)alephord2 10022
[Enderton] p. 213Theorem 8A(b)cardalephex 10036
[Enderton] p. 218Theorem Schema 8Eonfununi 8300
[Enderton] p. 222Definition of kardkarden 9843  kardex 9842
[Enderton] p. 238Theorem 8Roeoa 8555
[Enderton] p. 238Theorem 8Soeoe 8557
[Enderton] p. 240Exercise 25oarec 8519
[Enderton] p. 257Definition of cofinalitycflm 10196
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17650
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17592
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18561  mrieqv2d 17647  mrieqvd 17646
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17651
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17656  mreexexlem2d 17653
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18567  mreexfidimd 17658
[Frege1879] p. 11Statementdf3or2 44292
[Frege1879] p. 12Statementdf3an2 44293  dfxor4 44290  dfxor5 44291
[Frege1879] p. 26Axiom 1ax-frege1 44314
[Frege1879] p. 26Axiom 2ax-frege2 44315
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44319
[Frege1879] p. 31Proposition 4frege4 44323
[Frege1879] p. 32Proposition 5frege5 44324
[Frege1879] p. 33Proposition 6frege6 44330
[Frege1879] p. 34Proposition 7frege7 44332
[Frege1879] p. 35Axiom 8ax-frege8 44333  axfrege8 44331
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37887
[Frege1879] p. 35Proposition 9frege9 44336
[Frege1879] p. 36Proposition 10frege10 44344
[Frege1879] p. 36Proposition 11frege11 44338
[Frege1879] p. 37Proposition 12frege12 44337
[Frege1879] p. 37Proposition 13frege13 44346
[Frege1879] p. 37Proposition 14frege14 44347
[Frege1879] p. 38Proposition 15frege15 44350
[Frege1879] p. 38Proposition 16frege16 44340
[Frege1879] p. 39Proposition 17frege17 44345
[Frege1879] p. 39Proposition 18frege18 44342
[Frege1879] p. 39Proposition 19frege19 44348
[Frege1879] p. 40Proposition 20frege20 44352
[Frege1879] p. 40Proposition 21frege21 44351
[Frege1879] p. 41Proposition 22frege22 44343
[Frege1879] p. 42Proposition 23frege23 44349
[Frege1879] p. 42Proposition 24frege24 44339
[Frege1879] p. 42Proposition 25frege25 44341  rp-frege25 44329
[Frege1879] p. 42Proposition 26frege26 44334
[Frege1879] p. 43Axiom 28ax-frege28 44354
[Frege1879] p. 43Proposition 27frege27 44335
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 44355
[Frege1879] p. 44Axiom 31ax-frege31 44358  axfrege31 44357
[Frege1879] p. 44Proposition 30frege30 44356
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 44359
[Frege1879] p. 44Proposition 33frege33 44360
[Frege1879] p. 45Proposition 34frege34 44361
[Frege1879] p. 45Proposition 35frege35 44362
[Frege1879] p. 45Proposition 36frege36 44363
[Frege1879] p. 46Proposition 37frege37 44364
[Frege1879] p. 46Proposition 38frege38 44365
[Frege1879] p. 46Proposition 39frege39 44366
[Frege1879] p. 46Proposition 40frege40 44367
[Frege1879] p. 47Axiom 41ax-frege41 44369  axfrege41 44368
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 44370
[Frege1879] p. 47Proposition 43frege43 44371
[Frege1879] p. 47Proposition 44frege44 44372
[Frege1879] p. 47Proposition 45frege45 44373
[Frege1879] p. 48Proposition 46frege46 44374
[Frege1879] p. 48Proposition 47frege47 44375
[Frege1879] p. 49Proposition 48frege48 44376
[Frege1879] p. 49Proposition 49frege49 44377
[Frege1879] p. 49Proposition 50frege50 44378
[Frege1879] p. 50Axiom 52ax-frege52a 44381  ax-frege52c 44412  frege52aid 44382  frege52b 44413
[Frege1879] p. 50Axiom 54ax-frege54a 44386  ax-frege54c 44416  frege54b 44417
[Frege1879] p. 50Proposition 51frege51 44379
[Frege1879] p. 50Proposition 52dfsbcq 3741
[Frege1879] p. 50Proposition 53frege53a 44384  frege53aid 44383  frege53b 44414  frege53c 44438
[Frege1879] p. 50Proposition 54biid 263  eqid 2756
[Frege1879] p. 50Proposition 55frege55a 44392  frege55aid 44389  frege55b 44421  frege55c 44442  frege55cor1a 44393  frege55lem2a 44391  frege55lem2b 44420  frege55lem2c 44441
[Frege1879] p. 50Proposition 56frege56a 44395  frege56aid 44394  frege56b 44422  frege56c 44443
[Frege1879] p. 51Axiom 58ax-frege58a 44399  ax-frege58b 44425  frege58bid 44426  frege58c 44445
[Frege1879] p. 51Proposition 57frege57a 44397  frege57aid 44396  frege57b 44423  frege57c 44444
[Frege1879] p. 51Proposition 58spsbc 3752
[Frege1879] p. 51Proposition 59frege59a 44401  frege59b 44428  frege59c 44446
[Frege1879] p. 52Proposition 60frege60a 44402  frege60b 44429  frege60c 44447
[Frege1879] p. 52Proposition 61frege61a 44403  frege61b 44430  frege61c 44448
[Frege1879] p. 52Proposition 62frege62a 44404  frege62b 44431  frege62c 44449
[Frege1879] p. 52Proposition 63frege63a 44405  frege63b 44432  frege63c 44450
[Frege1879] p. 53Proposition 64frege64a 44406  frege64b 44433  frege64c 44451
[Frege1879] p. 53Proposition 65frege65a 44407  frege65b 44434  frege65c 44452
[Frege1879] p. 54Proposition 66frege66a 44408  frege66b 44435  frege66c 44453
[Frege1879] p. 54Proposition 67frege67a 44409  frege67b 44436  frege67c 44454
[Frege1879] p. 54Proposition 68frege68a 44410  frege68b 44437  frege68c 44455
[Frege1879] p. 55Definition 69dffrege69 44456
[Frege1879] p. 58Proposition 70frege70 44457
[Frege1879] p. 59Proposition 71frege71 44458
[Frege1879] p. 59Proposition 72frege72 44459
[Frege1879] p. 59Proposition 73frege73 44460
[Frege1879] p. 60Definition 76dffrege76 44463
[Frege1879] p. 60Proposition 74frege74 44461
[Frege1879] p. 60Proposition 75frege75 44462
[Frege1879] p. 62Proposition 77frege77 44464  frege77d 44270
[Frege1879] p. 63Proposition 78frege78 44465
[Frege1879] p. 63Proposition 79frege79 44466
[Frege1879] p. 63Proposition 80frege80 44467
[Frege1879] p. 63Proposition 81frege81 44468  frege81d 44271
[Frege1879] p. 64Proposition 82frege82 44469
[Frege1879] p. 65Proposition 83frege83 44470  frege83d 44272
[Frege1879] p. 65Proposition 84frege84 44471
[Frege1879] p. 66Proposition 85frege85 44472
[Frege1879] p. 66Proposition 86frege86 44473
[Frege1879] p. 66Proposition 87frege87 44474  frege87d 44274
[Frege1879] p. 67Proposition 88frege88 44475
[Frege1879] p. 68Proposition 89frege89 44476
[Frege1879] p. 68Proposition 90frege90 44477
[Frege1879] p. 68Proposition 91frege91 44478  frege91d 44275
[Frege1879] p. 69Proposition 92frege92 44479
[Frege1879] p. 70Proposition 93frege93 44480
[Frege1879] p. 70Proposition 94frege94 44481
[Frege1879] p. 70Proposition 95frege95 44482
[Frege1879] p. 71Definition 99dffrege99 44486
[Frege1879] p. 71Proposition 96frege96 44483  frege96d 44273
[Frege1879] p. 71Proposition 97frege97 44484  frege97d 44276
[Frege1879] p. 71Proposition 98frege98 44485  frege98d 44277
[Frege1879] p. 72Proposition 100frege100 44487
[Frege1879] p. 72Proposition 101frege101 44488
[Frege1879] p. 72Proposition 102frege102 44489  frege102d 44278
[Frege1879] p. 73Proposition 103frege103 44490
[Frege1879] p. 73Proposition 104frege104 44491
[Frege1879] p. 73Proposition 105frege105 44492
[Frege1879] p. 73Proposition 106frege106 44493  frege106d 44279
[Frege1879] p. 74Proposition 107frege107 44494
[Frege1879] p. 74Proposition 108frege108 44495  frege108d 44280
[Frege1879] p. 74Proposition 109frege109 44496  frege109d 44281
[Frege1879] p. 75Proposition 110frege110 44497
[Frege1879] p. 75Proposition 111frege111 44498  frege111d 44283
[Frege1879] p. 76Proposition 112frege112 44499
[Frege1879] p. 76Proposition 113frege113 44500
[Frege1879] p. 76Proposition 114frege114 44501  frege114d 44282
[Frege1879] p. 77Definition 115dffrege115 44502
[Frege1879] p. 77Proposition 116frege116 44503
[Frege1879] p. 78Proposition 117frege117 44504
[Frege1879] p. 78Proposition 118frege118 44505
[Frege1879] p. 78Proposition 119frege119 44506
[Frege1879] p. 78Proposition 120frege120 44507
[Frege1879] p. 79Proposition 121frege121 44508
[Frege1879] p. 79Proposition 122frege122 44509  frege122d 44284
[Frege1879] p. 79Proposition 123frege123 44510
[Frege1879] p. 80Proposition 124frege124 44511  frege124d 44285
[Frege1879] p. 81Proposition 125frege125 44512
[Frege1879] p. 81Proposition 126frege126 44513  frege126d 44286
[Frege1879] p. 82Proposition 127frege127 44514
[Frege1879] p. 83Proposition 128frege128 44515
[Frege1879] p. 83Proposition 129frege129 44516  frege129d 44287
[Frege1879] p. 84Proposition 130frege130 44517
[Frege1879] p. 85Proposition 131frege131 44518  frege131d 44288
[Frege1879] p. 86Proposition 132frege132 44519
[Frege1879] p. 86Proposition 133frege133 44520  frege133d 44289
[Fremlin1] p. 13Definition 111G (b)df-salgen 46835
[Fremlin1] p. 13Definition 111G (d)borelmbl 47158
[Fremlin1] p. 13Proposition 111G (b)salgenss 46858
[Fremlin1] p. 14Definition 112Aismea 46973
[Fremlin1] p. 15Remark 112B (d)psmeasure 46993
[Fremlin1] p. 15Property 112C (a)meadjun 46984  meadjunre 46998
[Fremlin1] p. 15Property 112C (b)meassle 46985
[Fremlin1] p. 15Property 112C (c)meaunle 46986
[Fremlin1] p. 16Property 112C (d)iundjiun 46982  meaiunle 46991  meaiunlelem 46990
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47003  meaiuninc2 47004  meaiuninc3 47007  meaiuninc3v 47006  meaiunincf 47005  meaiuninclem 47002
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47009  meaiininc2 47010  meaiininclem 47008
[Fremlin1] p. 19Theorem 113Ccaragen0 47028  caragendifcl 47036  caratheodory 47050  omelesplit 47040
[Fremlin1] p. 19Definition 113Aisome 47016  isomennd 47053  isomenndlem 47052
[Fremlin1] p. 19Remark 113B (c)omeunle 47038
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47057  voncmpl 47143
[Fremlin1] p. 19Definition 113A (ii)omessle 47020
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47045  carageniuncllem1 47043  carageniuncllem2 47044  caragenuncl 47035  caragenuncllem 47034  caragenunicl 47046
[Fremlin1] p. 21Remark 113Dcaragenel2d 47054
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47048  caratheodorylem2 47049
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47057
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47116  hoidmv1lelem1 47113  hoidmv1lelem2 47114  hoidmv1lelem3 47115
[Fremlin1] p. 25Definition 114Eisvonmbl 47160
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47116  hoidmvle 47122  hoidmvlelem1 47117  hoidmvlelem2 47118  hoidmvlelem3 47119  hoidmvlelem4 47120  hoidmvlelem5 47121  hsphoidmvle2 47107  hsphoif 47098  hsphoival 47101
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47070
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47078
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47105  hoidmvn0val 47106  hoidmvval 47099  hoidmvval0 47109  hoidmvval0b 47112
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47110  hsphoidmvle 47108
[Fremlin1] p. 30Definition 115Cdf-ovoln 47059  df-voln 47061
[Fremlin1] p. 30Proposition 115D (a)dmovn 47126  ovn0 47088  ovn0lem 47087  ovnf 47085  ovnome 47095  ovnssle 47083  ovnsslelem 47082  ovnsupge0 47079
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47125  ovnhoilem1 47123  ovnhoilem2 47124  vonhoi 47189
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47142  hoidifhspf 47140  hoidifhspval 47130  hoidifhspval2 47137  hoidifhspval3 47141  hspmbl 47151  hspmbllem1 47148  hspmbllem2 47149  hspmbllem3 47150
[Fremlin1] p. 31Definition 115Evoncmpl 47143  vonmea 47096
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47094  ovnsubadd2 47168  ovnsubadd2lem 47167  ovnsubaddlem1 47092  ovnsubaddlem2 47093
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47153  hoimbl2 47187  hoimbllem 47152  hspdifhsp 47138  opnvonmbl 47156  opnvonmbllem2 47155
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47158
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47201  iccvonmbllem 47200  ioovonmbl 47199
[Fremlin1] p. 32Proposition 115G (d)vonicc 47207  vonicclem2 47206  vonioo 47204  vonioolem2 47203  vonn0icc 47210  vonn0icc2 47214  vonn0ioo 47209  vonn0ioo2 47212
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47211  snvonmbl 47208  vonct 47215  vonsn 47213
[Fremlin1] p. 35Lemma 121Asubsalsal 46881
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46880  subsaliuncllem 46879
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47247  salpreimalegt 47231  salpreimaltle 47248
[Fremlin1] p. 35Proposition 121B (i)issmf 47250  issmff 47256  issmflem 47249
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47267  issmflelem 47266  smfpreimale 47276
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47278  issmfgtlem 47277
[Fremlin1] p. 36Definition 121Cdf-smblfn 47218  issmf 47250  issmff 47256  issmfge 47292  issmfgelem 47291  issmfgt 47278  issmfgtlem 47277  issmfle 47267  issmflelem 47266  issmflem 47249
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47229  salpreimagtlt 47252  salpreimalelt 47251
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47292  issmfgelem 47291
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47275
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47273  cnfsmf 47262
[Fremlin1] p. 36Proposition 121D (c)decsmf 47289  decsmflem 47288  incsmf 47264  incsmflem 47263
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47223  pimconstlt1 47224  smfconst 47271
[Fremlin1] p. 37Proposition 121E (b)smfadd 47287  smfaddlem1 47285  smfaddlem2 47286
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47318
[Fremlin1] p. 37Proposition 121E (d)smfmul 47317  smfmullem1 47313  smfmullem2 47314  smfmullem3 47315  smfmullem4 47316
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47319
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47322  smfpimbor1lem2 47321
[Fremlin1] p. 37Proposition 121E (g)smfco 47324
[Fremlin1] p. 37Proposition 121E (h)smfres 47312
[Fremlin1] p. 38Proposition 121E (e)smfrec 47311
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47320  smfresal 47310
[Fremlin1] p. 38Proposition 121F (a)smflim 47299  smflim2 47328  smflimlem1 47293  smflimlem2 47294  smflimlem3 47295  smflimlem4 47296  smflimlem5 47297  smflimlem6 47298  smflimmpt 47332
[Fremlin1] p. 38Proposition 121F (b)smfsup 47336  smfsuplem1 47333  smfsuplem2 47334  smfsuplem3 47335  smfsupmpt 47337  smfsupxr 47338
[Fremlin1] p. 38Proposition 121F (c)smfinf 47340  smfinflem 47339  smfinfmpt 47341
[Fremlin1] p. 39Remark 121Gsmflim 47299  smflim2 47328  smflimmpt 47332
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47330
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47360  smfdivdmmbl2 47363  smfinfdmmbl 47371  smfinfdmmbllem 47370  smfsupdmmbl 47367  smfsupdmmbllem 47366
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47350  smflimsuplem2 47343  smflimsuplem6 47347  smflimsuplem7 47348  smflimsuplem8 47349  smflimsupmpt 47351
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47353  smfliminflem 47352  smfliminfmpt 47354
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47218
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47364  fsupdm2 47365
[Fremlin1], p. 39Proposition 121Hadddmmbl 47355  adddmmbl2 47356  finfdm 47368  finfdm2 47369  fsupdm 47364  fsupdm2 47365  muldmmbl 47357  muldmmbl2 47358
[Fremlin1], p. 39Proposition 121F (c)finfdm 47368  finfdm2 47369
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25571
[Fremlin5] p. 213Lemma 565Cauniioovol 25614
[Fremlin5] p. 214Lemma 565Cauniioombl 25624
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38145
[Fremlin5] p. 220Theorem 565Maftc1anc 38148
[FreydScedrov] p. 283Axiom of Infinityax-inf 9583  inf1 9567  inf2 9568
[Gleason] p. 117Proposition 9-2.1df-enq 10859  enqer 10869
[Gleason] p. 117Proposition 9-2.2df-1nq 10864  df-nq 10860
[Gleason] p. 117Proposition 9-2.3df-plpq 10856  df-plq 10862
[Gleason] p. 119Proposition 9-2.4caovmo 7622  df-mpq 10857  df-mq 10863
[Gleason] p. 119Proposition 9-2.5df-rq 10865
[Gleason] p. 119Proposition 9-2.6ltexnq 10923
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10924  ltbtwnnq 10926
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10919
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10920
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10927
[Gleason] p. 121Definition 9-3.1df-np 10929
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10941
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10943
[Gleason] p. 122Definitiondf-1p 10930
[Gleason] p. 122Remark (1)prub 10942
[Gleason] p. 122Lemma 9-3.4prlem934 10981
[Gleason] p. 122Proposition 9-3.2df-ltp 10933
[Gleason] p. 122Proposition 9-3.3ltsopr 10980  psslinpr 10979  supexpr 11002  suplem1pr 11000  suplem2pr 11001
[Gleason] p. 123Proposition 9-3.5addclpr 10966  addclprlem1 10964  addclprlem2 10965  df-plp 10931
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10970
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10969
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10982
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10991  ltexprlem1 10984  ltexprlem2 10985  ltexprlem3 10986  ltexprlem4 10987  ltexprlem5 10988  ltexprlem6 10989  ltexprlem7 10990
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10993  ltaprlem 10992
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10994
[Gleason] p. 124Lemma 9-3.6prlem936 10995
[Gleason] p. 124Proposition 9-3.7df-mp 10932  mulclpr 10968  mulclprlem 10967  reclem2pr 10996
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10977
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10972
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10971
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10976
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10999  reclem3pr 10997  reclem4pr 10998
[Gleason] p. 126Proposition 9-4.1df-enr 11003  enrer 11011
[Gleason] p. 126Proposition 9-4.2df-0r 11008  df-1r 11009  df-nr 11004
[Gleason] p. 126Proposition 9-4.3df-mr 11006  df-plr 11005  negexsr 11050  recexsr 11055  recexsrlem 11051
[Gleason] p. 127Proposition 9-4.4df-ltr 11007
[Gleason] p. 130Proposition 10-1.3creui 12180  creur 12179  cru 12177
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11136  axcnre 11112
[Gleason] p. 132Definition 10-3.1crim 15118  crimd 15235  crimi 15196  crre 15117  crred 15234  crrei 15195
[Gleason] p. 132Definition 10-3.2remim 15120  remimd 15201
[Gleason] p. 133Definition 10.36absval2 15287  absval2d 15451  absval2i 15401
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15144  cjaddd 15223  cjaddi 15191
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15145  cjmuld 15224  cjmuli 15192
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15143  cjcjd 15202  cjcji 15174
[Gleason] p. 133Proposition 10-3.4(f)cjre 15142  cjreb 15126  cjrebd 15205  cjrebi 15177  cjred 15229  rere 15125  rereb 15123  rerebd 15204  rerebi 15176  rered 15227
[Gleason] p. 133Proposition 10-3.4(h)addcj 15151  addcjd 15215  addcji 15186
[Gleason] p. 133Proposition 10-3.7(a)absval 15241
[Gleason] p. 133Proposition 10-3.7(b)abscj 15282  abscjd 15456  abscji 15405
[Gleason] p. 133Proposition 10-3.7(c)abs00 15292  abs00d 15452  abs00i 15402  absne0d 15453
[Gleason] p. 133Proposition 10-3.7(d)releabs 15325  releabsd 15457  releabsi 15406
[Gleason] p. 133Proposition 10-3.7(f)absmul 15297  absmuld 15460  absmuli 15408
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15285  sqabsaddi 15409
[Gleason] p. 133Proposition 10-3.7(h)abstri 15334  abstrid 15462  abstrii 15412
[Gleason] p. 134Definition 10-4.1df-exp 14065  exp0 14068  expp1 14071  expp1d 14150
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26714  cxpaddd 26752  expadd 14107  expaddd 14151  expaddz 14109
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26723  cxpmuld 26772  expmul 14110  expmuld 14152  expmulz 14111
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26720  mulcxpd 26763  mulexp 14104  mulexpd 14164  mulexpz 14105
[Gleason] p. 140Exercise 1znnen 16220
[Gleason] p. 141Definition 11-2.1fzval 13504
[Gleason] p. 168Proposition 12-2.1(a)climadd 15635  rlimadd 15646  rlimdiv 15649
[Gleason] p. 168Proposition 12-2.1(b)climsub 15637  rlimsub 15647
[Gleason] p. 168Proposition 12-2.1(c)climmul 15636  rlimmul 15648
[Gleason] p. 171Corollary 12-2.2climmulc2 15640
[Gleason] p. 172Corollary 12-2.5climrecl 15586
[Gleason] p. 172Proposition 12-2.4(c)climabs 15607  climcj 15608  climim 15610  climre 15609  rlimabs 15612  rlimcj 15613  rlimim 15615  rlimre 15614
[Gleason] p. 173Definition 12-3.1df-ltxr 11211  df-xr 11210  ltxr 13107
[Gleason] p. 175Definition 12-4.1df-limsup 15474  limsupval 15477
[Gleason] p. 180Theorem 12-5.1climsup 15673
[Gleason] p. 180Theorem 12-5.3caucvg 15682  caucvgb 15683  caucvgbf 46011  caucvgr 15679  climcau 15674
[Gleason] p. 182Exercise 3cvgcmp 15820
[Gleason] p. 182Exercise 4cvgrat 15889
[Gleason] p. 195Theorem 13-2.12abs1m 15339
[Gleason] p. 217Lemma 13-4.1btwnzge0 13828
[Gleason] p. 223Definition 14-1.1df-met 21391
[Gleason] p. 223Definition 14-1.1(a)met0 24376  xmet0 24375
[Gleason] p. 223Definition 14-1.1(b)metgt0 24392
[Gleason] p. 223Definition 14-1.1(c)metsym 24383
[Gleason] p. 223Definition 14-1.1(d)mettri 24385  mstri 24502  xmettri 24384  xmstri 24501
[Gleason] p. 225Definition 14-1.5xpsmet 24415
[Gleason] p. 230Proposition 14-2.6txlm 23681
[Gleason] p. 240Theorem 14-4.3metcnp4 25345
[Gleason] p. 240Proposition 14-4.2metcnp3 24573
[Gleason] p. 243Proposition 14-4.16addcn 24899  addcn2 15597  mulcn 24901  mulcn2 15599  subcn 24900  subcn2 15598
[Gleason] p. 295Remarkbcval3 14309  bcval4 14310
[Gleason] p. 295Equation 2bcpasc 14324
[Gleason] p. 295Definition of binomial coefficientbcval 14307  df-bc 14306
[Gleason] p. 296Remarkbcn0 14313  bcnn 14315
[Gleason] p. 296Theorem 15-2.8binom 15836
[Gleason] p. 308Equation 2ef0 16097
[Gleason] p. 308Equation 3efcj 16098
[Gleason] p. 309Corollary 15-4.3efne0 16104
[Gleason] p. 309Corollary 15-4.4efexp 16109
[Gleason] p. 310Equation 14sinadd 16172
[Gleason] p. 310Equation 15cosadd 16173
[Gleason] p. 311Equation 17sincossq 16184
[Gleason] p. 311Equation 18cosbnd 16189  sinbnd 16188
[Gleason] p. 311Lemma 15-4.7sqeqor 14219  sqeqori 14217
[Gleason] p. 311Definition of ` `df-pi 16078
[Godowski] p. 730Equation SFgoeqi 32415
[GodowskiGreechie] p. 249Equation IV3oai 31810
[Golan] p. 1Remarksrgisid 20231
[Golan] p. 1Definitiondf-srg 20209
[Golan] p. 149Definitiondf-slmd 33335
[Gonshor] p. 7Definitiondf-cuts 27823
[Gonshor] p. 9Theorem 2.5lesrec 27862  lesrecd 27863
[Gonshor] p. 10Theorem 2.6cofcut1 27983  cofcut1d 27984
[Gonshor] p. 10Theorem 2.7cofcut2 27985  cofcut2d 27986
[Gonshor] p. 12Theorem 2.9cofcutr 27987  cofcutr1d 27988  cofcutr2d 27989
[Gonshor] p. 13Definitiondf-adds 28023
[Gonshor] p. 14Theorem 3.1addsprop 28039
[Gonshor] p. 15Theorem 3.2addsunif 28065
[Gonshor] p. 17Theorem 3.4mulsprop 28193
[Gonshor] p. 18Theorem 3.5mulsunif 28213
[Gonshor] p. 28Lemma 4.2halfcut 28521
[Gonshor] p. 28Theorem 4.2pw2cut 28523
[Gonshor] p. 30Theorem 4.2addhalfcut 28522
[Gonshor] p. 39Theorem 4.4(b)elreno2 28558
[Gonshor] p. 95Theorem 6.1addbday 28081
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36457
[Gratzer] p. 23Section 0.6df-mre 17590
[Gratzer] p. 27Section 0.6df-mri 17592
[Hall] p. 1Section 1.1df-asslaw 48758  df-cllaw 48756  df-comlaw 48757
[Hall] p. 2Section 1.2df-clintop 48770
[Hall] p. 7Section 1.3df-sgrp2 48791
[Halmos] p. 28Partition ` `df-parts 39315  dfmembpart2 39320
[Halmos] p. 31Theorem 17.3riesz1 32207  riesz2 32208
[Halmos] p. 41Definition of Hermitianhmopadj2 32083
[Halmos] p. 42Definition of projector orderingpjordi 32315
[Halmos] p. 43Theorem 26.1elpjhmop 32327  elpjidm 32326  pjnmopi 32290
[Halmos] p. 44Remarkpjinormi 31829  pjinormii 31818
[Halmos] p. 44Theorem 26.2elpjch 32331  pjrn 31849  pjrni 31844  pjvec 31838
[Halmos] p. 44Theorem 26.3pjnorm2 31869
[Halmos] p. 44Theorem 26.4hmopidmpj 32296  hmopidmpji 32294
[Halmos] p. 45Theorem 27.1pjinvari 32333
[Halmos] p. 45Theorem 27.3pjoci 32322  pjocvec 31839
[Halmos] p. 45Theorem 27.4pjorthcoi 32311
[Halmos] p. 48Theorem 29.2pjssposi 32314
[Halmos] p. 48Theorem 29.3pjssdif1i 32317  pjssdif2i 32316
[Halmos] p. 50Definition of spectrumdf-spec 31997
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1809
[Hatcher] p. 25Definitiondf-phtpc 25027  df-phtpy 25006
[Hatcher] p. 26Definitiondf-pco 25040  df-pi1 25043
[Hatcher] p. 26Proposition 1.2phtpcer 25030
[Hatcher] p. 26Proposition 1.3pi1grp 25085
[Hefferon] p. 240Definition 3.12df-dmat 22523  df-dmatalt 48968
[Helfgott] p. 2Theoremtgoldbach 48387
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48372
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48384  bgoldbtbnd 48379  bgoldbtbnd 48379  tgblthelfgott 48385
[Helfgott] p. 5Proposition 1.1circlevma 34893
[Helfgott] p. 69Statement 7.49circlemethhgt 34894
[Helfgott] p. 69Statement 7.50hgt750lema 34908  hgt750lemb 34907  hgt750leme 34909  hgt750lemf 34904  hgt750lemg 34905
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48381  tgoldbachgt 34914  tgoldbachgtALTV 48382  tgoldbachgtd 34913
[Helfgott] p. 70Statement 7.49ax-hgt749 34895
[Herstein] p. 54Exercise 28df-grpo 30635
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18962  grpoideu 30651  mndideu 18755
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18992  grpoinveu 30661
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19023  grpo2inv 30673
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19036  grpoinvop 30675
[Herstein] p. 57Exercise 1dfgrp3e 19058
[Hitchcock] p. 5Rule A3mptnan 1782
[Hitchcock] p. 5Rule A4mptxor 1783
[Hitchcock] p. 5Rule A5mtpxor 1785
[Holland] p. 1519Theorem 2sumdmdi 32562
[Holland] p. 1520Lemma 5cdj1i 32575  cdj3i 32583  cdj3lem1 32576  cdjreui 32574
[Holland] p. 1524Lemma 7mddmdin0i 32573
[Holland95] p. 13Theorem 3.6hlathil 42533
[Holland95] p. 14Line 15hgmapvs 42463
[Holland95] p. 14Line 16hdmaplkr 42485
[Holland95] p. 14Line 17hdmapellkr 42486
[Holland95] p. 14Line 19hdmapglnm2 42483
[Holland95] p. 14Line 20hdmapip0com 42489
[Holland95] p. 14Theorem 3.6hdmapevec2 42408
[Holland95] p. 14Lines 24 and 25hdmapoc 42503
[Holland95] p. 204Definition of involutiondf-srng 20862
[Holland95] p. 212Definition of subspacedf-psubsp 40075
[Holland95] p. 214Lemma 3.3lclkrlem2v 42100
[Holland95] p. 214Definition 3.2df-lpolN 42053
[Holland95] p. 214Definition of nonsingularpnonsingN 40505
[Holland95] p. 215Lemma 3.3(1)dihoml4 41949  poml4N 40525
[Holland95] p. 215Lemma 3.3(2)dochexmid 42040  pexmidALTN 40550  pexmidN 40541
[Holland95] p. 218Theorem 3.6lclkr 42105
[Holland95] p. 218Definition of dual vector spacedf-ldual 39696  ldualset 39697
[Holland95] p. 222Item 1df-lines 40073  df-pointsN 40074
[Holland95] p. 222Item 2df-polarityN 40475
[Holland95] p. 223Remarkispsubcl2N 40519  omllaw4 39818  pol1N 40482  polcon3N 40489
[Holland95] p. 223Definitiondf-psubclN 40507
[Holland95] p. 223Equation for polaritypolval2N 40478
[Holmes] p. 40Definitiondf-xrn 38827
[Hughes] p. 44Equation 1.21bax-his3 31226
[Hughes] p. 47Definition of projection operatordfpjop 32324
[Hughes] p. 49Equation 1.30eighmre 32105  eigre 31977  eigrei 31976
[Hughes] p. 49Equation 1.31eighmorth 32106  eigorth 31980  eigorthi 31979
[Hughes] p. 137Remark (ii)eigposi 31978
[Huneke] p. 1Claim 1frgrncvvdeq 30450
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30446
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30447
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30448
[Huneke] p. 2Claim 2frgrregorufr 30466  frgrregorufr0 30465  frgrregorufrg 30467
[Huneke] p. 2Claim 3frgrhash2wsp 30473  frrusgrord 30482  frrusgrord0 30481
[Huneke] p. 2Statementdf-clwwlknon 30229
[Huneke] p. 2Statement 4frgrwopreglem4 30456
[Huneke] p. 2Statement 5frgrwopreg1 30459  frgrwopreg2 30460  frgrwopregasn 30457  frgrwopregbsn 30458
[Huneke] p. 2Statement 6frgrwopreglem5 30462
[Huneke] p. 2Statement 7fusgreghash2wspv 30476
[Huneke] p. 2Statement 8fusgreghash2wsp 30479
[Huneke] p. 2Statement 9clwlksndivn 30227  numclwlk1 30512  numclwlk1lem1 30510  numclwlk1lem2 30511  numclwwlk1 30502  numclwwlk8 30533
[Huneke] p. 2Definition 3frgrwopreglem1 30453
[Huneke] p. 2Definition 4df-clwlks 29910
[Huneke] p. 2Definition 62clwwlk 30488
[Huneke] p. 2Definition 7numclwwlkovh 30514  numclwwlkovh0 30513
[Huneke] p. 2Statement 10numclwwlk2 30522
[Huneke] p. 2Statement 11rusgrnumwlkg 30119
[Huneke] p. 2Statement 12numclwwlk3 30526
[Huneke] p. 2Statement 13numclwwlk5 30529
[Huneke] p. 2Statement 14numclwwlk7 30532
[Indrzejczak] p. 33Definition ` `Enatded 30544  natded 30544
[Indrzejczak] p. 33Definition ` `Inatded 30544
[Indrzejczak] p. 34Definition ` `Enatded 30544  natded 30544
[Indrzejczak] p. 34Definition ` `Inatded 30544
[Jech] p. 4Definition of classcv 1553  cvjust 2750
[Jech] p. 42Lemma 6.1alephexp1 10527
[Jech] p. 42Equation 6.1alephadd 10525  alephmul 10526
[Jech] p. 43Lemma 6.2infmap 10524  infmap2 10163
[Jech] p. 71Lemma 9.3jech9.3 9762
[Jech] p. 72Equation 9.3scott0 9834  scottex 9833
[Jech] p. 72Exercise 9.1rankval4 9815  rankval4b 35351
[Jech] p. 72Scheme "Collection Principle"cp 9839
[Jech] p. 78Noteopthprc 5704
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43440
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43528
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43529
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43452
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43456
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43457  rmyp1 43458
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43459  rmym1 43460
[JonesMatijasevic] p. 695Equation 2.11rmx0 43450  rmx1 43451  rmxluc 43461
[JonesMatijasevic] p. 695Equation 2.12rmy0 43454  rmy1 43455  rmyluc 43462
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43464
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43465
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43485  jm2.17b 43486  jm2.17c 43487
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43518
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43522
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43513
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43488  jm2.24nn 43484
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43527
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43533  rmygeid 43489
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43545
[Juillerat] p. 11Section *5etransc 46805  etransclem47 46803  etransclem48 46804
[Juillerat] p. 12Equation (7)etransclem44 46800
[Juillerat] p. 12Equation *(7)etransclem46 46802
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46788
[Juillerat] p. 13Proofetransclem35 46791
[Juillerat] p. 13Part of case 2 proven inetransclem38 46794
[Juillerat] p. 13Part of case 2 provenetransclem24 46780
[Juillerat] p. 13Part of case 2: proven inetransclem41 46797
[Juillerat] p. 14Proofetransclem23 46779
[KalishMontague] p. 81Note 1ax-6 1981
[KalishMontague] p. 85Lemma 2equid 2026
[KalishMontague] p. 85Lemma 3equcomi 2031
[KalishMontague] p. 86Lemma 7cbvalivw 2021  cbvaliw 2020  wl-cbvmotv 37964  wl-motae 37966  wl-moteq 37965
[KalishMontague] p. 87Lemma 8spimvw 2000  spimw 1984
[KalishMontague] p. 87Lemma 9spfw 2047  spw 2048
[Kalmbach] p. 14Definition of latticechabs1 31658  chabs1i 31660  chabs2 31659  chabs2i 31661  chjass 31675  chjassi 31628  latabs1 18483  latabs2 18484
[Kalmbach] p. 15Definition of atomdf-at 32480  ela 32481
[Kalmbach] p. 15Definition of coverscvbr2 32425  cvrval2 39846
[Kalmbach] p. 16Definitiondf-ol 39750  df-oml 39751
[Kalmbach] p. 20Definition of commutescmbr 31726  cmbri 31732  cmtvalN 39783  df-cm 31725  df-cmtN 39749
[Kalmbach] p. 22Remarkomllaw5N 39819  pjoml5 31755  pjoml5i 31730
[Kalmbach] p. 22Definitionpjoml2 31753  pjoml2i 31727
[Kalmbach] p. 22Theorem 2(v)cmcm 31756  cmcmi 31734  cmcmii 31739  cmtcomN 39821
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39817  omlsi 31546  pjoml 31578  pjomli 31577
[Kalmbach] p. 22Definition of OML lawomllaw2N 39816
[Kalmbach] p. 23Remarkcmbr2i 31738  cmcm3 31757  cmcm3i 31736  cmcm3ii 31741  cmcm4i 31737  cmt3N 39823  cmt4N 39824  cmtbr2N 39825
[Kalmbach] p. 23Lemma 3cmbr3 31750  cmbr3i 31742  cmtbr3N 39826
[Kalmbach] p. 25Theorem 5fh1 31760  fh1i 31763  fh2 31761  fh2i 31764  omlfh1N 39830
[Kalmbach] p. 65Remarkchjatom 32499  chslej 31640  chsleji 31600  shslej 31522  shsleji 31512
[Kalmbach] p. 65Proposition 1chocin 31637  chocini 31596  chsupcl 31482  chsupval2 31552  h0elch 31397  helch 31385  hsupval2 31551  ocin 31438  ococss 31435  shococss 31436
[Kalmbach] p. 65Definition of subspace sumshsval 31454
[Kalmbach] p. 66Remarkdf-pjh 31537  pjssmi 32307  pjssmii 31823
[Kalmbach] p. 67Lemma 3osum 31787  osumi 31784
[Kalmbach] p. 67Lemma 4pjci 32342
[Kalmbach] p. 103Exercise 6atmd2 32542
[Kalmbach] p. 103Exercise 12mdsl0 32452
[Kalmbach] p. 140Remarkhatomic 32502  hatomici 32501  hatomistici 32504
[Kalmbach] p. 140Proposition 1atlatmstc 39891
[Kalmbach] p. 140Proposition 1(i)atexch 32523  lsatexch 39615
[Kalmbach] p. 140Proposition 1(ii)chcv1 32497  cvlcvr1 39911  cvr1 39982
[Kalmbach] p. 140Proposition 1(iii)cvexch 32516  cvexchi 32511  cvrexch 39992
[Kalmbach] p. 149Remark 2chrelati 32506  hlrelat 39974  hlrelat5N 39973  lrelat 39586
[Kalmbach] p. 153Exercise 5lsmcv 21184  lsmsatcv 39582  spansncv 31795  spansncvi 31794
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39601  spansncv2 32435
[Kalmbach] p. 266Definitiondf-st 32353
[Kalmbach2] p. 8Definition of adjointdf-adjh 31991
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10594  fpwwe2 10591
[KanamoriPincus] p. 416Corollary 1.3canth4 10595
[KanamoriPincus] p. 417Corollary 1.6canthp1 10602
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10597
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10599
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10612
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10616  gchxpidm 10617
[KanamoriPincus] p. 419Theorem 2.1gchacg 10628  gchhar 10627
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10161  unxpwdom 9527
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10618
[Kreyszig] p. 3Property M1metcl 24365  xmetcl 24364
[Kreyszig] p. 4Property M2meteq0 24372
[Kreyszig] p. 8Definition 1.1-8dscmet 24605
[Kreyszig] p. 12Equation 5conjmul 11898  muleqadd 11821
[Kreyszig] p. 18Definition 1.3-2mopnval 24471
[Kreyszig] p. 19Remarkmopntopon 24472
[Kreyszig] p. 19Theorem T1mopn0 24531  mopnm 24477
[Kreyszig] p. 19Theorem T2unimopn 24529
[Kreyszig] p. 19Definition of neighborhoodneibl 24534
[Kreyszig] p. 20Definition 1.3-3metcnp2 24575
[Kreyszig] p. 25Definition 1.4-1lmbr 23291  lmmbr 25293  lmmbr2 25294
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23413
[Kreyszig] p. 28Theorem 1.4-5lmcau 25348
[Kreyszig] p. 28Definition 1.4-3iscau 25311  iscmet2 25329
[Kreyszig] p. 30Theorem 1.4-7cmetss 25351
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23494  metelcls 25340
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25341  metcld2 25342
[Kreyszig] p. 51Equation 2clmvneg1 25134  lmodvneg1 20945  nvinv 30781  vcm 30718
[Kreyszig] p. 51Equation 1aclm0vs 25130  lmod0vs 20935  slmd0vs 33358  vc0 30716
[Kreyszig] p. 51Equation 1blmodvs0 20936  slmdvs0 33359  vcz 30717
[Kreyszig] p. 58Definition 2.2-1imsmet 30833  ngpmet 24636  nrmmetd 24607
[Kreyszig] p. 59Equation 1imsdval 30828  imsdval2 30829  ncvspds 25196  ngpds 24637
[Kreyszig] p. 63Problem 1nmval 24622  nvnd 30830
[Kreyszig] p. 64Problem 2nmeq0 24651  nmge0 24650  nvge0 30815  nvz 30811
[Kreyszig] p. 64Problem 3nmrtri 24657  nvabs 30814
[Kreyszig] p. 91Definition 2.7-1isblo3i 30943
[Kreyszig] p. 92Equation 2df-nmoo 30887
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30949  blocni 30947
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30948
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25239  ipeq0 21663  ipz 30861
[Kreyszig] p. 135Problem 2cphpyth 25251  pythi 30992
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30996
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25273
[Kreyszig] p. 144Equation 4supcvg 15862
[Kreyszig] p. 144Theorem 3.3-1minvec 25471  minveco 31026
[Kreyszig] p. 196Definition 3.9-1df-aj 30892
[Kreyszig] p. 247Theorem 4.7-2bcth 25364
[Kreyszig] p. 249Theorem 4.7-3ubth 31015
[Kreyszig] p. 470Definition of positive operator orderingleop 32265  leopg 32264
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32283
[Kreyszig] p. 525Theorem 10.1-1htth 31060
[Kulpa] p. 547Theorempoimir 38100
[Kulpa] p. 547Equation (1)poimirlem32 38099
[Kulpa] p. 547Equation (2)poimirlem31 38098
[Kulpa] p. 548Theorembroucube 38101
[Kulpa] p. 548Equation (6)poimirlem26 38093
[Kulpa] p. 548Equation (7)poimirlem27 38094
[Kunen] p. 10Axiom 0ax6e 2408  axnul 5249
[Kunen] p. 11Axiom 3axnul 5249
[Kunen] p. 12Axiom 6zfrep6 5233
[Kunen] p. 24Definition 10.24mapval 8808  mapvalg 8806
[Kunen] p. 30Lemma 10.20fodomg 10469
[Kunen] p. 31Definition 10.24mapex 7910
[Kunen] p. 95Definition 2.1df-r1 9712
[Kunen] p. 97Lemma 2.10r1elss 9754  r1elssi 9753
[Kunen] p. 107Exercise 4rankop 9806  rankopb 9800  rankuni 9811  rankxplim 9827  rankxpsuc 9830
[Kunen2] p. 47Lemma I.9.9relpfr 45478
[Kunen2] p. 53Lemma I.9.21trfr 45486
[Kunen2] p. 53Lemma I.9.24(2)wffr 45485
[Kunen2] p. 53Definition I.9.20tcfr 45487
[Kunen2] p. 95Lemma I.16.2ralabso 45492  rexabso 45493
[Kunen2] p. 96Example I.16.3disjabso 45499  n0abso 45500  ssabso 45498
[Kunen2] p. 111Lemma II.2.4(1)traxext 45501
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45511
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45506
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45509
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45510
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45505
[Kunen2] p. 112Corollary II.2.5wfaxext 45517  wfaxpr 45522  wfaxreg 45524  wfaxrep 45518  wfaxsep 45519  wfaxun 45523
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45508
[Kunen2] p. 113Corollary II.2.9wfaxpow 45521
[Kunen2] p. 114Theorem II.2.13wfaxext 45517
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45516  omelaxinf2 45513
[Kunen2] p. 114Corollary II.2.12wfac8prim 45526  wfaxinf2 45525
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45539  permaxext 45529  permaxinf2 45537  permaxnul 45532  permaxpow 45533  permaxpr 45534  permaxrep 45530  permaxsep 45531  permaxun 45535
[Kunen2] p. 148Definition II.9.1brpermmodel 45527
[Kunen2] p. 149Exercise II.9.3permac8prim 45538
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4956
[Lang] , p. 225Corollary 1.3finexttrb 33916
[Lang] p. Definitiondf-rn 5651
[Lang] p. 3Statementlidrideqd 18679  mndbn0 18760
[Lang] p. 3Definitiondf-mnd 18745
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18697
[Lang] p. 4Property of composites. Second formulagsumccat 18851
[Lang] p. 5Equationgsumreidx 19933
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48752
[Lang] p. 6Examplenn0mnd 48749
[Lang] p. 6Equationgsumxp2 19996
[Lang] p. 6Statementcycsubm 19219
[Lang] p. 6Definitionmulgnn0gsum 19098
[Lang] p. 6Observationmndlsmidm 19686
[Lang] p. 7Definitiondfgrp2e 18981
[Lang] p. 30Definitiondf-tocyc 33241
[Lang] p. 32Property (a)cyc3genpm 33286
[Lang] p. 32Property (b)cyc3conja 33291  cycpmconjv 33276
[Lang] p. 53Definitiondf-cat 17676
[Lang] p. 53Axiom CAT 1cat1 18106  cat1lem 18105
[Lang] p. 54Definitiondf-iso 17758
[Lang] p. 57Definitiondf-inito 17993  df-termo 17994
[Lang] p. 58Exampleirinitoringc 21504
[Lang] p. 58Statementinitoeu1 18020  termoeu1 18027
[Lang] p. 62Definitiondf-func 17867
[Lang] p. 65Definitiondf-nat 17955
[Lang] p. 91Notedf-ringc 20668
[Lang] p. 92Statementmxidlprm 33612
[Lang] p. 92Definitionisprmidlc 33587
[Lang] p. 128Remarkdsmmlmod 21770
[Lang] p. 129Prooflincscm 49000  lincscmcl 49002  lincsum 48999  lincsumcl 49001
[Lang] p. 129Statementlincolss 49004
[Lang] p. 129Observationdsmmfi 21763
[Lang] p. 141Theorem 5.3dimkerim 33878  qusdimsum 33879
[Lang] p. 141Corollary 5.4lssdimle 33859
[Lang] p. 147Definitionsnlindsntor 49041
[Lang] p. 504Statementmat1 22480  matring 22476
[Lang] p. 504Definitiondf-mamu 22424
[Lang] p. 505Statementmamuass 22435  mamutpos 22491  matassa 22477  mattposvs 22488  tposmap 22490
[Lang] p. 513Definitionmdet1 22634  mdetf 22628
[Lang] p. 513Theorem 4.4cramer 22724
[Lang] p. 514Proposition 4.6mdetleib 22620
[Lang] p. 514Proposition 4.8mdettpos 22644
[Lang] p. 515Definitiondf-minmar1 22668  smadiadetr 22708
[Lang] p. 515Corollary 4.9mdetero 22643  mdetralt 22641
[Lang] p. 517Proposition 4.15mdetmul 22656
[Lang] p. 518Definitiondf-madu 22667
[Lang] p. 518Proposition 4.16madulid 22678  madurid 22677  matinv 22710
[Lang] p. 561Theorem 3.1cayleyhamilton 22923
[Lang], p. 190Chapter 6vieta 33831
[Lang], p. 224Proposition 1.1extdgfialg 33945  finextalg 33949
[Lang], p. 224Proposition 1.2extdgmul 33914  fedgmul 33882
[Lang], p. 225Proposition 1.4algextdeg 33976
[Lang], p. 561Remarkchpmatply1 22865
[Lang], p. 561Definitiondf-chpmat 22860
[Lang2] p. 3Notationsdf-ind 12186
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44858
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44853
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44859
[LeBlanc] p. 277Rule R2axnul 5249
[Levy] p. 12Axiom 4.3.1df-clab 2735  wl-df.clab 37949
[Levy] p. 59Definitiondf-ttrcl 9653
[Levy] p. 64Theorem 5.6(ii)frinsg 9699
[Levy] p. 338Axiomdf-clel 2831  df-cleq 2748  wl-df.cleq 37950
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 37953
[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 37953
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2831  df-cleq 2748  wl-df.cleq 37950
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2735  wl-df.clab 37949
[Levy] p. 358Axiomdf-clab 2735  wl-df.clab 37949
[Levy58] p. 2Definition Iisfin1-3 10333
[Levy58] p. 2Definition IIdf-fin2 10233
[Levy58] p. 2Definition Iadf-fin1a 10232
[Levy58] p. 2Definition IIIdf-fin3 10235
[Levy58] p. 3Definition Vdf-fin5 10236
[Levy58] p. 3Definition IVdf-fin4 10234
[Levy58] p. 4Definition VIdf-fin6 10237
[Levy58] p. 4Definition VIIdf-fin7 10238
[Levy58], p. 3Theorem 1fin1a2 10362
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27720
[Lipparini] p. 3Lemma 2.1.4noresle 27731
[Lipparini] p. 6Proposition 4.2noinfbnd1 27763  nosupbnd1 27748
[Lipparini] p. 6Proposition 4.3noinfbnd2 27765  nosupbnd2 27750
[Lipparini] p. 7Theorem 5.1noetasuplem3 27769  noetasuplem4 27770
[Lipparini] p. 7Corollary 4.4nosupinfsep 27766
[Lopez-Astorga] p. 12Rule 1mptnan 1782
[Lopez-Astorga] p. 12Rule 2mptxor 1783
[Lopez-Astorga] p. 12Rule 3mtpxor 1785
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32550
[Maeda] p. 168Lemma 5mdsym 32554  mdsymi 32553
[Maeda] p. 168Lemma 4(i)mdsymlem4 32548  mdsymlem6 32550  mdsymlem7 32551
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32552
[MaedaMaeda] p. 1Remarkssdmd1 32455  ssdmd2 32456  ssmd1 32453  ssmd2 32454
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32451
[MaedaMaeda] p. 1Definition 1.1df-dmd 32423  df-md 32422  mdbr 32436
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32473  mdslj1i 32461  mdslj2i 32462  mdslle1i 32459  mdslle2i 32460  mdslmd1i 32471  mdslmd2i 32472
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32463  mdsl2bi 32465  mdsl2i 32464
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32477
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32474
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32475
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32452
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32457  mdsl3 32458
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32476
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32571
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39893  hlrelat1 39972
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39611
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32478  cvmdi 32466  cvnbtwn4 32431  cvrnbtwn4 39851
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32479
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39912  cvp 32517  cvrp 39988  lcvp 39612
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32541
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32540
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39905  hlexch4N 39964
[MaedaMaeda] p. 34Exercise 7.1atabsi 32543
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40015
[MaedaMaeda] p. 61Definition 15.10psubN 40321  atpsubN 40325  df-pointsN 40074  pointpsubN 40323
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40076  pmap11 40334  pmaple 40333  pmapsub 40340  pmapval 40329
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40337  pmap1N 40339
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40342  pmapglb2N 40343  pmapglb2xN 40344  pmapglbx 40341
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40424
[MaedaMaeda] p. 67Postulate PS1ps-1 40049
[MaedaMaeda] p. 68Lemma 16.2df-padd 40368  paddclN 40414  paddidm 40413
[MaedaMaeda] p. 68Condition PS2ps-2 40050
[MaedaMaeda] p. 68Equation 16.2.1paddass 40410
[MaedaMaeda] p. 69Lemma 16.4ps-1 40049
[MaedaMaeda] p. 69Theorem 16.4ps-2 40050
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19691  lsmmod2 19692  lssats 39584  shatomici 32500  shatomistici 32503  shmodi 31532  shmodsi 31531
[MaedaMaeda] p. 130Remark 29.6dmdmd 32442  mdsymlem7 32551
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31731
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31635
[MaedaMaeda] p. 139Remarksumdmdii 32557
[Margaris] p. 40Rule Cexlimiv 1944
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 399  df-ex 1794  df-or 857  dfbi2 477
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30541
[Margaris] p. 59Section 14notnotrALTVD 45438
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45439
[Margaris] p. 79Rule Cexinst01 45149  exinst11 45150
[Margaris] p. 89Theorem 19.219.2 1990  19.2g 2217  r19.2z 4447
[Margaris] p. 89Theorem 19.319.3 2231  rr19.3v 3621
[Margaris] p. 89Theorem 19.5alcom 2187
[Margaris] p. 89Theorem 19.6alex 1840
[Margaris] p. 89Theorem 19.7alnex 1795
[Margaris] p. 89Theorem 19.819.8a 2210
[Margaris] p. 89Theorem 19.919.9 2234  19.9h 2314  exlimd 2247  exlimdh 2318
[Margaris] p. 89Theorem 19.11excom 2190  excomim 2191
[Margaris] p. 89Theorem 19.1219.12 2353
[Margaris] p. 90Section 19conventions-labels 30542  conventions-labels 30542  conventions-labels 30542  conventions-labels 30542
[Margaris] p. 90Theorem 19.14exnal 1841
[Margaris] p. 90Theorem 19.152albi 44902  albi 1832
[Margaris] p. 90Theorem 19.1619.16 2254
[Margaris] p. 90Theorem 19.1719.17 2255
[Margaris] p. 90Theorem 19.182exbi 44904  exbi 1861
[Margaris] p. 90Theorem 19.1919.19 2258
[Margaris] p. 90Theorem 19.202alim 44901  2alimdv 1932  alimd 2241  alimdh 1831  alimdv 1930  ax-4 1823  ralimdaa 3257  ralimdv 3170  ralimdva 3168  ralimdvva 3203  sbcimdv 3807
[Margaris] p. 90Theorem 19.2119.21 2236  19.21h 2315  19.21t 2235  19.21vv 44900  alrimd 2244  alrimdd 2243  alrimdh 1877  alrimdv 1943  alrimi 2242  alrimih 1838  alrimiv 1941  alrimivv 1942  bj-alrimdh 37015  hbralrimi 3146  r19.21be 3249  r19.21bi 3248  ralrimd 3261  ralrimdv 3154  ralrimdva 3156  ralrimdvv 3200  ralrimdvva 3211  ralrimi 3254  ralrimia 3255  ralrimiv 3147  ralrimiva 3148  ralrimivv 3197  ralrimivva 3199  ralrimivvva 3202  ralrimivw 3152
[Margaris] p. 90Theorem 19.222exim 44903  2eximdv 1933  bj-exim 37030  exim 1848  eximd 2245  eximdh 1878  eximdv 1931  rexim 3097  reximd2a 3266  reximdai 3258  reximdd 45674  reximddv 3172  reximddv2 3215  reximddv3 3173  reximdv 3171  reximdv2 3166  reximdva 3169  reximdvai 3167  reximdvva 3204  reximi2 3089
[Margaris] p. 90Theorem 19.2319.23 2240  19.23bi 2220  19.23h 2316  19.23t 2239  exlimdv 1947  exlimdvv 1948  exlimexi 45048  exlimiv 1944  exlimivv 1946  rexlimd3 45670  rexlimdv 3155  rexlimdv3a 3161  rexlimdva 3157  rexlimdva2 3159  rexlimdvaa 3158  rexlimdvv 3212  rexlimdvva 3213  rexlimdvvva 3214  rexlimdvw 3162  rexlimiv 3150  rexlimiva 3149  rexlimivv 3198
[Margaris] p. 90Theorem 19.2419.24 2005
[Margaris] p. 90Theorem 19.2519.25 1894
[Margaris] p. 90Theorem 19.2619.26 1884
[Margaris] p. 90Theorem 19.2719.27 2256  r19.27z 4458  r19.27zv 4459
[Margaris] p. 90Theorem 19.2819.28 2257  19.28vv 44910  r19.28z 4450  r19.28zf 45685  r19.28zv 4454  rr19.28v 3622
[Margaris] p. 90Theorem 19.2919.29 1887  r19.29d2r 3143  r19.29imd 3121
[Margaris] p. 90Theorem 19.3019.30 1895
[Margaris] p. 90Theorem 19.3119.31 2263  19.31vv 44908
[Margaris] p. 90Theorem 19.3219.32 2262  r19.32 47640
[Margaris] p. 90Theorem 19.3319.33-2 44906  19.33 1898
[Margaris] p. 90Theorem 19.3419.34 2006
[Margaris] p. 90Theorem 19.3519.35 1891
[Margaris] p. 90Theorem 19.3619.36 2259  19.36vv 44907  r19.36zv 4460
[Margaris] p. 90Theorem 19.3719.37 2261  19.37vv 44909  r19.37zv 4455
[Margaris] p. 90Theorem 19.3819.38 1853
[Margaris] p. 90Theorem 19.3919.39 2004
[Margaris] p. 90Theorem 19.4019.40-2 1901  19.40 1900  r19.40 3122
[Margaris] p. 90Theorem 19.4119.41 2264  19.41rg 45074
[Margaris] p. 90Theorem 19.4219.42 2265
[Margaris] p. 90Theorem 19.4319.43 1896
[Margaris] p. 90Theorem 19.4419.44 2266  r19.44zv 4457
[Margaris] p. 90Theorem 19.4519.45 2267  r19.45zv 4456
[Margaris] p. 110Exercise 2(b)eu1 2631
[Mayet] p. 370Remarkjpi 32412  largei 32409  stri 32399
[Mayet3] p. 9Definition of CH-statesdf-hst 32354  ishst 32356
[Mayet3] p. 10Theoremhstrbi 32408  hstri 32407
[Mayet3] p. 1223Theorem 4.1mayete3i 31870
[Mayet3] p. 1240Theorem 7.1mayetes3i 31871
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32420
[MegPav2000] p. 2345Definition 3.4-1chintcl 31474  chsupcl 31482
[MegPav2000] p. 2345Definition 3.4-2hatomic 32502
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32496
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32523
[MegPav2000] p. 2366Figure 7pl42N 40555
[MegPav2002] p. 362Lemma 2.2latj31 18495  latj32 18493  latjass 18491
[Megill] p. 444Axiom C5ax-5 1924  ax5ALT 39479
[Megill] p. 444Section 7conventions 30541
[Megill] p. 445Lemma L12aecom-o 39473  ax-c11n 39460  axc11n 2451
[Megill] p. 446Lemma L17equtrr 2036
[Megill] p. 446Lemma L18ax6fromc10 39468
[Megill] p. 446Lemma L19hbnae-o 39500  hbnae 2457
[Megill] p. 447Remark 9.1dfsb1 2506  sbid 2284  sbidd-misc 50288  sbidd 50287
[Megill] p. 448Remark 9.6axc14 2488
[Megill] p. 448Scheme C4'ax-c4 39456
[Megill] p. 448Scheme C5'ax-c5 39455  sp 2212
[Megill] p. 448Scheme C6'ax-11 2185
[Megill] p. 448Scheme C7'ax-c7 39457
[Megill] p. 448Scheme C8'ax-7 2022
[Megill] p. 448Scheme C9'ax-c9 39462
[Megill] p. 448Scheme C10'ax-6 1981  ax-c10 39458
[Megill] p. 448Scheme C11'ax-c11 39459
[Megill] p. 448Scheme C12'ax-8 2138
[Megill] p. 448Scheme C13'ax-9 2146
[Megill] p. 448Scheme C14'ax-c14 39463
[Megill] p. 448Scheme C15'ax-c15 39461
[Megill] p. 448Scheme C16'ax-c16 39464
[Megill] p. 448Theorem 9.4dral1-o 39476  dral1 2464  dral2-o 39502  dral2 2463  drex1 2466  drex2 2467  drsb1 2520  drsb2 2295
[Megill] p. 449Theorem 9.7sbcom2 2200  sbequ 2110  sbid2v 2534
[Megill] p. 450Example in Appendixhba1-o 39469  hba1 2321
[Mendelson] p. 35Axiom A3hirstL-ax3 47434
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3827  rspsbca 3828  stdpc4 2092
[Mendelson] p. 69Axiom 5ax-c4 39456  ra4 3834  stdpc5 2237
[Mendelson] p. 81Rule Cexlimiv 1944
[Mendelson] p. 95Axiom 6stdpc6 2042
[Mendelson] p. 95Axiom 7stdpc7 2279
[Mendelson] p. 225Axiom system NBGru 3737
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5477
[Mendelson] p. 231Exercise 4.10(k)inv1 4346
[Mendelson] p. 231Exercise 4.10(l)unv 4347
[Mendelson] p. 231Exercise 4.10(n)dfin3 4224
[Mendelson] p. 231Exercise 4.10(o)df-nul 4281
[Mendelson] p. 231Exercise 4.10(q)dfin4 4225
[Mendelson] p. 231Exercise 4.10(s)ddif 4089
[Mendelson] p. 231Definition of uniondfun3 4223
[Mendelson] p. 235Exercise 4.12(c)univ 5412
[Mendelson] p. 235Exercise 4.12(d)pwv 4856
[Mendelson] p. 235Exercise 4.12(j)pwin 5531
[Mendelson] p. 235Exercise 4.12(k)pwunss 4567
[Mendelson] p. 235Exercise 4.12(l)pwssun 5532
[Mendelson] p. 235Exercise 4.12(n)uniin 4883
[Mendelson] p. 235Exercise 4.12(p)reli 5792
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6245
[Mendelson] p. 244Proposition 4.8(g)epweon 7747
[Mendelson] p. 246Definition of successordf-suc 6341
[Mendelson] p. 250Exercise 4.36oelim2 8553
[Mendelson] p. 254Proposition 4.22(b)xpen 9101
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9022  xpsneng 9023
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9029  xpcomeng 9030
[Mendelson] p. 254Proposition 4.22(e)xpassen 9032
[Mendelson] p. 255Definitionbrsdom 8944
[Mendelson] p. 255Exercise 4.39endisj 9025
[Mendelson] p. 255Exercise 4.41mapprc 8800
[Mendelson] p. 255Exercise 4.43mapsnen 9007  mapsnend 9006
[Mendelson] p. 255Exercise 4.45mapunen 9107
[Mendelson] p. 255Exercise 4.47xpmapen 9106
[Mendelson] p. 255Exercise 4.42(a)map0e 8853
[Mendelson] p. 255Exercise 4.42(b)map1 9010
[Mendelson] p. 257Proposition 4.24(a)undom 9026
[Mendelson] p. 258Exercise 4.56(c)djuassen 10125  djucomen 10124
[Mendelson] p. 258Exercise 4.56(f)djudom1 10129
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10123
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8488
[Mendelson] p. 266Proposition 4.34(f)oaordex 8515
[Mendelson] p. 275Proposition 4.42(d)entri3 10506
[Mendelson] p. 281Definitiondf-r1 9712
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9761
[Mendelson] p. 287Axiom system MKru 3737
[MertziosUnger] p. 152Definitiondf-frgr 30400
[MertziosUnger] p. 153Remark 1frgrconngr 30435
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30437  vdgn1frgrv3 30438
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30439
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30432
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30425  2pthfrgrrn 30423  2pthfrgrrn2 30424
[Mittelstaedt] p. 9Definitiondf-oc 31394
[Monk1] p. 22Remarkconventions 30541
[Monk1] p. 22Theorem 3.1conventions 30541
[Monk1] p. 26Theorem 2.8(vii)ssin 4185
[Monk1] p. 33Theorem 3.2(i)ssrel 5748  ssrelf 32760
[Monk1] p. 33Theorem 3.2(ii)eqrel 5749
[Monk1] p. 34Definition 3.3df-opab 5157
[Monk1] p. 36Theorem 3.7(i)coi1 6239  coi2 6240
[Monk1] p. 36Theorem 3.8(v)dm0 5889  rn0 5895
[Monk1] p. 36Theorem 3.7(ii)cnvi 5850
[Monk1] p. 37Theorem 3.13(i)relxp 5658
[Monk1] p. 37Theorem 3.13(x)dmxp 5898  rnxp 6145
[Monk1] p. 37Theorem 3.13(ii)0xp 5739  xp0 5740
[Monk1] p. 38Theorem 3.16(ii)ima0 6056
[Monk1] p. 38Theorem 3.16(viii)imai 6053
[Monk1] p. 39Theorem 3.17imaex 7884  imaexg 7883
[Monk1] p. 39Theorem 3.16(xi)imassrn 6050
[Monk1] p. 41Theorem 4.3(i)fnopfv 7045  funfvop 7020
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6910
[Monk1] p. 42Theorem 4.4(iii)fvelima 6921
[Monk1] p. 43Theorem 4.6funun 6556
[Monk1] p. 43Theorem 4.8(iv)dff13 7227  dff13f 7228
[Monk1] p. 46Theorem 4.15(v)funex 7192  funrnex 7924
[Monk1] p. 50Definition 5.4fniunfv 7220
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6203
[Monk1] p. 52Theorem 5.11(viii)ssint 4916
[Monk1] p. 52Definition 5.13 (i)1stval2 7976  df-1st 7959
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7977  df-2nd 7960
[Monk1] p. 112Theorem 15.17(v)ranksn 9802  ranksnb 9775
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9803
[Monk1] p. 112Theorem 15.17(iii)rankun 9804  rankunb 9798
[Monk1] p. 113Theorem 15.18r1val3 9786
[Monk1] p. 113Definition 15.19df-r1 9712  r1val2 9785
[Monk1] p. 117Lemmazorn2 10453  zorn2g 10450
[Monk1] p. 133Theorem 18.11cardom 9934
[Monk1] p. 133Theorem 18.12canth3 10508
[Monk1] p. 133Theorem 18.14carduni 9929
[Monk2] p. 105Axiom C4ax-4 1823
[Monk2] p. 105Axiom C7ax-7 2022
[Monk2] p. 105Axiom C8ax-12 2206  ax-c15 39461  ax12v2 2208
[Monk2] p. 108Lemma 5ax-c4 39456
[Monk2] p. 109Lemma 12ax-11 2185
[Monk2] p. 109Lemma 15equvini 2480  equvinv 2043  eqvinop 5449
[Monk2] p. 113Axiom C5-1ax-5 1924  ax5ALT 39479
[Monk2] p. 113Axiom C5-2ax-10 2169
[Monk2] p. 113Axiom C5-3ax-11 2185
[Monk2] p. 114Lemma 21sp 2212
[Monk2] p. 114Lemma 22axc4 2347  hba1-o 39469  hba1 2321
[Monk2] p. 114Lemma 23nfia1 2181
[Monk2] p. 114Lemma 24nfa2 2203  nfra2 3357  nfra2w 3292
[Moore] p. 53Part Idf-mre 17590
[Munkres] p. 77Example 2distop 23028  indistop 23035  indistopon 23034
[Munkres] p. 77Example 3fctop 23037  fctop2 23038
[Munkres] p. 77Example 4cctop 23039
[Munkres] p. 78Definition of basisdf-bases 22979  isbasis3g 22982
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17448  tgval2 22989
[Munkres] p. 79Remarktgcl 23002
[Munkres] p. 80Lemma 2.1tgval3 22996
[Munkres] p. 80Lemma 2.2tgss2 23020  tgss3 23019
[Munkres] p. 81Lemma 2.3basgen 23021  basgen2 23022
[Munkres] p. 83Exercise 3topdifinf 37791  topdifinfeq 37792  topdifinffin 37790  topdifinfindis 37788
[Munkres] p. 89Definition of subspace topologyresttop 23193
[Munkres] p. 93Theorem 6.1(1)0cld 23071  topcld 23068
[Munkres] p. 93Theorem 6.1(2)iincld 23072
[Munkres] p. 93Theorem 6.1(3)uncld 23074
[Munkres] p. 94Definition of closureclsval 23070
[Munkres] p. 94Definition of interiorntrval 23069
[Munkres] p. 95Theorem 6.5(a)clsndisj 23108  elcls 23106
[Munkres] p. 95Theorem 6.5(b)elcls3 23116
[Munkres] p. 97Theorem 6.6clslp 23181  neindisj 23150
[Munkres] p. 97Corollary 6.7cldlp 23183
[Munkres] p. 97Definition of limit pointislp2 23178  lpval 23172
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23348
[Munkres] p. 102Definition of continuous functiondf-cn 23260  iscn 23268  iscn2 23271
[Munkres] p. 107Theorem 7.2(g)cncnp 23313  cncnp2 23314  cncnpi 23311  df-cnp 23261  iscnp 23270  iscnp2 23272
[Munkres] p. 127Theorem 10.1metcn 24576
[Munkres] p. 128Theorem 10.3metcn4 25346
[Nathanson] p. 123Remarkreprgt 34872  reprinfz1 34873  reprlt 34870
[Nathanson] p. 123Definitiondf-repr 34860
[Nathanson] p. 123Chapter 5.1circlemethnat 34892
[Nathanson] p. 123Propositionbreprexp 34884  breprexpnat 34885  itgexpif 34857
[NielsenChuang] p. 195Equation 4.73unierri 32246
[OeSilva] p. 2042Section 2ax-bgbltosilva 48380
[Pfenning] p. 17Definition XMnatded 30544
[Pfenning] p. 17Definition NNCnatded 30544  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30544
[Pfenning] p. 18Rule"natded 30544
[Pfenning] p. 18Definition /\Inatded 30544
[Pfenning] p. 18Definition ` `Enatded 30544  natded 30544  natded 30544  natded 30544  natded 30544
[Pfenning] p. 18Definition ` `Inatded 30544  natded 30544  natded 30544  natded 30544  natded 30544
[Pfenning] p. 18Definition ` `ELnatded 30544
[Pfenning] p. 18Definition ` `ERnatded 30544
[Pfenning] p. 18Definition ` `Ea,unatded 30544
[Pfenning] p. 18Definition ` `IRnatded 30544
[Pfenning] p. 18Definition ` `Ianatded 30544
[Pfenning] p. 127Definition =Enatded 30544
[Pfenning] p. 127Definition =Inatded 30544
[Ponnusamy] p. 361Theorem 6.44cphip0l 25237  df-dip 30843  dip0l 30860  ip0l 21661
[Ponnusamy] p. 361Equation 6.45cphipval 25278  ipval 30845
[Ponnusamy] p. 362Equation I1dipcj 30856  ipcj 21659
[Ponnusamy] p. 362Equation I3cphdir 25240  dipdir 30984  ipdir 21664  ipdiri 30972
[Ponnusamy] p. 362Equation I4ipidsq 30852  nmsq 25229
[Ponnusamy] p. 362Equation 6.46ip0i 30967
[Ponnusamy] p. 362Equation 6.47ip1i 30969
[Ponnusamy] p. 362Equation 6.48ip2i 30970
[Ponnusamy] p. 363Equation I2cphass 25246  dipass 30987  ipass 21670  ipassi 30983
[Prugovecki] p. 186Definition of brabraval 32086  df-bra 31992
[Prugovecki] p. 376Equation 8.1df-kb 31993  kbval 32096
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32524
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40460
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32538  atcvat4i 32539  cvrat3 40014  cvrat4 40015  lsatcvat3 39624
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32424  cvrval 39841  df-cv 32421  df-lcv 39591  lspsncv0 21189
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40472
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40473
[Quine] p. 16Definition 2.1df-clab 2735  rabid 3429  rabidd 45681  wl-df.clab 37949
[Quine] p. 17Definition 2.1''dfsb7 2307
[Quine] p. 18Definition 2.7df-cleq 2748  wl-df.cleq 37950
[Quine] p. 19Definition 2.9conventions 30541  df-v 3450
[Quine] p. 34Theorem 5.1eqabb 2895
[Quine] p. 35Theorem 5.2abid1 2892  abid2f 2948
[Quine] p. 40Theorem 6.1sb5 2304
[Quine] p. 40Theorem 6.2sb6 2112  sbalex 2271
[Quine] p. 41Theorem 6.3df-clel 2831  wl-df.clel 37953
[Quine] p. 41Theorem 6.4eqid 2756  eqid1 30608
[Quine] p. 41Theorem 6.5eqcom 2763
[Quine] p. 42Theorem 6.6df-sbc 3740
[Quine] p. 42Theorem 6.7dfsbcq 3741  dfsbcq2 3742
[Quine] p. 43Theorem 6.8vex 3452
[Quine] p. 43Theorem 6.9isset 3462
[Quine] p. 44Theorem 7.3spcgf 3545  spcgv 3550  spcimgf 3512
[Quine] p. 44Theorem 6.11spsbc 3752  spsbcd 3753
[Quine] p. 44Theorem 6.12elex 3469
[Quine] p. 44Theorem 6.13elab 3633  elabg 3630  elabgf 3628
[Quine] p. 44Theorem 6.14noel 4285
[Quine] p. 48Theorem 7.2snprc 4670
[Quine] p. 48Definition 7.1df-pr 4579  df-sn 4577
[Quine] p. 49Theorem 7.4snss 4737  snssg 4736
[Quine] p. 49Theorem 7.5prss 4772  prssg 4771
[Quine] p. 49Theorem 7.6prid1 4715  prid1g 4713  prid2 4716  prid2g 4714  snid 4615  snidg 4613
[Quine] p. 51Theorem 7.12snex 5390
[Quine] p. 51Theorem 7.13prex 5389
[Quine] p. 53Theorem 8.2unisn 4878  unisnALT 45449  unisng 4877
[Quine] p. 53Theorem 8.3uniun 4882
[Quine] p. 54Theorem 8.6elssuni 4891
[Quine] p. 54Theorem 8.7uni0 4888
[Quine] p. 56Theorem 8.17uniabio 6480
[Quine] p. 56Definition 8.18dfaiota2 47628  dfiota2 6467
[Quine] p. 57Theorem 8.19aiotaval 47637  iotaval 6484
[Quine] p. 57Theorem 8.22iotanul 6490
[Quine] p. 58Theorem 8.23iotaex 6486
[Quine] p. 58Definition 9.1df-op 4583
[Quine] p. 61Theorem 9.5opabid 5489  opabidw 5488  opelopab 5506  opelopaba 5500  opelopabaf 5508  opelopabf 5509  opelopabg 5502  opelopabga 5497  opelopabgf 5504  oprabid 7417  oprabidw 7416
[Quine] p. 64Definition 9.11df-xp 5646
[Quine] p. 64Definition 9.12df-cnv 5648
[Quine] p. 64Definition 9.15df-id 5535
[Quine] p. 65Theorem 10.3fun0 6575
[Quine] p. 65Theorem 10.4funi 6542
[Quine] p. 65Theorem 10.5funsn 6563  funsng 6561
[Quine] p. 65Definition 10.1df-fun 6512
[Quine] p. 65Definition 10.2args 6071  dffv4 6853
[Quine] p. 68Definition 10.11conventions 30541  df-fv 6518  fv2 6851
[Quine] p. 124Theorem 17.3nn0opth2 14275  nn0opth2i 14274  nn0opthi 14273  omopthi 8619
[Quine] p. 177Definition 25.2df-rdg 8369
[Quine] p. 232Equation icarddom 10501
[Quine] p. 284Axiom 39(vi)funimaex 6598  funimaexg 6597
[Quine] p. 331Axiom system NFru 3737
[ReedSimon] p. 36Definition (iii)ax-his3 31226
[ReedSimon] p. 63Exercise 4(a)df-dip 30843  polid 31301  polid2i 31299  polidi 31300
[ReedSimon] p. 63Exercise 4(b)df-ph 30955
[ReedSimon] p. 195Remarklnophm 32161  lnophmi 32160
[Retherford] p. 49Exercise 1(i)leopadd 32274
[Retherford] p. 49Exercise 1(ii)leopmul 32276  leopmuli 32275
[Retherford] p. 49Exercise 1(iv)leoptr 32279
[Retherford] p. 49Definition VI.1df-leop 31994  leoppos 32268
[Retherford] p. 49Exercise 1(iii)leoptri 32278
[Retherford] p. 49Definition of operator orderingleop3 32267
[Ribenboim] p. 181Remarknprmdvdsfacm1 48181
[Ribenboim], p. 181Statementppivalnn 48189
[Roman] p. 4Definitiondf-dmat 22523  df-dmatalt 48968
[Roman] p. 18Part Preliminariesdf-rng 20175
[Roman] p. 19Part Preliminariesdf-ring 20257
[Roman] p. 46Theorem 1.6isldepslvec2 49055
[Roman] p. 112Noteisldepslvec2 49055  ldepsnlinc 49078  zlmodzxznm 49067
[Roman] p. 112Examplezlmodzxzequa 49066  zlmodzxzequap 49069  zlmodzxzldep 49074
[Roman] p. 170Theorem 7.8cayleyhamilton 22923
[Rosenlicht] p. 80Theoremheicant 38102
[Rosser] p. 281Definitiondf-op 4583
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34896
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34897
[Rotman] p. 28Remarkpgrpgt2nabl 48936  pmtr3ncom 19491
[Rotman] p. 31Theorem 3.4symggen2 19487
[Rotman] p. 42Theorem 3.15cayley 19430  cayleyth 19431
[Rudin] p. 164Equation 27efcan 16102
[Rudin] p. 164Equation 30efzval 16110
[Rudin] p. 167Equation 48absefi 16204
[Sanford] p. 39Remarkax-mp 5  mto 199
[Sanford] p. 39Rule 3mtpxor 1785
[Sanford] p. 39Rule 4mptxor 1783
[Sanford] p. 40Rule 1mptnan 1782
[Schechter] p. 51Definition of antisymmetryintasym 6092
[Schechter] p. 51Definition of irreflexivityintirr 6095
[Schechter] p. 51Definition of symmetrycnvsym 6091
[Schechter] p. 51Definition of transitivitycotr 6089
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17590
[Schechter] p. 79Definition of Moore closuredf-mrc 17591
[Schechter] p. 82Section 4.5df-mrc 17591
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17593
[Schechter] p. 139Definition AC3dfac9 10083
[Schechter] p. 141Definition (MC)dfac11 43587
[Schechter] p. 149Axiom DC1ax-dc 10393  axdc3 10401
[Schechter] p. 187Definition of "ring with unit"isring 20259  isrngo 38344
[Schechter] p. 276Remark 11.6.espan0 31684
[Schechter] p. 276Definition of spandf-span 31451  spanval 31475
[Schechter] p. 428Definition 15.35bastop1 23026
[Schloeder] p. 1Lemma 1.3onelon 6360  onelord 43776  ordelon 6359  ordelord 6357
[Schloeder] p. 1Lemma 1.7onepsuc 43777  sucidg 6418
[Schloeder] p. 1Remark 1.50elon 6390  onsuc 7782  ord0 6389  ordsuci 7780
[Schloeder] p. 1Theorem 1.9epsoon 43778
[Schloeder] p. 1Definition 1.1dftr5 5205
[Schloeder] p. 1Definition 1.2dford3 43553  elon2 6346
[Schloeder] p. 1Definition 1.4df-suc 6341
[Schloeder] p. 1Definition 1.6epel 5543  epelg 5541
[Schloeder] p. 1Theorem 1.9(i)elirr 9538  epirron 43779  ordirr 6353
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43781  oneptr 43780  ontr1 6382
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6378  oneptri 43782  ordtri3or 6367
[Schloeder] p. 2Lemma 1.10ondif1 8458  ord0eln0 6391
[Schloeder] p. 2Lemma 1.13elsuci 6404  onsucss 43791  trsucss 6425
[Schloeder] p. 2Lemma 1.14ordsucss 7787
[Schloeder] p. 2Lemma 1.15onnbtwn 6431  ordnbtwn 6430
[Schloeder] p. 2Lemma 1.16orddif0suc 43793  ordnexbtwnsuc 43792
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10348  onsucf1lem 43794  onsucf1o 43797  onsucf1olem 43795  onsucrn 43796
[Schloeder] p. 2Lemma 1.18dflim7 43798
[Schloeder] p. 2Remark 1.12ordzsl 7814
[Schloeder] p. 2Theorem 1.10ondif1i 43787  ordne0gt0 43786
[Schloeder] p. 2Definition 1.11dflim6 43789  limnsuc 43790  onsucelab 43788
[Schloeder] p. 3Remark 1.21omex 9588
[Schloeder] p. 3Theorem 1.19tfinds 7829
[Schloeder] p. 3Theorem 1.22omelon 9591  ordom 7845
[Schloeder] p. 3Definition 1.20dfom3 9592
[Schloeder] p. 4Lemma 2.21onn 8598
[Schloeder] p. 4Lemma 2.7ssonuni 7752  ssorduni 7751
[Schloeder] p. 4Remark 2.4oa1suc 8488
[Schloeder] p. 4Theorem 1.23dfom5 9595  limom 7851
[Schloeder] p. 4Definition 2.1df-1o 8425  df1o2 8432
[Schloeder] p. 4Definition 2.3oa0 8473  oa0suclim 43800  oalim 8489  oasuc 8481
[Schloeder] p. 4Definition 2.5om0 8474  om0suclim 43801  omlim 8490  omsuc 8483
[Schloeder] p. 4Definition 2.6oe0 8479  oe0m1 8478  oe0suclim 43802  oelim 8491  oesuc 8484
[Schloeder] p. 5Lemma 2.10onsupuni 43754
[Schloeder] p. 5Lemma 2.11onsupsucismax 43804
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43805
[Schloeder] p. 5Lemma 2.13limexissup 43806  limexissupab 43808  limiun 43807  limuni 6397
[Schloeder] p. 5Lemma 2.14oa0r 8495
[Schloeder] p. 5Lemma 2.15om1 8499  om1om1r 43809  om1r 8500
[Schloeder] p. 5Remark 2.8oacl 8492  oaomoecl 43803  oecl 8494  omcl 8493
[Schloeder] p. 5Definition 2.9onsupintrab 43756
[Schloeder] p. 6Lemma 2.16oe1 8501
[Schloeder] p. 6Lemma 2.17oe1m 8502
[Schloeder] p. 6Lemma 2.18oe0rif 43810
[Schloeder] p. 6Theorem 2.19oasubex 43811
[Schloeder] p. 6Theorem 2.20nnacl 8569  nnamecl 43812  nnecl 8571  nnmcl 8570
[Schloeder] p. 7Lemma 3.1onsucwordi 43813
[Schloeder] p. 7Lemma 3.2oaword1 8509
[Schloeder] p. 7Lemma 3.3oaword2 8510
[Schloeder] p. 7Lemma 3.4oalimcl 8517
[Schloeder] p. 7Lemma 3.5oaltublim 43815
[Schloeder] p. 8Lemma 3.6oaordi3 43816
[Schloeder] p. 8Lemma 3.81oaomeqom 43818
[Schloeder] p. 8Lemma 3.10oa00 8516
[Schloeder] p. 8Lemma 3.11omge1 43822  omword1 8530
[Schloeder] p. 8Remark 3.9oaordnr 43821  oaordnrex 43820
[Schloeder] p. 8Theorem 3.7oaord3 43817
[Schloeder] p. 9Lemma 3.12omge2 43823  omword2 8531
[Schloeder] p. 9Lemma 3.13omlim2 43824
[Schloeder] p. 9Lemma 3.14omord2lim 43825
[Schloeder] p. 9Lemma 3.15omord2i 43826  omordi 8523
[Schloeder] p. 9Theorem 3.16omord 8525  omord2com 43827
[Schloeder] p. 10Lemma 3.172omomeqom 43828  df-2o 8426
[Schloeder] p. 10Lemma 3.19oege1 43831  oewordi 8549
[Schloeder] p. 10Lemma 3.20oege2 43832  oeworde 8551
[Schloeder] p. 10Lemma 3.21rp-oelim2 43833
[Schloeder] p. 10Lemma 3.22oeord2lim 43834
[Schloeder] p. 10Remark 3.18omnord1 43830  omnord1ex 43829
[Schloeder] p. 11Lemma 3.23oeord2i 43835
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43837
[Schloeder] p. 11Remark 3.26oenord1 43841  oenord1ex 43840
[Schloeder] p. 11Theorem 4.1oaomoencom 43842
[Schloeder] p. 11Theorem 4.2oaass 8518
[Schloeder] p. 11Theorem 3.24oeord2com 43836
[Schloeder] p. 12Theorem 4.3odi 8536
[Schloeder] p. 13Theorem 4.4omass 8537
[Schloeder] p. 14Remark 4.6oenass 43844
[Schloeder] p. 14Theorem 4.7oeoa 8555
[Schloeder] p. 15Lemma 5.1cantnftermord 43845
[Schloeder] p. 15Lemma 5.2cantnfub 43846  cantnfub2 43847
[Schloeder] p. 16Theorem 5.3cantnf2 43850
[Schwabhauser] p. 10Axiom A1axcgrrflx 29054  axtgcgrrflx 28601
[Schwabhauser] p. 10Axiom A2axcgrtr 29055
[Schwabhauser] p. 10Axiom A3axcgrid 29056  axtgcgrid 28602
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28587
[Schwabhauser] p. 11Axiom A4axsegcon 29067  axtgsegcon 28603  df-trkgcb 28589
[Schwabhauser] p. 11Axiom A5ax5seg 29078  axtg5seg 28604  df-trkgcb 28589
[Schwabhauser] p. 11Axiom A6axbtwnid 29079  axtgbtwnid 28605  df-trkgb 28588
[Schwabhauser] p. 12Axiom A7axpasch 29081  axtgpasch 28606  df-trkgb 28588
[Schwabhauser] p. 12Axiom A8axlowdim2 29100  df-trkg2d 34916
[Schwabhauser] p. 13Axiom A8axtglowdim2 28609
[Schwabhauser] p. 13Axiom A9axtgupdim2 28610  df-trkg2d 34916
[Schwabhauser] p. 13Axiom A10axeuclid 29103  axtgeucl 28611  df-trkge 28590
[Schwabhauser] p. 13Axiom A11axcont 29116  axtgcont 28608  axtgcont1 28607  df-trkgb 28588
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36285
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36287
[Schwabhauser] p. 27Theorem 2.3cgrtr 36290
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36294
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36295  tgcgrcomimp 28616  tgcgrcoml 28618  tgcgrcomr 28617
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36300  tgcgrtriv 28623
[Schwabhauser] p. 28Theorem 2.105segofs 36304  tg5segofs 34927
[Schwabhauser] p. 28Definition 2.10df-afs 34924  df-ofs 36281
[Schwabhauser] p. 29Theorem 2.11cgrextend 36306  tgcgrextend 28624
[Schwabhauser] p. 29Theorem 2.12segconeq 36308  tgsegconeq 28625
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36320  btwntriv2 36310  tgbtwntriv2 28626
[Schwabhauser] p. 30Theorem 3.2btwncomim 36311  tgbtwncom 28627
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36314  tgbtwntriv1 28630
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36315  tgbtwnswapid 28631
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36321  btwnintr 36317  tgbtwnexch2 28635  tgbtwnintr 28632
[Schwabhauser] p. 30Theorem 3.6btwnexch 36323  btwnexch3 36318  tgbtwnexch 28637  tgbtwnexch3 28633
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36322  tgbtwnouttr 28636  tgbtwnouttr2 28634
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29099
[Schwabhauser] p. 32Theorem 3.14btwndiff 36325  tgbtwndiff 28645
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28638  trisegint 36326
[Schwabhauser] p. 34Theorem 4.2ifscgr 36342  tgifscgr 28647
[Schwabhauser] p. 34Theorem 4.11colcom 28697  colrot1 28698  colrot2 28699  lncom 28761  lnrot1 28762  lnrot2 28763
[Schwabhauser] p. 34Definition 4.1df-ifs 36338
[Schwabhauser] p. 35Theorem 4.3cgrsub 36343  tgcgrsub 28648
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36353  tgcgrxfr 28657
[Schwabhauser] p. 35Statement 4.4ercgrg 28656
[Schwabhauser] p. 35Definition 4.4df-cgr3 36339  df-cgrg 28650
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28650
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36354  tgbtwnxfr 28669
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36360  colinearperm2 36362  colinearperm3 36361  colinearperm4 36363  colinearperm5 36364
[Schwabhauser] p. 36Definition 4.8df-ismt 28672
[Schwabhauser] p. 36Definition 4.10df-colinear 36337  tgellng 28692  tglng 28685
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36365
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36373  lnxfr 28705
[Schwabhauser] p. 37Theorem 4.14lineext 36374  lnext 28706
[Schwabhauser] p. 37Theorem 4.16fscgr 36378  tgfscgr 28707
[Schwabhauser] p. 37Theorem 4.17linecgr 36379  lncgr 28708
[Schwabhauser] p. 37Definition 4.15df-fs 36340
[Schwabhauser] p. 38Theorem 4.18lineid 36381  lnid 28709
[Schwabhauser] p. 38Theorem 4.19idinside 36382  tgidinside 28710
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36399  tgbtwnconn1 28714
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36400  tgbtwnconn2 28715
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36401  tgbtwnconn3 28716
[Schwabhauser] p. 41Theorem 5.5brsegle2 36407
[Schwabhauser] p. 41Definition 5.4df-segle 36405  legov 28724
[Schwabhauser] p. 41Definition 5.5legov2 28725
[Schwabhauser] p. 42Remark 5.13legso 28738
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36408
[Schwabhauser] p. 42Theorem 5.7seglerflx 36410
[Schwabhauser] p. 42Theorem 5.8segletr 36412
[Schwabhauser] p. 42Theorem 5.9segleantisym 36413
[Schwabhauser] p. 42Theorem 5.10seglelin 36414
[Schwabhauser] p. 42Theorem 5.11seglemin 36411
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36416
[Schwabhauser] p. 42Proposition 5.7legid 28726
[Schwabhauser] p. 42Proposition 5.8legtrd 28728
[Schwabhauser] p. 42Proposition 5.9legtri3 28729
[Schwabhauser] p. 42Proposition 5.10legtrid 28730
[Schwabhauser] p. 42Proposition 5.11leg0 28731
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36423
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36424
[Schwabhauser] p. 43Theorem 6.4broutsideof 36419  df-outsideof 36418
[Schwabhauser] p. 43Definition 6.1broutsideof2 36420  ishlg 28741
[Schwabhauser] p. 44Theorem 6.4hlln 28746
[Schwabhauser] p. 44Theorem 6.5hlid 28748  outsideofrflx 36425
[Schwabhauser] p. 44Theorem 6.6hlcomb 28742  hlcomd 28743  outsideofcom 36426
[Schwabhauser] p. 44Theorem 6.7hltr 28749  outsideoftr 36427
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28757  outsideofeu 36429
[Schwabhauser] p. 44Definition 6.8df-ray 36436
[Schwabhauser] p. 45Part 2df-lines2 36437
[Schwabhauser] p. 45Theorem 6.13outsidele 36430
[Schwabhauser] p. 45Theorem 6.15lineunray 36445
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36446  tglineelsb2 28771
[Schwabhauser] p. 45Theorem 6.17linecom 36448  linerflx1 36447  linerflx2 36449  tglinecom 28774  tglinerflx1 28772  tglinerflx2 28773
[Schwabhauser] p. 45Theorem 6.18linethru 36451  tglinethru 28775
[Schwabhauser] p. 45Definition 6.14df-line2 36435  tglng 28685
[Schwabhauser] p. 45Proposition 6.13legbtwn 28733
[Schwabhauser] p. 46Theorem 6.19linethrueu 36454  tglinethrueu 28778
[Schwabhauser] p. 46Theorem 6.21lineintmo 36455  tglineineq 28782  tglineinteq 28784  tglineintmo 28781
[Schwabhauser] p. 46Theorem 6.23colline 28788
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28789
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28790
[Schwabhauser] p. 49Theorem 7.3mirinv 28805
[Schwabhauser] p. 49Theorem 7.7mirmir 28801
[Schwabhauser] p. 49Theorem 7.8mirreu3 28793
[Schwabhauser] p. 49Definition 7.5df-mir 28792  ismir 28798  mirbtwn 28797  mircgr 28796  mirfv 28795  mirval 28794
[Schwabhauser] p. 50Theorem 7.8mirreu 28803
[Schwabhauser] p. 50Theorem 7.9mireq 28804
[Schwabhauser] p. 50Theorem 7.10mirinv 28805
[Schwabhauser] p. 50Theorem 7.11mirf1o 28808
[Schwabhauser] p. 50Theorem 7.13miriso 28809
[Schwabhauser] p. 51Theorem 7.14mirmot 28814
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28811  mirbtwni 28810
[Schwabhauser] p. 51Theorem 7.16mircgrs 28812
[Schwabhauser] p. 51Theorem 7.17miduniq 28824
[Schwabhauser] p. 52Lemma 7.21symquadlem 28828
[Schwabhauser] p. 52Theorem 7.18miduniq1 28825
[Schwabhauser] p. 52Theorem 7.19miduniq2 28826
[Schwabhauser] p. 52Theorem 7.20colmid 28827
[Schwabhauser] p. 53Lemma 7.22krippen 28830
[Schwabhauser] p. 55Lemma 7.25midexlem 28831
[Schwabhauser] p. 57Theorem 8.2ragcom 28837
[Schwabhauser] p. 57Definition 8.1df-rag 28833  israg 28836
[Schwabhauser] p. 58Theorem 8.3ragcol 28838
[Schwabhauser] p. 58Theorem 8.4ragmir 28839
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28841
[Schwabhauser] p. 58Theorem 8.6ragflat2 28842
[Schwabhauser] p. 58Theorem 8.7ragflat 28843
[Schwabhauser] p. 58Theorem 8.8ragtriva 28844
[Schwabhauser] p. 58Theorem 8.9ragflat3 28845  ragncol 28848
[Schwabhauser] p. 58Theorem 8.10ragcgr 28846
[Schwabhauser] p. 59Theorem 8.12perpcom 28852
[Schwabhauser] p. 59Theorem 8.13ragperp 28856
[Schwabhauser] p. 59Theorem 8.14perpneq 28853
[Schwabhauser] p. 59Definition 8.11df-perpg 28835  isperp 28851
[Schwabhauser] p. 59Definition 8.13isperp2 28854
[Schwabhauser] p. 60Theorem 8.18foot 28861
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28869  colperpexlem2 28870
[Schwabhauser] p. 63Theorem 8.21colperpex 28872  colperpexlem3 28871
[Schwabhauser] p. 64Theorem 8.22mideu 28877  midex 28876
[Schwabhauser] p. 66Lemma 8.24opphllem 28874
[Schwabhauser] p. 67Theorem 9.2oppcom 28883
[Schwabhauser] p. 67Definition 9.1islnopp 28878
[Schwabhauser] p. 68Lemma 9.3opphllem2 28887
[Schwabhauser] p. 68Lemma 9.4opphllem5 28890  opphllem6 28891
[Schwabhauser] p. 69Theorem 9.5opphl 28893
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28606
[Schwabhauser] p. 70Theorem 9.6outpasch 28894
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28902
[Schwabhauser] p. 71Definition 9.7df-hpg 28897  hpgbr 28899
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28904
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28903
[Schwabhauser] p. 72Theorem 9.11hpgid 28905
[Schwabhauser] p. 72Theorem 9.12hpgcom 28906
[Schwabhauser] p. 72Theorem 9.13hpgtr 28907
[Schwabhauser] p. 73Theorem 9.18colopp 28908
[Schwabhauser] p. 73Theorem 9.19colhp 28909
[Schwabhauser] p. 88Theorem 10.2lmieu 28923
[Schwabhauser] p. 88Definition 10.1df-mid 28913
[Schwabhauser] p. 89Theorem 10.4lmicom 28927
[Schwabhauser] p. 89Theorem 10.5lmilmi 28928
[Schwabhauser] p. 89Theorem 10.6lmireu 28929
[Schwabhauser] p. 89Theorem 10.7lmieq 28930
[Schwabhauser] p. 89Theorem 10.8lmiinv 28931
[Schwabhauser] p. 89Theorem 10.9lmif1o 28934
[Schwabhauser] p. 89Theorem 10.10lmiiso 28936
[Schwabhauser] p. 89Definition 10.3df-lmi 28914
[Schwabhauser] p. 90Theorem 10.11lmimot 28937
[Schwabhauser] p. 91Theorem 10.12hypcgr 28940
[Schwabhauser] p. 92Theorem 10.14lmiopp 28941
[Schwabhauser] p. 92Theorem 10.15lnperpex 28942
[Schwabhauser] p. 92Theorem 10.16trgcopy 28943  trgcopyeu 28945
[Schwabhauser] p. 95Definition 11.2dfcgra2 28969
[Schwabhauser] p. 95Definition 11.3iscgra 28948
[Schwabhauser] p. 95Proposition 11.4cgracgr 28957
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28955  cgrahl2 28956
[Schwabhauser] p. 96Theorem 11.6cgraid 28958
[Schwabhauser] p. 96Theorem 11.9cgraswap 28959
[Schwabhauser] p. 97Theorem 11.7cgracom 28961
[Schwabhauser] p. 97Theorem 11.8cgratr 28962
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28965  cgrahl 28966
[Schwabhauser] p. 98Theorem 11.13sacgr 28970
[Schwabhauser] p. 98Theorem 11.14oacgr 28971
[Schwabhauser] p. 98Theorem 11.15acopy 28972  acopyeu 28973
[Schwabhauser] p. 101Theorem 11.24inagswap 28980
[Schwabhauser] p. 101Theorem 11.25inaghl 28984
[Schwabhauser] p. 101Definition 11.23isinag 28977
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28992
[Schwabhauser] p. 102Definition 11.27df-leag 28985  isleag 28986
[Schwabhauser] p. 107Theorem 11.49tgsas 28994  tgsas1 28993  tgsas2 28995  tgsas3 28996
[Schwabhauser] p. 108Theorem 11.50tgasa 28998  tgasa1 28997
[Schwabhauser] p. 109Theorem 11.51tgsss1 28999  tgsss2 29000  tgsss3 29001
[Shapiro] p. 230Theorem 6.5.1dchrhash 27305  dchrsum 27303  dchrsum2 27302  sumdchr 27306
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27307  sum2dchr 27308
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20084  ablfacrp2 20085
[Shapiro], p. 328Equation 9.2.4vmasum 27250
[Shapiro], p. 329Equation 9.2.7logfac2 27251
[Shapiro], p. 329Equation 9.2.9logfacrlim 27258
[Shapiro], p. 331Equation 9.2.13vmadivsum 27516
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27519
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27573  vmalogdivsum2 27572
[Shapiro], p. 375Theorem 9.4.1dirith 27563  dirith2 27562
[Shapiro], p. 375Equation 9.4.3rplogsum 27561  rpvmasum 27560  rpvmasum2 27546
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27521
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27559
[Shapiro], p. 377Lemma 9.4.1dchrisum 27526  dchrisumlem1 27523  dchrisumlem2 27524  dchrisumlem3 27525  dchrisumlema 27522
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27529
[Shapiro], p. 379Equation 9.4.16dchrmusum 27558  dchrmusumlem 27556  dchrvmasumlem 27557
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27528
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27530
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27554  dchrisum0re 27547  dchrisumn0 27555
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27540
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27544
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27545
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27600  pntrsumbnd2 27601  pntrsumo1 27599
[Shapiro], p. 405Equation 10.2.1mudivsum 27564
[Shapiro], p. 406Equation 10.2.6mulogsum 27566
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27568
[Shapiro], p. 407Equation 10.2.8mulog2sum 27571
[Shapiro], p. 418Equation 10.4.6logsqvma 27576
[Shapiro], p. 418Equation 10.4.8logsqvma2 27577
[Shapiro], p. 419Equation 10.4.10selberg 27582
[Shapiro], p. 420Equation 10.4.12selberg2lem 27584
[Shapiro], p. 420Equation 10.4.14selberg2 27585
[Shapiro], p. 422Equation 10.6.7selberg3 27593
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27594
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27591  selberg3lem2 27592
[Shapiro], p. 422Equation 10.4.23selberg4 27595
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27589
[Shapiro], p. 428Equation 10.6.2selbergr 27602
[Shapiro], p. 429Equation 10.6.8selberg3r 27603
[Shapiro], p. 430Equation 10.6.11selberg4r 27604
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27618
[Shapiro], p. 434Equation 10.6.27pntlema 27630  pntlemb 27631  pntlemc 27629  pntlemd 27628  pntlemg 27632
[Shapiro], p. 435Equation 10.6.29pntlema 27630
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27622
[Shapiro], p. 436Lemma 10.6.2pntibnd 27627
[Shapiro], p. 436Equation 10.6.34pntlema 27630
[Shapiro], p. 436Equation 10.6.35pntlem3 27643  pntleml 27645
[Stewart] p. 91Lemma 7.3constrss 33994
[Stewart] p. 92Definition 7.4.df-constr 33981
[Stewart] p. 96Theorem 7.10constraddcl 34013  constrinvcl 34024  constrmulcl 34022  constrnegcl 34014  constrsqrtcl 34030
[Stewart] p. 97Theorem 7.11constrextdg2 34000
[Stewart] p. 98Theorem 7.12constrext2chn 34010
[Stewart] p. 99Theorem 7.132sqr3nconstr 34032
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34042
[Stoll] p. 13Definition corresponds to dfsymdif3 4253
[Stoll] p. 16Exercise 4.40dif 4353  dif0 4325
[Stoll] p. 16Exercise 4.8difdifdir 4439
[Stoll] p. 17Theorem 5.1(5)unvdif 4423
[Stoll] p. 19Theorem 5.2(13)undm 4244
[Stoll] p. 19Theorem 5.2(13')indm 4245
[Stoll] p. 20Remarkinvdif 4226
[Stoll] p. 25Definition of ordered tripledf-ot 4585
[Stoll] p. 43Definitionuniiun 5010
[Stoll] p. 44Definitionintiin 5011
[Stoll] p. 45Definitiondf-iin 4946
[Stoll] p. 45Definition indexed uniondf-iun 4945
[Stoll] p. 176Theorem 3.4(27)iman 404
[Stoll] p. 262Example 4.1dfsymdif3 4253
[Strang] p. 242Section 6.3expgrowth 44859
[Suppes] p. 22Theorem 2eq0 4297  eq0f 4294
[Suppes] p. 22Theorem 4eqss 3946  eqssd 3948  eqssi 3947
[Suppes] p. 23Theorem 5ss0 4350  ss0b 4349
[Suppes] p. 23Theorem 6sstr 3939  sstrALT2 45358
[Suppes] p. 23Theorem 7pssirr 4051
[Suppes] p. 23Theorem 8pssn2lp 4053
[Suppes] p. 23Theorem 9psstr 4056
[Suppes] p. 23Theorem 10pssss 4046
[Suppes] p. 25Theorem 12elin 3915  elun 4101
[Suppes] p. 26Theorem 15inidm 4173
[Suppes] p. 26Theorem 16in0 4343
[Suppes] p. 27Theorem 23unidm 4105
[Suppes] p. 27Theorem 24un0 4342
[Suppes] p. 27Theorem 25ssun1 4125
[Suppes] p. 27Theorem 26ssequn1 4133
[Suppes] p. 27Theorem 27unss 4137
[Suppes] p. 27Theorem 28indir 4233
[Suppes] p. 27Theorem 29undir 4234
[Suppes] p. 28Theorem 32difid 4323
[Suppes] p. 29Theorem 33difin 4219
[Suppes] p. 29Theorem 34indif 4227
[Suppes] p. 29Theorem 35undif1 4424
[Suppes] p. 29Theorem 36difun2 4429
[Suppes] p. 29Theorem 37difin0 4422
[Suppes] p. 29Theorem 38disjdif 4420
[Suppes] p. 29Theorem 39difundi 4237
[Suppes] p. 29Theorem 40difindi 4239
[Suppes] p. 30Theorem 41nalset 5258
[Suppes] p. 39Theorem 61uniss 4867
[Suppes] p. 39Theorem 65uniop 5478
[Suppes] p. 41Theorem 70intsn 4936
[Suppes] p. 42Theorem 71intpr 4934  intprg 4933
[Suppes] p. 42Theorem 73op1stb 5433
[Suppes] p. 42Theorem 78intun 4932
[Suppes] p. 44Definition 15(a)dfiun2 4983  dfiun2g 4981
[Suppes] p. 44Definition 15(b)dfiin2 4984
[Suppes] p. 47Theorem 86elpw 4553  elpw2 5284  elpw2g 5283  elpwg 4552  elpwgdedVD 45440
[Suppes] p. 47Theorem 87pwid 4572
[Suppes] p. 47Theorem 89pw0 4764
[Suppes] p. 48Theorem 90pwpw0 4765
[Suppes] p. 52Theorem 101xpss12 5655
[Suppes] p. 52Theorem 102xpindi 5798  xpindir 5799
[Suppes] p. 52Theorem 103xpundi 5709  xpundir 5710
[Suppes] p. 54Theorem 105elirrv 9535
[Suppes] p. 58Theorem 2relss 5747
[Suppes] p. 59Theorem 4eldm 5869  eldm2 5870  eldm2g 5868  eldmg 5867
[Suppes] p. 59Definition 3df-dm 5650
[Suppes] p. 60Theorem 6dmin 5880
[Suppes] p. 60Theorem 8rnun 6119
[Suppes] p. 60Theorem 9rnin 6120
[Suppes] p. 60Definition 4dfrn2 5857
[Suppes] p. 61Theorem 11brcnv 5847  brcnvg 5844
[Suppes] p. 62Equation 5elcnv 5841  elcnv2 5842
[Suppes] p. 62Theorem 12relcnv 6083
[Suppes] p. 62Theorem 15cnvin 6118
[Suppes] p. 62Theorem 16cnvun 6116
[Suppes] p. 63Definitiondftrrels2 39106
[Suppes] p. 63Theorem 20co02 6237
[Suppes] p. 63Theorem 21dmcoss 5944
[Suppes] p. 63Definition 7df-co 5649
[Suppes] p. 64Theorem 26cnvco 5854
[Suppes] p. 64Theorem 27coass 6242
[Suppes] p. 65Theorem 31resundi 5972
[Suppes] p. 65Theorem 34elima 6044  elima2 6045  elima3 6046  elimag 6043
[Suppes] p. 65Theorem 35imaundi 6124
[Suppes] p. 66Theorem 40dminss 6128
[Suppes] p. 66Theorem 41imainss 6129
[Suppes] p. 67Exercise 11cnvxp 6132
[Suppes] p. 81Definition 34dfec2 8669
[Suppes] p. 82Theorem 72elec 8713  elecALTV 38718  elecg 8711
[Suppes] p. 82Theorem 73eqvrelth 39142  erth 8721  erth2 8722
[Suppes] p. 83Theorem 74eqvreldisj 39145  erdisj 8724
[Suppes] p. 83Definition 35, df-parts 39315  dfmembpart2 39320
[Suppes] p. 89Theorem 96map0b 8854
[Suppes] p. 89Theorem 97map0 8858  map0g 8855
[Suppes] p. 89Theorem 98mapsn 8859  mapsnd 8857
[Suppes] p. 89Theorem 99mapss 8860
[Suppes] p. 91Definition 12(ii)alephsuc 10014
[Suppes] p. 91Definition 12(iii)alephlim 10013
[Suppes] p. 92Theorem 1enref 8955  enrefg 8954
[Suppes] p. 92Theorem 2ensym 8973  ensymb 8972  ensymi 8974
[Suppes] p. 92Theorem 3entr 8976
[Suppes] p. 92Theorem 4unen 9015
[Suppes] p. 94Theorem 15endom 8949
[Suppes] p. 94Theorem 16ssdomg 8970
[Suppes] p. 94Theorem 17domtr 8977
[Suppes] p. 95Theorem 18sbth 9058
[Suppes] p. 97Theorem 23canth2 9091  canth2g 9092
[Suppes] p. 97Definition 3brsdom2 9062  df-sdom 8919  dfsdom2 9061
[Suppes] p. 97Theorem 21(i)sdomirr 9075
[Suppes] p. 97Theorem 22(i)domnsym 9064
[Suppes] p. 97Theorem 21(ii)sdomnsym 9063
[Suppes] p. 97Theorem 22(ii)domsdomtr 9073
[Suppes] p. 97Theorem 22(iv)brdom2 8952
[Suppes] p. 97Theorem 21(iii)sdomtr 9076
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9071
[Suppes] p. 98Exercise 4fundmen 9001  fundmeng 9002
[Suppes] p. 98Exercise 6xpdom3 9036
[Suppes] p. 98Exercise 11sdomentr 9072
[Suppes] p. 104Theorem 37fofi 9246
[Suppes] p. 104Theorem 38pwfi 9252
[Suppes] p. 105Theorem 40pwfi 9252
[Suppes] p. 111Axiom for cardinal numberscarden 10498
[Suppes] p. 130Definition 3df-tr 5202
[Suppes] p. 132Theorem 9ssonuni 7752
[Suppes] p. 134Definition 6df-suc 6341
[Suppes] p. 136Theorem Schema 22findes 7870  finds 7866  finds1 7869  finds2 7868
[Suppes] p. 151Theorem 42isfinite 9597  isfinite2 9231  isfiniteg 9233  unbnn 9229
[Suppes] p. 162Definition 5df-ltnq 10866  df-ltpq 10858
[Suppes] p. 197Theorem Schema 4tfindes 7832  tfinds 7829  tfinds2 7833
[Suppes] p. 209Theorem 18oaord1 8508
[Suppes] p. 209Theorem 21oaword2 8510
[Suppes] p. 211Theorem 25oaass 8518
[Suppes] p. 225Definition 8iscard2 9924
[Suppes] p. 227Theorem 56ondomon 10510
[Suppes] p. 228Theorem 59harcard 9926
[Suppes] p. 228Definition 12(i)aleph0 10012
[Suppes] p. 228Theorem Schema 61onintss 6387
[Suppes] p. 228Theorem Schema 62onminesb 7765  onminsb 7766
[Suppes] p. 229Theorem 64alephval2 10520
[Suppes] p. 229Theorem 65alephcard 10016
[Suppes] p. 229Theorem 66alephord2i 10023
[Suppes] p. 229Theorem 67alephnbtwn 10017
[Suppes] p. 229Definition 12df-aleph 9888
[Suppes] p. 242Theorem 6weth 10442
[Suppes] p. 242Theorem 8entric 10504
[Suppes] p. 242Theorem 9carden 10498
[Szendrei] p. 11Line 6df-cloneop 35994
[Szendrei] p. 11Paragraph 3df-suppos 35998
[TakeutiZaring] p. 8Axiom 1ax-ext 2728
[TakeutiZaring] p. 13Definition 4.5df-cleq 2748  wl-df.cleq 37950
[TakeutiZaring] p. 13Proposition 4.6df-clel 2831  wl-df.clel 37953
[TakeutiZaring] p. 13Proposition 4.9cvjust 2750
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2776
[TakeutiZaring] p. 14Definition 4.16df-oprab 7389
[TakeutiZaring] p. 14Proposition 4.14ru 3737
[TakeutiZaring] p. 15Axiom 2zfpair 5372
[TakeutiZaring] p. 15Exercise 1elpr 4601  elpr2 4603  elpr2g 4602  elprg 4599
[TakeutiZaring] p. 15Exercise 2elsn 4591  elsn2 4618  elsn2g 4617  elsng 4590  velsn 4592
[TakeutiZaring] p. 15Exercise 3elop 5429
[TakeutiZaring] p. 15Exercise 4sneq 4586  sneqr 4792
[TakeutiZaring] p. 15Definition 5.1dfpr2 4597  dfsn2 4589  dfsn2ALT 4598
[TakeutiZaring] p. 16Axiom 3uniex 7713
[TakeutiZaring] p. 16Exercise 6opth 5438
[TakeutiZaring] p. 16Exercise 7opex 5425
[TakeutiZaring] p. 16Exercise 8rext 5409
[TakeutiZaring] p. 16Corollary 5.8unex 7716  unexg 7715
[TakeutiZaring] p. 16Definition 5.3dftp2 4644
[TakeutiZaring] p. 16Definition 5.5df-uni 4860
[TakeutiZaring] p. 16Definition 5.6df-in 3906  df-un 3904
[TakeutiZaring] p. 16Proposition 5.7unipr 4876  uniprg 4875
[TakeutiZaring] p. 17Axiom 4vpwex 5328
[TakeutiZaring] p. 17Exercise 1eltp 4642
[TakeutiZaring] p. 17Exercise 5elsuc 6407  elsucg 6405  sstr2 3938
[TakeutiZaring] p. 17Exercise 6uncom 4106
[TakeutiZaring] p. 17Exercise 7incom 4156
[TakeutiZaring] p. 17Exercise 8unass 4119
[TakeutiZaring] p. 17Exercise 9inass 4174
[TakeutiZaring] p. 17Exercise 10indi 4231
[TakeutiZaring] p. 17Exercise 11undi 4232
[TakeutiZaring] p. 17Definition 5.9df-pss 3919  df-ss 3916
[TakeutiZaring] p. 17Definition 5.10df-pw 4551
[TakeutiZaring] p. 18Exercise 7unss2 4134
[TakeutiZaring] p. 18Exercise 9dfss2 3917  sseqin2 4170
[TakeutiZaring] p. 18Exercise 10ssid 3953
[TakeutiZaring] p. 18Exercise 12inss1 4183  inss2 4184
[TakeutiZaring] p. 18Exercise 13nss 3995
[TakeutiZaring] p. 18Exercise 15unieq 4870
[TakeutiZaring] p. 18Exercise 18sspwb 5410  sspwimp 45441  sspwimpALT 45448  sspwimpALT2 45451  sspwimpcf 45443
[TakeutiZaring] p. 18Exercise 19pweqb 5417
[TakeutiZaring] p. 19Axiom 5ax-rep 5221
[TakeutiZaring] p. 20Definitiondf-rab 3409
[TakeutiZaring] p. 20Corollary 5.160ex 5251
[TakeutiZaring] p. 20Definition 5.12df-dif 3902
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 36961  dfnul2 4283
[TakeutiZaring] p. 20Proposition 5.15difid 4323
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4300  n0f 4296  neq0 4299  neq0f 4295
[TakeutiZaring] p. 21Axiom 6zfreg 9534
[TakeutiZaring] p. 21Axiom 6'zfregs 9677
[TakeutiZaring] p. 21Theorem 5.22setind 9692
[TakeutiZaring] p. 21Definition 5.20df-v 3450
[TakeutiZaring] p. 21Proposition 5.21vprc 5264
[TakeutiZaring] p. 22Exercise 10ss 4348
[TakeutiZaring] p. 22Exercise 3ssex 5271  ssexg 5273
[TakeutiZaring] p. 22Exercise 4inex1 5267
[TakeutiZaring] p. 22Exercise 5ruv 9546
[TakeutiZaring] p. 22Exercise 6elirr 9538
[TakeutiZaring] p. 22Exercise 7ssdif0 4313
[TakeutiZaring] p. 22Exercise 11difdif 4083
[TakeutiZaring] p. 22Exercise 13undif3 4247  undif3VD 45405
[TakeutiZaring] p. 22Exercise 14difss 4084
[TakeutiZaring] p. 22Exercise 15sscon 4091
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3071
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3081
[TakeutiZaring] p. 23Proposition 6.2xpex 7725  xpexg 7722
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5647
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6581
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6760  fun11 6584
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6523  svrelfun 6582
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5856
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5858
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5652
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5653
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5649
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6169  dfrel2 6164
[TakeutiZaring] p. 25Exercise 3xpss 5656
[TakeutiZaring] p. 25Exercise 5relun 5777
[TakeutiZaring] p. 25Exercise 6reluni 5784
[TakeutiZaring] p. 25Exercise 9inxp 5797
[TakeutiZaring] p. 25Exercise 12relres 5984
[TakeutiZaring] p. 25Exercise 13opelres 5964  opelresi 5966
[TakeutiZaring] p. 25Exercise 14dmres 5991
[TakeutiZaring] p. 25Exercise 15resss 5980
[TakeutiZaring] p. 25Exercise 17resabs1 5985
[TakeutiZaring] p. 25Exercise 18funres 6552
[TakeutiZaring] p. 25Exercise 24relco 6087
[TakeutiZaring] p. 25Exercise 29funco 6550
[TakeutiZaring] p. 25Exercise 30f1co 6762
[TakeutiZaring] p. 26Definition 6.10eu2 2630
[TakeutiZaring] p. 26Definition 6.11conventions 30541  df-fv 6518  fv3 6874
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7895  cnvexg 7894
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7879  dmexg 7871
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7880  rnexg 7872
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44977
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7890
[TakeutiZaring] p. 27Corollary 6.13fvex 6869
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47716  tz6.12-1-afv2 47783  tz6.12-1 6879  tz6.12-afv 47715  tz6.12-afv2 47782  tz6.12 6880  tz6.12c-afv2 47784  tz6.12c 6878
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47779  tz6.12-2 6843  tz6.12i-afv2 47785  tz6.12i 6882
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6513
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6514
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6516  wfo 6508
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6515  wf1 6507
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6517  wf1o 6509
[TakeutiZaring] p. 28Exercise 4eqfnfv 7000  eqfnfv2 7001  eqfnfv2f 7004
[TakeutiZaring] p. 28Exercise 5fvco 6954
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7190
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7188
[TakeutiZaring] p. 29Exercise 9funimaex 6598  funimaexg 6597
[TakeutiZaring] p. 29Definition 6.18df-br 5095
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5549
[TakeutiZaring] p. 30Definition 6.21dffr2 5601  dffr3 6078  eliniseg 6073  iniseg 6076
[TakeutiZaring] p. 30Definition 6.22df-eprel 5540
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5617  fr3nr 7744  frirr 5616
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5593
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7746
[TakeutiZaring] p. 31Exercise 1frss 5604
[TakeutiZaring] p. 31Exercise 4wess 5626
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6323  tz6.26i 6324  wefrc 5634  wereu2 5637
[TakeutiZaring] p. 32Theorem 6.27wfi 6325  wfii 6326
[TakeutiZaring] p. 32Definition 6.28df-isom 6519
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7302
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7303
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7309
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7310
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7311
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7315
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7322
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7324
[TakeutiZaring] p. 35Notationwtr 5201
[TakeutiZaring] p. 35Theorem 7.2trelpss 44978  tz7.2 5623
[TakeutiZaring] p. 35Definition 7.1dftr3 5206
[TakeutiZaring] p. 36Proposition 7.4ordwe 6348
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6356
[TakeutiZaring] p. 36Proposition 7.6ordelord 6357  ordelordALT 45061  ordelordALTVD 45390
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6363  ordelssne 6362
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6361
[TakeutiZaring] p. 37Proposition 7.9ordin 6365
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7754
[TakeutiZaring] p. 38Corollary 7.15ordsson 7755
[TakeutiZaring] p. 38Definition 7.11df-on 6339
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6367
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45073  ordon 7749
[TakeutiZaring] p. 38Proposition 7.13onprc 7750
[TakeutiZaring] p. 39Theorem 7.17tfi 7822
[TakeutiZaring] p. 40Exercise 3ontr2 6383
[TakeutiZaring] p. 40Exercise 7dftr2 5203
[TakeutiZaring] p. 40Exercise 9onssmin 7764
[TakeutiZaring] p. 40Exercise 11unon 7800
[TakeutiZaring] p. 40Exercise 12ordun 6441
[TakeutiZaring] p. 40Exercise 14ordequn 6440
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7751
[TakeutiZaring] p. 40Proposition 7.20elssuni 4891
[TakeutiZaring] p. 41Definition 7.22df-suc 6341
[TakeutiZaring] p. 41Proposition 7.23sssucid 6417  sucidg 6418
[TakeutiZaring] p. 41Proposition 7.24onsuc 7782
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6431  ordnbtwn 6430
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7797
[TakeutiZaring] p. 42Exercise 1df-lim 6340
[TakeutiZaring] p. 42Exercise 4omssnlim 7850
[TakeutiZaring] p. 42Exercise 7ssnlim 7855
[TakeutiZaring] p. 42Exercise 8onsucssi 7810  ordelsuc 7789
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7791
[TakeutiZaring] p. 42Definition 7.27nlimon 7820
[TakeutiZaring] p. 42Definition 7.28dfom2 7837
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7858
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7859
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7860
[TakeutiZaring] p. 43Remarkomon 7847
[TakeutiZaring] p. 43Axiom 7inf3 9580  omex 9588
[TakeutiZaring] p. 43Theorem 7.32ordom 7845
[TakeutiZaring] p. 43Corollary 7.31find 7865
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7862
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7863
[TakeutiZaring] p. 44Exercise 1limomss 7840
[TakeutiZaring] p. 44Exercise 2int0 4914
[TakeutiZaring] p. 44Exercise 3trintss 5220
[TakeutiZaring] p. 44Exercise 4intss1 4915
[TakeutiZaring] p. 44Exercise 5intex 5294
[TakeutiZaring] p. 44Exercise 6oninton 7767
[TakeutiZaring] p. 44Exercise 11ordintdif 6386
[TakeutiZaring] p. 44Definition 7.35df-int 4900
[TakeutiZaring] p. 44Proposition 7.34noinfep 9605
[TakeutiZaring] p. 45Exercise 4onint 7762
[TakeutiZaring] p. 47Lemma 1tfrlem1 8334
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8356
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8357
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8358
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8365  tz7.44-2 8366  tz7.44-3 8367
[TakeutiZaring] p. 50Exercise 1smogt 8326
[TakeutiZaring] p. 50Exercise 3smoiso 8321
[TakeutiZaring] p. 50Definition 7.46df-smo 8305
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8404  tz7.49c 8405
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8402
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8401
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8403
[TakeutiZaring] p. 53Proposition 7.532eu5 2676
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9957
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9958
[TakeutiZaring] p. 56Definition 8.1oalim 8489  oasuc 8481
[TakeutiZaring] p. 57Remarktfindsg 7830
[TakeutiZaring] p. 57Proposition 8.2oacl 8492
[TakeutiZaring] p. 57Proposition 8.3oa0 8473  oa0r 8495
[TakeutiZaring] p. 57Proposition 8.16omcl 8493
[TakeutiZaring] p. 58Corollary 8.5oacan 8505
[TakeutiZaring] p. 58Proposition 8.4nnaord 8577  nnaordi 8576  oaord 8504  oaordi 8503
[TakeutiZaring] p. 59Proposition 8.6iunss2 5001  uniss2 4894
[TakeutiZaring] p. 59Proposition 8.7oawordri 8507
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8512  oawordex 8514
[TakeutiZaring] p. 59Proposition 8.9nnacl 8569
[TakeutiZaring] p. 59Proposition 8.10oaabs 8606
[TakeutiZaring] p. 60Remarkoancom 9596
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8517
[TakeutiZaring] p. 62Exercise 1nnarcl 8574
[TakeutiZaring] p. 62Exercise 5oaword1 8509
[TakeutiZaring] p. 62Definition 8.15om0x 8476  omlim 8490  omsuc 8483
[TakeutiZaring] p. 62Definition 8.15(a)om0 8474
[TakeutiZaring] p. 63Proposition 8.17nnecl 8571  nnmcl 8570
[TakeutiZaring] p. 63Proposition 8.19nnmord 8590  nnmordi 8589  omord 8525  omordi 8523
[TakeutiZaring] p. 63Proposition 8.20omcan 8526
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8594  omwordri 8529
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8496
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8499  om1r 8500
[TakeutiZaring] p. 64Proposition 8.22om00 8532
[TakeutiZaring] p. 64Proposition 8.23omordlim 8534
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8535
[TakeutiZaring] p. 64Proposition 8.25odi 8536
[TakeutiZaring] p. 65Theorem 8.26omass 8537
[TakeutiZaring] p. 67Definition 8.30nnesuc 8566  oe0 8479  oelim 8491  oesuc 8484  onesuc 8487
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8477
[TakeutiZaring] p. 67Proposition 8.32oen0 8544
[TakeutiZaring] p. 67Proposition 8.33oeordi 8545
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8478
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8502
[TakeutiZaring] p. 68Corollary 8.34oeord 8546
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8552
[TakeutiZaring] p. 68Proposition 8.35oewordri 8550
[TakeutiZaring] p. 68Proposition 8.37oeworde 8551
[TakeutiZaring] p. 69Proposition 8.41oeoa 8555
[TakeutiZaring] p. 70Proposition 8.42oeoe 8557
[TakeutiZaring] p. 73Theorem 9.1trcl 9673  tz9.1 9674
[TakeutiZaring] p. 76Definition 9.9df-r1 9712  r10 9716  r1lim 9720  r1limg 9719  r1suc 9718  r1sucg 9717
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9728  r1ord2 9729  r1ordg 9726
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9738
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9763  tz9.13 9739  tz9.13g 9740
[TakeutiZaring] p. 79Definition 9.14df-rank 9713  rankval 9764  rankvalb 9745  rankvalg 9765
[TakeutiZaring] p. 79Proposition 9.16rankel 9787  rankelb 9772
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9801  rankval3 9788  rankval3b 9774
[TakeutiZaring] p. 79Proposition 9.18rankonid 9777
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9743
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9782  rankr1c 9769  rankr1g 9780
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9783
[TakeutiZaring] p. 80Exercise 1rankss 9797  rankssb 9796
[TakeutiZaring] p. 80Exercise 2unbndrank 9790
[TakeutiZaring] p. 80Proposition 9.19bndrank 9789
[TakeutiZaring] p. 83Axiom of Choiceac4 10422  dfac3 10067
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9976  numth 10419  numth2 10418
[TakeutiZaring] p. 85Definition 10.4cardval 10493
[TakeutiZaring] p. 85Proposition 10.5cardid 10494  cardid2 9901
[TakeutiZaring] p. 85Proposition 10.9oncard 9908
[TakeutiZaring] p. 85Proposition 10.10carden 10498
[TakeutiZaring] p. 85Proposition 10.11cardidm 9907
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9892
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9913
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9905
[TakeutiZaring] p. 87Proposition 10.15pwen 9111
[TakeutiZaring] p. 88Exercise 1en0 8988
[TakeutiZaring] p. 88Exercise 7infensuc 9116
[TakeutiZaring] p. 89Exercise 10omxpen 9040
[TakeutiZaring] p. 90Corollary 10.23cardnn 9911
[TakeutiZaring] p. 90Definition 10.27alephiso 10044
[TakeutiZaring] p. 90Proposition 10.20nneneq 9163
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9171
[TakeutiZaring] p. 90Proposition 10.26alephprc 10045
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9168
[TakeutiZaring] p. 91Exercise 2alephle 10034
[TakeutiZaring] p. 91Exercise 3aleph0 10012
[TakeutiZaring] p. 91Exercise 4cardlim 9920
[TakeutiZaring] p. 91Exercise 7infpss 10162
[TakeutiZaring] p. 91Exercise 8infcntss 9256
[TakeutiZaring] p. 91Definition 10.29df-fin 8920  isfi 8945
[TakeutiZaring] p. 92Proposition 10.32onfin 9172
[TakeutiZaring] p. 92Proposition 10.34imadomg 10481
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9033
[TakeutiZaring] p. 93Proposition 10.35fodomb 10473
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10132  unxpdom 9192
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9922  cardsdomelir 9921
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9194
[TakeutiZaring] p. 94Proposition 10.39infxpen 9960
[TakeutiZaring] p. 95Definition 10.42df-map 8798
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10509  infxpidm2 9963
[TakeutiZaring] p. 95Proposition 10.41infdju 10153  infxp 10160
[TakeutiZaring] p. 96Proposition 10.44pw2en 9045  pw2f1o 9043
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9104
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10434
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10429  ac6s5 10438
[TakeutiZaring] p. 98Theorem 10.47unidom 10490
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10491  uniimadomf 10492
[TakeutiZaring] p. 100Definition 11.1cfcof 10221
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10216
[TakeutiZaring] p. 102Exercise 1cfle 10200
[TakeutiZaring] p. 102Exercise 2cf0 10197
[TakeutiZaring] p. 102Exercise 3cfsuc 10204
[TakeutiZaring] p. 102Exercise 4cfom 10211
[TakeutiZaring] p. 102Proposition 11.9coftr 10220
[TakeutiZaring] p. 103Theorem 11.15alephreg 10530
[TakeutiZaring] p. 103Proposition 11.11cardcf 10198
[TakeutiZaring] p. 103Proposition 11.13alephsing 10223
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10043
[TakeutiZaring] p. 104Proposition 11.16carduniima 10042
[TakeutiZaring] p. 104Proposition 11.18alephfp 10054  alephfp2 10055
[TakeutiZaring] p. 106Theorem 11.20gchina 10647
[TakeutiZaring] p. 106Theorem 11.21mappwen 10058
[TakeutiZaring] p. 107Theorem 11.26konigth 10517
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10531
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10532
[Tarski] p. 67Axiom B5ax-c5 39455
[Tarski] p. 67Scheme B5sp 2212
[Tarski] p. 68Lemma 6avril1 30604  equid 2026
[Tarski] p. 69Lemma 7equcomi 2031
[Tarski] p. 70Lemma 14spim 2412  spime 2414  spimew 1985
[Tarski] p. 70Lemma 16ax-12 2206  ax-c15 39461  ax12i 1980
[Tarski] p. 70Lemmas 16 and 17sb6 2112
[Tarski] p. 75Axiom B7ax6v 1982
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1924  ax5ALT 39479
[Tarski], p. 75Scheme B8 of system S2ax-7 2022  ax-8 2138  ax-9 2146
[Tarski1999] p. 178Axiom 4axtgsegcon 28603
[Tarski1999] p. 178Axiom 5axtg5seg 28604
[Tarski1999] p. 179Axiom 7axtgpasch 28606
[Tarski1999] p. 180Axiom 7.1axtgpasch 28606
[Tarski1999] p. 185Axiom 11axtgcont1 28607
[Truss] p. 114Theorem 5.18ruc 16251
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38106
[Viaclovsky8] p. 3Proposition 7ismblfin 38108
[Weierstrass] p. 272Definitiondf-mdet 22618  mdetuni 22655
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 912
[WhiteheadRussell] p. 96Axiom *1.3olc 877
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 878
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 928
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 978
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 189
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 37887
[WhiteheadRussell] p. 100Theorem *2.05frege5 44324  imim2 58  wl-luk-imim2 37882
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47561  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 905
[WhiteheadRussell] p. 101Theorem *2.06barbara 2683  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 911
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37885
[WhiteheadRussell] p. 101Theorem *2.11exmid 903
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 906
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 45450  wl-luk-notnotr 37886
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44354  axfrege28 44353  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 876
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 933
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37879
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 898
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 950
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30542  pm2.27 42  wl-luk-pm2.27 37877
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 931
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38818
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 932
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 980
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 981
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 979
[WhiteheadRussell] p. 105Definition *2.33df-3or 1096
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 915
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 916
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 953
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 890
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 891
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 192
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 892
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 893
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 894
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 860
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 861
[WhiteheadRussell] p. 107Theorem *2.55orel1 897
[WhiteheadRussell] p. 107Theorem *2.56orel2 899
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 193
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 908
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 951
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 952
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 194
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 900  pm2.67 901
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 907
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 983
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 909
[WhiteheadRussell] p. 108Theorem *2.69looinv 205
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 984
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 985
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 942
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 940
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 982
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 986
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 941
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1002
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 472  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1003
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1004
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1005
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1006
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 474
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 462
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 405
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 810
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 451
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 452
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 485  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 487  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 772
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 773
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 815
[WhiteheadRussell] p. 113Fact)pm3.45 630
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 817
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 495
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 496
[WhiteheadRussell] p. 113Theorem *3.44jao 971  pm3.44 970
[WhiteheadRussell] p. 113Theorem *3.47anim12 816
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 476
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 974
[WhiteheadRussell] p. 116Theorem *4.1con34b 318
[WhiteheadRussell] p. 117Theorem *4.2biid 263
[WhiteheadRussell] p. 117Theorem *4.11notbi 321
[WhiteheadRussell] p. 117Theorem *4.12con2bi 355
[WhiteheadRussell] p. 117Theorem *4.13notnotb 317
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 814
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 841
[WhiteheadRussell] p. 117Theorem *4.21bicom 224
[WhiteheadRussell] p. 117Theorem *4.22biantr 813  bitr 812
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 570
[WhiteheadRussell] p. 117Theorem *4.25oridm 913  pm4.25 914
[WhiteheadRussell] p. 118Theorem *4.3ancom 463
[WhiteheadRussell] p. 118Theorem *4.4andi 1018
[WhiteheadRussell] p. 118Theorem *4.31orcom 879
[WhiteheadRussell] p. 118Theorem *4.32anass 471
[WhiteheadRussell] p. 118Theorem *4.33orass 930
[WhiteheadRussell] p. 118Theorem *4.36anbi1 641
[WhiteheadRussell] p. 118Theorem *4.37orbi1 926
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 645
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 987
[WhiteheadRussell] p. 118Definition *4.34df-3an 1097
[WhiteheadRussell] p. 119Theorem *4.41ordi 1016
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1062
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1033
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1007
[WhiteheadRussell] p. 119Theorem *4.45orabs 1009  pm4.45 1008  pm4.45im 836
[WhiteheadRussell] p. 120Theorem *4.5anor 993
[WhiteheadRussell] p. 120Theorem *4.6imor 862
[WhiteheadRussell] p. 120Theorem *4.7anclb 552
[WhiteheadRussell] p. 120Theorem *4.51ianor 992
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 995
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 996
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 997
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 998
[WhiteheadRussell] p. 120Theorem *4.56ioran 994  pm4.56 999
[WhiteheadRussell] p. 120Theorem *4.57oran 1000  pm4.57 1001
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 407
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 865
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 400
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 858
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 408
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 859
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 401
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 564  pm4.71d 568  pm4.71i 566  pm4.71r 565  pm4.71rd 569  pm4.71ri 567
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 960
[WhiteheadRussell] p. 121Theorem *4.73iba 534
[WhiteheadRussell] p. 121Theorem *4.74biorf 945
[WhiteheadRussell] p. 121Theorem *4.76jcab 524  pm4.76 525
[WhiteheadRussell] p. 121Theorem *4.77jaob 972  pm4.77 973
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 943
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1014
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 395
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 396
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1034
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1035
[WhiteheadRussell] p. 122Theorem *4.84imbi1 349
[WhiteheadRussell] p. 122Theorem *4.85imbi2 350
[WhiteheadRussell] p. 122Theorem *4.86bibi1 353
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 390  impexp 453  pm4.87 852
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 831
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 955  pm5.11g 954
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 956
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 958
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 957
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1023
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1024
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1022
[WhiteheadRussell] p. 124Theorem *5.18nbbn 385  pm5.18 383
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 389
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 832
[WhiteheadRussell] p. 124Theorem *5.22xor 1025
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1058
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1059
[WhiteheadRussell] p. 124Theorem *5.25dfor2 910
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 579
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 391
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 363
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1012
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 964
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 839
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 580
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 844
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 833
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 842
[WhiteheadRussell] p. 125Theorem *5.41imdi 392  pm5.41 393
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 550
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 549
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1015
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1028
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 959
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1011
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1029
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1030
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1038
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 368
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 272
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1039
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37012
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44882
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44883
[WhiteheadRussell] p. 147Theorem *10.2219.26 1884
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44884
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44885
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44886
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1907
[WhiteheadRussell] p. 151Theorem *10.301albitr 44887
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44888
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44889
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44890
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44891
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44893
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44894
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44895
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44892
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2117
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44898
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44899
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2095
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2188
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1843
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1844
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44900
[WhiteheadRussell] p. 162Theorem *11.322alim 44901
[WhiteheadRussell] p. 162Theorem *11.332albi 44902
[WhiteheadRussell] p. 162Theorem *11.342exim 44903
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44905
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44904
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1901
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44907
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44908
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44906
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1842
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44909
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44910
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1860
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44911
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2371
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1874
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44916
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44912
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44913
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44914
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44915
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44920
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44917
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44918
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44919
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44921
[WhiteheadRussell] p. 175Definition *14.02df-eu 2590
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44931  pm13.13b 44932
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44933
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3032
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3033
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3620
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44939
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44940
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44934
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45076  pm13.193 44935
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44936
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44937
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44938
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44945
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44944
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44943
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3801
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44946  pm14.122b 44947  pm14.122c 44948
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44949  pm14.123b 44950  pm14.123c 44951
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44953
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44952
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44954
[WhiteheadRussell] p. 190Theorem *14.22iota4 6491
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44955
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6492
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44956
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44958
[WhiteheadRussell] p. 192Theorem *14.26eupick 2654  eupickbi 2657  sbaniota 44959
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44957
[WhiteheadRussell] p. 192Theorem *14.271eubi 2605
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44960
[WhiteheadRussell] p. 235Definition *30.01conventions 30541  df-fv 6518
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9949  pm54.43lem 9948
[Young] p. 141Definition of operator orderingleop2 32266
[Young] p. 142Example 12.2(i)0leop 32272  idleop 32273
[vandenDries] p. 42Lemma 61irrapx1 43353
[vandenDries] p. 43Theorem 62pellex 43360  pellexlem1 43354

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