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 17714
[Adamek] p. 21Condition 3.1(b)df-cat 17714
[Adamek] p. 22Example 3.3(1)df-setc 18123
[Adamek] p. 24Example 3.3(4.c)0cat 17735  0funcg 49714  df-termc 50102
[Adamek] p. 24Example 3.3(4.d)df-prstc 50179  prsthinc 50093
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50207  df-mndtc 50207
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50203
[Adamek] p. 25Definition 3.5df-oppc 17758
[Adamek] p. 25Example 3.6(1)oduoppcciso 50195
[Adamek] p. 25Example 3.6(2)oppgoppcco 50220  oppgoppchom 50219  oppgoppcid 50221
[Adamek] p. 28Remark 3.9oppciso 17828
[Adamek] p. 28Remark 3.12invf1o 17816  invisoinvl 17837
[Adamek] p. 28Example 3.13idinv 17836  idiso 17835
[Adamek] p. 28Corollary 3.11inveq 17821
[Adamek] p. 28Definition 3.8df-inv 17795  df-iso 17796  dfiso2 17819
[Adamek] p. 28Proposition 3.10sectcan 17802
[Adamek] p. 29Remark 3.16cicer 17853  cicerALT 49675
[Adamek] p. 29Definition 3.15cic 17846  df-cic 17843
[Adamek] p. 29Definition 3.17df-func 17905
[Adamek] p. 29Proposition 3.14(1)invinv 17817
[Adamek] p. 29Proposition 3.14(2)invco 17818  isoco 17824
[Adamek] p. 30Remark 3.19df-func 17905
[Adamek] p. 30Example 3.20(1)idfucl 17928
[Adamek] p. 30Example 3.20(2)diag1 49933
[Adamek] p. 32Proposition 3.21funciso 17921
[Adamek] p. 33Example 3.26(1)discsnterm 50203  discthing 50090
[Adamek] p. 33Example 3.26(2)df-thinc 50047  prsthinc 50093  thincciso 50082  thincciso2 50084  thincciso3 50085  thinccisod 50083
[Adamek] p. 33Example 3.26(3)df-mndtc 50207
[Adamek] p. 33Proposition 3.23cofucl 17935  cofucla 49725
[Adamek] p. 34Remark 3.28(1)cofidfth 49791
[Adamek] p. 34Remark 3.28(2)catciso 18158  catcisoi 50029
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18213
[Adamek] p. 34Definition 3.27(2)df-fth 17954
[Adamek] p. 34Definition 3.27(3)df-full 17953
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18213
[Adamek] p. 35Corollary 3.32ffthiso 17978
[Adamek] p. 35Proposition 3.30(c)cofth 17984
[Adamek] p. 35Proposition 3.30(d)cofull 17983
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18198
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18198
[Adamek] p. 39Remark 3.422oppf 49761
[Adamek] p. 39Definition 3.41df-oppf 49752  funcoppc 17922
[Adamek] p. 39Definition 3.44.df-catc 18146  elcatchom 50026
[Adamek] p. 39Proposition 3.43(c)fthoppc 17972  fthoppf 49793
[Adamek] p. 39Proposition 3.43(d)fulloppc 17971  fulloppf 49792
[Adamek] p. 40Remark 3.48catccat 18155
[Adamek] p. 40Definition 3.470funcg 49714  df-catc 18146
[Adamek] p. 45Exercise 3Gincat 50230
[Adamek] p. 48Remark 4.2(2)cnelsubc 50233  nelsubc3 49700
[Adamek] p. 48Remark 4.2(3)imasubc 49780  imasubc2 49781  imasubc3 49785
[Adamek] p. 48Example 4.3(1.a)0subcat 17885
[Adamek] p. 48Example 4.3(1.b)catsubcat 17886
[Adamek] p. 48Definition 4.1(1)nelsubc3 49700
[Adamek] p. 48Definition 4.1(2)fullsubc 17897
[Adamek] p. 48Definition 4.1(a)df-subc 17859
[Adamek] p. 49Remark 4.4idsubc 49789
[Adamek] p. 49Remark 4.4(1)idemb 49788
[Adamek] p. 49Remark 4.4(2)idfullsubc 49790  ressffth 17987
[Adamek] p. 58Exercise 4Asetc1onsubc 50231
[Adamek] p. 83Definition 6.1df-nat 17993
[Adamek] p. 87Remark 6.14(a)fuccocl 18014
[Adamek] p. 87Remark 6.14(b)fucass 18018
[Adamek] p. 87Definition 6.15df-fuc 17994
[Adamek] p. 88Remark 6.16fuccat 18020
[Adamek] p. 101Definition 7.10funcg 49714  df-inito 18031
[Adamek] p. 101Example 7.2(3)0funcg 49714  df-termc 50102  initc 49720
[Adamek] p. 101Example 7.2 (6)irinitoringc 21589
[Adamek] p. 102Definition 7.4df-termo 18032  oppctermo 49865
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18059
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18063
[Adamek] p. 103Remark 7.8oppczeroo 49866
[Adamek] p. 103Definition 7.7df-zeroo 18033
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21590
[Adamek] p. 103Proposition 7.6termoeu1w 18066
[Adamek] p. 106Definition 7.19df-sect 17794
[Adamek] p. 107Example 7.20(7)thincinv 50098
[Adamek] p. 108Example 7.25(4)thincsect2 50097
[Adamek] p. 110Example 7.33(9)thincmon 50062
[Adamek] p. 110Proposition 7.35sectmon 17829
[Adamek] p. 112Proposition 7.42sectepi 17831
[Adamek] p. 185Section 10.67updjud 9908
[Adamek] p. 193Definition 11.1(1)df-lmd 50274
[Adamek] p. 193Definition 11.3(1)df-lmd 50274
[Adamek] p. 194Definition 11.3(2)df-lmd 50274
[Adamek] p. 202Definition 11.27(1)df-cmd 50275
[Adamek] p. 202Definition 11.27(2)df-cmd 50275
[Adamek] p. 478Item Rngdf-ringc 20722
[AhoHopUll] p. 2Section 1.1df-bigo 49179
[AhoHopUll] p. 12Section 1.3df-blen 49201
[AhoHopUll] p. 318Section 9.1df-concat 14598  df-pfx 14699  df-substr 14669  df-word 14541  lencl 14560  wrd0 14566
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24826  df-nmoo 31006
[AkhiezerGlazman] p. 64Theoremhmopidmch 32414  hmopidmchi 32412
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32462  pjcmul2i 32463
[AkhiezerGlazman] p. 72Theoremcnvunop 32179  unoplin 32181
[AkhiezerGlazman] p. 72Equation 2unopadj 32180  unopadj2 32199
[AkhiezerGlazman] p. 73Theoremelunop2 32274  lnopunii 32273
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32347
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28078
[Alling] p. 184Axiom Bbdayfo 27799
[Alling] p. 184Axiom Oltsso 27798
[Alling] p. 184Axiom SDnodense 27814
[Alling] p. 185Lemma 0nocvxmin 27906
[Alling] p. 185Theoremconway 27930
[Alling] p. 185Axiom FEnoeta 27865
[Alling] p. 186Theorem 4lesrec 27950  lesrecd 27951
[Alling], p. 2Definitionrp-brsslt 44011
[Alling], p. 3Notenla0001 44014  nla0002 44012  nla0003 44013
[Apostol] p. 18Theorem I.1addcan 11382  addcan2d 11402  addcan2i 11392  addcand 11401  addcani 11391
[Apostol] p. 18Theorem I.2negeu 11435
[Apostol] p. 18Theorem I.3negsub 11494  negsubd 11563  negsubi 11524
[Apostol] p. 18Theorem I.4negneg 11496  negnegd 11548  negnegi 11516
[Apostol] p. 18Theorem I.5subdi 11635  subdid 11658  subdii 11651  subdir 11636  subdird 11659  subdiri 11652
[Apostol] p. 18Theorem I.6mul01 11377  mul01d 11397  mul01i 11388  mul02 11376  mul02d 11396  mul02i 11387
[Apostol] p. 18Theorem I.7mulcan 11839  mulcan2d 11836  mulcand 11835  mulcani 11841
[Apostol] p. 18Theorem I.8receu 11847  xreceu 33154
[Apostol] p. 18Theorem I.9divrec 11876  divrecd 11985  divreci 11951  divreczi 11944
[Apostol] p. 18Theorem I.10recrec 11903  recreci 11938
[Apostol] p. 18Theorem I.11mul0or 11842  mul0ord 11850  mul0ori 11849
[Apostol] p. 18Theorem I.12mul2neg 11641  mul2negd 11657  mul2negi 11650  mulneg1 11638  mulneg1d 11655  mulneg1i 11648
[Apostol] p. 18Theorem I.13divadddiv 11921  divadddivd 12026  divadddivi 11968
[Apostol] p. 18Theorem I.14divmuldiv 11906  divmuldivd 12023  divmuldivi 11966  rdivmuldivd 20486
[Apostol] p. 18Theorem I.15divdivdiv 11907  divdivdivd 12029  divdivdivi 11969
[Apostol] p. 20Axiom 7rpaddcl 13031  rpaddcld 13066  rpmulcl 13032  rpmulcld 13067
[Apostol] p. 20Axiom 8rpneg 13041
[Apostol] p. 20Axiom 90nrp 13044
[Apostol] p. 20Theorem I.17lttri 11324
[Apostol] p. 20Theorem I.18ltadd1d 11795  ltadd1dd 11813  ltadd1i 11756
[Apostol] p. 20Theorem I.19ltmul1 12056  ltmul1a 12055  ltmul1i 12124  ltmul1ii 12134  ltmul2 12057  ltmul2d 13093  ltmul2dd 13107  ltmul2i 12127
[Apostol] p. 20Theorem I.20msqgt0 11722  msqgt0d 11769  msqgt0i 11739
[Apostol] p. 20Theorem I.210lt1 11724
[Apostol] p. 20Theorem I.23lt0neg1 11708  lt0neg1d 11771  ltneg 11702  ltnegd 11780  ltnegi 11746
[Apostol] p. 20Theorem I.25lt2add 11687  lt2addd 11825  lt2addi 11764
[Apostol] p. 20Definition of positive numbersdf-rp 13008
[Apostol] p. 21Exercise 4recgt0 12052  recgt0d 12140  recgt0i 12111  recgt0ii 12112
[Apostol] p. 22Definition of integersdf-z 12583
[Apostol] p. 22Definition of positive integersdfnn3 12238
[Apostol] p. 22Definition of rationalsdf-q 12964
[Apostol] p. 24Theorem I.26supeu 9402
[Apostol] p. 26Theorem I.28nnunb 12491
[Apostol] p. 26Theorem I.29arch 12492  archd 45738
[Apostol] p. 28Exercise 2btwnz 12690
[Apostol] p. 28Exercise 3nnrecl 12493
[Apostol] p. 28Exercise 4rebtwnz 12962
[Apostol] p. 28Exercise 5zbtwnre 12961
[Apostol] p. 28Exercise 6qbtwnre 13216
[Apostol] p. 28Exercise 10(a)zeneo 16387  zneo 12670  zneoALTV 48289
[Apostol] p. 29Theorem I.35cxpsqrtth 26853  msqsqrtd 15484  resqrtth 15296  sqrtth 15406  sqrtthi 15412  sqsqrtd 15483
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12227
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12928
[Apostol] p. 361Remarkcrreczi 14255
[Apostol] p. 363Remarkabsgt0i 15441
[Apostol] p. 363Exampleabssubd 15497  abssubi 15445
[ApostolNT] p. 7Remarkfmtno0 48147  fmtno1 48148  fmtno2 48157  fmtno3 48158  fmtno4 48159  fmtno5fac 48189  fmtnofz04prm 48184
[ApostolNT] p. 7Definitiondf-fmtno 48135
[ApostolNT] p. 8Definitiondf-ppi 27222
[ApostolNT] p. 14Definitiondf-dvds 16301
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16317
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16342
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16337
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16330
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16332
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16318
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16319
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16324
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16359
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16361
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16363
[ApostolNT] p. 15Definitiondf-gcd 16543  dfgcd2 16594
[ApostolNT] p. 16Definitionisprm2 16730
[ApostolNT] p. 16Theorem 1.5coprmdvds 16701
[ApostolNT] p. 16Theorem 1.7prminf 16965
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16561
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16595
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16597
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16576
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16568
[ApostolNT] p. 17Theorem 1.8coprm 16760
[ApostolNT] p. 17Theorem 1.9euclemma 16762
[ApostolNT] p. 17Theorem 1.101arith2 16978
[ApostolNT] p. 18Theorem 1.13prmrec 16972
[ApostolNT] p. 19Theorem 1.14divalg 16451
[ApostolNT] p. 20Theorem 1.15eucalg 16635
[ApostolNT] p. 24Definitiondf-mu 27223
[ApostolNT] p. 25Definitiondf-phi 16815
[ApostolNT] p. 25Theorem 2.1musum 27313
[ApostolNT] p. 26Theorem 2.2phisum 16840
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16825
[ApostolNT] p. 28Theorem 2.5(c)phimul 16829
[ApostolNT] p. 32Definitiondf-vma 27220
[ApostolNT] p. 32Theorem 2.9muinv 27315
[ApostolNT] p. 32Theorem 2.10vmasum 27338
[ApostolNT] p. 38Remarkdf-sgm 27224
[ApostolNT] p. 38Definitiondf-sgm 27224
[ApostolNT] p. 75Definitiondf-chp 27221  df-cht 27219
[ApostolNT] p. 104Definitioncongr 16712
[ApostolNT] p. 106Remarkdvdsval3 16304
[ApostolNT] p. 106Definitionmoddvds 16311
[ApostolNT] p. 107Example 2mod2eq0even 16394
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16395
[ApostolNT] p. 107Example 4zmod1congr 13912
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13952
[ApostolNT] p. 107Theorem 5.2(c)modexp 14265
[ApostolNT] p. 108Theorem 5.3modmulconst 16336
[ApostolNT] p. 109Theorem 5.4cncongr1 16715
[ApostolNT] p. 109Theorem 5.6gcdmodi 17124
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16717
[ApostolNT] p. 113Theorem 5.17eulerth 16832
[ApostolNT] p. 113Theorem 5.18vfermltl 16851
[ApostolNT] p. 114Theorem 5.19fermltl 16833
[ApostolNT] p. 116Theorem 5.24wilthimp 27194
[ApostolNT] p. 179Definitiondf-lgs 27417  lgsprme0 27461
[ApostolNT] p. 180Example 11lgs 27462
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27438
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27453
[ApostolNT] p. 181Theorem 9.4m1lgs 27510
[ApostolNT] p. 181Theorem 9.52lgs 27529  2lgsoddprm 27538
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27496
[ApostolNT] p. 185Theorem 9.8lgsquad 27505
[ApostolNT] p. 188Definitiondf-lgs 27417  lgs1 27463
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27454
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27456
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27464
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27465
[Baer] p. 40Property (b)mapdord 42274
[Baer] p. 40Property (c)mapd11 42275
[Baer] p. 40Property (e)mapdin 42298  mapdlsm 42300
[Baer] p. 40Property (f)mapd0 42301
[Baer] p. 40Definition of projectivitydf-mapd 42261  mapd1o 42284
[Baer] p. 41Property (g)mapdat 42303
[Baer] p. 44Part (1)mapdpg 42342
[Baer] p. 45Part (2)hdmap1eq 42437  mapdheq 42364  mapdheq2 42365  mapdheq2biN 42366
[Baer] p. 45Part (3)baerlem3 42349
[Baer] p. 46Part (4)mapdheq4 42368  mapdheq4lem 42367
[Baer] p. 46Part (5)baerlem5a 42350  baerlem5abmN 42354  baerlem5amN 42352  baerlem5b 42351  baerlem5bmN 42353
[Baer] p. 47Part (6)hdmap1l6 42457  hdmap1l6a 42445  hdmap1l6e 42450  hdmap1l6f 42451  hdmap1l6g 42452  hdmap1l6lem1 42443  hdmap1l6lem2 42444  mapdh6N 42383  mapdh6aN 42371  mapdh6eN 42376  mapdh6fN 42377  mapdh6gN 42378  mapdh6lem1N 42369  mapdh6lem2N 42370
[Baer] p. 48Part 9hdmapval 42464
[Baer] p. 48Part 10hdmap10 42476
[Baer] p. 48Part 11hdmapadd 42479
[Baer] p. 48Part (6)hdmap1l6h 42453  mapdh6hN 42379
[Baer] p. 48Part (7)mapdh75cN 42389  mapdh75d 42390  mapdh75e 42388  mapdh75fN 42391  mapdh7cN 42385  mapdh7dN 42386  mapdh7eN 42384  mapdh7fN 42387
[Baer] p. 48Part (8)mapdh8 42424  mapdh8a 42411  mapdh8aa 42412  mapdh8ab 42413  mapdh8ac 42414  mapdh8ad 42415  mapdh8b 42416  mapdh8c 42417  mapdh8d 42419  mapdh8d0N 42418  mapdh8e 42420  mapdh8g 42421  mapdh8i 42422  mapdh8j 42423
[Baer] p. 48Part (9)mapdh9a 42425
[Baer] p. 48Equation 10mapdhvmap 42405
[Baer] p. 49Part 12hdmap11 42484  hdmapeq0 42480  hdmapf1oN 42501  hdmapneg 42482  hdmaprnN 42500  hdmaprnlem1N 42485  hdmaprnlem3N 42486  hdmaprnlem3uN 42487  hdmaprnlem4N 42489  hdmaprnlem6N 42490  hdmaprnlem7N 42491  hdmaprnlem8N 42492  hdmaprnlem9N 42493  hdmapsub 42483
[Baer] p. 49Part 14hdmap14lem1 42504  hdmap14lem10 42513  hdmap14lem1a 42502  hdmap14lem2N 42505  hdmap14lem2a 42503  hdmap14lem3 42506  hdmap14lem8 42511  hdmap14lem9 42512
[Baer] p. 50Part 14hdmap14lem11 42514  hdmap14lem12 42515  hdmap14lem13 42516  hdmap14lem14 42517  hdmap14lem15 42518  hgmapval 42523
[Baer] p. 50Part 15hgmapadd 42530  hgmapmul 42531  hgmaprnlem2N 42533  hgmapvs 42527
[Baer] p. 50Part 16hgmaprnN 42537
[Baer] p. 110Lemma 1hdmapip0com 42553
[Baer] p. 110Line 27hdmapinvlem1 42554
[Baer] p. 110Line 28hdmapinvlem2 42555
[Baer] p. 110Line 30hdmapinvlem3 42556
[Baer] p. 110Part 1.2hdmapglem5 42558  hgmapvv 42562
[Baer] p. 110Proposition 1hdmapinvlem4 42557
[Baer] p. 111Line 10hgmapvvlem1 42559
[Baer] p. 111Line 15hdmapg 42566  hdmapglem7 42565
[Bauer], p. 483Theorem 1.22irrexpq 26854  2irrexpqALT 26923
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2599
[BellMachover] p. 460Notationdf-mo 2569
[BellMachover] p. 460Definitionmo3 2594
[BellMachover] p. 461Axiom Extax-ext 2737
[BellMachover] p. 462Theorem 1.1axextmo 2741
[BellMachover] p. 463Axiom Repaxrep5 5240
[BellMachover] p. 463Scheme Sepax-sep 5251
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37561  sepex 5255
[BellMachover] p. 466Problemaxpow2 5329
[BellMachover] p. 466Axiom Powaxpow3 5330
[BellMachover] p. 466Axiom Unionaxun2 7724
[BellMachover] p. 468Definitiondf-ord 6353
[BellMachover] p. 469Theorem 2.2(i)ordirr 6368
[BellMachover] p. 469Theorem 2.2(iii)onelon 6375
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6370
[BellMachover] p. 471Definition of Ndf-om 7851
[BellMachover] p. 471Problem 2.5(ii)uniordint 7788
[BellMachover] p. 471Definition of Limdf-lim 6355
[BellMachover] p. 472Axiom Infzfinf2 9599
[BellMachover] p. 473Theorem 2.8limom 7866
[BellMachover] p. 477Equation 3.1df-r1 9724
[BellMachover] p. 478Definitionrankval2 9778  rankval2b 35407
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9742  r1ord3g 9739
[BellMachover] p. 480Axiom Regzfreg 9546
[BellMachover] p. 488Axiom ACac5 10449  dfac4 10094
[BellMachover] p. 490Definition of alephalephval3 10082
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39955
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32614
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32656  chirredi 32655
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32644
[Beran] p. 3Definition of joinsshjval3 31615
[Beran] p. 39Theorem 2.3(i)cmcm2 31877  cmcm2i 31854  cmcm2ii 31859  cmt2N 39886
[Beran] p. 40Theorem 2.3(iii)lecm 31878  lecmi 31863  lecmii 31864
[Beran] p. 45Theorem 3.4cmcmlem 31852
[Beran] p. 49Theorem 4.2cm2j 31881  cm2ji 31886  cm2mi 31887
[Beran] p. 95Definitiondf-sh 31468  issh2 31470
[Beran] p. 95Lemma 3.1(S5)his5 31347
[Beran] p. 95Lemma 3.1(S6)his6 31360
[Beran] p. 95Lemma 3.1(S7)his7 31351
[Beran] p. 95Lemma 3.2(S8)ho01i 32089
[Beran] p. 95Lemma 3.2(S9)hoeq1 32091
[Beran] p. 95Lemma 3.2(S10)ho02i 32090
[Beran] p. 95Lemma 3.2(S11)hoeq2 32092
[Beran] p. 95Postulate (S1)ax-his1 31343  his1i 31361
[Beran] p. 95Postulate (S2)ax-his2 31344
[Beran] p. 95Postulate (S3)ax-his3 31345
[Beran] p. 95Postulate (S4)ax-his4 31346
[Beran] p. 96Definition of normdf-hnorm 31229  dfhnorm2 31383  normval 31385
[Beran] p. 96Definition for Cauchy sequencehcau 31445
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31234
[Beran] p. 96Definition of complete subspaceisch3 31502
[Beran] p. 96Definition of convergedf-hlim 31233  hlimi 31449
[Beran] p. 97Theorem 3.3(i)norm-i-i 31394  norm-i 31390
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31398  norm-ii 31399  normlem0 31370  normlem1 31371  normlem2 31372  normlem3 31373  normlem4 31374  normlem5 31375  normlem6 31376  normlem7 31377  normlem7tALT 31380
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31400  norm-iii 31401
[Beran] p. 98Remark 3.4bcs 31442  bcsiALT 31440  bcsiHIL 31441
[Beran] p. 98Remark 3.4(B)normlem9at 31382  normpar 31416  normpari 31415
[Beran] p. 98Remark 3.4(C)normpyc 31407  normpyth 31406  normpythi 31403
[Beran] p. 99Remarklnfn0 32308  lnfn0i 32303  lnop0 32227  lnop0i 32231
[Beran] p. 99Theorem 3.5(i)nmcexi 32287  nmcfnex 32314  nmcfnexi 32312  nmcopex 32290  nmcopexi 32288
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32315  nmcfnlbi 32313  nmcoplb 32291  nmcoplbi 32289
[Beran] p. 99Theorem 3.5(iii)lnfncon 32317  lnfnconi 32316  lnopcon 32296  lnopconi 32295
[Beran] p. 100Lemma 3.6normpar2i 31417
[Beran] p. 101Lemma 3.6norm3adifi 31414  norm3adifii 31409  norm3dif 31411  norm3difi 31408
[Beran] p. 102Theorem 3.7(i)chocunii 31562  pjhth 31654  pjhtheu 31655  pjpjhth 31686  pjpjhthi 31687  pjth 25559
[Beran] p. 102Theorem 3.7(ii)ococ 31667  ococi 31666
[Beran] p. 103Remark 3.8nlelchi 32322
[Beran] p. 104Theorem 3.9riesz3i 32323  riesz4 32325  riesz4i 32324
[Beran] p. 104Theorem 3.10cnlnadj 32340  cnlnadjeu 32339  cnlnadjeui 32338  cnlnadji 32337  cnlnadjlem1 32328  nmopadjlei 32349
[Beran] p. 106Theorem 3.11(i)adjeq0 32352
[Beran] p. 106Theorem 3.11(v)nmopadji 32351
[Beran] p. 106Theorem 3.11(ii)adjmul 32353
[Beran] p. 106Theorem 3.11(iv)adjadj 32197
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32363  nmopcoadji 32362
[Beran] p. 106Theorem 3.11(iii)adjadd 32354
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32364
[Beran] p. 106Theorem 3.11(viii)adjcoi 32361  pjadj2coi 32465  pjadjcoi 32422
[Beran] p. 107Definitiondf-ch 31482  isch2 31484
[Beran] p. 107Remark 3.12choccl 31567  isch3 31502  occl 31565  ocsh 31544  shoccl 31566  shocsh 31545
[Beran] p. 107Remark 3.12(B)ococin 31669
[Beran] p. 108Theorem 3.13chintcl 31593
[Beran] p. 109Property (i)pjadj2 32448  pjadj3 32449  pjadji 31946  pjadjii 31935
[Beran] p. 109Property (ii)pjidmco 32442  pjidmcoi 32438  pjidmi 31934
[Beran] p. 110Definition of projector orderingpjordi 32434
[Beran] p. 111Remarkho0val 32011  pjch1 31931
[Beran] p. 111Definitiondf-hfmul 31995  df-hfsum 31994  df-hodif 31993  df-homul 31992  df-hosum 31991
[Beran] p. 111Lemma 4.4(i)pjo 31932
[Beran] p. 111Lemma 4.4(ii)pjch 31955  pjchi 31693
[Beran] p. 111Lemma 4.4(iii)pjoc2 31700  pjoc2i 31699
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31941
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32426  pjssmii 31942
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32425
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32424
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32429
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32427  pjssge0ii 31943
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32428  pjdifnormii 31944
[Bobzien] p. 116Statement T3stoic3 1799
[Bobzien] p. 117Statement T2stoic2a 1797
[Bobzien] p. 117Statement T4stoic4a 1800
[Bobzien] p. 117Conclusion the contradictorystoic1a 1795
[Bogachev] p. 16Definition 1.5df-oms 34599
[Bogachev] p. 17Lemma 1.5.4omssubadd 34607
[Bogachev] p. 17Example 1.5.2omsmon 34605
[Bogachev] p. 41Definition 1.11.2df-carsg 34609
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34629
[Bogachev] p. 116Definition 2.3.1df-itgm 34660  df-sitm 34638
[Bogachev] p. 118Chapter 2.4.4df-itgm 34660
[Bogachev] p. 118Definition 2.4.1df-sitg 34637
[Bollobas] p. 1Section I.1df-edg 29307  isuhgrop 29329  isusgrop 29421  isuspgrop 29420
[Bollobas] p. 2Section I.1df-isubgr 48481  df-subgr 29527  uhgrspan1 29562  uhgrspansubgr 29550
[Bollobas] p. 3Definitiondf-gric 48501  gricuspgr 48538  isuspgrim 48516
[Bollobas] p. 3Section I.1cusgrsize 29713  df-clnbgr 48439  df-cusgr 29671  df-nbgr 29592  fusgrmaxsize 29723
[Bollobas] p. 4Definitiondf-upwlks 48754  df-wlks 29858
[Bollobas] p. 4Section I.1finsumvtxdg2size 29809  finsumvtxdgeven 29811  fusgr1th 29810  fusgrvtxdgonume 29813  vtxdgoddnumeven 29812
[Bollobas] p. 5Notationdf-pths 29972
[Bollobas] p. 5Definitiondf-crcts 30044  df-cycls 30045  df-trls 29949  df-wlkson 29859
[Bollobas] p. 7Section I.1df-ushgr 29318
[BourbakiAlg1] p. 1Definition 1df-clintop 48820  df-cllaw 48806  df-mgm 18688  df-mgm2 48839
[BourbakiAlg1] p. 4Definition 5df-assintop 48821  df-asslaw 48808  df-sgrp 18767  df-sgrp2 48841
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48840  df-comlaw 48807
[BourbakiAlg1] p. 12Definition 2df-mnd 18783
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33259  mndlactf1o 33263  mndractf1 33261  mndractf1o 33264
[BourbakiAlg1] p. 92Definition 1df-ring 20308
[BourbakiAlg1] p. 93Section I.8.1df-rng 20222
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33940
[BourbakiAlg2] p. 113Chapter 5.assafld 33944  assarrginv 33943
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33985  fldextrspunfld 33983  fldextrspunlem1 33982  fldextrspunlem2 33984  fldextrspunlsp 33981  fldextrspunlsplem 33980
[BourbakiCAlg2], p. 228Proposition 21arithidom 33744  dfufd2 33757
[BourbakiEns] p. Proposition 8fcof1 7275  fcofo 7276
[BourbakiTop1] p. Remarkxnegmnf 13227  xnegpnf 13226
[BourbakiTop1] p. Remark rexneg 13228
[BourbakiTop1] p. Remark 3ust0 24338  ustfilxp 24331
[BourbakiTop1] p. Axiom GT'tgpsubcn 24208
[BourbakiTop1] p. Criterionishmeo 23877
[BourbakiTop1] p. Example 1cstucnd 24401  iducn 24400  snfil 23982
[BourbakiTop1] p. Example 2neifil 23998
[BourbakiTop1] p. Theorem 1cnextcn 24185
[BourbakiTop1] p. Theorem 2ucnextcn 24421
[BourbakiTop1] p. Theorem 3df-hcmp 34264
[BourbakiTop1] p. Paragraph 3infil 23981
[BourbakiTop1] p. Definition 1df-ucn 24393  df-ust 24319  filintn0 23979  filn0 23980  istgp 24195  ucnprima 24399
[BourbakiTop1] p. Definition 2df-cfilu 24404
[BourbakiTop1] p. Definition 3df-cusp 24415  df-usp 24375  df-utop 24349  trust 24347
[BourbakiTop1] p. Definition 6df-pcmp 34163
[BourbakiTop1] p. Property V_issnei2 23234
[BourbakiTop1] p. Theorem 1(d)iscncl 23387
[BourbakiTop1] p. Condition F_Iustssel 24324
[BourbakiTop1] p. Condition U_Iustdiag 24327
[BourbakiTop1] p. Property V_iiinnei 23243
[BourbakiTop1] p. Property V_ivneiptopreu 23251  neissex 23245
[BourbakiTop1] p. Proposition 1neips 23231  neiss 23227  ucncn 24402  ustund 24340  ustuqtop 24364
[BourbakiTop1] p. Proposition 2cnpco 23385  neiptopreu 23251  utop2nei 24368  utop3cls 24369
[BourbakiTop1] p. Proposition 3fmucnd 24409  uspreg 24391  utopreg 24370
[BourbakiTop1] p. Proposition 4imasncld 23809  imasncls 23810  imasnopn 23808
[BourbakiTop1] p. Proposition 9cnpflf2 24118
[BourbakiTop1] p. Condition F_IIustincl 24326
[BourbakiTop1] p. Condition U_IIustinvel 24328
[BourbakiTop1] p. Property V_iiielnei 23229
[BourbakiTop1] p. Proposition 11cnextucn 24420
[BourbakiTop1] p. Condition F_IIbustbasel 24325
[BourbakiTop1] p. Condition U_IIIustexhalf 24329
[BourbakiTop1] p. Definition C'''df-cmp 23505
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23964
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23012
[BourbakiTop2] p. 195Definition 1df-ldlf 34160
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46634
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46636  stoweid 46635
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46573  stoweidlem10 46582  stoweidlem14 46586  stoweidlem15 46587  stoweidlem35 46607  stoweidlem36 46608  stoweidlem37 46609  stoweidlem38 46610  stoweidlem40 46612  stoweidlem41 46613  stoweidlem43 46615  stoweidlem44 46616  stoweidlem46 46618  stoweidlem5 46577  stoweidlem50 46622  stoweidlem52 46624  stoweidlem53 46625  stoweidlem55 46627  stoweidlem56 46628
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46595  stoweidlem24 46596  stoweidlem27 46599  stoweidlem28 46600  stoweidlem30 46602
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46606  stoweidlem59 46631  stoweidlem60 46632
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46617  stoweidlem49 46621  stoweidlem7 46579
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46603  stoweidlem39 46611  stoweidlem42 46614  stoweidlem48 46620  stoweidlem51 46623  stoweidlem54 46626  stoweidlem57 46629  stoweidlem58 46630
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46597
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46589
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46583  stoweidlem13 46585  stoweidlem26 46598  stoweidlem61 46633
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46590
[Bruck] p. 1Section I.1df-clintop 48820  df-mgm 18688  df-mgm2 48839
[Bruck] p. 23Section II.1df-sgrp 18767  df-sgrp2 48841
[Bruck] p. 28Theorem 3.2dfgrp3 19096
[ChoquetDD] p. 2Definition of mappingdf-mpt 5187
[Church] p. 129Section II.24df-ifp 1077  dfifp2 1078
[Clemente] p. 10Definition ITnatded 30663
[Clemente] p. 10Definition I` `m,nnatded 30663
[Clemente] p. 11Definition E=>m,nnatded 30663
[Clemente] p. 11Definition I=>m,nnatded 30663
[Clemente] p. 11Definition E` `(1)natded 30663
[Clemente] p. 11Definition E` `(2)natded 30663
[Clemente] p. 12Definition E` `m,n,pnatded 30663
[Clemente] p. 12Definition I` `n(1)natded 30663
[Clemente] p. 12Definition I` `n(2)natded 30663
[Clemente] p. 13Definition I` `m,n,pnatded 30663
[Clemente] p. 14Proof 5.11natded 30663
[Clemente] p. 14Definition E` `nnatded 30663
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30665  ex-natded5.2 30664
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30668  ex-natded5.3 30667
[Clemente] p. 18Theorem 5.5ex-natded5.5 30670
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30672  ex-natded5.7 30671
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30674  ex-natded5.8 30673
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30676  ex-natded5.13 30675
[Clemente] p. 32Definition I` `nnatded 30663
[Clemente] p. 32Definition E` `m,n,p,anatded 30663
[Clemente] p. 32Definition E` `n,tnatded 30663
[Clemente] p. 32Definition I` `n,tnatded 30663
[Clemente] p. 43Theorem 9.20ex-natded9.20 30677
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30678
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30680  ex-natded9.26 30679
[Cohen] p. 301Remarkrelogoprlem 26714
[Cohen] p. 301Property 2relogmul 26715  relogmuld 26748
[Cohen] p. 301Property 3relogdiv 26716  relogdivd 26749
[Cohen] p. 301Property 4relogexp 26719
[Cohen] p. 301Property 1alog1 26708
[Cohen] p. 301Property 1bloge 26709
[Cohen4] p. 348Observationrelogbcxpb 26910
[Cohen4] p. 349Propertyrelogbf 26914
[Cohen4] p. 352Definitionelogb 26893
[Cohen4] p. 361Property 2relogbmul 26900
[Cohen4] p. 361Property 3logbrec 26905  relogbdiv 26902
[Cohen4] p. 361Property 4relogbreexp 26898
[Cohen4] p. 361Property 6relogbexp 26903
[Cohen4] p. 361Property 1(a)logbid1 26891
[Cohen4] p. 361Property 1(b)logb1 26892
[Cohen4] p. 367Propertylogbchbase 26894
[Cohen4] p. 377Property 2logblt 26907
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34592  sxbrsigalem4 34594
[Cohn] p. 81Section II.5acsdomd 18603  acsinfd 18602  acsinfdimd 18604  acsmap2d 18601  acsmapd 18600
[Cohn] p. 143Example 5.1.1sxbrsiga 34597
[Connell] p. 57Definitiondf-scmat 22609  df-scmatalt 49030
[Conway] p. 4Definitionlesrec 27950  lesrecd 27951
[Conway] p. 5Definitionaddsval 28113  addsval2 28114  df-adds 28111  df-muls 28258  df-negs 28172
[Conway] p. 7Theorem0lt1s 27963
[Conway] p. 12Theorem 12pw2cut2 28613
[Conway] p. 16Theorem 0(i)sltsright 28012
[Conway] p. 16Theorem 0(ii)sltsleft 28011
[Conway] p. 16Theorem 0(iii)lesid 27889
[Conway] p. 17Theorem 3addsass 28156  addsassd 28157  addscom 28117  addscomd 28118  addsrid 28115  addsridd 28116
[Conway] p. 17Definitiondf-0s 27958
[Conway] p. 17Theorem 4(ii)negnegs 28195
[Conway] p. 17Theorem 4(iii)negsid 28192  negsidd 28193
[Conway] p. 18Theorem 5leadds1 28140  leadds1d 28146
[Conway] p. 18Definitiondf-1s 27959
[Conway] p. 18Theorem 6(ii)negscl 28187  negscld 28188
[Conway] p. 18Theorem 6(iii)addscld 28131
[Conway] p. 19Notemulsunif2 28321
[Conway] p. 19Theorem 7addsdi 28306  addsdid 28307  addsdird 28308  mulnegs1d 28311  mulnegs2d 28312  mulsass 28317  mulsassd 28318  mulscom 28290  mulscomd 28291
[Conway] p. 19Theorem 8(i)mulscl 28285  mulscld 28286
[Conway] p. 19Theorem 8(iii)lemulsd 28289  ltmuls 28287  ltmulsd 28288
[Conway] p. 20Theorem 9mulsgt0 28295  mulsgt0d 28296
[Conway] p. 21Theorem 10(iv)precsex 28369
[Conway] p. 23Theorem 11eqcuts3 27955
[Conway] p. 24Definitiondf-reno 28641
[Conway] p. 24Theorem 13(ii)readdscl 28650  remulscl 28653  renegscl 28649
[Conway] p. 27Definitiondf-ons 28403  elons2 28409
[Conway] p. 27Theorem 14ltonsex 28413
[Conway] p. 28Theorem 15oncutlt 28415  onswe 28423
[Conway] p. 29Remarkmadebday 28051  newbday 28053  oldbday 28052
[Conway] p. 29Definitiondf-made 27978  df-new 27980  df-old 27979
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13885
[Crawley] p. 1Definition of posetdf-poset 18359
[Crawley] p. 107Theorem 13.2hlsupr 40022
[Crawley] p. 110Theorem 13.3arglem1N 40826  dalaw 40522
[Crawley] p. 111Theorem 13.4hlathil 42597
[Crawley] p. 111Definition of set Wdf-watsN 40626
[Crawley] p. 111Definition of dilationdf-dilN 40742  df-ldil 40740  isldil 40746
[Crawley] p. 111Definition of translationdf-ltrn 40741  df-trnN 40743  isltrn 40755  ltrnu 40757
[Crawley] p. 112Lemma Acdlema1N 40427  cdlema2N 40428  exatleN 40040
[Crawley] p. 112Lemma B1cvrat 40112  cdlemb 40430  cdlemb2 40677  cdlemb3 41242  idltrn 40786  l1cvat 39691  lhpat 40679  lhpat2 40681  lshpat 39692  ltrnel 40775  ltrnmw 40787
[Crawley] p. 112Lemma Ccdlemc1 40827  cdlemc2 40828  ltrnnidn 40810  trlat 40805  trljat1 40802  trljat2 40803  trljat3 40804  trlne 40821  trlnidat 40809  trlnle 40822
[Crawley] p. 112Definition of automorphismdf-pautN 40627
[Crawley] p. 113Lemma Ccdlemc 40833  cdlemc3 40829  cdlemc4 40830
[Crawley] p. 113Lemma Dcdlemd 40843  cdlemd1 40834  cdlemd2 40835  cdlemd3 40836  cdlemd4 40837  cdlemd5 40838  cdlemd6 40839  cdlemd7 40840  cdlemd8 40841  cdlemd9 40842  cdleme31sde 41021  cdleme31se 41018  cdleme31se2 41019  cdleme31snd 41022  cdleme32a 41077  cdleme32b 41078  cdleme32c 41079  cdleme32d 41080  cdleme32e 41081  cdleme32f 41082  cdleme32fva 41073  cdleme32fva1 41074  cdleme32fvcl 41076  cdleme32le 41083  cdleme48fv 41135  cdleme4gfv 41143  cdleme50eq 41177  cdleme50f 41178  cdleme50f1 41179  cdleme50f1o 41182  cdleme50laut 41183  cdleme50ldil 41184  cdleme50lebi 41176  cdleme50rn 41181  cdleme50rnlem 41180  cdlemeg49le 41147  cdlemeg49lebilem 41175
[Crawley] p. 113Lemma Ecdleme 41196  cdleme00a 40845  cdleme01N 40857  cdleme02N 40858  cdleme0a 40847  cdleme0aa 40846  cdleme0b 40848  cdleme0c 40849  cdleme0cp 40850  cdleme0cq 40851  cdleme0dN 40852  cdleme0e 40853  cdleme0ex1N 40859  cdleme0ex2N 40860  cdleme0fN 40854  cdleme0gN 40855  cdleme0moN 40861  cdleme1 40863  cdleme10 40890  cdleme10tN 40894  cdleme11 40906  cdleme11a 40896  cdleme11c 40897  cdleme11dN 40898  cdleme11e 40899  cdleme11fN 40900  cdleme11g 40901  cdleme11h 40902  cdleme11j 40903  cdleme11k 40904  cdleme11l 40905  cdleme12 40907  cdleme13 40908  cdleme14 40909  cdleme15 40914  cdleme15a 40910  cdleme15b 40911  cdleme15c 40912  cdleme15d 40913  cdleme16 40921  cdleme16aN 40895  cdleme16b 40915  cdleme16c 40916  cdleme16d 40917  cdleme16e 40918  cdleme16f 40919  cdleme16g 40920  cdleme19a 40939  cdleme19b 40940  cdleme19c 40941  cdleme19d 40942  cdleme19e 40943  cdleme19f 40944  cdleme1b 40862  cdleme2 40864  cdleme20aN 40945  cdleme20bN 40946  cdleme20c 40947  cdleme20d 40948  cdleme20e 40949  cdleme20f 40950  cdleme20g 40951  cdleme20h 40952  cdleme20i 40953  cdleme20j 40954  cdleme20k 40955  cdleme20l 40958  cdleme20l1 40956  cdleme20l2 40957  cdleme20m 40959  cdleme20y 40938  cdleme20zN 40937  cdleme21 40973  cdleme21d 40966  cdleme21e 40967  cdleme22a 40976  cdleme22aa 40975  cdleme22b 40977  cdleme22cN 40978  cdleme22d 40979  cdleme22e 40980  cdleme22eALTN 40981  cdleme22f 40982  cdleme22f2 40983  cdleme22g 40984  cdleme23a 40985  cdleme23b 40986  cdleme23c 40987  cdleme26e 40995  cdleme26eALTN 40997  cdleme26ee 40996  cdleme26f 40999  cdleme26f2 41001  cdleme26f2ALTN 41000  cdleme26fALTN 40998  cdleme27N 41005  cdleme27a 41003  cdleme27cl 41002  cdleme28c 41008  cdleme3 40873  cdleme30a 41014  cdleme31fv 41026  cdleme31fv1 41027  cdleme31fv1s 41028  cdleme31fv2 41029  cdleme31id 41030  cdleme31sc 41020  cdleme31sdnN 41023  cdleme31sn 41016  cdleme31sn1 41017  cdleme31sn1c 41024  cdleme31sn2 41025  cdleme31so 41015  cdleme35a 41084  cdleme35b 41086  cdleme35c 41087  cdleme35d 41088  cdleme35e 41089  cdleme35f 41090  cdleme35fnpq 41085  cdleme35g 41091  cdleme35h 41092  cdleme35h2 41093  cdleme35sn2aw 41094  cdleme35sn3a 41095  cdleme36a 41096  cdleme36m 41097  cdleme37m 41098  cdleme38m 41099  cdleme38n 41100  cdleme39a 41101  cdleme39n 41102  cdleme3b 40865  cdleme3c 40866  cdleme3d 40867  cdleme3e 40868  cdleme3fN 40869  cdleme3fa 40872  cdleme3g 40870  cdleme3h 40871  cdleme4 40874  cdleme40m 41103  cdleme40n 41104  cdleme40v 41105  cdleme40w 41106  cdleme41fva11 41113  cdleme41sn3aw 41110  cdleme41sn4aw 41111  cdleme41snaw 41112  cdleme42a 41107  cdleme42b 41114  cdleme42c 41108  cdleme42d 41109  cdleme42e 41115  cdleme42f 41116  cdleme42g 41117  cdleme42h 41118  cdleme42i 41119  cdleme42k 41120  cdleme42ke 41121  cdleme42keg 41122  cdleme42mN 41123  cdleme42mgN 41124  cdleme43aN 41125  cdleme43bN 41126  cdleme43cN 41127  cdleme43dN 41128  cdleme5 40876  cdleme50ex 41195  cdleme50ltrn 41193  cdleme51finvN 41192  cdleme51finvfvN 41191  cdleme51finvtrN 41194  cdleme6 40877  cdleme7 40885  cdleme7a 40879  cdleme7aa 40878  cdleme7b 40880  cdleme7c 40881  cdleme7d 40882  cdleme7e 40883  cdleme7ga 40884  cdleme8 40886  cdleme8tN 40891  cdleme9 40889  cdleme9a 40887  cdleme9b 40888  cdleme9tN 40893  cdleme9taN 40892  cdlemeda 40934  cdlemedb 40933  cdlemednpq 40935  cdlemednuN 40936  cdlemefr27cl 41039  cdlemefr32fva1 41046  cdlemefr32fvaN 41045  cdlemefrs32fva 41036  cdlemefrs32fva1 41037  cdlemefs27cl 41049  cdlemefs32fva1 41059  cdlemefs32fvaN 41058  cdlemesner 40932  cdlemeulpq 40856
[Crawley] p. 114Lemma E4atex 40712  4atexlem7 40711  cdleme0nex 40926  cdleme17a 40922  cdleme17c 40924  cdleme17d 41134  cdleme17d1 40925  cdleme17d2 41131  cdleme18a 40927  cdleme18b 40928  cdleme18c 40929  cdleme18d 40931  cdleme4a 40875
[Crawley] p. 115Lemma Ecdleme21a 40961  cdleme21at 40964  cdleme21b 40962  cdleme21c 40963  cdleme21ct 40965  cdleme21f 40968  cdleme21g 40969  cdleme21h 40970  cdleme21i 40971  cdleme22gb 40930
[Crawley] p. 116Lemma Fcdlemf 41199  cdlemf1 41197  cdlemf2 41198
[Crawley] p. 116Lemma Gcdlemftr1 41203  cdlemg16 41293  cdlemg28 41340  cdlemg28a 41329  cdlemg28b 41339  cdlemg3a 41233  cdlemg42 41365  cdlemg43 41366  cdlemg44 41369  cdlemg44a 41367  cdlemg46 41371  cdlemg47 41372  cdlemg9 41270  ltrnco 41355  ltrncom 41374  tgrpabl 41387  trlco 41363
[Crawley] p. 116Definition of Gdf-tgrp 41379
[Crawley] p. 117Lemma Gcdlemg17 41313  cdlemg17b 41298
[Crawley] p. 117Definition of Edf-edring-rN 41392  df-edring 41393
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41396
[Crawley] p. 118Remarktendopltp 41416
[Crawley] p. 118Lemma Hcdlemh 41453  cdlemh1 41451  cdlemh2 41452
[Crawley] p. 118Lemma Icdlemi 41456  cdlemi1 41454  cdlemi2 41455
[Crawley] p. 118Lemma Jcdlemj1 41457  cdlemj2 41458  cdlemj3 41459  tendocan 41460
[Crawley] p. 118Lemma Kcdlemk 41610  cdlemk1 41467  cdlemk10 41479  cdlemk11 41485  cdlemk11t 41582  cdlemk11ta 41565  cdlemk11tb 41567  cdlemk11tc 41581  cdlemk11u-2N 41525  cdlemk11u 41507  cdlemk12 41486  cdlemk12u-2N 41526  cdlemk12u 41508  cdlemk13-2N 41512  cdlemk13 41488  cdlemk14-2N 41514  cdlemk14 41490  cdlemk15-2N 41515  cdlemk15 41491  cdlemk16-2N 41516  cdlemk16 41493  cdlemk16a 41492  cdlemk17-2N 41517  cdlemk17 41494  cdlemk18-2N 41522  cdlemk18-3N 41536  cdlemk18 41504  cdlemk19-2N 41523  cdlemk19 41505  cdlemk19u 41606  cdlemk1u 41495  cdlemk2 41468  cdlemk20-2N 41528  cdlemk20 41510  cdlemk21-2N 41527  cdlemk21N 41509  cdlemk22-3 41537  cdlemk22 41529  cdlemk23-3 41538  cdlemk24-3 41539  cdlemk25-3 41540  cdlemk26-3 41542  cdlemk26b-3 41541  cdlemk27-3 41543  cdlemk28-3 41544  cdlemk29-3 41547  cdlemk3 41469  cdlemk30 41530  cdlemk31 41532  cdlemk32 41533  cdlemk33N 41545  cdlemk34 41546  cdlemk35 41548  cdlemk36 41549  cdlemk37 41550  cdlemk38 41551  cdlemk39 41552  cdlemk39u 41604  cdlemk4 41470  cdlemk41 41556  cdlemk42 41577  cdlemk42yN 41580  cdlemk43N 41599  cdlemk45 41583  cdlemk46 41584  cdlemk47 41585  cdlemk48 41586  cdlemk49 41587  cdlemk5 41472  cdlemk50 41588  cdlemk51 41589  cdlemk52 41590  cdlemk53 41593  cdlemk54 41594  cdlemk55 41597  cdlemk55u 41602  cdlemk56 41607  cdlemk5a 41471  cdlemk5auN 41496  cdlemk5u 41497  cdlemk6 41473  cdlemk6u 41498  cdlemk7 41484  cdlemk7u-2N 41524  cdlemk7u 41506  cdlemk8 41474  cdlemk9 41475  cdlemk9bN 41476  cdlemki 41477  cdlemkid 41572  cdlemkj-2N 41518  cdlemkj 41499  cdlemksat 41482  cdlemksel 41481  cdlemksv 41480  cdlemksv2 41483  cdlemkuat 41502  cdlemkuel-2N 41520  cdlemkuel-3 41534  cdlemkuel 41501  cdlemkuv-2N 41519  cdlemkuv2-2 41521  cdlemkuv2-3N 41535  cdlemkuv2 41503  cdlemkuvN 41500  cdlemkvcl 41478  cdlemky 41562  cdlemkyyN 41598  tendoex 41611
[Crawley] p. 120Remarkdva1dim 41621
[Crawley] p. 120Lemma Lcdleml1N 41612  cdleml2N 41613  cdleml3N 41614  cdleml4N 41615  cdleml5N 41616  cdleml6 41617  cdleml7 41618  cdleml8 41619  cdleml9 41620  dia1dim 41697
[Crawley] p. 120Lemma Mdia11N 41684  diaf11N 41685  dialss 41682  diaord 41683  dibf11N 41797  djajN 41773
[Crawley] p. 120Definition of isomorphism mapdiaval 41668
[Crawley] p. 121Lemma Mcdlemm10N 41754  dia2dimlem1 41700  dia2dimlem2 41701  dia2dimlem3 41702  dia2dimlem4 41703  dia2dimlem5 41704  diaf1oN 41766  diarnN 41765  dvheveccl 41748  dvhopN 41752
[Crawley] p. 121Lemma Ncdlemn 41848  cdlemn10 41842  cdlemn11 41847  cdlemn11a 41843  cdlemn11b 41844  cdlemn11c 41845  cdlemn11pre 41846  cdlemn2 41831  cdlemn2a 41832  cdlemn3 41833  cdlemn4 41834  cdlemn4a 41835  cdlemn5 41837  cdlemn5pre 41836  cdlemn6 41838  cdlemn7 41839  cdlemn8 41840  cdlemn9 41841  diclspsn 41830
[Crawley] p. 121Definition of phi(q)df-dic 41809
[Crawley] p. 122Lemma Ndih11 41901  dihf11 41903  dihjust 41853  dihjustlem 41852  dihord 41900  dihord1 41854  dihord10 41859  dihord11b 41858  dihord11c 41860  dihord2 41863  dihord2a 41855  dihord2b 41856  dihord2cN 41857  dihord2pre 41861  dihord2pre2 41862  dihordlem6 41849  dihordlem7 41850  dihordlem7b 41851
[Crawley] p. 122Definition of isomorphism mapdihffval 41866  dihfval 41867  dihval 41868
[Diestel] p. 3Definitiondf-gric 48501  df-grim 48498  isuspgrim 48516
[Diestel] p. 3Section 1.1df-cusgr 29671  df-nbgr 29592
[Diestel] p. 3Definition by df-grisom 48497
[Diestel] p. 4Section 1.1df-isubgr 48481  df-subgr 29527  uhgrspan1 29562  uhgrspansubgr 29550
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29813  vtxdgoddnumeven 29812
[Diestel] p. 27Section 1.10df-ushgr 29318
[EGA] p. 80Notation 1.1.1rspecval 34171
[EGA] p. 80Proposition 1.1.2zartop 34183
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34175  zarcls1 34176
[EGA] p. 81Corollary 1.1.8zart0 34186
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34189
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34192
[Eisenberg] p. 67Definition 5.3df-dif 3910
[Eisenberg] p. 82Definition 6.3dfom3 9604
[Eisenberg] p. 125Definition 8.21df-map 8814
[Eisenberg] p. 216Example 13.2(4)omenps 9612
[Eisenberg] p. 310Theorem 19.8cardprc 9954
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10527
[Enderton] p. 18Axiom of Empty Setaxnul 5260
[Enderton] p. 19Definitiondf-tp 4590
[Enderton] p. 26Exercise 5unissb 4902
[Enderton] p. 26Exercise 10pwel 5343
[Enderton] p. 28Exercise 7(b)pwun 5545
[Enderton] p. 30Theorem "Distributive laws"iinin1 5041  iinin2 5040  iinun2 5033  iunin1 5032  iunin1f 32812  iunin2 5031  uniin1 5035  uniin2 5036
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5039  iundif2 5034
[Enderton] p. 32Exercise 20unineq 4243
[Enderton] p. 33Exercise 23iinuni 5060
[Enderton] p. 33Exercise 25iununi 5061
[Enderton] p. 33Exercise 24(a)iinpw 5068
[Enderton] p. 33Exercise 24(b)iunpw 7758  iunpwss 5069
[Enderton] p. 36Definitionopthwiener 5488
[Enderton] p. 38Exercise 6(a)unipw 5422
[Enderton] p. 38Exercise 6(b)pwuni 4907
[Enderton] p. 41Lemma 3Dopeluu 5443  rnex 7895  rnexg 7887
[Enderton] p. 41Exercise 8dmuni 5895  rnuni 6137
[Enderton] p. 42Definition of a functiondffun7 6552  dffun8 6553
[Enderton] p. 43Definition of function valuefunfv2 6959
[Enderton] p. 43Definition of single-rootedfuncnv 6594
[Enderton] p. 44Definition (d)dfima2 6055  dfima3 6056
[Enderton] p. 47Theorem 3Hfvco2 6968
[Enderton] p. 49Axiom of Choice (first form)ac7 10445  ac7g 10446  df-ac 10088  dfac2 10103  dfac2a 10101  dfac2b 10102  dfac3 10093  dfac7 10104
[Enderton] p. 50Theorem 3K(a)imauni 7234
[Enderton] p. 52Definitiondf-map 8814
[Enderton] p. 53Exercise 21coass 6257
[Enderton] p. 53Exercise 27dmco 6246
[Enderton] p. 53Exercise 14(a)funin 6601
[Enderton] p. 53Exercise 22(a)imass2 6095
[Enderton] p. 54Remarkixpf 8906  ixpssmap 8918
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8884
[Enderton] p. 55Axiom of Choice (second form)ac9 10455  ac9s 10465
[Enderton] p. 56Theorem 3Meqvrelref 39205  erref 8703
[Enderton] p. 57Lemma 3Neqvrelthi 39208  erthi 8739
[Enderton] p. 57Definitiondf-ec 8684
[Enderton] p. 58Definitiondf-qs 8688
[Enderton] p. 61Exercise 35df-ec 8684
[Enderton] p. 65Exercise 56(a)dmun 5891
[Enderton] p. 68Definition of successordf-suc 6356
[Enderton] p. 71Definitiondf-tr 5213  dftr4 5218
[Enderton] p. 72Theorem 4Eunisuc 6431  unisucg 6430
[Enderton] p. 73Exercise 6unisuc 6431  unisucg 6430
[Enderton] p. 73Exercise 5(a)truni 5228
[Enderton] p. 73Exercise 5(b)trint 5230  trintALT 45454
[Enderton] p. 79Theorem 4I(A1)nna0 8578
[Enderton] p. 79Theorem 4I(A2)nnasuc 8580  onasuc 8501
[Enderton] p. 79Definition of operation valuedf-ov 7403
[Enderton] p. 80Theorem 4J(A1)nnm0 8579
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8581  onmsuc 8502
[Enderton] p. 81Theorem 4K(1)nnaass 8596
[Enderton] p. 81Theorem 4K(2)nna0r 8583  nnacom 8591
[Enderton] p. 81Theorem 4K(3)nndi 8597
[Enderton] p. 81Theorem 4K(4)nnmass 8598
[Enderton] p. 81Theorem 4K(5)nnmcom 8600
[Enderton] p. 82Exercise 16nnm0r 8584  nnmsucr 8599
[Enderton] p. 88Exercise 23nnaordex 8612
[Enderton] p. 129Definitiondf-en 8932
[Enderton] p. 132Theorem 6B(b)canth 7354
[Enderton] p. 133Exercise 1xpomen 9987
[Enderton] p. 133Exercise 2qnnen 16259
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9179
[Enderton] p. 135Corollary 6Cphp3 9181
[Enderton] p. 136Corollary 6Enneneq 9178
[Enderton] p. 136Corollary 6D(a)pssinf 9210
[Enderton] p. 136Corollary 6D(b)ominf 9212
[Enderton] p. 137Lemma 6Fpssnn 9141
[Enderton] p. 138Corollary 6Gssfi 9145
[Enderton] p. 139Theorem 6H(c)mapen 9117
[Enderton] p. 142Theorem 6I(3)xpdjuen 10151
[Enderton] p. 142Theorem 6I(4)mapdjuen 10152
[Enderton] p. 143Theorem 6Jdju0en 10147  dju1en 10143
[Enderton] p. 144Exercise 13iunfi 9288  unifi 9289  unifi2 9290
[Enderton] p. 144Corollary 6Kundif2 4434  unfi 9143  unfi2 9258
[Enderton] p. 145Figure 38ffoss 7931
[Enderton] p. 145Definitiondf-dom 8933
[Enderton] p. 146Example 1domen 8946  domeng 8947
[Enderton] p. 146Example 3nndomo 9190  nnsdom 9611  nnsdomg 9247
[Enderton] p. 149Theorem 6L(a)djudom2 10155
[Enderton] p. 149Theorem 6L(c)mapdom1 9118  xpdom1 9052  xpdom1g 9050  xpdom2g 9049
[Enderton] p. 149Theorem 6L(d)mapdom2 9124
[Enderton] p. 151Theorem 6Mzorn 10479  zorng 10476
[Enderton] p. 151Theorem 6M(4)ac8 10464  dfac5 10100
[Enderton] p. 159Theorem 6Qunictb 10548
[Enderton] p. 164Exampleinfdif 10179
[Enderton] p. 168Definitiondf-po 5560
[Enderton] p. 192Theorem 7M(a)oneli 6465
[Enderton] p. 192Theorem 7M(b)ontr1 6397
[Enderton] p. 192Theorem 7M(c)onirri 6464
[Enderton] p. 193Corollary 7N(b)0elon 6405
[Enderton] p. 193Corollary 7N(c)onsuci 7823
[Enderton] p. 193Corollary 7N(d)ssonunii 7768
[Enderton] p. 194Remarkonprc 7765
[Enderton] p. 194Exercise 16suc11 6459
[Enderton] p. 197Definitiondf-card 9913
[Enderton] p. 197Theorem 7Pcarden 10523
[Enderton] p. 200Exercise 25tfis 7839
[Enderton] p. 202Lemma 7Tr1tr 9736
[Enderton] p. 202Definitiondf-r1 9724
[Enderton] p. 202Theorem 7Qr1val1 9746
[Enderton] p. 204Theorem 7V(b)rankval4 9827  rankval4b 35408
[Enderton] p. 206Theorem 7X(b)en2lp 9563
[Enderton] p. 207Exercise 30rankpr 9817  rankprb 9811  rankpw 9803  rankpwi 9783  rankuniss 9826
[Enderton] p. 207Exercise 34opthreg 9575
[Enderton] p. 208Exercise 35suc11reg 9576
[Enderton] p. 212Definition of alephalephval3 10082
[Enderton] p. 213Theorem 8A(a)alephord2 10048
[Enderton] p. 213Theorem 8A(b)cardalephex 10062
[Enderton] p. 218Theorem Schema 8Eonfununi 8316
[Enderton] p. 222Definition of kardkarden 9869  kardex 9868
[Enderton] p. 238Theorem 8Roeoa 8571
[Enderton] p. 238Theorem 8Soeoe 8573
[Enderton] p. 240Exercise 25oarec 8535
[Enderton] p. 257Definition of cofinalitycflm 10221
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17688
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17630
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18599  mrieqv2d 17685  mrieqvd 17684
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17689
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17694  mreexexlem2d 17691
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18605  mreexfidimd 17696
[Frege1879] p. 11Statementdf3or2 44356
[Frege1879] p. 12Statementdf3an2 44357  dfxor4 44354  dfxor5 44355
[Frege1879] p. 26Axiom 1ax-frege1 44378
[Frege1879] p. 26Axiom 2ax-frege2 44379
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44383
[Frege1879] p. 31Proposition 4frege4 44387
[Frege1879] p. 32Proposition 5frege5 44388
[Frege1879] p. 33Proposition 6frege6 44394
[Frege1879] p. 34Proposition 7frege7 44396
[Frege1879] p. 35Axiom 8ax-frege8 44397  axfrege8 44395
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 37951
[Frege1879] p. 35Proposition 9frege9 44400
[Frege1879] p. 36Proposition 10frege10 44408
[Frege1879] p. 36Proposition 11frege11 44402
[Frege1879] p. 37Proposition 12frege12 44401
[Frege1879] p. 37Proposition 13frege13 44410
[Frege1879] p. 37Proposition 14frege14 44411
[Frege1879] p. 38Proposition 15frege15 44414
[Frege1879] p. 38Proposition 16frege16 44404
[Frege1879] p. 39Proposition 17frege17 44409
[Frege1879] p. 39Proposition 18frege18 44406
[Frege1879] p. 39Proposition 19frege19 44412
[Frege1879] p. 40Proposition 20frege20 44416
[Frege1879] p. 40Proposition 21frege21 44415
[Frege1879] p. 41Proposition 22frege22 44407
[Frege1879] p. 42Proposition 23frege23 44413
[Frege1879] p. 42Proposition 24frege24 44403
[Frege1879] p. 42Proposition 25frege25 44405  rp-frege25 44393
[Frege1879] p. 42Proposition 26frege26 44398
[Frege1879] p. 43Axiom 28ax-frege28 44418
[Frege1879] p. 43Proposition 27frege27 44399
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44419
[Frege1879] p. 44Axiom 31ax-frege31 44422  axfrege31 44421
[Frege1879] p. 44Proposition 30frege30 44420
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44423
[Frege1879] p. 44Proposition 33frege33 44424
[Frege1879] p. 45Proposition 34frege34 44425
[Frege1879] p. 45Proposition 35frege35 44426
[Frege1879] p. 45Proposition 36frege36 44427
[Frege1879] p. 46Proposition 37frege37 44428
[Frege1879] p. 46Proposition 38frege38 44429
[Frege1879] p. 46Proposition 39frege39 44430
[Frege1879] p. 46Proposition 40frege40 44431
[Frege1879] p. 47Axiom 41ax-frege41 44433  axfrege41 44432
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44434
[Frege1879] p. 47Proposition 43frege43 44435
[Frege1879] p. 47Proposition 44frege44 44436
[Frege1879] p. 47Proposition 45frege45 44437
[Frege1879] p. 48Proposition 46frege46 44438
[Frege1879] p. 48Proposition 47frege47 44439
[Frege1879] p. 49Proposition 48frege48 44440
[Frege1879] p. 49Proposition 49frege49 44441
[Frege1879] p. 49Proposition 50frege50 44442
[Frege1879] p. 50Axiom 52ax-frege52a 44445  ax-frege52c 44476  frege52aid 44446  frege52b 44477
[Frege1879] p. 50Axiom 54ax-frege54a 44450  ax-frege54c 44480  frege54b 44481
[Frege1879] p. 50Proposition 51frege51 44443
[Frege1879] p. 50Proposition 52dfsbcq 3749
[Frege1879] p. 50Proposition 53frege53a 44448  frege53aid 44447  frege53b 44478  frege53c 44502
[Frege1879] p. 50Proposition 54biid 264  eqid 2765
[Frege1879] p. 50Proposition 55frege55a 44456  frege55aid 44453  frege55b 44485  frege55c 44506  frege55cor1a 44457  frege55lem2a 44455  frege55lem2b 44484  frege55lem2c 44505
[Frege1879] p. 50Proposition 56frege56a 44459  frege56aid 44458  frege56b 44486  frege56c 44507
[Frege1879] p. 51Axiom 58ax-frege58a 44463  ax-frege58b 44489  frege58bid 44490  frege58c 44509
[Frege1879] p. 51Proposition 57frege57a 44461  frege57aid 44460  frege57b 44487  frege57c 44508
[Frege1879] p. 51Proposition 58spsbc 3760
[Frege1879] p. 51Proposition 59frege59a 44465  frege59b 44492  frege59c 44510
[Frege1879] p. 52Proposition 60frege60a 44466  frege60b 44493  frege60c 44511
[Frege1879] p. 52Proposition 61frege61a 44467  frege61b 44494  frege61c 44512
[Frege1879] p. 52Proposition 62frege62a 44468  frege62b 44495  frege62c 44513
[Frege1879] p. 52Proposition 63frege63a 44469  frege63b 44496  frege63c 44514
[Frege1879] p. 53Proposition 64frege64a 44470  frege64b 44497  frege64c 44515
[Frege1879] p. 53Proposition 65frege65a 44471  frege65b 44498  frege65c 44516
[Frege1879] p. 54Proposition 66frege66a 44472  frege66b 44499  frege66c 44517
[Frege1879] p. 54Proposition 67frege67a 44473  frege67b 44500  frege67c 44518
[Frege1879] p. 54Proposition 68frege68a 44474  frege68b 44501  frege68c 44519
[Frege1879] p. 55Definition 69dffrege69 44520
[Frege1879] p. 58Proposition 70frege70 44521
[Frege1879] p. 59Proposition 71frege71 44522
[Frege1879] p. 59Proposition 72frege72 44523
[Frege1879] p. 59Proposition 73frege73 44524
[Frege1879] p. 60Definition 76dffrege76 44527
[Frege1879] p. 60Proposition 74frege74 44525
[Frege1879] p. 60Proposition 75frege75 44526
[Frege1879] p. 62Proposition 77frege77 44528  frege77d 44334
[Frege1879] p. 63Proposition 78frege78 44529
[Frege1879] p. 63Proposition 79frege79 44530
[Frege1879] p. 63Proposition 80frege80 44531
[Frege1879] p. 63Proposition 81frege81 44532  frege81d 44335
[Frege1879] p. 64Proposition 82frege82 44533
[Frege1879] p. 65Proposition 83frege83 44534  frege83d 44336
[Frege1879] p. 65Proposition 84frege84 44535
[Frege1879] p. 66Proposition 85frege85 44536
[Frege1879] p. 66Proposition 86frege86 44537
[Frege1879] p. 66Proposition 87frege87 44538  frege87d 44338
[Frege1879] p. 67Proposition 88frege88 44539
[Frege1879] p. 68Proposition 89frege89 44540
[Frege1879] p. 68Proposition 90frege90 44541
[Frege1879] p. 68Proposition 91frege91 44542  frege91d 44339
[Frege1879] p. 69Proposition 92frege92 44543
[Frege1879] p. 70Proposition 93frege93 44544
[Frege1879] p. 70Proposition 94frege94 44545
[Frege1879] p. 70Proposition 95frege95 44546
[Frege1879] p. 71Definition 99dffrege99 44550
[Frege1879] p. 71Proposition 96frege96 44547  frege96d 44337
[Frege1879] p. 71Proposition 97frege97 44548  frege97d 44340
[Frege1879] p. 71Proposition 98frege98 44549  frege98d 44341
[Frege1879] p. 72Proposition 100frege100 44551
[Frege1879] p. 72Proposition 101frege101 44552
[Frege1879] p. 72Proposition 102frege102 44553  frege102d 44342
[Frege1879] p. 73Proposition 103frege103 44554
[Frege1879] p. 73Proposition 104frege104 44555
[Frege1879] p. 73Proposition 105frege105 44556
[Frege1879] p. 73Proposition 106frege106 44557  frege106d 44343
[Frege1879] p. 74Proposition 107frege107 44558
[Frege1879] p. 74Proposition 108frege108 44559  frege108d 44344
[Frege1879] p. 74Proposition 109frege109 44560  frege109d 44345
[Frege1879] p. 75Proposition 110frege110 44561
[Frege1879] p. 75Proposition 111frege111 44562  frege111d 44347
[Frege1879] p. 76Proposition 112frege112 44563
[Frege1879] p. 76Proposition 113frege113 44564
[Frege1879] p. 76Proposition 114frege114 44565  frege114d 44346
[Frege1879] p. 77Definition 115dffrege115 44566
[Frege1879] p. 77Proposition 116frege116 44567
[Frege1879] p. 78Proposition 117frege117 44568
[Frege1879] p. 78Proposition 118frege118 44569
[Frege1879] p. 78Proposition 119frege119 44570
[Frege1879] p. 78Proposition 120frege120 44571
[Frege1879] p. 79Proposition 121frege121 44572
[Frege1879] p. 79Proposition 122frege122 44573  frege122d 44348
[Frege1879] p. 79Proposition 123frege123 44574
[Frege1879] p. 80Proposition 124frege124 44575  frege124d 44349
[Frege1879] p. 81Proposition 125frege125 44576
[Frege1879] p. 81Proposition 126frege126 44577  frege126d 44350
[Frege1879] p. 82Proposition 127frege127 44578
[Frege1879] p. 83Proposition 128frege128 44579
[Frege1879] p. 83Proposition 129frege129 44580  frege129d 44351
[Frege1879] p. 84Proposition 130frege130 44581
[Frege1879] p. 85Proposition 131frege131 44582  frege131d 44352
[Frege1879] p. 86Proposition 132frege132 44583
[Frege1879] p. 86Proposition 133frege133 44584  frege133d 44353
[Fremlin1] p. 13Definition 111G (b)df-salgen 46885
[Fremlin1] p. 13Definition 111G (d)borelmbl 47208
[Fremlin1] p. 13Proposition 111G (b)salgenss 46908
[Fremlin1] p. 14Definition 112Aismea 47023
[Fremlin1] p. 15Remark 112B (d)psmeasure 47043
[Fremlin1] p. 15Property 112C (a)meadjun 47034  meadjunre 47048
[Fremlin1] p. 15Property 112C (b)meassle 47035
[Fremlin1] p. 15Property 112C (c)meaunle 47036
[Fremlin1] p. 16Property 112C (d)iundjiun 47032  meaiunle 47041  meaiunlelem 47040
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47053  meaiuninc2 47054  meaiuninc3 47057  meaiuninc3v 47056  meaiunincf 47055  meaiuninclem 47052
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47059  meaiininc2 47060  meaiininclem 47058
[Fremlin1] p. 19Theorem 113Ccaragen0 47078  caragendifcl 47086  caratheodory 47100  omelesplit 47090
[Fremlin1] p. 19Definition 113Aisome 47066  isomennd 47103  isomenndlem 47102
[Fremlin1] p. 19Remark 113B (c)omeunle 47088
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47107  voncmpl 47193
[Fremlin1] p. 19Definition 113A (ii)omessle 47070
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47095  carageniuncllem1 47093  carageniuncllem2 47094  caragenuncl 47085  caragenuncllem 47084  caragenunicl 47096
[Fremlin1] p. 21Remark 113Dcaragenel2d 47104
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47098  caratheodorylem2 47099
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47107
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47166  hoidmv1lelem1 47163  hoidmv1lelem2 47164  hoidmv1lelem3 47165
[Fremlin1] p. 25Definition 114Eisvonmbl 47210
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47166  hoidmvle 47172  hoidmvlelem1 47167  hoidmvlelem2 47168  hoidmvlelem3 47169  hoidmvlelem4 47170  hoidmvlelem5 47171  hsphoidmvle2 47157  hsphoif 47148  hsphoival 47151
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47120
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47128
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47155  hoidmvn0val 47156  hoidmvval 47149  hoidmvval0 47159  hoidmvval0b 47162
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47160  hsphoidmvle 47158
[Fremlin1] p. 30Definition 115Cdf-ovoln 47109  df-voln 47111
[Fremlin1] p. 30Proposition 115D (a)dmovn 47176  ovn0 47138  ovn0lem 47137  ovnf 47135  ovnome 47145  ovnssle 47133  ovnsslelem 47132  ovnsupge0 47129
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47175  ovnhoilem1 47173  ovnhoilem2 47174  vonhoi 47239
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47192  hoidifhspf 47190  hoidifhspval 47180  hoidifhspval2 47187  hoidifhspval3 47191  hspmbl 47201  hspmbllem1 47198  hspmbllem2 47199  hspmbllem3 47200
[Fremlin1] p. 31Definition 115Evoncmpl 47193  vonmea 47146
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47144  ovnsubadd2 47218  ovnsubadd2lem 47217  ovnsubaddlem1 47142  ovnsubaddlem2 47143
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47203  hoimbl2 47237  hoimbllem 47202  hspdifhsp 47188  opnvonmbl 47206  opnvonmbllem2 47205
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47208
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47251  iccvonmbllem 47250  ioovonmbl 47249
[Fremlin1] p. 32Proposition 115G (d)vonicc 47257  vonicclem2 47256  vonioo 47254  vonioolem2 47253  vonn0icc 47260  vonn0icc2 47264  vonn0ioo 47259  vonn0ioo2 47262
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47261  snvonmbl 47258  vonct 47265  vonsn 47263
[Fremlin1] p. 35Lemma 121Asubsalsal 46931
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46930  subsaliuncllem 46929
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47297  salpreimalegt 47281  salpreimaltle 47298
[Fremlin1] p. 35Proposition 121B (i)issmf 47300  issmff 47306  issmflem 47299
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47317  issmflelem 47316  smfpreimale 47326
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47328  issmfgtlem 47327
[Fremlin1] p. 36Definition 121Cdf-smblfn 47268  issmf 47300  issmff 47306  issmfge 47342  issmfgelem 47341  issmfgt 47328  issmfgtlem 47327  issmfle 47317  issmflelem 47316  issmflem 47299
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47279  salpreimagtlt 47302  salpreimalelt 47301
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47342  issmfgelem 47341
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47325
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47323  cnfsmf 47312
[Fremlin1] p. 36Proposition 121D (c)decsmf 47339  decsmflem 47338  incsmf 47314  incsmflem 47313
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47273  pimconstlt1 47274  smfconst 47321
[Fremlin1] p. 37Proposition 121E (b)smfadd 47337  smfaddlem1 47335  smfaddlem2 47336
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47368
[Fremlin1] p. 37Proposition 121E (d)smfmul 47367  smfmullem1 47363  smfmullem2 47364  smfmullem3 47365  smfmullem4 47366
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47369
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47372  smfpimbor1lem2 47371
[Fremlin1] p. 37Proposition 121E (g)smfco 47374
[Fremlin1] p. 37Proposition 121E (h)smfres 47362
[Fremlin1] p. 38Proposition 121E (e)smfrec 47361
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47370  smfresal 47360
[Fremlin1] p. 38Proposition 121F (a)smflim 47349  smflim2 47378  smflimlem1 47343  smflimlem2 47344  smflimlem3 47345  smflimlem4 47346  smflimlem5 47347  smflimlem6 47348  smflimmpt 47382
[Fremlin1] p. 38Proposition 121F (b)smfsup 47386  smfsuplem1 47383  smfsuplem2 47384  smfsuplem3 47385  smfsupmpt 47387  smfsupxr 47388
[Fremlin1] p. 38Proposition 121F (c)smfinf 47390  smfinflem 47389  smfinfmpt 47391
[Fremlin1] p. 39Remark 121Gsmflim 47349  smflim2 47378  smflimmpt 47382
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47380
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47410  smfdivdmmbl2 47413  smfinfdmmbl 47421  smfinfdmmbllem 47420  smfsupdmmbl 47417  smfsupdmmbllem 47416
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47400  smflimsuplem2 47393  smflimsuplem6 47397  smflimsuplem7 47398  smflimsuplem8 47399  smflimsupmpt 47401
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47403  smfliminflem 47402  smfliminfmpt 47404
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47268
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47414  fsupdm2 47415
[Fremlin1], p. 39Proposition 121Hadddmmbl 47405  adddmmbl2 47406  finfdm 47418  finfdm2 47419  fsupdm 47414  fsupdm2 47415  muldmmbl 47407  muldmmbl2 47408
[Fremlin1], p. 39Proposition 121F (c)finfdm 47418  finfdm2 47419
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25656
[Fremlin5] p. 213Lemma 565Cauniioovol 25699
[Fremlin5] p. 214Lemma 565Cauniioombl 25709
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38209
[Fremlin5] p. 220Theorem 565Maftc1anc 38212
[FreydScedrov] p. 283Axiom of Infinityax-inf 9595  inf1 9579  inf2 9580
[Gleason] p. 117Proposition 9-2.1df-enq 10884  enqer 10894
[Gleason] p. 117Proposition 9-2.2df-1nq 10889  df-nq 10885
[Gleason] p. 117Proposition 9-2.3df-plpq 10881  df-plq 10887
[Gleason] p. 119Proposition 9-2.4caovmo 7637  df-mpq 10882  df-mq 10888
[Gleason] p. 119Proposition 9-2.5df-rq 10890
[Gleason] p. 119Proposition 9-2.6ltexnq 10948
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10949  ltbtwnnq 10951
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10944
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10945
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10952
[Gleason] p. 121Definition 9-3.1df-np 10954
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10966
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10968
[Gleason] p. 122Definitiondf-1p 10955
[Gleason] p. 122Remark (1)prub 10967
[Gleason] p. 122Lemma 9-3.4prlem934 11006
[Gleason] p. 122Proposition 9-3.2df-ltp 10958
[Gleason] p. 122Proposition 9-3.3ltsopr 11005  psslinpr 11004  supexpr 11027  suplem1pr 11025  suplem2pr 11026
[Gleason] p. 123Proposition 9-3.5addclpr 10991  addclprlem1 10989  addclprlem2 10990  df-plp 10956
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10995
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10994
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11007
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11016  ltexprlem1 11009  ltexprlem2 11010  ltexprlem3 11011  ltexprlem4 11012  ltexprlem5 11013  ltexprlem6 11014  ltexprlem7 11015
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11018  ltaprlem 11017
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11019
[Gleason] p. 124Lemma 9-3.6prlem936 11020
[Gleason] p. 124Proposition 9-3.7df-mp 10957  mulclpr 10993  mulclprlem 10992  reclem2pr 11021
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11002
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10997
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10996
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11001
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11024  reclem3pr 11022  reclem4pr 11023
[Gleason] p. 126Proposition 9-4.1df-enr 11028  enrer 11036
[Gleason] p. 126Proposition 9-4.2df-0r 11033  df-1r 11034  df-nr 11029
[Gleason] p. 126Proposition 9-4.3df-mr 11031  df-plr 11030  negexsr 11075  recexsr 11080  recexsrlem 11076
[Gleason] p. 127Proposition 9-4.4df-ltr 11032
[Gleason] p. 130Proposition 10-1.3creui 12204  creur 12203  cru 12201
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11161  axcnre 11137
[Gleason] p. 132Definition 10-3.1crim 15156  crimd 15273  crimi 15234  crre 15155  crred 15272  crrei 15233
[Gleason] p. 132Definition 10-3.2remim 15158  remimd 15239
[Gleason] p. 133Definition 10.36absval2 15325  absval2d 15489  absval2i 15439
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15182  cjaddd 15261  cjaddi 15229
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15183  cjmuld 15262  cjmuli 15230
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15181  cjcjd 15240  cjcji 15212
[Gleason] p. 133Proposition 10-3.4(f)cjre 15180  cjreb 15164  cjrebd 15243  cjrebi 15215  cjred 15267  rere 15163  rereb 15161  rerebd 15242  rerebi 15214  rered 15265
[Gleason] p. 133Proposition 10-3.4(h)addcj 15189  addcjd 15253  addcji 15224
[Gleason] p. 133Proposition 10-3.7(a)absval 15279
[Gleason] p. 133Proposition 10-3.7(b)abscj 15320  abscjd 15494  abscji 15443
[Gleason] p. 133Proposition 10-3.7(c)abs00 15330  abs00d 15490  abs00i 15440  absne0d 15491
[Gleason] p. 133Proposition 10-3.7(d)releabs 15363  releabsd 15495  releabsi 15444
[Gleason] p. 133Proposition 10-3.7(f)absmul 15335  absmuld 15498  absmuli 15446
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15323  sqabsaddi 15447
[Gleason] p. 133Proposition 10-3.7(h)abstri 15372  abstrid 15500  abstrii 15450
[Gleason] p. 134Definition 10-4.1df-exp 14089  exp0 14092  expp1 14095  expp1d 14174
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26802  cxpaddd 26840  expadd 14131  expaddd 14175  expaddz 14133
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26811  cxpmuld 26860  expmul 14134  expmuld 14176  expmulz 14135
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26808  mulcxpd 26851  mulexp 14128  mulexpd 14188  mulexpz 14129
[Gleason] p. 140Exercise 1znnen 16258
[Gleason] p. 141Definition 11-2.1fzval 13528
[Gleason] p. 168Proposition 12-2.1(a)climadd 15673  rlimadd 15684  rlimdiv 15687
[Gleason] p. 168Proposition 12-2.1(b)climsub 15675  rlimsub 15685
[Gleason] p. 168Proposition 12-2.1(c)climmul 15674  rlimmul 15686
[Gleason] p. 171Corollary 12-2.2climmulc2 15678
[Gleason] p. 172Corollary 12-2.5climrecl 15624
[Gleason] p. 172Proposition 12-2.4(c)climabs 15645  climcj 15646  climim 15648  climre 15647  rlimabs 15650  rlimcj 15651  rlimim 15653  rlimre 15652
[Gleason] p. 173Definition 12-3.1df-ltxr 11236  df-xr 11235  ltxr 13131
[Gleason] p. 175Definition 12-4.1df-limsup 15512  limsupval 15515
[Gleason] p. 180Theorem 12-5.1climsup 15711
[Gleason] p. 180Theorem 12-5.3caucvg 15720  caucvgb 15721  caucvgbf 46061  caucvgr 15717  climcau 15712
[Gleason] p. 182Exercise 3cvgcmp 15858
[Gleason] p. 182Exercise 4cvgrat 15927
[Gleason] p. 195Theorem 13-2.12abs1m 15377
[Gleason] p. 217Lemma 13-4.1btwnzge0 13852
[Gleason] p. 223Definition 14-1.1df-met 21476
[Gleason] p. 223Definition 14-1.1(a)met0 24461  xmet0 24460
[Gleason] p. 223Definition 14-1.1(b)metgt0 24477
[Gleason] p. 223Definition 14-1.1(c)metsym 24468
[Gleason] p. 223Definition 14-1.1(d)mettri 24470  mstri 24587  xmettri 24469  xmstri 24586
[Gleason] p. 225Definition 14-1.5xpsmet 24500
[Gleason] p. 230Proposition 14-2.6txlm 23766
[Gleason] p. 240Theorem 14-4.3metcnp4 25430
[Gleason] p. 240Proposition 14-4.2metcnp3 24658
[Gleason] p. 243Proposition 14-4.16addcn 24984  addcn2 15635  mulcn 24986  mulcn2 15637  subcn 24985  subcn2 15636
[Gleason] p. 295Remarkbcval3 14333  bcval4 14334
[Gleason] p. 295Equation 2bcpasc 14348
[Gleason] p. 295Definition of binomial coefficientbcval 14331  df-bc 14330
[Gleason] p. 296Remarkbcn0 14337  bcnn 14339
[Gleason] p. 296Theorem 15-2.8binom 15874
[Gleason] p. 308Equation 2ef0 16135
[Gleason] p. 308Equation 3efcj 16136
[Gleason] p. 309Corollary 15-4.3efne0 16142
[Gleason] p. 309Corollary 15-4.4efexp 16147
[Gleason] p. 310Equation 14sinadd 16210
[Gleason] p. 310Equation 15cosadd 16211
[Gleason] p. 311Equation 17sincossq 16222
[Gleason] p. 311Equation 18cosbnd 16227  sinbnd 16226
[Gleason] p. 311Lemma 15-4.7sqeqor 14243  sqeqori 14241
[Gleason] p. 311Definition of ` `df-pi 16116
[Godowski] p. 730Equation SFgoeqi 32534
[GodowskiGreechie] p. 249Equation IV3oai 31929
[Golan] p. 1Remarksrgisid 20282
[Golan] p. 1Definitiondf-srg 20260
[Golan] p. 149Definitiondf-slmd 33434
[Gonshor] p. 7Definitiondf-cuts 27911
[Gonshor] p. 9Theorem 2.5lesrec 27950  lesrecd 27951
[Gonshor] p. 10Theorem 2.6cofcut1 28071  cofcut1d 28072
[Gonshor] p. 10Theorem 2.7cofcut2 28073  cofcut2d 28074
[Gonshor] p. 12Theorem 2.9cofcutr 28075  cofcutr1d 28076  cofcutr2d 28077
[Gonshor] p. 13Definitiondf-adds 28111
[Gonshor] p. 14Theorem 3.1addsprop 28127
[Gonshor] p. 15Theorem 3.2addsunif 28153
[Gonshor] p. 17Theorem 3.4mulsprop 28281
[Gonshor] p. 18Theorem 3.5mulsunif 28301
[Gonshor] p. 28Lemma 4.2halfcut 28609
[Gonshor] p. 28Theorem 4.2pw2cut 28611
[Gonshor] p. 30Theorem 4.2addhalfcut 28610
[Gonshor] p. 39Theorem 4.4(b)elreno2 28646
[Gonshor] p. 95Theorem 6.1addbday 28169
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36522
[Gratzer] p. 23Section 0.6df-mre 17628
[Gratzer] p. 27Section 0.6df-mri 17630
[Hall] p. 1Section 1.1df-asslaw 48808  df-cllaw 48806  df-comlaw 48807
[Hall] p. 2Section 1.2df-clintop 48820
[Hall] p. 7Section 1.3df-sgrp2 48841
[Halmos] p. 28Partition ` `df-parts 39379  dfmembpart2 39384
[Halmos] p. 31Theorem 17.3riesz1 32326  riesz2 32327
[Halmos] p. 41Definition of Hermitianhmopadj2 32202
[Halmos] p. 42Definition of projector orderingpjordi 32434
[Halmos] p. 43Theorem 26.1elpjhmop 32446  elpjidm 32445  pjnmopi 32409
[Halmos] p. 44Remarkpjinormi 31948  pjinormii 31937
[Halmos] p. 44Theorem 26.2elpjch 32450  pjrn 31968  pjrni 31963  pjvec 31957
[Halmos] p. 44Theorem 26.3pjnorm2 31988
[Halmos] p. 44Theorem 26.4hmopidmpj 32415  hmopidmpji 32413
[Halmos] p. 45Theorem 27.1pjinvari 32452
[Halmos] p. 45Theorem 27.3pjoci 32441  pjocvec 31958
[Halmos] p. 45Theorem 27.4pjorthcoi 32430
[Halmos] p. 48Theorem 29.2pjssposi 32433
[Halmos] p. 48Theorem 29.3pjssdif1i 32436  pjssdif2i 32435
[Halmos] p. 50Definition of spectrumdf-spec 32116
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 24
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1818
[Hatcher] p. 25Definitiondf-phtpc 25112  df-phtpy 25091
[Hatcher] p. 26Definitiondf-pco 25125  df-pi1 25128
[Hatcher] p. 26Proposition 1.2phtpcer 25115
[Hatcher] p. 26Proposition 1.3pi1grp 25170
[Hefferon] p. 240Definition 3.12df-dmat 22608  df-dmatalt 49029
[Helfgott] p. 2Theoremtgoldbach 48437
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48422
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48434  bgoldbtbnd 48429  bgoldbtbnd 48429  tgblthelfgott 48435
[Helfgott] p. 5Proposition 1.1circlevma 34946
[Helfgott] p. 69Statement 7.49circlemethhgt 34947
[Helfgott] p. 69Statement 7.50hgt750lema 34961  hgt750lemb 34960  hgt750leme 34962  hgt750lemf 34957  hgt750lemg 34958
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48431  tgoldbachgt 34967  tgoldbachgtALTV 48432  tgoldbachgtd 34966
[Helfgott] p. 70Statement 7.49ax-hgt749 34948
[Herstein] p. 54Exercise 28df-grpo 30754
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19001  grpoideu 30770  mndideu 18793
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19031  grpoinveu 30780
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19062  grpo2inv 30792
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19075  grpoinvop 30794
[Herstein] p. 57Exercise 1dfgrp3e 19097
[Hitchcock] p. 5Rule A3mptnan 1791
[Hitchcock] p. 5Rule A4mptxor 1792
[Hitchcock] p. 5Rule A5mtpxor 1794
[Holland] p. 1519Theorem 2sumdmdi 32681
[Holland] p. 1520Lemma 5cdj1i 32694  cdj3i 32702  cdj3lem1 32695  cdjreui 32693
[Holland] p. 1524Lemma 7mddmdin0i 32692
[Holland95] p. 13Theorem 3.6hlathil 42597
[Holland95] p. 14Line 15hgmapvs 42527
[Holland95] p. 14Line 16hdmaplkr 42549
[Holland95] p. 14Line 17hdmapellkr 42550
[Holland95] p. 14Line 19hdmapglnm2 42547
[Holland95] p. 14Line 20hdmapip0com 42553
[Holland95] p. 14Theorem 3.6hdmapevec2 42472
[Holland95] p. 14Lines 24 and 25hdmapoc 42567
[Holland95] p. 204Definition of involutiondf-srng 20912
[Holland95] p. 212Definition of subspacedf-psubsp 40139
[Holland95] p. 214Lemma 3.3lclkrlem2v 42164
[Holland95] p. 214Definition 3.2df-lpolN 42117
[Holland95] p. 214Definition of nonsingularpnonsingN 40569
[Holland95] p. 215Lemma 3.3(1)dihoml4 42013  poml4N 40589
[Holland95] p. 215Lemma 3.3(2)dochexmid 42104  pexmidALTN 40614  pexmidN 40605
[Holland95] p. 218Theorem 3.6lclkr 42169
[Holland95] p. 218Definition of dual vector spacedf-ldual 39760  ldualset 39761
[Holland95] p. 222Item 1df-lines 40137  df-pointsN 40138
[Holland95] p. 222Item 2df-polarityN 40539
[Holland95] p. 223Remarkispsubcl2N 40583  omllaw4 39882  pol1N 40546  polcon3N 40553
[Holland95] p. 223Definitiondf-psubclN 40571
[Holland95] p. 223Equation for polaritypolval2N 40542
[Holmes] p. 40Definitiondf-xrn 38891
[Hughes] p. 44Equation 1.21bax-his3 31345
[Hughes] p. 47Definition of projection operatordfpjop 32443
[Hughes] p. 49Equation 1.30eighmre 32224  eigre 32096  eigrei 32095
[Hughes] p. 49Equation 1.31eighmorth 32225  eigorth 32099  eigorthi 32098
[Hughes] p. 137Remark (ii)eigposi 32097
[Huneke] p. 1Claim 1frgrncvvdeq 30569
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30565
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30566
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30567
[Huneke] p. 2Claim 2frgrregorufr 30585  frgrregorufr0 30584  frgrregorufrg 30586
[Huneke] p. 2Claim 3frgrhash2wsp 30592  frrusgrord 30601  frrusgrord0 30600
[Huneke] p. 2Statementdf-clwwlknon 30348
[Huneke] p. 2Statement 4frgrwopreglem4 30575
[Huneke] p. 2Statement 5frgrwopreg1 30578  frgrwopreg2 30579  frgrwopregasn 30576  frgrwopregbsn 30577
[Huneke] p. 2Statement 6frgrwopreglem5 30581
[Huneke] p. 2Statement 7fusgreghash2wspv 30595
[Huneke] p. 2Statement 8fusgreghash2wsp 30598
[Huneke] p. 2Statement 9clwlksndivn 30346  numclwlk1 30631  numclwlk1lem1 30629  numclwlk1lem2 30630  numclwwlk1 30621  numclwwlk8 30652
[Huneke] p. 2Definition 3frgrwopreglem1 30572
[Huneke] p. 2Definition 4df-clwlks 30029
[Huneke] p. 2Definition 62clwwlk 30607
[Huneke] p. 2Definition 7numclwwlkovh 30633  numclwwlkovh0 30632
[Huneke] p. 2Statement 10numclwwlk2 30641
[Huneke] p. 2Statement 11rusgrnumwlkg 30238
[Huneke] p. 2Statement 12numclwwlk3 30645
[Huneke] p. 2Statement 13numclwwlk5 30648
[Huneke] p. 2Statement 14numclwwlk7 30651
[Indrzejczak] p. 33Definition ` `Enatded 30663  natded 30663
[Indrzejczak] p. 33Definition ` `Inatded 30663
[Indrzejczak] p. 34Definition ` `Enatded 30663  natded 30663
[Indrzejczak] p. 34Definition ` `Inatded 30663
[Jech] p. 4Definition of classcv 1562  cvjust 2759
[Jech] p. 42Lemma 6.1alephexp1 10552
[Jech] p. 42Equation 6.1alephadd 10550  alephmul 10551
[Jech] p. 43Lemma 6.2infmap 10549  infmap2 10188
[Jech] p. 71Lemma 9.3jech9.3 9774
[Jech] p. 72Equation 9.3scott0 9848  scottex 9847
[Jech] p. 72Exercise 9.1rankval4 9827  rankval4b 35408
[Jech] p. 72Scheme "Collection Principle"cp 9865
[Jech] p. 78Noteopthprc 5716
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43504
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43592
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43593
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43516
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43520
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43521  rmyp1 43522
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43523  rmym1 43524
[JonesMatijasevic] p. 695Equation 2.11rmx0 43514  rmx1 43515  rmxluc 43525
[JonesMatijasevic] p. 695Equation 2.12rmy0 43518  rmy1 43519  rmyluc 43526
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43528
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43529
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43549  jm2.17b 43550  jm2.17c 43551
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43582
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43586
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43577
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43552  jm2.24nn 43548
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43591
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43597  rmygeid 43553
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43609
[Juillerat] p. 11Section *5etransc 46855  etransclem47 46853  etransclem48 46854
[Juillerat] p. 12Equation (7)etransclem44 46850
[Juillerat] p. 12Equation *(7)etransclem46 46852
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46838
[Juillerat] p. 13Proofetransclem35 46841
[Juillerat] p. 13Part of case 2 proven inetransclem38 46844
[Juillerat] p. 13Part of case 2 provenetransclem24 46830
[Juillerat] p. 13Part of case 2: proven inetransclem41 46847
[Juillerat] p. 14Proofetransclem23 46829
[KalishMontague] p. 81Note 1ax-6 1990
[KalishMontague] p. 85Lemma 2equid 2035
[KalishMontague] p. 85Lemma 3equcomi 2040
[KalishMontague] p. 86Lemma 7cbvalivw 2030  cbvaliw 2029  wl-cbvmotv 38028  wl-motae 38030  wl-moteq 38029
[KalishMontague] p. 87Lemma 8spimvw 2009  spimw 1993
[KalishMontague] p. 87Lemma 9spfw 2056  spw 2057
[Kalmbach] p. 14Definition of latticechabs1 31777  chabs1i 31779  chabs2 31778  chabs2i 31780  chjass 31794  chjassi 31747  latabs1 18521  latabs2 18522
[Kalmbach] p. 15Definition of atomdf-at 32599  ela 32600
[Kalmbach] p. 15Definition of coverscvbr2 32544  cvrval2 39910
[Kalmbach] p. 16Definitiondf-ol 39814  df-oml 39815
[Kalmbach] p. 20Definition of commutescmbr 31845  cmbri 31851  cmtvalN 39847  df-cm 31844  df-cmtN 39813
[Kalmbach] p. 22Remarkomllaw5N 39883  pjoml5 31874  pjoml5i 31849
[Kalmbach] p. 22Definitionpjoml2 31872  pjoml2i 31846
[Kalmbach] p. 22Theorem 2(v)cmcm 31875  cmcmi 31853  cmcmii 31858  cmtcomN 39885
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39881  omlsi 31665  pjoml 31697  pjomli 31696
[Kalmbach] p. 22Definition of OML lawomllaw2N 39880
[Kalmbach] p. 23Remarkcmbr2i 31857  cmcm3 31876  cmcm3i 31855  cmcm3ii 31860  cmcm4i 31856  cmt3N 39887  cmt4N 39888  cmtbr2N 39889
[Kalmbach] p. 23Lemma 3cmbr3 31869  cmbr3i 31861  cmtbr3N 39890
[Kalmbach] p. 25Theorem 5fh1 31879  fh1i 31882  fh2 31880  fh2i 31883  omlfh1N 39894
[Kalmbach] p. 65Remarkchjatom 32618  chslej 31759  chsleji 31719  shslej 31641  shsleji 31631
[Kalmbach] p. 65Proposition 1chocin 31756  chocini 31715  chsupcl 31601  chsupval2 31671  h0elch 31516  helch 31504  hsupval2 31670  ocin 31557  ococss 31554  shococss 31555
[Kalmbach] p. 65Definition of subspace sumshsval 31573
[Kalmbach] p. 66Remarkdf-pjh 31656  pjssmi 32426  pjssmii 31942
[Kalmbach] p. 67Lemma 3osum 31906  osumi 31903
[Kalmbach] p. 67Lemma 4pjci 32461
[Kalmbach] p. 103Exercise 6atmd2 32661
[Kalmbach] p. 103Exercise 12mdsl0 32571
[Kalmbach] p. 140Remarkhatomic 32621  hatomici 32620  hatomistici 32623
[Kalmbach] p. 140Proposition 1atlatmstc 39955
[Kalmbach] p. 140Proposition 1(i)atexch 32642  lsatexch 39679
[Kalmbach] p. 140Proposition 1(ii)chcv1 32616  cvlcvr1 39975  cvr1 40046
[Kalmbach] p. 140Proposition 1(iii)cvexch 32635  cvexchi 32630  cvrexch 40056
[Kalmbach] p. 149Remark 2chrelati 32625  hlrelat 40038  hlrelat5N 40037  lrelat 39650
[Kalmbach] p. 153Exercise 5lsmcv 21234  lsmsatcv 39646  spansncv 31914  spansncvi 31913
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39665  spansncv2 32554
[Kalmbach] p. 266Definitiondf-st 32472
[Kalmbach2] p. 8Definition of adjointdf-adjh 32110
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10619  fpwwe2 10616
[KanamoriPincus] p. 416Corollary 1.3canth4 10620
[KanamoriPincus] p. 417Corollary 1.6canthp1 10627
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10622
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10624
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10637
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10641  gchxpidm 10642
[KanamoriPincus] p. 419Theorem 2.1gchacg 10653  gchhar 10652
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10186  unxpwdom 9539
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10643
[Kreyszig] p. 3Property M1metcl 24450  xmetcl 24449
[Kreyszig] p. 4Property M2meteq0 24457
[Kreyszig] p. 8Definition 1.1-8dscmet 24690
[Kreyszig] p. 12Equation 5conjmul 11923  muleqadd 11846
[Kreyszig] p. 18Definition 1.3-2mopnval 24556
[Kreyszig] p. 19Remarkmopntopon 24557
[Kreyszig] p. 19Theorem T1mopn0 24616  mopnm 24562
[Kreyszig] p. 19Theorem T2unimopn 24614
[Kreyszig] p. 19Definition of neighborhoodneibl 24619
[Kreyszig] p. 20Definition 1.3-3metcnp2 24660
[Kreyszig] p. 25Definition 1.4-1lmbr 23376  lmmbr 25378  lmmbr2 25379
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23498
[Kreyszig] p. 28Theorem 1.4-5lmcau 25433
[Kreyszig] p. 28Definition 1.4-3iscau 25396  iscmet2 25414
[Kreyszig] p. 30Theorem 1.4-7cmetss 25436
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23579  metelcls 25425
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25426  metcld2 25427
[Kreyszig] p. 51Equation 2clmvneg1 25219  lmodvneg1 20995  nvinv 30900  vcm 30837
[Kreyszig] p. 51Equation 1aclm0vs 25215  lmod0vs 20985  slmd0vs 33457  vc0 30835
[Kreyszig] p. 51Equation 1blmodvs0 20986  slmdvs0 33458  vcz 30836
[Kreyszig] p. 58Definition 2.2-1imsmet 30952  ngpmet 24721  nrmmetd 24692
[Kreyszig] p. 59Equation 1imsdval 30947  imsdval2 30948  ncvspds 25281  ngpds 24722
[Kreyszig] p. 63Problem 1nmval 24707  nvnd 30949
[Kreyszig] p. 64Problem 2nmeq0 24736  nmge0 24735  nvge0 30934  nvz 30930
[Kreyszig] p. 64Problem 3nmrtri 24742  nvabs 30933
[Kreyszig] p. 91Definition 2.7-1isblo3i 31062
[Kreyszig] p. 92Equation 2df-nmoo 31006
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31068  blocni 31066
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31067
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25324  ipeq0 21748  ipz 30980
[Kreyszig] p. 135Problem 2cphpyth 25336  pythi 31111
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31115
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25358
[Kreyszig] p. 144Equation 4supcvg 15900
[Kreyszig] p. 144Theorem 3.3-1minvec 25556  minveco 31145
[Kreyszig] p. 196Definition 3.9-1df-aj 31011
[Kreyszig] p. 247Theorem 4.7-2bcth 25449
[Kreyszig] p. 249Theorem 4.7-3ubth 31134
[Kreyszig] p. 470Definition of positive operator orderingleop 32384  leopg 32383
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32402
[Kreyszig] p. 525Theorem 10.1-1htth 31179
[Kulpa] p. 547Theorempoimir 38164
[Kulpa] p. 547Equation (1)poimirlem32 38163
[Kulpa] p. 547Equation (2)poimirlem31 38162
[Kulpa] p. 548Theorembroucube 38165
[Kulpa] p. 548Equation (6)poimirlem26 38157
[Kulpa] p. 548Equation (7)poimirlem27 38158
[Kunen] p. 10Axiom 0ax6e 2417  axnul 5260
[Kunen] p. 11Axiom 3axnul 5260
[Kunen] p. 12Axiom 6zfrep6 5244
[Kunen] p. 24Definition 10.24mapval 8823  mapvalg 8821
[Kunen] p. 30Lemma 10.20fodomg 10494
[Kunen] p. 31Definition 10.24mapex 7925
[Kunen] p. 95Definition 2.1df-r1 9724
[Kunen] p. 97Lemma 2.10r1elss 9766  r1elssi 9765
[Kunen] p. 107Exercise 4rankop 9818  rankopb 9812  rankuni 9823  rankxplim 9839  rankxpsuc 9842
[Kunen2] p. 47Lemma I.9.9relpfr 45528
[Kunen2] p. 53Lemma I.9.21trfr 45536
[Kunen2] p. 53Lemma I.9.24(2)wffr 45535
[Kunen2] p. 53Definition I.9.20tcfr 45537
[Kunen2] p. 95Lemma I.16.2ralabso 45542  rexabso 45543
[Kunen2] p. 96Example I.16.3disjabso 45549  n0abso 45550  ssabso 45548
[Kunen2] p. 111Lemma II.2.4(1)traxext 45551
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45561
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45556
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45559
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45560
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45555
[Kunen2] p. 112Corollary II.2.5wfaxext 45567  wfaxpr 45572  wfaxreg 45574  wfaxrep 45568  wfaxsep 45569  wfaxun 45573
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45558
[Kunen2] p. 113Corollary II.2.9wfaxpow 45571
[Kunen2] p. 114Theorem II.2.13wfaxext 45567
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45566  omelaxinf2 45563
[Kunen2] p. 114Corollary II.2.12wfac8prim 45576  wfaxinf2 45575
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45589  permaxext 45579  permaxinf2 45587  permaxnul 45582  permaxpow 45583  permaxpr 45584  permaxrep 45580  permaxsep 45581  permaxun 45585
[Kunen2] p. 148Definition II.9.1brpermmodel 45577
[Kunen2] p. 149Exercise II.9.3permac8prim 45588
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4965
[Lang] , p. 225Corollary 1.3finexttrb 33972
[Lang] p. Definitiondf-rn 5663
[Lang] p. 3Statementlidrideqd 18717  mndbn0 18798
[Lang] p. 3Definitiondf-mnd 18783
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18735
[Lang] p. 4Property of composites. Second formulagsumccat 18890
[Lang] p. 5Equationgsumreidx 19978
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48802
[Lang] p. 6Examplenn0mnd 48799
[Lang] p. 6Equationgsumxp2 20041
[Lang] p. 6Statementcycsubm 19264
[Lang] p. 6Definitionmulgnn0gsum 19137
[Lang] p. 6Observationmndlsmidm 19731
[Lang] p. 7Definitiondfgrp2e 19020
[Lang] p. 30Definitiondf-tocyc 33340
[Lang] p. 32Property (a)cyc3genpm 33385
[Lang] p. 32Property (b)cyc3conja 33390  cycpmconjv 33375
[Lang] p. 53Definitiondf-cat 17714
[Lang] p. 53Axiom CAT 1cat1 18144  cat1lem 18143
[Lang] p. 54Definitiondf-iso 17796
[Lang] p. 57Definitiondf-inito 18031  df-termo 18032
[Lang] p. 58Exampleirinitoringc 21589
[Lang] p. 58Statementinitoeu1 18058  termoeu1 18065
[Lang] p. 62Definitiondf-func 17905
[Lang] p. 65Definitiondf-nat 17993
[Lang] p. 91Notedf-ringc 20722
[Lang] p. 92Statementmxidlprm 33670
[Lang] p. 92Definitionisprmidlc 21434
[Lang] p. 128Remarkdsmmlmod 21855
[Lang] p. 129Prooflincscm 49061  lincscmcl 49063  lincsum 49060  lincsumcl 49062
[Lang] p. 129Statementlincolss 49065
[Lang] p. 129Observationdsmmfi 21848
[Lang] p. 141Theorem 5.3dimkerim 33934  qusdimsum 33935
[Lang] p. 141Corollary 5.4lssdimle 33915
[Lang] p. 147Definitionsnlindsntor 49102
[Lang] p. 504Statementmat1 22565  matring 22561
[Lang] p. 504Definitiondf-mamu 22509
[Lang] p. 505Statementmamuass 22520  mamutpos 22576  matassa 22562  mattposvs 22573  tposmap 22575
[Lang] p. 513Definitionmdet1 22719  mdetf 22713
[Lang] p. 513Theorem 4.4cramer 22809
[Lang] p. 514Proposition 4.6mdetleib 22705
[Lang] p. 514Proposition 4.8mdettpos 22729
[Lang] p. 515Definitiondf-minmar1 22753  smadiadetr 22793
[Lang] p. 515Corollary 4.9mdetero 22728  mdetralt 22726
[Lang] p. 517Proposition 4.15mdetmul 22741
[Lang] p. 518Definitiondf-madu 22752
[Lang] p. 518Proposition 4.16madulid 22763  madurid 22762  matinv 22795
[Lang] p. 561Theorem 3.1cayleyhamilton 23008
[Lang], p. 190Chapter 6vieta 33887
[Lang], p. 224Proposition 1.1extdgfialg 34001  finextalg 34005
[Lang], p. 224Proposition 1.2extdgmul 33970  fedgmul 33938
[Lang], p. 225Proposition 1.4algextdeg 34032
[Lang], p. 561Remarkchpmatply1 22950
[Lang], p. 561Definitiondf-chpmat 22945
[Lang2] p. 3Notationsdf-ind 12210
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44908
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44903
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44909
[LeBlanc] p. 277Rule R2axnul 5260
[Levy] p. 12Axiom 4.3.1df-clab 2744  wl-df.clab 38013
[Levy] p. 59Definitiondf-ttrcl 9665
[Levy] p. 64Theorem 5.6(ii)frinsg 9711
[Levy] p. 338Axiomdf-clel 2840  df-cleq 2757  wl-df.cleq 38014
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38017
[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 38017
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2840  df-cleq 2757  wl-df.cleq 38014
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2744  wl-df.clab 38013
[Levy] p. 358Axiomdf-clab 2744  wl-df.clab 38013
[Levy58] p. 2Definition Iisfin1-3 10358
[Levy58] p. 2Definition IIdf-fin2 10258
[Levy58] p. 2Definition Iadf-fin1a 10257
[Levy58] p. 2Definition IIIdf-fin3 10260
[Levy58] p. 3Definition Vdf-fin5 10261
[Levy58] p. 3Definition IVdf-fin4 10259
[Levy58] p. 4Definition VIdf-fin6 10262
[Levy58] p. 4Definition VIIdf-fin7 10263
[Levy58], p. 3Theorem 1fin1a2 10387
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27808
[Lipparini] p. 3Lemma 2.1.4noresle 27819
[Lipparini] p. 6Proposition 4.2noinfbnd1 27851  nosupbnd1 27836
[Lipparini] p. 6Proposition 4.3noinfbnd2 27853  nosupbnd2 27838
[Lipparini] p. 7Theorem 5.1noetasuplem3 27857  noetasuplem4 27858
[Lipparini] p. 7Corollary 4.4nosupinfsep 27854
[Lopez-Astorga] p. 12Rule 1mptnan 1791
[Lopez-Astorga] p. 12Rule 2mptxor 1792
[Lopez-Astorga] p. 12Rule 3mtpxor 1794
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32669
[Maeda] p. 168Lemma 5mdsym 32673  mdsymi 32672
[Maeda] p. 168Lemma 4(i)mdsymlem4 32667  mdsymlem6 32669  mdsymlem7 32670
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32671
[MaedaMaeda] p. 1Remarkssdmd1 32574  ssdmd2 32575  ssmd1 32572  ssmd2 32573
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32570
[MaedaMaeda] p. 1Definition 1.1df-dmd 32542  df-md 32541  mdbr 32555
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32592  mdslj1i 32580  mdslj2i 32581  mdslle1i 32578  mdslle2i 32579  mdslmd1i 32590  mdslmd2i 32591
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32582  mdsl2bi 32584  mdsl2i 32583
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32596
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32593
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32594
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32571
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32576  mdsl3 32577
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32595
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32690
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39957  hlrelat1 40036
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39675
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32597  cvmdi 32585  cvnbtwn4 32550  cvrnbtwn4 39915
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32598
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39976  cvp 32636  cvrp 40052  lcvp 39676
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32660
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32659
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39969  hlexch4N 40028
[MaedaMaeda] p. 34Exercise 7.1atabsi 32662
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40079
[MaedaMaeda] p. 61Definition 15.10psubN 40385  atpsubN 40389  df-pointsN 40138  pointpsubN 40387
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40140  pmap11 40398  pmaple 40397  pmapsub 40404  pmapval 40393
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40401  pmap1N 40403
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40406  pmapglb2N 40407  pmapglb2xN 40408  pmapglbx 40405
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40488
[MaedaMaeda] p. 67Postulate PS1ps-1 40113
[MaedaMaeda] p. 68Lemma 16.2df-padd 40432  paddclN 40478  paddidm 40477
[MaedaMaeda] p. 68Condition PS2ps-2 40114
[MaedaMaeda] p. 68Equation 16.2.1paddass 40474
[MaedaMaeda] p. 69Lemma 16.4ps-1 40113
[MaedaMaeda] p. 69Theorem 16.4ps-2 40114
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19736  lsmmod2 19737  lssats 39648  shatomici 32619  shatomistici 32622  shmodi 31651  shmodsi 31650
[MaedaMaeda] p. 130Remark 29.6dmdmd 32561  mdsymlem7 32670
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31850
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31754
[MaedaMaeda] p. 139Remarksumdmdii 32676
[Margaris] p. 40Rule Cexlimiv 1953
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 401  df-ex 1803  df-or 861  dfbi2 479
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 30660
[Margaris] p. 59Section 14notnotrALTVD 45488
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45489
[Margaris] p. 79Rule Cexinst01 45199  exinst11 45200
[Margaris] p. 89Theorem 19.219.2 1999  19.2g 2226  r19.2z 4456
[Margaris] p. 89Theorem 19.319.3 2240  rr19.3v 3629
[Margaris] p. 89Theorem 19.5alcom 2196
[Margaris] p. 89Theorem 19.6alex 1849
[Margaris] p. 89Theorem 19.7alnex 1804
[Margaris] p. 89Theorem 19.819.8a 2219
[Margaris] p. 89Theorem 19.919.9 2243  19.9h 2323  exlimd 2256  exlimdh 2327
[Margaris] p. 89Theorem 19.11excom 2199  excomim 2200
[Margaris] p. 89Theorem 19.1219.12 2362
[Margaris] p. 90Section 19conventions-labels 30661  conventions-labels 30661  conventions-labels 30661  conventions-labels 30661
[Margaris] p. 90Theorem 19.14exnal 1850
[Margaris] p. 90Theorem 19.152albi 44952  albi 1841
[Margaris] p. 90Theorem 19.1619.16 2263
[Margaris] p. 90Theorem 19.1719.17 2264
[Margaris] p. 90Theorem 19.182exbi 44954  exbi 1870
[Margaris] p. 90Theorem 19.1919.19 2267
[Margaris] p. 90Theorem 19.202alim 44951  2alimdv 1941  alimd 2250  alimdh 1840  alimdv 1939  ax-4 1832  ralimdaa 3266  ralimdv 3179  ralimdva 3177  ralimdvva 3212  sbcimdv 3815
[Margaris] p. 90Theorem 19.2119.21 2245  19.21h 2324  19.21t 2244  19.21vv 44950  alrimd 2253  alrimdd 2252  alrimdh 1886  alrimdv 1952  alrimi 2251  alrimih 1847  alrimiv 1950  alrimivv 1951  bj-alrimdh 37079  hbralrimi 3155  r19.21be 3258  r19.21bi 3257  ralrimd 3270  ralrimdv 3163  ralrimdva 3165  ralrimdvv 3209  ralrimdvva 3220  ralrimi 3263  ralrimia 3264  ralrimiv 3156  ralrimiva 3157  ralrimivv 3206  ralrimivva 3208  ralrimivvva 3211  ralrimivw 3161
[Margaris] p. 90Theorem 19.222exim 44953  2eximdv 1942  bj-exim 37094  exim 1857  eximd 2254  eximdh 1887  eximdv 1940  rexim 3106  reximd2a 3275  reximdai 3267  reximdd 45724  reximddv 3181  reximddv2 3224  reximddv3 3182  reximdv 3180  reximdv2 3175  reximdva 3178  reximdvai 3176  reximdvva 3213  reximi2 3098
[Margaris] p. 90Theorem 19.2319.23 2249  19.23bi 2229  19.23h 2325  19.23t 2248  exlimdv 1956  exlimdvv 1957  exlimexi 45098  exlimiv 1953  exlimivv 1955  rexlimd3 45720  rexlimdv 3164  rexlimdv3a 3170  rexlimdva 3166  rexlimdva2 3168  rexlimdvaa 3167  rexlimdvv 3221  rexlimdvva 3222  rexlimdvvva 3223  rexlimdvw 3171  rexlimiv 3159  rexlimiva 3158  rexlimivv 3207
[Margaris] p. 90Theorem 19.2419.24 2014
[Margaris] p. 90Theorem 19.2519.25 1903
[Margaris] p. 90Theorem 19.2619.26 1893
[Margaris] p. 90Theorem 19.2719.27 2265  r19.27z 4467  r19.27zv 4468
[Margaris] p. 90Theorem 19.2819.28 2266  19.28vv 44960  r19.28z 4459  r19.28zf 45735  r19.28zv 4463  rr19.28v 3630
[Margaris] p. 90Theorem 19.2919.29 1896  r19.29d2r 3152  r19.29imd 3130
[Margaris] p. 90Theorem 19.3019.30 1904
[Margaris] p. 90Theorem 19.3119.31 2272  19.31vv 44958
[Margaris] p. 90Theorem 19.3219.32 2271  r19.32 47690
[Margaris] p. 90Theorem 19.3319.33-2 44956  19.33 1907
[Margaris] p. 90Theorem 19.3419.34 2015
[Margaris] p. 90Theorem 19.3519.35 1900
[Margaris] p. 90Theorem 19.3619.36 2268  19.36vv 44957  r19.36zv 4469
[Margaris] p. 90Theorem 19.3719.37 2270  19.37vv 44959  r19.37zv 4464
[Margaris] p. 90Theorem 19.3819.38 1862
[Margaris] p. 90Theorem 19.3919.39 2013
[Margaris] p. 90Theorem 19.4019.40-2 1910  19.40 1909  r19.40 3131
[Margaris] p. 90Theorem 19.4119.41 2273  19.41rg 45124
[Margaris] p. 90Theorem 19.4219.42 2274
[Margaris] p. 90Theorem 19.4319.43 1905
[Margaris] p. 90Theorem 19.4419.44 2275  r19.44zv 4466
[Margaris] p. 90Theorem 19.4519.45 2276  r19.45zv 4465
[Margaris] p. 110Exercise 2(b)eu1 2640
[Mayet] p. 370Remarkjpi 32531  largei 32528  stri 32518
[Mayet3] p. 9Definition of CH-statesdf-hst 32473  ishst 32475
[Mayet3] p. 10Theoremhstrbi 32527  hstri 32526
[Mayet3] p. 1223Theorem 4.1mayete3i 31989
[Mayet3] p. 1240Theorem 7.1mayetes3i 31990
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32539
[MegPav2000] p. 2345Definition 3.4-1chintcl 31593  chsupcl 31601
[MegPav2000] p. 2345Definition 3.4-2hatomic 32621
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32615
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32642
[MegPav2000] p. 2366Figure 7pl42N 40619
[MegPav2002] p. 362Lemma 2.2latj31 18533  latj32 18531  latjass 18529
[Megill] p. 444Axiom C5ax-5 1933  ax5ALT 39543
[Megill] p. 444Section 7conventions 30660
[Megill] p. 445Lemma L12aecom-o 39537  ax-c11n 39524  axc11n 2460
[Megill] p. 446Lemma L17equtrr 2045
[Megill] p. 446Lemma L18ax6fromc10 39532
[Megill] p. 446Lemma L19hbnae-o 39564  hbnae 2466
[Megill] p. 447Remark 9.1dfsb1 2515  sbid 2293  sbidd-misc 50348  sbidd 50347
[Megill] p. 448Remark 9.6axc14 2497
[Megill] p. 448Scheme C4'ax-c4 39520
[Megill] p. 448Scheme C5'ax-c5 39519  sp 2221
[Megill] p. 448Scheme C6'ax-11 2194
[Megill] p. 448Scheme C7'ax-c7 39521
[Megill] p. 448Scheme C8'ax-7 2031
[Megill] p. 448Scheme C9'ax-c9 39526
[Megill] p. 448Scheme C10'ax-6 1990  ax-c10 39522
[Megill] p. 448Scheme C11'ax-c11 39523
[Megill] p. 448Scheme C12'ax-8 2147
[Megill] p. 448Scheme C13'ax-9 2155
[Megill] p. 448Scheme C14'ax-c14 39527
[Megill] p. 448Scheme C15'ax-c15 39525
[Megill] p. 448Scheme C16'ax-c16 39528
[Megill] p. 448Theorem 9.4dral1-o 39540  dral1 2473  dral2-o 39566  dral2 2472  drex1 2475  drex2 2476  drsb1 2529  drsb2 2304
[Megill] p. 449Theorem 9.7sbcom2 2209  sbequ 2119  sbid2v 2543
[Megill] p. 450Example in Appendixhba1-o 39533  hba1 2330
[Mendelson] p. 35Axiom A3hirstL-ax3 47484
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3835  rspsbca 3836  stdpc4 2101
[Mendelson] p. 69Axiom 5ax-c4 39520  ra4 3842  stdpc5 2246
[Mendelson] p. 81Rule Cexlimiv 1953
[Mendelson] p. 95Axiom 6stdpc6 2051
[Mendelson] p. 95Axiom 7stdpc7 2288
[Mendelson] p. 225Axiom system NBGru 3746
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5488
[Mendelson] p. 231Exercise 4.10(k)inv1 4355
[Mendelson] p. 231Exercise 4.10(l)unv 4356
[Mendelson] p. 231Exercise 4.10(n)dfin3 4232
[Mendelson] p. 231Exercise 4.10(o)df-nul 4289
[Mendelson] p. 231Exercise 4.10(q)dfin4 4233
[Mendelson] p. 231Exercise 4.10(s)ddif 4097
[Mendelson] p. 231Definition of uniondfun3 4231
[Mendelson] p. 235Exercise 4.12(c)univ 5423
[Mendelson] p. 235Exercise 4.12(d)pwv 4865
[Mendelson] p. 235Exercise 4.12(j)pwin 5543
[Mendelson] p. 235Exercise 4.12(k)pwunss 4576
[Mendelson] p. 235Exercise 4.12(l)pwssun 5544
[Mendelson] p. 235Exercise 4.12(n)uniin 4892
[Mendelson] p. 235Exercise 4.12(p)reli 5804
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6260
[Mendelson] p. 244Proposition 4.8(g)epweon 7762
[Mendelson] p. 246Definition of successordf-suc 6356
[Mendelson] p. 250Exercise 4.36oelim2 8569
[Mendelson] p. 254Proposition 4.22(b)xpen 9116
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9037  xpsneng 9038
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9044  xpcomeng 9045
[Mendelson] p. 254Proposition 4.22(e)xpassen 9047
[Mendelson] p. 255Definitionbrsdom 8959
[Mendelson] p. 255Exercise 4.39endisj 9040
[Mendelson] p. 255Exercise 4.41mapprc 8816
[Mendelson] p. 255Exercise 4.43mapsnen 9022  mapsnend 9021
[Mendelson] p. 255Exercise 4.45mapunen 9122
[Mendelson] p. 255Exercise 4.47xpmapen 9121
[Mendelson] p. 255Exercise 4.42(a)map0e 8868
[Mendelson] p. 255Exercise 4.42(b)map1 9025
[Mendelson] p. 257Proposition 4.24(a)undom 9041
[Mendelson] p. 258Exercise 4.56(c)djuassen 10150  djucomen 10149
[Mendelson] p. 258Exercise 4.56(f)djudom1 10154
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10148
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8504
[Mendelson] p. 266Proposition 4.34(f)oaordex 8531
[Mendelson] p. 275Proposition 4.42(d)entri3 10531
[Mendelson] p. 281Definitiondf-r1 9724
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9773
[Mendelson] p. 287Axiom system MKru 3746
[MertziosUnger] p. 152Definitiondf-frgr 30519
[MertziosUnger] p. 153Remark 1frgrconngr 30554
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30556  vdgn1frgrv3 30557
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30558
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30551
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30544  2pthfrgrrn 30542  2pthfrgrrn2 30543
[Mittelstaedt] p. 9Definitiondf-oc 31513
[Monk1] p. 22Remarkconventions 30660
[Monk1] p. 22Theorem 3.1conventions 30660
[Monk1] p. 26Theorem 2.8(vii)ssin 4193
[Monk1] p. 33Theorem 3.2(i)ssrel 5760  ssrelf 32872
[Monk1] p. 33Theorem 3.2(ii)eqrel 5761
[Monk1] p. 34Definition 3.3df-opab 5168
[Monk1] p. 36Theorem 3.7(i)coi1 6254  coi2 6255
[Monk1] p. 36Theorem 3.8(v)dm0 5901  rn0 5907
[Monk1] p. 36Theorem 3.7(ii)cnvi 5862
[Monk1] p. 37Theorem 3.13(i)relxp 5670
[Monk1] p. 37Theorem 3.13(x)dmxp 5910  rnxp 6160
[Monk1] p. 37Theorem 3.13(ii)0xp 5751  xp0 5752
[Monk1] p. 38Theorem 3.16(ii)ima0 6070
[Monk1] p. 38Theorem 3.16(viii)imai 6067
[Monk1] p. 39Theorem 3.17imaex 7899  imaexg 7898
[Monk1] p. 39Theorem 3.16(xi)imassrn 6064
[Monk1] p. 41Theorem 4.3(i)fnopfv 7060  funfvop 7035
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6925
[Monk1] p. 42Theorem 4.4(iii)fvelima 6936
[Monk1] p. 43Theorem 4.6funun 6571
[Monk1] p. 43Theorem 4.8(iv)dff13 7242  dff13f 7243
[Monk1] p. 46Theorem 4.15(v)funex 7207  funrnex 7939
[Monk1] p. 50Definition 5.4fniunfv 7235
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6218
[Monk1] p. 52Theorem 5.11(viii)ssint 4925
[Monk1] p. 52Definition 5.13 (i)1stval2 7991  df-1st 7974
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7992  df-2nd 7975
[Monk1] p. 112Theorem 15.17(v)ranksn 9814  ranksnb 9787
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9815
[Monk1] p. 112Theorem 15.17(iii)rankun 9816  rankunb 9810
[Monk1] p. 113Theorem 15.18r1val3 9798
[Monk1] p. 113Definition 15.19df-r1 9724  r1val2 9797
[Monk1] p. 117Lemmazorn2 10478  zorn2g 10475
[Monk1] p. 133Theorem 18.11cardom 9960
[Monk1] p. 133Theorem 18.12canth3 10533
[Monk1] p. 133Theorem 18.14carduni 9955
[Monk2] p. 105Axiom C4ax-4 1832
[Monk2] p. 105Axiom C7ax-7 2031
[Monk2] p. 105Axiom C8ax-12 2215  ax-c15 39525  ax12v2 2217
[Monk2] p. 108Lemma 5ax-c4 39520
[Monk2] p. 109Lemma 12ax-11 2194
[Monk2] p. 109Lemma 15equvini 2489  equvinv 2052  eqvinop 5460
[Monk2] p. 113Axiom C5-1ax-5 1933  ax5ALT 39543
[Monk2] p. 113Axiom C5-2ax-10 2178
[Monk2] p. 113Axiom C5-3ax-11 2194
[Monk2] p. 114Lemma 21sp 2221
[Monk2] p. 114Lemma 22axc4 2356  hba1-o 39533  hba1 2330
[Monk2] p. 114Lemma 23nfia1 2190
[Monk2] p. 114Lemma 24nfa2 2212  nfra2 3366  nfra2w 3301
[Moore] p. 53Part Idf-mre 17628
[Munkres] p. 77Example 2distop 23113  indistop 23120  indistopon 23119
[Munkres] p. 77Example 3fctop 23122  fctop2 23123
[Munkres] p. 77Example 4cctop 23124
[Munkres] p. 78Definition of basisdf-bases 23064  isbasis3g 23067
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17486  tgval2 23074
[Munkres] p. 79Remarktgcl 23087
[Munkres] p. 80Lemma 2.1tgval3 23081
[Munkres] p. 80Lemma 2.2tgss2 23105  tgss3 23104
[Munkres] p. 81Lemma 2.3basgen 23106  basgen2 23107
[Munkres] p. 83Exercise 3topdifinf 37855  topdifinfeq 37856  topdifinffin 37854  topdifinfindis 37852
[Munkres] p. 89Definition of subspace topologyresttop 23278
[Munkres] p. 93Theorem 6.1(1)0cld 23156  topcld 23153
[Munkres] p. 93Theorem 6.1(2)iincld 23157
[Munkres] p. 93Theorem 6.1(3)uncld 23159
[Munkres] p. 94Definition of closureclsval 23155
[Munkres] p. 94Definition of interiorntrval 23154
[Munkres] p. 95Theorem 6.5(a)clsndisj 23193  elcls 23191
[Munkres] p. 95Theorem 6.5(b)elcls3 23201
[Munkres] p. 97Theorem 6.6clslp 23266  neindisj 23235
[Munkres] p. 97Corollary 6.7cldlp 23268
[Munkres] p. 97Definition of limit pointislp2 23263  lpval 23257
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23433
[Munkres] p. 102Definition of continuous functiondf-cn 23345  iscn 23353  iscn2 23356
[Munkres] p. 107Theorem 7.2(g)cncnp 23398  cncnp2 23399  cncnpi 23396  df-cnp 23346  iscnp 23355  iscnp2 23357
[Munkres] p. 127Theorem 10.1metcn 24661
[Munkres] p. 128Theorem 10.3metcn4 25431
[Nathanson] p. 123Remarkreprgt 34925  reprinfz1 34926  reprlt 34923
[Nathanson] p. 123Definitiondf-repr 34913
[Nathanson] p. 123Chapter 5.1circlemethnat 34945
[Nathanson] p. 123Propositionbreprexp 34937  breprexpnat 34938  itgexpif 34910
[NielsenChuang] p. 195Equation 4.73unierri 32365
[OeSilva] p. 2042Section 2ax-bgbltosilva 48430
[Pfenning] p. 17Definition XMnatded 30663
[Pfenning] p. 17Definition NNCnatded 30663  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 30663
[Pfenning] p. 18Rule"natded 30663
[Pfenning] p. 18Definition /\Inatded 30663
[Pfenning] p. 18Definition ` `Enatded 30663  natded 30663  natded 30663  natded 30663  natded 30663
[Pfenning] p. 18Definition ` `Inatded 30663  natded 30663  natded 30663  natded 30663  natded 30663
[Pfenning] p. 18Definition ` `ELnatded 30663
[Pfenning] p. 18Definition ` `ERnatded 30663
[Pfenning] p. 18Definition ` `Ea,unatded 30663
[Pfenning] p. 18Definition ` `IRnatded 30663
[Pfenning] p. 18Definition ` `Ianatded 30663
[Pfenning] p. 127Definition =Enatded 30663
[Pfenning] p. 127Definition =Inatded 30663
[Ponnusamy] p. 361Theorem 6.44cphip0l 25322  df-dip 30962  dip0l 30979  ip0l 21746
[Ponnusamy] p. 361Equation 6.45cphipval 25363  ipval 30964
[Ponnusamy] p. 362Equation I1dipcj 30975  ipcj 21744
[Ponnusamy] p. 362Equation I3cphdir 25325  dipdir 31103  ipdir 21749  ipdiri 31091
[Ponnusamy] p. 362Equation I4ipidsq 30971  nmsq 25314
[Ponnusamy] p. 362Equation 6.46ip0i 31086
[Ponnusamy] p. 362Equation 6.47ip1i 31088
[Ponnusamy] p. 362Equation 6.48ip2i 31089
[Ponnusamy] p. 363Equation I2cphass 25331  dipass 31106  ipass 21755  ipassi 31102
[Prugovecki] p. 186Definition of brabraval 32205  df-bra 32111
[Prugovecki] p. 376Equation 8.1df-kb 32112  kbval 32215
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32643
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40524
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32657  atcvat4i 32658  cvrat3 40078  cvrat4 40079  lsatcvat3 39688
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32543  cvrval 39905  df-cv 32540  df-lcv 39655  lspsncv0 21239
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40536
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40537
[Quine] p. 16Definition 2.1df-clab 2744  rabid 3438  rabidd 45731  wl-df.clab 38013
[Quine] p. 17Definition 2.1''dfsb7 2316
[Quine] p. 18Definition 2.7df-cleq 2757  wl-df.cleq 38014
[Quine] p. 19Definition 2.9conventions 30660  df-v 3459
[Quine] p. 34Theorem 5.1eqabb 2904
[Quine] p. 35Theorem 5.2abid1 2901  abid2f 2957
[Quine] p. 40Theorem 6.1sb5 2313
[Quine] p. 40Theorem 6.2sb6 2121  sbalex 2280
[Quine] p. 41Theorem 6.3df-clel 2840  wl-df.clel 38017
[Quine] p. 41Theorem 6.4eqid 2765  eqid1 30727
[Quine] p. 41Theorem 6.5eqcom 2772
[Quine] p. 42Theorem 6.6df-sbc 3748
[Quine] p. 42Theorem 6.7dfsbcq 3749  dfsbcq2 3750
[Quine] p. 43Theorem 6.8vex 3461
[Quine] p. 43Theorem 6.9isset 3471
[Quine] p. 44Theorem 7.3spcgf 3553  spcgv 3558  spcimgf 3521
[Quine] p. 44Theorem 6.11spsbc 3760  spsbcd 3761
[Quine] p. 44Theorem 6.12elex 3478
[Quine] p. 44Theorem 6.13elab 3641  elabg 3638  elabgf 3636
[Quine] p. 44Theorem 6.14noel 4293
[Quine] p. 48Theorem 7.2snprc 4679
[Quine] p. 48Definition 7.1df-pr 4588  df-sn 4586
[Quine] p. 49Theorem 7.4snss 4746  snssg 4745
[Quine] p. 49Theorem 7.5prss 4781  prssg 4780
[Quine] p. 49Theorem 7.6prid1 4724  prid1g 4722  prid2 4725  prid2g 4723  snid 4624  snidg 4622
[Quine] p. 51Theorem 7.12snex 5401
[Quine] p. 51Theorem 7.13prex 5400
[Quine] p. 53Theorem 8.2unisn 4887  unisnALT 45499  unisng 4886
[Quine] p. 53Theorem 8.3uniun 4891
[Quine] p. 54Theorem 8.6elssuni 4900
[Quine] p. 54Theorem 8.7uni0 4897
[Quine] p. 56Theorem 8.17uniabio 6495
[Quine] p. 56Definition 8.18dfaiota2 47678  dfiota2 6482
[Quine] p. 57Theorem 8.19aiotaval 47687  iotaval 6499
[Quine] p. 57Theorem 8.22iotanul 6505
[Quine] p. 58Theorem 8.23iotaex 6501
[Quine] p. 58Definition 9.1df-op 4592
[Quine] p. 61Theorem 9.5opabid 5500  opabidw 5499  opelopab 5518  opelopaba 5511  opelopabaf 5520  opelopabf 5521  opelopabg 5514  opelopabga 5508  opelopabgf 5516  oprabid 7432  oprabidw 7431
[Quine] p. 64Definition 9.11df-xp 5658
[Quine] p. 64Definition 9.12df-cnv 5660
[Quine] p. 64Definition 9.15df-id 5547
[Quine] p. 65Theorem 10.3fun0 6590
[Quine] p. 65Theorem 10.4funi 6557
[Quine] p. 65Theorem 10.5funsn 6578  funsng 6576
[Quine] p. 65Definition 10.1df-fun 6527
[Quine] p. 65Definition 10.2args 6085  dffv4 6868
[Quine] p. 68Definition 10.11conventions 30660  df-fv 6533  fv2 6866
[Quine] p. 124Theorem 17.3nn0opth2 14299  nn0opth2i 14298  nn0opthi 14297  omopthi 8635
[Quine] p. 177Definition 25.2df-rdg 8385
[Quine] p. 232Equation icarddom 10526
[Quine] p. 284Axiom 39(vi)funimaex 6613  funimaexg 6612
[Quine] p. 331Axiom system NFru 3746
[ReedSimon] p. 36Definition (iii)ax-his3 31345
[ReedSimon] p. 63Exercise 4(a)df-dip 30962  polid 31420  polid2i 31418  polidi 31419
[ReedSimon] p. 63Exercise 4(b)df-ph 31074
[ReedSimon] p. 195Remarklnophm 32280  lnophmi 32279
[Retherford] p. 49Exercise 1(i)leopadd 32393
[Retherford] p. 49Exercise 1(ii)leopmul 32395  leopmuli 32394
[Retherford] p. 49Exercise 1(iv)leoptr 32398
[Retherford] p. 49Definition VI.1df-leop 32113  leoppos 32387
[Retherford] p. 49Exercise 1(iii)leoptri 32397
[Retherford] p. 49Definition of operator orderingleop3 32386
[Ribenboim] p. 181Remarknprmdvdsfacm1 48231
[Ribenboim], p. 181Statementppivalnn 48239
[Roman] p. 4Definitiondf-dmat 22608  df-dmatalt 49029
[Roman] p. 18Part Preliminariesdf-rng 20222
[Roman] p. 19Part Preliminariesdf-ring 20308
[Roman] p. 46Theorem 1.6isldepslvec2 49116
[Roman] p. 112Noteisldepslvec2 49116  ldepsnlinc 49139  zlmodzxznm 49128
[Roman] p. 112Examplezlmodzxzequa 49127  zlmodzxzequap 49130  zlmodzxzldep 49135
[Roman] p. 170Theorem 7.8cayleyhamilton 23008
[Rosenlicht] p. 80Theoremheicant 38166
[Rosser] p. 281Definitiondf-op 4592
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34949
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34950
[Rotman] p. 28Remarkpgrpgt2nabl 48997  pmtr3ncom 19536
[Rotman] p. 31Theorem 3.4symggen2 19532
[Rotman] p. 42Theorem 3.15cayley 19475  cayleyth 19476
[Rudin] p. 164Equation 27efcan 16140
[Rudin] p. 164Equation 30efzval 16148
[Rudin] p. 167Equation 48absefi 16242
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1794
[Sanford] p. 39Rule 4mptxor 1792
[Sanford] p. 40Rule 1mptnan 1791
[Schechter] p. 51Definition of antisymmetryintasym 6106
[Schechter] p. 51Definition of irreflexivityintirr 6109
[Schechter] p. 51Definition of symmetrycnvsym 6105
[Schechter] p. 51Definition of transitivitycotr 6103
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17628
[Schechter] p. 79Definition of Moore closuredf-mrc 17629
[Schechter] p. 82Section 4.5df-mrc 17629
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17631
[Schechter] p. 139Definition AC3dfac9 10108
[Schechter] p. 141Definition (MC)dfac11 43651
[Schechter] p. 149Axiom DC1ax-dc 10418  axdc3 10426
[Schechter] p. 187Definition of "ring with unit"isring 20310  isrngo 38408
[Schechter] p. 276Remark 11.6.espan0 31803
[Schechter] p. 276Definition of spandf-span 31570  spanval 31594
[Schechter] p. 428Definition 15.35bastop1 23111
[Schloeder] p. 1Lemma 1.3onelon 6375  onelord 43840  ordelon 6374  ordelord 6372
[Schloeder] p. 1Lemma 1.7onepsuc 43841  sucidg 6433
[Schloeder] p. 1Remark 1.50elon 6405  onsuc 7797  ord0 6404  ordsuci 7795
[Schloeder] p. 1Theorem 1.9epsoon 43842
[Schloeder] p. 1Definition 1.1dftr5 5216
[Schloeder] p. 1Definition 1.2dford3 43617  elon2 6361
[Schloeder] p. 1Definition 1.4df-suc 6356
[Schloeder] p. 1Definition 1.6epel 5555  epelg 5553
[Schloeder] p. 1Theorem 1.9(i)elirr 9550  epirron 43843  ordirr 6368
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43845  oneptr 43844  ontr1 6397
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6393  oneptri 43846  ordtri3or 6382
[Schloeder] p. 2Lemma 1.10ondif1 8474  ord0eln0 6406
[Schloeder] p. 2Lemma 1.13elsuci 6419  onsucss 43855  trsucss 6440
[Schloeder] p. 2Lemma 1.14ordsucss 7802
[Schloeder] p. 2Lemma 1.15onnbtwn 6446  ordnbtwn 6445
[Schloeder] p. 2Lemma 1.16orddif0suc 43857  ordnexbtwnsuc 43856
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10373  onsucf1lem 43858  onsucf1o 43861  onsucf1olem 43859  onsucrn 43860
[Schloeder] p. 2Lemma 1.18dflim7 43862
[Schloeder] p. 2Remark 1.12ordzsl 7829
[Schloeder] p. 2Theorem 1.10ondif1i 43851  ordne0gt0 43850
[Schloeder] p. 2Definition 1.11dflim6 43853  limnsuc 43854  onsucelab 43852
[Schloeder] p. 3Remark 1.21omex 9600
[Schloeder] p. 3Theorem 1.19tfinds 7844
[Schloeder] p. 3Theorem 1.22omelon 9603  ordom 7860
[Schloeder] p. 3Definition 1.20dfom3 9604
[Schloeder] p. 4Lemma 2.21onn 8614
[Schloeder] p. 4Lemma 2.7ssonuni 7767  ssorduni 7766
[Schloeder] p. 4Remark 2.4oa1suc 8504
[Schloeder] p. 4Theorem 1.23dfom5 9607  limom 7866
[Schloeder] p. 4Definition 2.1df-1o 8441  df1o2 8448
[Schloeder] p. 4Definition 2.3oa0 8489  oa0suclim 43864  oalim 8505  oasuc 8497
[Schloeder] p. 4Definition 2.5om0 8490  om0suclim 43865  omlim 8506  omsuc 8499
[Schloeder] p. 4Definition 2.6oe0 8495  oe0m1 8494  oe0suclim 43866  oelim 8507  oesuc 8500
[Schloeder] p. 5Lemma 2.10onsupuni 43818
[Schloeder] p. 5Lemma 2.11onsupsucismax 43868
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43869
[Schloeder] p. 5Lemma 2.13limexissup 43870  limexissupab 43872  limiun 43871  limuni 6412
[Schloeder] p. 5Lemma 2.14oa0r 8511
[Schloeder] p. 5Lemma 2.15om1 8515  om1om1r 43873  om1r 8516
[Schloeder] p. 5Remark 2.8oacl 8508  oaomoecl 43867  oecl 8510  omcl 8509
[Schloeder] p. 5Definition 2.9onsupintrab 43820
[Schloeder] p. 6Lemma 2.16oe1 8517
[Schloeder] p. 6Lemma 2.17oe1m 8518
[Schloeder] p. 6Lemma 2.18oe0rif 43874
[Schloeder] p. 6Theorem 2.19oasubex 43875
[Schloeder] p. 6Theorem 2.20nnacl 8585  nnamecl 43876  nnecl 8587  nnmcl 8586
[Schloeder] p. 7Lemma 3.1onsucwordi 43877
[Schloeder] p. 7Lemma 3.2oaword1 8525
[Schloeder] p. 7Lemma 3.3oaword2 8526
[Schloeder] p. 7Lemma 3.4oalimcl 8533
[Schloeder] p. 7Lemma 3.5oaltublim 43879
[Schloeder] p. 8Lemma 3.6oaordi3 43880
[Schloeder] p. 8Lemma 3.81oaomeqom 43882
[Schloeder] p. 8Lemma 3.10oa00 8532
[Schloeder] p. 8Lemma 3.11omge1 43886  omword1 8546
[Schloeder] p. 8Remark 3.9oaordnr 43885  oaordnrex 43884
[Schloeder] p. 8Theorem 3.7oaord3 43881
[Schloeder] p. 9Lemma 3.12omge2 43887  omword2 8547
[Schloeder] p. 9Lemma 3.13omlim2 43888
[Schloeder] p. 9Lemma 3.14omord2lim 43889
[Schloeder] p. 9Lemma 3.15omord2i 43890  omordi 8539
[Schloeder] p. 9Theorem 3.16omord 8541  omord2com 43891
[Schloeder] p. 10Lemma 3.172omomeqom 43892  df-2o 8442
[Schloeder] p. 10Lemma 3.19oege1 43895  oewordi 8565
[Schloeder] p. 10Lemma 3.20oege2 43896  oeworde 8567
[Schloeder] p. 10Lemma 3.21rp-oelim2 43897
[Schloeder] p. 10Lemma 3.22oeord2lim 43898
[Schloeder] p. 10Remark 3.18omnord1 43894  omnord1ex 43893
[Schloeder] p. 11Lemma 3.23oeord2i 43899
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43901
[Schloeder] p. 11Remark 3.26oenord1 43905  oenord1ex 43904
[Schloeder] p. 11Theorem 4.1oaomoencom 43906
[Schloeder] p. 11Theorem 4.2oaass 8534
[Schloeder] p. 11Theorem 3.24oeord2com 43900
[Schloeder] p. 12Theorem 4.3odi 8552
[Schloeder] p. 13Theorem 4.4omass 8553
[Schloeder] p. 14Remark 4.6oenass 43908
[Schloeder] p. 14Theorem 4.7oeoa 8571
[Schloeder] p. 15Lemma 5.1cantnftermord 43909
[Schloeder] p. 15Lemma 5.2cantnfub 43910  cantnfub2 43911
[Schloeder] p. 16Theorem 5.3cantnf2 43914
[Schwabhauser] p. 10Axiom A1axcgrrflx 29173  axtgcgrrflx 28689
[Schwabhauser] p. 10Axiom A2axcgrtr 29174
[Schwabhauser] p. 10Axiom A3axcgrid 29175  axtgcgrid 28690
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28675
[Schwabhauser] p. 11Axiom A4axsegcon 29186  axtgsegcon 28691  df-trkgcb 28677
[Schwabhauser] p. 11Axiom A5ax5seg 29197  axtg5seg 28692  df-trkgcb 28677
[Schwabhauser] p. 11Axiom A6axbtwnid 29198  axtgbtwnid 28693  df-trkgb 28676
[Schwabhauser] p. 12Axiom A7axpasch 29200  axtgpasch 28694  df-trkgb 28676
[Schwabhauser] p. 12Axiom A8axlowdim2 29219  df-trkg2d 34969
[Schwabhauser] p. 13Axiom A8axtglowdim2 28697
[Schwabhauser] p. 13Axiom A9axtgupdim2 28698  df-trkg2d 34969
[Schwabhauser] p. 13Axiom A10axeuclid 29222  axtgeucl 28699  df-trkge 28678
[Schwabhauser] p. 13Axiom A11axcont 29235  axtgcont 28696  axtgcont1 28695  df-trkgb 28676
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36350
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36352
[Schwabhauser] p. 27Theorem 2.3cgrtr 36355
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36359
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36360  tgcgrcomimp 28704  tgcgrcoml 28706  tgcgrcomr 28705
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36365  tgcgrtriv 28711
[Schwabhauser] p. 28Theorem 2.105segofs 36369  tg5segofs 34980
[Schwabhauser] p. 28Definition 2.10df-afs 34977  df-ofs 36346
[Schwabhauser] p. 29Theorem 2.11cgrextend 36371  tgcgrextend 28712
[Schwabhauser] p. 29Theorem 2.12segconeq 36373  tgsegconeq 28713
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36385  btwntriv2 36375  tgbtwntriv2 28714
[Schwabhauser] p. 30Theorem 3.2btwncomim 36376  tgbtwncom 28715
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36379  tgbtwntriv1 28718
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36380  tgbtwnswapid 28719
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36386  btwnintr 36382  tgbtwnexch2 28723  tgbtwnintr 28720
[Schwabhauser] p. 30Theorem 3.6btwnexch 36388  btwnexch3 36383  tgbtwnexch 28725  tgbtwnexch3 28721
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36387  tgbtwnouttr 28724  tgbtwnouttr2 28722
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29218
[Schwabhauser] p. 32Theorem 3.14btwndiff 36390  tgbtwndiff 28733
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28726  trisegint 36391
[Schwabhauser] p. 34Theorem 4.2ifscgr 36407  tgifscgr 28735
[Schwabhauser] p. 34Theorem 4.11colcom 28785  colrot1 28786  colrot2 28787  lncom 28849  lnrot1 28850  lnrot2 28851
[Schwabhauser] p. 34Definition 4.1df-ifs 36403
[Schwabhauser] p. 35Theorem 4.3cgrsub 36408  tgcgrsub 28736
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36418  tgcgrxfr 28745
[Schwabhauser] p. 35Statement 4.4ercgrg 28744
[Schwabhauser] p. 35Definition 4.4df-cgr3 36404  df-cgrg 28738
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28738
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36419  tgbtwnxfr 28757
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36425  colinearperm2 36427  colinearperm3 36426  colinearperm4 36428  colinearperm5 36429
[Schwabhauser] p. 36Definition 4.8df-ismt 28760
[Schwabhauser] p. 36Definition 4.10df-colinear 36402  tgellng 28780  tglng 28773
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36430
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36438  lnxfr 28793
[Schwabhauser] p. 37Theorem 4.14lineext 36439  lnext 28794
[Schwabhauser] p. 37Theorem 4.16fscgr 36443  tgfscgr 28795
[Schwabhauser] p. 37Theorem 4.17linecgr 36444  lncgr 28796
[Schwabhauser] p. 37Definition 4.15df-fs 36405
[Schwabhauser] p. 38Theorem 4.18lineid 36446  lnid 28797
[Schwabhauser] p. 38Theorem 4.19idinside 36447  tgidinside 28798
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36464  tgbtwnconn1 28802
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36465  tgbtwnconn2 28803
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36466  tgbtwnconn3 28804
[Schwabhauser] p. 41Theorem 5.5brsegle2 36472
[Schwabhauser] p. 41Definition 5.4df-segle 36470  legov 28812
[Schwabhauser] p. 41Definition 5.5legov2 28813
[Schwabhauser] p. 42Remark 5.13legso 28826
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36473
[Schwabhauser] p. 42Theorem 5.7seglerflx 36475
[Schwabhauser] p. 42Theorem 5.8segletr 36477
[Schwabhauser] p. 42Theorem 5.9segleantisym 36478
[Schwabhauser] p. 42Theorem 5.10seglelin 36479
[Schwabhauser] p. 42Theorem 5.11seglemin 36476
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36481
[Schwabhauser] p. 42Proposition 5.7legid 28814
[Schwabhauser] p. 42Proposition 5.8legtrd 28816
[Schwabhauser] p. 42Proposition 5.9legtri3 28817
[Schwabhauser] p. 42Proposition 5.10legtrid 28818
[Schwabhauser] p. 42Proposition 5.11leg0 28819
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36488
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36489
[Schwabhauser] p. 43Theorem 6.4broutsideof 36484  df-outsideof 36483
[Schwabhauser] p. 43Definition 6.1broutsideof2 36485  ishlg 28829
[Schwabhauser] p. 44Theorem 6.4hlln 28834
[Schwabhauser] p. 44Theorem 6.5hlid 28836  outsideofrflx 36490
[Schwabhauser] p. 44Theorem 6.6hlcomb 28830  hlcomd 28831  outsideofcom 36491
[Schwabhauser] p. 44Theorem 6.7hltr 28837  outsideoftr 36492
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28845  outsideofeu 36494
[Schwabhauser] p. 44Definition 6.8df-ray 36501
[Schwabhauser] p. 45Part 2df-lines2 36502
[Schwabhauser] p. 45Theorem 6.13outsidele 36495
[Schwabhauser] p. 45Theorem 6.15lineunray 36510
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36511  tglineelsb2 28859
[Schwabhauser] p. 45Theorem 6.17linecom 36513  linerflx1 36512  linerflx2 36514  tglinecom 28862  tglinerflx1 28860  tglinerflx2 28861
[Schwabhauser] p. 45Theorem 6.18linethru 36516  tglinethru 28863
[Schwabhauser] p. 45Definition 6.14df-line2 36500  tglng 28773
[Schwabhauser] p. 45Proposition 6.13legbtwn 28821
[Schwabhauser] p. 46Theorem 6.19linethrueu 36519  tglinethrueu 28866
[Schwabhauser] p. 46Theorem 6.21lineintmo 36520  tglineineq 28870  tglineinsn 28871  tglineinteq 28873  tglineintmo 28869
[Schwabhauser] p. 46Theorem 6.23colline 28877
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28878
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28879
[Schwabhauser] p. 49Theorem 7.3mirinv 28897
[Schwabhauser] p. 49Theorem 7.7mirmir 28893
[Schwabhauser] p. 49Theorem 7.8mirreu3 28885
[Schwabhauser] p. 49Definition 7.5df-mir 28884  ismir 28890  mirbtwn 28889  mircgr 28888  mirfv 28887  mirval 28886
[Schwabhauser] p. 50Theorem 7.8mirreu 28895
[Schwabhauser] p. 50Theorem 7.9mireq 28896
[Schwabhauser] p. 50Theorem 7.10mirinv 28897
[Schwabhauser] p. 50Theorem 7.11mirf1o 28900
[Schwabhauser] p. 50Theorem 7.13miriso 28901
[Schwabhauser] p. 51Theorem 7.14mirmot 28906
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28903  mirbtwni 28902
[Schwabhauser] p. 51Theorem 7.16mircgrs 28904
[Schwabhauser] p. 51Theorem 7.17miduniq 28916
[Schwabhauser] p. 52Lemma 7.21symquadlem 28920
[Schwabhauser] p. 52Theorem 7.18miduniq1 28917
[Schwabhauser] p. 52Theorem 7.19miduniq2 28918
[Schwabhauser] p. 52Theorem 7.20colmid 28919
[Schwabhauser] p. 53Lemma 7.22krippen 28922
[Schwabhauser] p. 55Lemma 7.25midexlem 28923
[Schwabhauser] p. 57Theorem 8.2ragcom 28929
[Schwabhauser] p. 57Definition 8.1df-rag 28925  israg 28928
[Schwabhauser] p. 58Theorem 8.3ragcol 28930
[Schwabhauser] p. 58Theorem 8.4ragmir 28931
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28933
[Schwabhauser] p. 58Theorem 8.6ragflat2 28934
[Schwabhauser] p. 58Theorem 8.7ragflat 28935
[Schwabhauser] p. 58Theorem 8.8ragtriva 28936
[Schwabhauser] p. 58Theorem 8.9ragflat3 28937  ragncol 28940
[Schwabhauser] p. 58Theorem 8.10ragcgr 28938
[Schwabhauser] p. 59Theorem 8.12perpcom 28944
[Schwabhauser] p. 59Theorem 8.13ragperp 28948
[Schwabhauser] p. 59Theorem 8.14perpneq 28945
[Schwabhauser] p. 59Definition 8.11df-perpg 28927  isperp 28943
[Schwabhauser] p. 59Definition 8.13isperp2 28946
[Schwabhauser] p. 60Theorem 8.18foot 28953
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28961  colperpexlem2 28962
[Schwabhauser] p. 63Theorem 8.21colperpex 28964  colperpexlem3 28963
[Schwabhauser] p. 64Theorem 8.22mideu 28969  midex 28968
[Schwabhauser] p. 66Lemma 8.24opphllem 28966
[Schwabhauser] p. 67Theorem 9.2oppcom 28975
[Schwabhauser] p. 67Definition 9.1islnopp 28970
[Schwabhauser] p. 68Lemma 9.3opphllem2 28979
[Schwabhauser] p. 68Lemma 9.4opphllem5 28982  opphllem6 28983
[Schwabhauser] p. 69Theorem 9.5opphl 28985
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28694
[Schwabhauser] p. 70Theorem 9.6outpasch 28986
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28994
[Schwabhauser] p. 71Definition 9.7df-hpg 28989  hpgbr 28991
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28996
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28995
[Schwabhauser] p. 72Theorem 9.11hpgid 28997
[Schwabhauser] p. 72Theorem 9.12hpgcom 28998
[Schwabhauser] p. 72Theorem 9.13hpgtr 28999
[Schwabhauser] p. 73Theorem 9.18colopp 29000
[Schwabhauser] p. 73Theorem 9.19colhp 29001
[Schwabhauser] p. 74Lemma 9.22lnincplng 29014
[Schwabhauser] p. 74Theorem 9.21plngcp 29016
[Schwabhauser] p. 74Theorem 9.24plngrot 29020
[Schwabhauser] p. 74Definition 9.20df-plng 29004  elplng 29010
[Schwabhauser] p. 75Theorem 9.25lnssplng 29022
[Schwabhauser] p. 76Theorem 9.26plng3p 29023
[Schwabhauser] p. 88Theorem 10.2lmieu 29036
[Schwabhauser] p. 88Definition 10.1df-mid 29026
[Schwabhauser] p. 89Theorem 10.4lmicom 29040
[Schwabhauser] p. 89Theorem 10.5lmilmi 29041
[Schwabhauser] p. 89Theorem 10.6lmireu 29042
[Schwabhauser] p. 89Theorem 10.7lmieq 29043
[Schwabhauser] p. 89Theorem 10.8lmiinv 29044
[Schwabhauser] p. 89Theorem 10.9lmif1o 29047
[Schwabhauser] p. 89Theorem 10.10lmiiso 29049
[Schwabhauser] p. 89Definition 10.3df-lmi 29027
[Schwabhauser] p. 90Theorem 10.11lmimot 29050
[Schwabhauser] p. 91Theorem 10.12hypcgr 29053
[Schwabhauser] p. 92Theorem 10.14lmiopp 29054
[Schwabhauser] p. 92Theorem 10.15lnperpex 29055
[Schwabhauser] p. 92Theorem 10.16trgcopy 29056  trgcopyeu 29058
[Schwabhauser] p. 95Definition 11.2dfcgra2 29082
[Schwabhauser] p. 95Definition 11.3iscgra 29061
[Schwabhauser] p. 95Proposition 11.4cgracgr 29070
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29068  cgrahl2 29069
[Schwabhauser] p. 96Theorem 11.6cgraid 29071
[Schwabhauser] p. 96Theorem 11.9cgraswap 29072
[Schwabhauser] p. 97Theorem 11.7cgracom 29074
[Schwabhauser] p. 97Theorem 11.8cgratr 29075
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29078  cgrahl 29079
[Schwabhauser] p. 98Theorem 11.13sacgr 29083
[Schwabhauser] p. 98Theorem 11.14oacgr 29084
[Schwabhauser] p. 98Theorem 11.15acopy 29085  acopyeu 29086
[Schwabhauser] p. 101Theorem 11.24inagswap 29093
[Schwabhauser] p. 101Theorem 11.25inaghl 29097
[Schwabhauser] p. 101Definition 11.23isinag 29090
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29105
[Schwabhauser] p. 102Definition 11.27df-leag 29098  isleag 29099
[Schwabhauser] p. 107Theorem 11.49tgsas 29107  tgsas1 29106  tgsas2 29108  tgsas3 29109
[Schwabhauser] p. 108Theorem 11.50tgasa 29111  tgasa1 29110
[Schwabhauser] p. 109Theorem 11.51tgsss1 29112  tgsss2 29113  tgsss3 29114
[Schwabhauser] p. 121Definition 12.2df-prlng 29122
[Schwabhauser] p. 122Theorem 12.4prlngref 29125
[Schwabhauser] p. 122Theorem 12.5prlngsym 29126
[Shapiro] p. 230Theorem 6.5.1dchrhash 27393  dchrsum 27391  dchrsum2 27390  sumdchr 27394
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27395  sum2dchr 27396
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20129  ablfacrp2 20130
[Shapiro], p. 328Equation 9.2.4vmasum 27338
[Shapiro], p. 329Equation 9.2.7logfac2 27339
[Shapiro], p. 329Equation 9.2.9logfacrlim 27346
[Shapiro], p. 331Equation 9.2.13vmadivsum 27604
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27607
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27661  vmalogdivsum2 27660
[Shapiro], p. 375Theorem 9.4.1dirith 27651  dirith2 27650
[Shapiro], p. 375Equation 9.4.3rplogsum 27649  rpvmasum 27648  rpvmasum2 27634
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27609
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27647
[Shapiro], p. 377Lemma 9.4.1dchrisum 27614  dchrisumlem1 27611  dchrisumlem2 27612  dchrisumlem3 27613  dchrisumlema 27610
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27617
[Shapiro], p. 379Equation 9.4.16dchrmusum 27646  dchrmusumlem 27644  dchrvmasumlem 27645
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27616
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27618
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27642  dchrisum0re 27635  dchrisumn0 27643
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27628
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27632
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27633
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27688  pntrsumbnd2 27689  pntrsumo1 27687
[Shapiro], p. 405Equation 10.2.1mudivsum 27652
[Shapiro], p. 406Equation 10.2.6mulogsum 27654
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27656
[Shapiro], p. 407Equation 10.2.8mulog2sum 27659
[Shapiro], p. 418Equation 10.4.6logsqvma 27664
[Shapiro], p. 418Equation 10.4.8logsqvma2 27665
[Shapiro], p. 419Equation 10.4.10selberg 27670
[Shapiro], p. 420Equation 10.4.12selberg2lem 27672
[Shapiro], p. 420Equation 10.4.14selberg2 27673
[Shapiro], p. 422Equation 10.6.7selberg3 27681
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27682
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27679  selberg3lem2 27680
[Shapiro], p. 422Equation 10.4.23selberg4 27683
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27677
[Shapiro], p. 428Equation 10.6.2selbergr 27690
[Shapiro], p. 429Equation 10.6.8selberg3r 27691
[Shapiro], p. 430Equation 10.6.11selberg4r 27692
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27706
[Shapiro], p. 434Equation 10.6.27pntlema 27718  pntlemb 27719  pntlemc 27717  pntlemd 27716  pntlemg 27720
[Shapiro], p. 435Equation 10.6.29pntlema 27718
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27710
[Shapiro], p. 436Lemma 10.6.2pntibnd 27715
[Shapiro], p. 436Equation 10.6.34pntlema 27718
[Shapiro], p. 436Equation 10.6.35pntlem3 27731  pntleml 27733
[Stewart] p. 91Lemma 7.3constrss 34050
[Stewart] p. 92Definition 7.4.df-constr 34037
[Stewart] p. 96Theorem 7.10constraddcl 34069  constrinvcl 34080  constrmulcl 34078  constrnegcl 34070  constrsqrtcl 34086
[Stewart] p. 97Theorem 7.11constrextdg2 34056
[Stewart] p. 98Theorem 7.12constrext2chn 34066
[Stewart] p. 99Theorem 7.132sqr3nconstr 34088
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34098
[Stoll] p. 13Definition corresponds to dfsymdif3 4261
[Stoll] p. 16Exercise 4.40dif 4362  dif0 4334
[Stoll] p. 16Exercise 4.8difdifdir 4448
[Stoll] p. 17Theorem 5.1(5)unvdif 4432
[Stoll] p. 19Theorem 5.2(13)undm 4252
[Stoll] p. 19Theorem 5.2(13')indm 4253
[Stoll] p. 20Remarkinvdif 4234
[Stoll] p. 25Definition of ordered tripledf-ot 4594
[Stoll] p. 43Definitionuniiun 5019
[Stoll] p. 44Definitionintiin 5020
[Stoll] p. 45Definitiondf-iin 4955
[Stoll] p. 45Definition indexed uniondf-iun 4954
[Stoll] p. 176Theorem 3.4(27)iman 406
[Stoll] p. 262Example 4.1dfsymdif3 4261
[Strang] p. 242Section 6.3expgrowth 44909
[Suppes] p. 22Theorem 2eq0 4305  eq0f 4302
[Suppes] p. 22Theorem 4eqss 3954  eqssd 3956  eqssi 3955
[Suppes] p. 23Theorem 5ss0 4359  ss0b 4358
[Suppes] p. 23Theorem 6sstr 3947  sstrALT2 45408
[Suppes] p. 23Theorem 7pssirr 4059
[Suppes] p. 23Theorem 8pssn2lp 4061
[Suppes] p. 23Theorem 9psstr 4064
[Suppes] p. 23Theorem 10pssss 4054
[Suppes] p. 25Theorem 12elin 3923  elun 4109
[Suppes] p. 26Theorem 15inidm 4181
[Suppes] p. 26Theorem 16in0 4352
[Suppes] p. 27Theorem 23unidm 4113
[Suppes] p. 27Theorem 24un0 4351
[Suppes] p. 27Theorem 25ssun1 4133
[Suppes] p. 27Theorem 26ssequn1 4141
[Suppes] p. 27Theorem 27unss 4145
[Suppes] p. 27Theorem 28indir 4241
[Suppes] p. 27Theorem 29undir 4242
[Suppes] p. 28Theorem 32difid 4332
[Suppes] p. 29Theorem 33difin 4227
[Suppes] p. 29Theorem 34indif 4235
[Suppes] p. 29Theorem 35undif1 4433
[Suppes] p. 29Theorem 36difun2 4438
[Suppes] p. 29Theorem 37difin0 4431
[Suppes] p. 29Theorem 38disjdif 4429
[Suppes] p. 29Theorem 39difundi 4245
[Suppes] p. 29Theorem 40difindi 4247
[Suppes] p. 30Theorem 41nalset 5269
[Suppes] p. 39Theorem 61uniss 4876
[Suppes] p. 39Theorem 65uniop 5489
[Suppes] p. 41Theorem 70intsn 4945
[Suppes] p. 42Theorem 71intpr 4943  intprg 4942
[Suppes] p. 42Theorem 73op1stb 5444
[Suppes] p. 42Theorem 78intun 4941
[Suppes] p. 44Definition 15(a)dfiun2 4992  dfiun2g 4990
[Suppes] p. 44Definition 15(b)dfiin2 4993
[Suppes] p. 47Theorem 86elpw 4562  elpw2 5295  elpw2g 5294  elpwg 4561  elpwgdedVD 45490
[Suppes] p. 47Theorem 87pwid 4581
[Suppes] p. 47Theorem 89pw0 4773
[Suppes] p. 48Theorem 90pwpw0 4774
[Suppes] p. 52Theorem 101xpss12 5667
[Suppes] p. 52Theorem 102xpindi 5810  xpindir 5811
[Suppes] p. 52Theorem 103xpundi 5721  xpundir 5722
[Suppes] p. 54Theorem 105elirrv 9547
[Suppes] p. 58Theorem 2relss 5759
[Suppes] p. 59Theorem 4eldm 5881  eldm2 5882  eldm2g 5880  eldmg 5879
[Suppes] p. 59Definition 3df-dm 5662
[Suppes] p. 60Theorem 6dmin 5892
[Suppes] p. 60Theorem 8rnun 6133
[Suppes] p. 60Theorem 9rnin 6134
[Suppes] p. 60Definition 4dfrn2 5869
[Suppes] p. 61Theorem 11brcnv 5859  brcnvg 5856
[Suppes] p. 62Equation 5elcnv 5853  elcnv2 5854
[Suppes] p. 62Theorem 12relcnv 6097
[Suppes] p. 62Theorem 15cnvin 6132
[Suppes] p. 62Theorem 16cnvun 6130
[Suppes] p. 63Definitiondftrrels2 39170
[Suppes] p. 63Theorem 20co02 6252
[Suppes] p. 63Theorem 21dmcoss 5956
[Suppes] p. 63Definition 7df-co 5661
[Suppes] p. 64Theorem 26cnvco 5866
[Suppes] p. 64Theorem 27coass 6257
[Suppes] p. 65Theorem 31resundi 5983
[Suppes] p. 65Theorem 34elima 6058  elima2 6059  elima3 6060  elimag 6057
[Suppes] p. 65Theorem 35imaundi 6138
[Suppes] p. 66Theorem 40dminss 6142
[Suppes] p. 66Theorem 41imainss 6143
[Suppes] p. 67Exercise 11cnvxp 6146
[Suppes] p. 81Definition 34dfec2 8685
[Suppes] p. 82Theorem 72elec 8729  elecALTV 38782  elecg 8727
[Suppes] p. 82Theorem 73eqvrelth 39206  erth 8737  erth2 8738
[Suppes] p. 83Theorem 74eqvreldisj 39209  erdisj 8740
[Suppes] p. 83Definition 35, df-parts 39379  dfmembpart2 39384
[Suppes] p. 89Theorem 96map0b 8869
[Suppes] p. 89Theorem 97map0 8873  map0g 8870
[Suppes] p. 89Theorem 98mapsn 8874  mapsnd 8872
[Suppes] p. 89Theorem 99mapss 8875
[Suppes] p. 91Definition 12(ii)alephsuc 10040
[Suppes] p. 91Definition 12(iii)alephlim 10039
[Suppes] p. 92Theorem 1enref 8970  enrefg 8969
[Suppes] p. 92Theorem 2ensym 8988  ensymb 8987  ensymi 8989
[Suppes] p. 92Theorem 3entr 8991
[Suppes] p. 92Theorem 4unen 9030
[Suppes] p. 94Theorem 15endom 8964
[Suppes] p. 94Theorem 16ssdomg 8985
[Suppes] p. 94Theorem 17domtr 8992
[Suppes] p. 95Theorem 18sbth 9073
[Suppes] p. 97Theorem 23canth2 9106  canth2g 9107
[Suppes] p. 97Definition 3brsdom2 9077  df-sdom 8934  dfsdom2 9076
[Suppes] p. 97Theorem 21(i)sdomirr 9090
[Suppes] p. 97Theorem 22(i)domnsym 9079
[Suppes] p. 97Theorem 21(ii)sdomnsym 9078
[Suppes] p. 97Theorem 22(ii)domsdomtr 9088
[Suppes] p. 97Theorem 22(iv)brdom2 8967
[Suppes] p. 97Theorem 21(iii)sdomtr 9091
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9086
[Suppes] p. 98Exercise 4fundmen 9016  fundmeng 9017
[Suppes] p. 98Exercise 6xpdom3 9051
[Suppes] p. 98Exercise 11sdomentr 9087
[Suppes] p. 104Theorem 37fofi 9261
[Suppes] p. 104Theorem 38pwfi 9266
[Suppes] p. 105Theorem 40pwfi 9266
[Suppes] p. 111Axiom for cardinal numberscarden 10523
[Suppes] p. 130Definition 3df-tr 5213
[Suppes] p. 132Theorem 9ssonuni 7767
[Suppes] p. 134Definition 6df-suc 6356
[Suppes] p. 136Theorem Schema 22findes 7885  finds 7881  finds1 7884  finds2 7883
[Suppes] p. 151Theorem 42isfinite 9609  isfinite2 9246  isfiniteg 9248  unbnn 9244
[Suppes] p. 162Definition 5df-ltnq 10891  df-ltpq 10883
[Suppes] p. 197Theorem Schema 4tfindes 7847  tfinds 7844  tfinds2 7848
[Suppes] p. 209Theorem 18oaord1 8524
[Suppes] p. 209Theorem 21oaword2 8526
[Suppes] p. 211Theorem 25oaass 8534
[Suppes] p. 225Definition 8iscard2 9950
[Suppes] p. 227Theorem 56ondomon 10535
[Suppes] p. 228Theorem 59harcard 9952
[Suppes] p. 228Definition 12(i)aleph0 10038
[Suppes] p. 228Theorem Schema 61onintss 6402
[Suppes] p. 228Theorem Schema 62onminesb 7780  onminsb 7781
[Suppes] p. 229Theorem 64alephval2 10545
[Suppes] p. 229Theorem 65alephcard 10042
[Suppes] p. 229Theorem 66alephord2i 10049
[Suppes] p. 229Theorem 67alephnbtwn 10043
[Suppes] p. 229Definition 12df-aleph 9914
[Suppes] p. 242Theorem 6weth 10467
[Suppes] p. 242Theorem 8entric 10529
[Suppes] p. 242Theorem 9carden 10523
[Szendrei] p. 11Line 6df-cloneop 36059
[Szendrei] p. 11Paragraph 3df-suppos 36063
[TakeutiZaring] p. 8Axiom 1ax-ext 2737
[TakeutiZaring] p. 13Definition 4.5df-cleq 2757  wl-df.cleq 38014
[TakeutiZaring] p. 13Proposition 4.6df-clel 2840  wl-df.clel 38017
[TakeutiZaring] p. 13Proposition 4.9cvjust 2759
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2785
[TakeutiZaring] p. 14Definition 4.16df-oprab 7404
[TakeutiZaring] p. 14Proposition 4.14ru 3746
[TakeutiZaring] p. 15Axiom 2zfpair 5383
[TakeutiZaring] p. 15Exercise 1elpr 4610  elpr2 4612  elpr2g 4611  elprg 4608
[TakeutiZaring] p. 15Exercise 2elsn 4600  elsn2 4627  elsn2g 4626  elsng 4599  velsn 4601
[TakeutiZaring] p. 15Exercise 3elop 5440
[TakeutiZaring] p. 15Exercise 4sneq 4595  sneqr 4801
[TakeutiZaring] p. 15Definition 5.1dfpr2 4606  dfsn2 4598  dfsn2ALT 4607
[TakeutiZaring] p. 16Axiom 3uniex 7728
[TakeutiZaring] p. 16Exercise 6opth 5449
[TakeutiZaring] p. 16Exercise 7opex 5436
[TakeutiZaring] p. 16Exercise 8rext 5420
[TakeutiZaring] p. 16Corollary 5.8unex 7731  unexg 7730
[TakeutiZaring] p. 16Definition 5.3dftp2 4653
[TakeutiZaring] p. 16Definition 5.5df-uni 4869
[TakeutiZaring] p. 16Definition 5.6df-in 3914  df-un 3912
[TakeutiZaring] p. 16Proposition 5.7unipr 4885  uniprg 4884
[TakeutiZaring] p. 17Axiom 4vpwex 5339
[TakeutiZaring] p. 17Exercise 1eltp 4651
[TakeutiZaring] p. 17Exercise 5elsuc 6422  elsucg 6420  sstr2 3946
[TakeutiZaring] p. 17Exercise 6uncom 4114
[TakeutiZaring] p. 17Exercise 7incom 4164
[TakeutiZaring] p. 17Exercise 8unass 4127
[TakeutiZaring] p. 17Exercise 9inass 4182
[TakeutiZaring] p. 17Exercise 10indi 4239
[TakeutiZaring] p. 17Exercise 11undi 4240
[TakeutiZaring] p. 17Definition 5.9df-pss 3927  df-ss 3924
[TakeutiZaring] p. 17Definition 5.10df-pw 4560
[TakeutiZaring] p. 18Exercise 7unss2 4142
[TakeutiZaring] p. 18Exercise 9dfss2 3925  sseqin2 4178
[TakeutiZaring] p. 18Exercise 10ssid 3961
[TakeutiZaring] p. 18Exercise 12inss1 4191  inss2 4192
[TakeutiZaring] p. 18Exercise 13nss 4003
[TakeutiZaring] p. 18Exercise 15unieq 4879
[TakeutiZaring] p. 18Exercise 18sspwb 5421  sspwimp 45491  sspwimpALT 45498  sspwimpALT2 45501  sspwimpcf 45493
[TakeutiZaring] p. 18Exercise 19pweqb 5428
[TakeutiZaring] p. 19Axiom 5ax-rep 5232
[TakeutiZaring] p. 20Definitiondf-rab 3418
[TakeutiZaring] p. 20Corollary 5.160ex 5262
[TakeutiZaring] p. 20Definition 5.12df-dif 3910
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37025  dfnul2 4291
[TakeutiZaring] p. 20Proposition 5.15difid 4332
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4308  n0f 4304  neq0 4307  neq0f 4303
[TakeutiZaring] p. 21Axiom 6zfreg 9546
[TakeutiZaring] p. 21Axiom 6'zfregs 9689
[TakeutiZaring] p. 21Theorem 5.22setind 9704
[TakeutiZaring] p. 21Definition 5.20df-v 3459
[TakeutiZaring] p. 21Proposition 5.21vprc 5275
[TakeutiZaring] p. 22Exercise 10ss 4357
[TakeutiZaring] p. 22Exercise 3ssex 5282  ssexg 5284
[TakeutiZaring] p. 22Exercise 4inex1 5278
[TakeutiZaring] p. 22Exercise 5ruv 9558
[TakeutiZaring] p. 22Exercise 6elirr 9550
[TakeutiZaring] p. 22Exercise 7ssdif0 4322
[TakeutiZaring] p. 22Exercise 11difdif 4091
[TakeutiZaring] p. 22Exercise 13undif3 4255  undif3VD 45455
[TakeutiZaring] p. 22Exercise 14difss 4092
[TakeutiZaring] p. 22Exercise 15sscon 4099
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3080
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3090
[TakeutiZaring] p. 23Proposition 6.2xpex 7740  xpexg 7737
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5659
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6596
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6775  fun11 6599
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6538  svrelfun 6597
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5868
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5870
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5664
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5665
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5661
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6184  dfrel2 6179
[TakeutiZaring] p. 25Exercise 3xpss 5668
[TakeutiZaring] p. 25Exercise 5relun 5789
[TakeutiZaring] p. 25Exercise 6reluni 5796
[TakeutiZaring] p. 25Exercise 9inxp 5809
[TakeutiZaring] p. 25Exercise 12relres 5995
[TakeutiZaring] p. 25Exercise 13opelres 5975  opelresi 5977
[TakeutiZaring] p. 25Exercise 14dmres 6002
[TakeutiZaring] p. 25Exercise 15resss 5991
[TakeutiZaring] p. 25Exercise 17resabs1 5996
[TakeutiZaring] p. 25Exercise 18funres 6567
[TakeutiZaring] p. 25Exercise 24relco 6101
[TakeutiZaring] p. 25Exercise 29funco 6565
[TakeutiZaring] p. 25Exercise 30f1co 6777
[TakeutiZaring] p. 26Definition 6.10eu2 2639
[TakeutiZaring] p. 26Definition 6.11conventions 30660  df-fv 6533  fv3 6889
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7910  cnvexg 7909
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7894  dmexg 7886
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7895  rnexg 7887
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45027
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7905
[TakeutiZaring] p. 27Corollary 6.13fvex 6884
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47766  tz6.12-1-afv2 47833  tz6.12-1 6894  tz6.12-afv 47765  tz6.12-afv2 47832  tz6.12 6895  tz6.12c-afv2 47834  tz6.12c 6893
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47829  tz6.12-2 6858  tz6.12i-afv2 47835  tz6.12i 6897
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6528
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6529
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6531  wfo 6523
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6530  wf1 6522
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6532  wf1o 6524
[TakeutiZaring] p. 28Exercise 4eqfnfv 7015  eqfnfv2 7016  eqfnfv2f 7019
[TakeutiZaring] p. 28Exercise 5fvco 6969
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7205
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7203
[TakeutiZaring] p. 29Exercise 9funimaex 6613  funimaexg 6612
[TakeutiZaring] p. 29Definition 6.18df-br 5106
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5561
[TakeutiZaring] p. 30Definition 6.21dffr2 5613  dffr3 6092  eliniseg 6087  iniseg 6090
[TakeutiZaring] p. 30Definition 6.22df-eprel 5552
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5629  fr3nr 7759  frirr 5628
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5605
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7761
[TakeutiZaring] p. 31Exercise 1frss 5616
[TakeutiZaring] p. 31Exercise 4wess 5638
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6338  tz6.26i 6339  wefrc 5646  wereu2 5649
[TakeutiZaring] p. 32Theorem 6.27wfi 6340  wfii 6341
[TakeutiZaring] p. 32Definition 6.28df-isom 6534
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7317
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7318
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7324
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7325
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7326
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7330
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7337
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7339
[TakeutiZaring] p. 35Notationwtr 5212
[TakeutiZaring] p. 35Theorem 7.2trelpss 45028  tz7.2 5635
[TakeutiZaring] p. 35Definition 7.1dftr3 5217
[TakeutiZaring] p. 36Proposition 7.4ordwe 6363
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6371
[TakeutiZaring] p. 36Proposition 7.6ordelord 6372  ordelordALT 45111  ordelordALTVD 45440
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6378  ordelssne 6377
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6376
[TakeutiZaring] p. 37Proposition 7.9ordin 6380
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7769
[TakeutiZaring] p. 38Corollary 7.15ordsson 7770
[TakeutiZaring] p. 38Definition 7.11df-on 6354
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6382
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45123  ordon 7764
[TakeutiZaring] p. 38Proposition 7.13onprc 7765
[TakeutiZaring] p. 39Theorem 7.17tfi 7837
[TakeutiZaring] p. 40Exercise 3ontr2 6398
[TakeutiZaring] p. 40Exercise 7dftr2 5214
[TakeutiZaring] p. 40Exercise 9onssmin 7779
[TakeutiZaring] p. 40Exercise 11unon 7815
[TakeutiZaring] p. 40Exercise 12ordun 6456
[TakeutiZaring] p. 40Exercise 14ordequn 6455
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7766
[TakeutiZaring] p. 40Proposition 7.20elssuni 4900
[TakeutiZaring] p. 41Definition 7.22df-suc 6356
[TakeutiZaring] p. 41Proposition 7.23sssucid 6432  sucidg 6433
[TakeutiZaring] p. 41Proposition 7.24onsuc 7797
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6446  ordnbtwn 6445
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7812
[TakeutiZaring] p. 42Exercise 1df-lim 6355
[TakeutiZaring] p. 42Exercise 4omssnlim 7865
[TakeutiZaring] p. 42Exercise 7ssnlim 7870
[TakeutiZaring] p. 42Exercise 8onsucssi 7825  ordelsuc 7804
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7806
[TakeutiZaring] p. 42Definition 7.27nlimon 7835
[TakeutiZaring] p. 42Definition 7.28dfom2 7852
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7873
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7874
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7875
[TakeutiZaring] p. 43Remarkomon 7862
[TakeutiZaring] p. 43Axiom 7inf3 9592  omex 9600
[TakeutiZaring] p. 43Theorem 7.32ordom 7860
[TakeutiZaring] p. 43Corollary 7.31find 7880
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7877
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7878
[TakeutiZaring] p. 44Exercise 1limomss 7855
[TakeutiZaring] p. 44Exercise 2int0 4923
[TakeutiZaring] p. 44Exercise 3trintss 5231
[TakeutiZaring] p. 44Exercise 4intss1 4924
[TakeutiZaring] p. 44Exercise 5intex 5305
[TakeutiZaring] p. 44Exercise 6oninton 7782
[TakeutiZaring] p. 44Exercise 11ordintdif 6401
[TakeutiZaring] p. 44Definition 7.35df-int 4909
[TakeutiZaring] p. 44Proposition 7.34noinfep 9617
[TakeutiZaring] p. 45Exercise 4onint 7777
[TakeutiZaring] p. 47Lemma 1tfrlem1 8350
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8372
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8373
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8374
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8381  tz7.44-2 8382  tz7.44-3 8383
[TakeutiZaring] p. 50Exercise 1smogt 8342
[TakeutiZaring] p. 50Exercise 3smoiso 8337
[TakeutiZaring] p. 50Definition 7.46df-smo 8321
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8420  tz7.49c 8421
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8418
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8417
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8419
[TakeutiZaring] p. 53Proposition 7.532eu5 2685
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9983
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9984
[TakeutiZaring] p. 56Definition 8.1oalim 8505  oasuc 8497
[TakeutiZaring] p. 57Remarktfindsg 7845
[TakeutiZaring] p. 57Proposition 8.2oacl 8508
[TakeutiZaring] p. 57Proposition 8.3oa0 8489  oa0r 8511
[TakeutiZaring] p. 57Proposition 8.16omcl 8509
[TakeutiZaring] p. 58Corollary 8.5oacan 8521
[TakeutiZaring] p. 58Proposition 8.4nnaord 8593  nnaordi 8592  oaord 8520  oaordi 8519
[TakeutiZaring] p. 59Proposition 8.6iunss2 5010  uniss2 4903
[TakeutiZaring] p. 59Proposition 8.7oawordri 8523
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8528  oawordex 8530
[TakeutiZaring] p. 59Proposition 8.9nnacl 8585
[TakeutiZaring] p. 59Proposition 8.10oaabs 8622
[TakeutiZaring] p. 60Remarkoancom 9608
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8533
[TakeutiZaring] p. 62Exercise 1nnarcl 8590
[TakeutiZaring] p. 62Exercise 5oaword1 8525
[TakeutiZaring] p. 62Definition 8.15om0x 8492  omlim 8506  omsuc 8499
[TakeutiZaring] p. 62Definition 8.15(a)om0 8490
[TakeutiZaring] p. 63Proposition 8.17nnecl 8587  nnmcl 8586
[TakeutiZaring] p. 63Proposition 8.19nnmord 8606  nnmordi 8605  omord 8541  omordi 8539
[TakeutiZaring] p. 63Proposition 8.20omcan 8542
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8610  omwordri 8545
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8512
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8515  om1r 8516
[TakeutiZaring] p. 64Proposition 8.22om00 8548
[TakeutiZaring] p. 64Proposition 8.23omordlim 8550
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8551
[TakeutiZaring] p. 64Proposition 8.25odi 8552
[TakeutiZaring] p. 65Theorem 8.26omass 8553
[TakeutiZaring] p. 67Definition 8.30nnesuc 8582  oe0 8495  oelim 8507  oesuc 8500  onesuc 8503
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8493
[TakeutiZaring] p. 67Proposition 8.32oen0 8560
[TakeutiZaring] p. 67Proposition 8.33oeordi 8561
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8494
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8518
[TakeutiZaring] p. 68Corollary 8.34oeord 8562
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8568
[TakeutiZaring] p. 68Proposition 8.35oewordri 8566
[TakeutiZaring] p. 68Proposition 8.37oeworde 8567
[TakeutiZaring] p. 69Proposition 8.41oeoa 8571
[TakeutiZaring] p. 70Proposition 8.42oeoe 8573
[TakeutiZaring] p. 73Theorem 9.1trcl 9685  tz9.1 9686
[TakeutiZaring] p. 76Definition 9.9df-r1 9724  r10 9728  r1lim 9732  r1limg 9731  r1suc 9730  r1sucg 9729
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9740  r1ord2 9741  r1ordg 9738
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9750
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9775  tz9.13 9751  tz9.13g 9752
[TakeutiZaring] p. 79Definition 9.14df-rank 9725  rankval 9776  rankvalb 9757  rankvalg 9777
[TakeutiZaring] p. 79Proposition 9.16rankel 9799  rankelb 9784
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9813  rankval3 9800  rankval3b 9786
[TakeutiZaring] p. 79Proposition 9.18rankonid 9789
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9755
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9794  rankr1c 9781  rankr1g 9792
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9795
[TakeutiZaring] p. 80Exercise 1rankss 9809  rankssb 9808
[TakeutiZaring] p. 80Exercise 2unbndrank 9802
[TakeutiZaring] p. 80Proposition 9.19bndrank 9801
[TakeutiZaring] p. 83Axiom of Choiceac4 10447  dfac3 10093
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10002  numth 10444  numth2 10443
[TakeutiZaring] p. 85Definition 10.4cardval 10518
[TakeutiZaring] p. 85Proposition 10.5cardid 10519  cardid2 9927
[TakeutiZaring] p. 85Proposition 10.9oncard 9934
[TakeutiZaring] p. 85Proposition 10.10carden 10523
[TakeutiZaring] p. 85Proposition 10.11cardidm 9933
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9918
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9939
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9931
[TakeutiZaring] p. 87Proposition 10.15pwen 9126
[TakeutiZaring] p. 88Exercise 1en0 9003
[TakeutiZaring] p. 88Exercise 7infensuc 9131
[TakeutiZaring] p. 89Exercise 10omxpen 9055
[TakeutiZaring] p. 90Corollary 10.23cardnn 9937
[TakeutiZaring] p. 90Definition 10.27alephiso 10070
[TakeutiZaring] p. 90Proposition 10.20nneneq 9178
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9186
[TakeutiZaring] p. 90Proposition 10.26alephprc 10071
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9183
[TakeutiZaring] p. 91Exercise 2alephle 10060
[TakeutiZaring] p. 91Exercise 3aleph0 10038
[TakeutiZaring] p. 91Exercise 4cardlim 9946
[TakeutiZaring] p. 91Exercise 7infpss 10187
[TakeutiZaring] p. 91Exercise 8infcntss 9270
[TakeutiZaring] p. 91Definition 10.29df-fin 8935  isfi 8960
[TakeutiZaring] p. 92Proposition 10.32onfin 9187
[TakeutiZaring] p. 92Proposition 10.34imadomg 10506
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9048
[TakeutiZaring] p. 93Proposition 10.35fodomb 10498
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10157  unxpdom 9207
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9948  cardsdomelir 9947
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9209
[TakeutiZaring] p. 94Proposition 10.39infxpen 9986
[TakeutiZaring] p. 95Definition 10.42df-map 8814
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10534  infxpidm2 9989
[TakeutiZaring] p. 95Proposition 10.41infdju 10178  infxp 10185
[TakeutiZaring] p. 96Proposition 10.44pw2en 9060  pw2f1o 9058
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9119
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10459
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10454  ac6s5 10463
[TakeutiZaring] p. 98Theorem 10.47unidom 10515
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10516  uniimadomf 10517
[TakeutiZaring] p. 100Definition 11.1cfcof 10246
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10241
[TakeutiZaring] p. 102Exercise 1cfle 10225
[TakeutiZaring] p. 102Exercise 2cf0 10222
[TakeutiZaring] p. 102Exercise 3cfsuc 10229
[TakeutiZaring] p. 102Exercise 4cfom 10236
[TakeutiZaring] p. 102Proposition 11.9coftr 10245
[TakeutiZaring] p. 103Theorem 11.15alephreg 10555
[TakeutiZaring] p. 103Proposition 11.11cardcf 10223
[TakeutiZaring] p. 103Proposition 11.13alephsing 10248
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10069
[TakeutiZaring] p. 104Proposition 11.16carduniima 10068
[TakeutiZaring] p. 104Proposition 11.18alephfp 10080  alephfp2 10081
[TakeutiZaring] p. 106Theorem 11.20gchina 10672
[TakeutiZaring] p. 106Theorem 11.21mappwen 10084
[TakeutiZaring] p. 107Theorem 11.26konigth 10542
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10556
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10557
[Tarski] p. 67Axiom B5ax-c5 39519
[Tarski] p. 67Scheme B5sp 2221
[Tarski] p. 68Lemma 6avril1 30723  equid 2035
[Tarski] p. 69Lemma 7equcomi 2040
[Tarski] p. 70Lemma 14spim 2421  spime 2423  spimew 1994
[Tarski] p. 70Lemma 16ax-12 2215  ax-c15 39525  ax12i 1989
[Tarski] p. 70Lemmas 16 and 17sb6 2121
[Tarski] p. 75Axiom B7ax6v 1991
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1933  ax5ALT 39543
[Tarski], p. 75Scheme B8 of system S2ax-7 2031  ax-8 2147  ax-9 2155
[Tarski1999] p. 178Axiom 4axtgsegcon 28691
[Tarski1999] p. 178Axiom 5axtg5seg 28692
[Tarski1999] p. 179Axiom 7axtgpasch 28694
[Tarski1999] p. 180Axiom 7.1axtgpasch 28694
[Tarski1999] p. 185Axiom 11axtgcont1 28695
[Truss] p. 114Theorem 5.18ruc 16289
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38170
[Viaclovsky8] p. 3Proposition 7ismblfin 38172
[Weierstrass] p. 272Definitiondf-mdet 22703  mdetuni 22740
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 916
[WhiteheadRussell] p. 96Axiom *1.3olc 881
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 882
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 932
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 983
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 190
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 136
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 91  wl-luk-pm2.04 37951
[WhiteheadRussell] p. 100Theorem *2.05frege5 44388  imim2 59  wl-luk-imim2 37946
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47611  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 909
[WhiteheadRussell] p. 101Theorem *2.06barbara 2692  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 915
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 37949
[WhiteheadRussell] p. 101Theorem *2.11exmid 907
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 910
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 45500  wl-luk-notnotr 37950
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44418  axfrege28 44417  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 880
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 937
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 37943
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 902
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 954
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30661  pm2.27 43  wl-luk-pm2.27 37941
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 935
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38882
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 936
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 985
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 986
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 984
[WhiteheadRussell] p. 105Definition *2.33df-3or 1102
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 919
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 920
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 957
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 894
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 895
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 896
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 897
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 898
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 864
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 865
[WhiteheadRussell] p. 107Theorem *2.55orel1 901
[WhiteheadRussell] p. 107Theorem *2.56orel2 903
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 912
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 955
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 956
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 195
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 904  pm2.67 905
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 911
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 988
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 913
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 989
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 990
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 946
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 944
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 987
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 991
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 85
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 945
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1007
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 474  pm3.2im 161
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1008
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1009
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1010
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1011
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 476
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 464
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 407
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 814
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 453
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 454
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 487  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 489  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 776
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 777
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 819
[WhiteheadRussell] p. 113Fact)pm3.45 633
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 821
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 497
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 498
[WhiteheadRussell] p. 113Theorem *3.44jao 975  pm3.44 974
[WhiteheadRussell] p. 113Theorem *3.47anim12 820
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 478
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 978
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 356
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 818
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 845
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 817  bitr 816
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 573
[WhiteheadRussell] p. 117Theorem *4.25oridm 917  pm4.25 918
[WhiteheadRussell] p. 118Theorem *4.3ancom 465
[WhiteheadRussell] p. 118Theorem *4.4andi 1023
[WhiteheadRussell] p. 118Theorem *4.31orcom 883
[WhiteheadRussell] p. 118Theorem *4.32anass 473
[WhiteheadRussell] p. 118Theorem *4.33orass 934
[WhiteheadRussell] p. 118Theorem *4.36anbi1 644
[WhiteheadRussell] p. 118Theorem *4.37orbi1 930
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 648
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 992
[WhiteheadRussell] p. 118Definition *4.34df-3an 1103
[WhiteheadRussell] p. 119Theorem *4.41ordi 1021
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1067
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1038
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1012
[WhiteheadRussell] p. 119Theorem *4.45orabs 1014  pm4.45 1013  pm4.45im 840
[WhiteheadRussell] p. 120Theorem *4.5anor 998
[WhiteheadRussell] p. 120Theorem *4.6imor 866
[WhiteheadRussell] p. 120Theorem *4.7anclb 554
[WhiteheadRussell] p. 120Theorem *4.51ianor 997
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 1000
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1001
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1002
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1003
[WhiteheadRussell] p. 120Theorem *4.56ioran 999  pm4.56 1004
[WhiteheadRussell] p. 120Theorem *4.57oran 1005  pm4.57 1006
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 409
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 869
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 402
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 862
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 410
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 863
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 403
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 566  pm4.71d 570  pm4.71i 568  pm4.71r 567  pm4.71rd 571  pm4.71ri 569
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 964
[WhiteheadRussell] p. 121Theorem *4.73iba 536
[WhiteheadRussell] p. 121Theorem *4.74biorf 949
[WhiteheadRussell] p. 121Theorem *4.76jcab 526  pm4.76 527
[WhiteheadRussell] p. 121Theorem *4.77jaob 976  pm4.77 977
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 947
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1019
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 397
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 398
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1039
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1040
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 391  impexp 455  pm4.87 856
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 835
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 959  pm5.11g 958
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 960
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 962
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 961
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1028
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1029
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1027
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 390
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 836
[WhiteheadRussell] p. 124Theorem *5.22xor 1030
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1063
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1064
[WhiteheadRussell] p. 124Theorem *5.25dfor2 914
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 582
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 392
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 364
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1017
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 968
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 843
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 583
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 848
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 837
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 846
[WhiteheadRussell] p. 125Theorem *5.41imdi 393  pm5.41 394
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 552
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 551
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1020
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1033
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 963
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1016
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1034
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1035
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1043
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1044
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37076
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44932
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44933
[WhiteheadRussell] p. 147Theorem *10.2219.26 1893
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44934
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44935
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44936
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1916
[WhiteheadRussell] p. 151Theorem *10.301albitr 44937
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44938
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44939
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44940
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44941
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44943
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44944
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44945
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44942
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2126
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44948
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44949
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2104
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2197
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1852
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1853
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44950
[WhiteheadRussell] p. 162Theorem *11.322alim 44951
[WhiteheadRussell] p. 162Theorem *11.332albi 44952
[WhiteheadRussell] p. 162Theorem *11.342exim 44953
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44955
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44954
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1910
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44957
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44958
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44956
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1851
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44959
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44960
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1869
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44961
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2380
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1883
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44966
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44962
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44963
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44964
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44965
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44970
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44967
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44968
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44969
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44971
[WhiteheadRussell] p. 175Definition *14.02df-eu 2599
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44981  pm13.13b 44982
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44983
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3041
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3042
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3628
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44989
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44990
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44984
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45126  pm13.193 44985
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44986
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44987
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44988
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44995
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44994
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44993
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3809
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44996  pm14.122b 44997  pm14.122c 44998
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44999  pm14.123b 45000  pm14.123c 45001
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45003
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45002
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45004
[WhiteheadRussell] p. 190Theorem *14.22iota4 6506
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45005
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6507
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45006
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45008
[WhiteheadRussell] p. 192Theorem *14.26eupick 2663  eupickbi 2666  sbaniota 45009
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45007
[WhiteheadRussell] p. 192Theorem *14.271eubi 2614
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45010
[WhiteheadRussell] p. 235Definition *30.01conventions 30660  df-fv 6533
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9975  pm54.43lem 9974
[Young] p. 141Definition of operator orderingleop2 32385
[Young] p. 142Example 12.2(i)0leop 32391  idleop 32392
[vandenDries] p. 42Lemma 61irrapx1 43417
[vandenDries] p. 43Theorem 62pellex 43424  pellexlem1 43418

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