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 17871
[Adamek] p. 21Condition 3.1(b)df-cat 17871
[Adamek] p. 22Example 3.3(1)df-setc 18280
[Adamek] p. 24Example 3.3(4.c)0cat 17892  0funcg 50405  df-termc 50813
[Adamek] p. 24Example 3.3(4.d)df-prstc 50893  prsthinc 50804
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50921  df-mndtc 50921
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50917
[Adamek] p. 25Definition 3.5df-oppc 17915
[Adamek] p. 25Example 3.6(1)oduoppcciso 50909
[Adamek] p. 25Example 3.6(2)oppgoppcco 50934  oppgoppchom 50933  oppgoppcid 50935
[Adamek] p. 28Remark 3.9oppciso 17985
[Adamek] p. 28Remark 3.12invf1o 17973  invisoinvl 17994
[Adamek] p. 28Example 3.13idinv 17993  idiso 17992
[Adamek] p. 28Corollary 3.11inveq 17978
[Adamek] p. 28Definition 3.8df-inv 17952  df-iso 17953  dfiso2 17976
[Adamek] p. 28Proposition 3.10sectcan 17959
[Adamek] p. 29Remark 3.16cicer 18010  cicerALT 50365
[Adamek] p. 29Definition 3.15cic 18003  df-cic 18000
[Adamek] p. 29Definition 3.17df-func 18062
[Adamek] p. 29Proposition 3.14(1)invinv 17974
[Adamek] p. 29Proposition 3.14(2)invco 17975  isoco 17981
[Adamek] p. 30Remark 3.19df-func 18062
[Adamek] p. 30Example 3.20(1)idfucl 18085
[Adamek] p. 30Example 3.20(2)diag1 50631
[Adamek] p. 32Proposition 3.21funciso 18078
[Adamek] p. 33Example 3.26(1)discsnterm 50917  discthing 50801
[Adamek] p. 33Example 3.26(2)df-thinc 50758  prsthinc 50804  thincciso 50793  thincciso2 50795  thincciso3 50796  thinccisod 50794
[Adamek] p. 33Example 3.26(3)df-mndtc 50921
[Adamek] p. 33Proposition 3.23cofucl 18092  cofucla 50416
[Adamek] p. 34Remark 3.28(1)cofidfth 50483
[Adamek] p. 34Remark 3.28(2)catciso 18315  catcisoi 50740
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18370
[Adamek] p. 34Definition 3.27(2)df-fth 18111
[Adamek] p. 34Definition 3.27(3)df-full 18110
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18370
[Adamek] p. 35Corollary 3.32ffthiso 18135
[Adamek] p. 35Proposition 3.30(c)cofth 18141
[Adamek] p. 35Proposition 3.30(d)cofull 18140
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18355
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18355
[Adamek] p. 39Remark 3.422oppf 50453
[Adamek] p. 39Definition 3.41df-oppf 50444  funcoppc 18079
[Adamek] p. 39Definition 3.44.df-catc 18303  elcatchom 50737
[Adamek] p. 39Proposition 3.43(c)fthoppc 18129  fthoppf 50485
[Adamek] p. 39Proposition 3.43(d)fulloppc 18128  fulloppf 50484
[Adamek] p. 40Remark 3.48catccat 18312
[Adamek] p. 40Definition 3.470funcg 50405  df-catc 18303
[Adamek] p. 45Exercise 3Gincat 50944
[Adamek] p. 48Remark 4.2(2)cnelsubc 50947  nelsubc3 50390
[Adamek] p. 48Remark 4.2(3)imasubc 50472  imasubc2 50473  imasubc3 50477
[Adamek] p. 48Example 4.3(1.a)0subcat 18042
[Adamek] p. 48Example 4.3(1.b)catsubcat 18043
[Adamek] p. 48Definition 4.1(1)nelsubc3 50390
[Adamek] p. 48Definition 4.1(2)fullsubc 18054
[Adamek] p. 48Definition 4.1(a)df-subc 18016
[Adamek] p. 49Remark 4.4idsubc 50481
[Adamek] p. 49Remark 4.4(1)idemb 50480
[Adamek] p. 49Remark 4.4(2)idfullsubc 50482  ressffth 18144
[Adamek] p. 58Exercise 4Asetc1onsubc 50945
[Adamek] p. 83Definition 6.1df-nat 18150
[Adamek] p. 87Remark 6.14(a)fuccocl 18171
[Adamek] p. 87Remark 6.14(b)fucass 18175
[Adamek] p. 87Definition 6.15df-fuc 18151
[Adamek] p. 88Remark 6.16fuccat 18177
[Adamek] p. 101Definition 7.10funcg 50405  df-inito 18188
[Adamek] p. 101Example 7.2(3)0funcg 50405  df-termc 50813  initc 50411
[Adamek] p. 101Example 7.2 (6)irinitoringc 21815
[Adamek] p. 102Definition 7.4df-termo 18189  oppctermo 50563
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18216
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18220
[Adamek] p. 103Remark 7.8oppczeroo 50564
[Adamek] p. 103Definition 7.7df-zeroo 18190
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21816
[Adamek] p. 103Proposition 7.6termoeu1w 18223
[Adamek] p. 106Definition 7.19df-sect 17951
[Adamek] p. 107Example 7.20(7)thincinv 50809
[Adamek] p. 108Example 7.25(4)thincsect2 50808
[Adamek] p. 110Example 7.33(9)thincmon 50773
[Adamek] p. 110Proposition 7.35sectmon 17986
[Adamek] p. 112Proposition 7.42sectepi 17988
[Adamek] p. 185Section 10.67updjud 10042
[Adamek] p. 193Definition 11.1(1)df-lmd 51033
[Adamek] p. 193Definition 11.3(1)df-lmd 51033
[Adamek] p. 194Definition 11.3(2)df-lmd 51033
[Adamek] p. 202Definition 11.27(1)df-cmd 51034
[Adamek] p. 202Definition 11.27(2)df-cmd 51034
[Adamek] p. 478Item Rngdf-ringc 20928
[AhoHopUll] p. 2Section 1.1df-bigo 49865
[AhoHopUll] p. 12Section 1.3df-blen 49887
[AhoHopUll] p. 318Section 9.1df-concat 14743  df-pfx 14849  df-substr 14817  df-word 14686  lencl 14705  wrd0 14711
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 25057  df-nmoo 31377
[AkhiezerGlazman] p. 64Theoremhmopidmch 32785  hmopidmchi 32783
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32833  pjcmul2i 32834
[AkhiezerGlazman] p. 72Theoremcnvunop 32550  unoplin 32552
[AkhiezerGlazman] p. 72Equation 2unopadj 32551  unopadj2 32570
[AkhiezerGlazman] p. 73Theoremelunop2 32645  lnopunii 32644
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32718
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28343
[Alling] p. 184Axiom Bbdayfo 28064
[Alling] p. 184Axiom Oltsso 28063
[Alling] p. 184Axiom SDnodense 28079
[Alling] p. 185Lemma 0nocvxmin 28171
[Alling] p. 185Theoremconway 28195
[Alling] p. 185Axiom FEnoeta 28130
[Alling] p. 186Theorem 4lesrec 28215  lesrecd 28216
[Alling], p. 2Definitionrp-brsslt 44616
[Alling], p. 3Notenla0001 44619  nla0002 44617  nla0003 44618
[Apostol] p. 18Theorem I.1addcan 11521  addcan2d 11541  addcan2i 11531  addcand 11540  addcani 11530
[Apostol] p. 18Theorem I.2negeu 11574
[Apostol] p. 18Theorem I.3negsub 11633  negsubd 11702  negsubi 11663
[Apostol] p. 18Theorem I.4negneg 11635  negnegd 11687  negnegi 11655
[Apostol] p. 18Theorem I.5subdi 11776  subdid 11799  subdii 11792  subdir 11777  subdird 11800  subdiri 11793
[Apostol] p. 18Theorem I.6mul01 11516  mul01d 11536  mul01i 11527  mul02 11515  mul02d 11535  mul02i 11526
[Apostol] p. 18Theorem I.7mulcan 11980  mulcan2d 11977  mulcand 11976  mulcani 11982
[Apostol] p. 18Theorem I.8receu 11988  xreceu 33558
[Apostol] p. 18Theorem I.9divrec 12017  divrecd 12123  divreci 12089  divreczi 12082
[Apostol] p. 18Theorem I.10recrec 12041  recreci 12076
[Apostol] p. 18Theorem I.11mul0or 11983  mul0ord 11991  mul0ori 11990
[Apostol] p. 18Theorem I.12mul2neg 11782  mul2negd 11798  mul2negi 11791  mulneg1 11779  mulneg1d 11796  mulneg1i 11789
[Apostol] p. 18Theorem I.13divadddiv 12059  divadddivd 12164  divadddivi 12106
[Apostol] p. 18Theorem I.14divmuldiv 12044  divmuldivd 12161  divmuldivi 12104  rdivmuldivd 20673
[Apostol] p. 18Theorem I.15divdivdiv 12045  divdivdivd 12167  divdivdivi 12107
[Apostol] p. 20Axiom 7rpaddcl 13171  rpaddcld 13206  rpmulcl 13172  rpmulcld 13207
[Apostol] p. 20Axiom 8rpneg 13181
[Apostol] p. 20Axiom 90nrp 13184
[Apostol] p. 20Theorem I.17lttri 11463
[Apostol] p. 20Theorem I.18ltadd1d 11936  ltadd1dd 11954  ltadd1i 11897
[Apostol] p. 20Theorem I.19ltmul1 12194  ltmul1a 12193  ltmul1i 12262  ltmul1ii 12272  ltmul2 12195  ltmul2d 13233  ltmul2dd 13247  ltmul2i 12265
[Apostol] p. 20Theorem I.20msqgt0 11863  msqgt0d 11910  msqgt0i 11880
[Apostol] p. 20Theorem I.210lt1 11865
[Apostol] p. 20Theorem I.23lt0neg1 11849  lt0neg1d 11912  ltneg 11843  ltnegd 11921  ltnegi 11887
[Apostol] p. 20Theorem I.25lt2add 11828  lt2addd 11966  lt2addi 11905
[Apostol] p. 20Definition of positive numbersdf-rp 13148
[Apostol] p. 21Exercise 4recgt0 12190  recgt0d 12278  recgt0i 12249  recgt0ii 12250
[Apostol] p. 22Definition of integersdf-z 12721
[Apostol] p. 22Definition of positive integersdfnn3 12376
[Apostol] p. 22Definition of rationalsdf-q 13103
[Apostol] p. 24Theorem I.26supeu 9473
[Apostol] p. 26Theorem I.28nnunb 12629
[Apostol] p. 26Theorem I.29arch 12630  archd 46382
[Apostol] p. 28Exercise 2btwnz 12829
[Apostol] p. 28Exercise 3nnrecl 12631
[Apostol] p. 28Exercise 4rebtwnz 13101
[Apostol] p. 28Exercise 5zbtwnre 13100
[Apostol] p. 28Exercise 6qbtwnre 13356
[Apostol] p. 28Exercise 10(a)zeneo 16538  zneo 12809  zneoALTV 48972
[Apostol] p. 29Theorem I.35cxpsqrtth 27088  msqsqrtd 15639  resqrtth 15451  sqrtth 15561  sqrtthi 15567  sqsqrtd 15638
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12365
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 13067
[Apostol] p. 361Remarkcrreczi 14399
[Apostol] p. 363Remarkabsgt0i 15596
[Apostol] p. 363Exampleabssubd 15652  abssubi 15600
[ApostolNT] p. 7Remarkfmtno0 48830  fmtno1 48831  fmtno2 48840  fmtno3 48841  fmtno4 48842  fmtno5fac 48872  fmtnofz04prm 48867
[ApostolNT] p. 7Definitiondf-fmtno 48818
[ApostolNT] p. 8Definitiondf-ppi 27457
[ApostolNT] p. 14Definitiondf-dvds 16452
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16468
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16493
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16488
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16481
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16483
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16469
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16470
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16475
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16510
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16512
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16514
[ApostolNT] p. 15Definitiondf-gcd 16694  dfgcd2 16748
[ApostolNT] p. 16Definitionisprm2 16886
[ApostolNT] p. 16Theorem 1.5coprmdvds 16857
[ApostolNT] p. 16Theorem 1.7prminf 17122
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16714
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16749
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16751
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16730
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16721
[ApostolNT] p. 17Theorem 1.8coprm 16916
[ApostolNT] p. 17Theorem 1.9euclemma 16918
[ApostolNT] p. 17Theorem 1.101arith2 17135
[ApostolNT] p. 18Theorem 1.13prmrec 17129
[ApostolNT] p. 19Theorem 1.14divalg 16602
[ApostolNT] p. 20Theorem 1.15eucalg 16791
[ApostolNT] p. 24Definitiondf-mu 27458
[ApostolNT] p. 25Definitiondf-phi 16972
[ApostolNT] p. 25Theorem 2.1musum 27548
[ApostolNT] p. 26Theorem 2.2phisum 16997
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16982
[ApostolNT] p. 28Theorem 2.5(c)phimul 16986
[ApostolNT] p. 32Definitiondf-vma 27455
[ApostolNT] p. 32Theorem 2.9muinv 27550
[ApostolNT] p. 32Theorem 2.10vmasum 27573
[ApostolNT] p. 38Remarkdf-sgm 27459
[ApostolNT] p. 38Definitiondf-sgm 27459
[ApostolNT] p. 75Definitiondf-chp 27456  df-cht 27454
[ApostolNT] p. 104Definitioncongr 16868
[ApostolNT] p. 106Remarkdvdsval3 16455
[ApostolNT] p. 106Definitionmoddvds 16462
[ApostolNT] p. 107Example 2mod2eq0even 16545
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16546
[ApostolNT] p. 107Example 4zmod1congr 14055
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 14095
[ApostolNT] p. 107Theorem 5.2(c)modexp 14409
[ApostolNT] p. 108Theorem 5.3modmulconst 16487
[ApostolNT] p. 109Theorem 5.4cncongr1 16871
[ApostolNT] p. 109Theorem 5.6gcdmodi 17281
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16873
[ApostolNT] p. 113Theorem 5.17eulerth 16989
[ApostolNT] p. 113Theorem 5.18vfermltl 17008
[ApostolNT] p. 114Theorem 5.19fermltl 16990
[ApostolNT] p. 116Theorem 5.24wilthimp 27429
[ApostolNT] p. 179Definitiondf-lgs 27652  lgsprme0 27696
[ApostolNT] p. 180Example 11lgs 27697
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27673
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27688
[ApostolNT] p. 181Theorem 9.4m1lgs 27745
[ApostolNT] p. 181Theorem 9.52lgs 27764  2lgsoddprm 27773
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27731
[ApostolNT] p. 185Theorem 9.8lgsquad 27740
[ApostolNT] p. 188Definitiondf-lgs 27652  lgs1 27698
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27689
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27691
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27699
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27700
[Baer] p. 40Property (b)mapdord 42887
[Baer] p. 40Property (c)mapd11 42888
[Baer] p. 40Property (e)mapdin 42911  mapdlsm 42913
[Baer] p. 40Property (f)mapd0 42914
[Baer] p. 40Definition of projectivitydf-mapd 42874  mapd1o 42897
[Baer] p. 41Property (g)mapdat 42916
[Baer] p. 44Part (1)mapdpg 42955
[Baer] p. 45Part (2)hdmap1eq 43050  mapdheq 42977  mapdheq2 42978  mapdheq2biN 42979
[Baer] p. 45Part (3)baerlem3 42962
[Baer] p. 46Part (4)mapdheq4 42981  mapdheq4lem 42980
[Baer] p. 46Part (5)baerlem5a 42963  baerlem5abmN 42967  baerlem5amN 42965  baerlem5b 42964  baerlem5bmN 42966
[Baer] p. 47Part (6)hdmap1l6 43070  hdmap1l6a 43058  hdmap1l6e 43063  hdmap1l6f 43064  hdmap1l6g 43065  hdmap1l6lem1 43056  hdmap1l6lem2 43057  mapdh6N 42996  mapdh6aN 42984  mapdh6eN 42989  mapdh6fN 42990  mapdh6gN 42991  mapdh6lem1N 42982  mapdh6lem2N 42983
[Baer] p. 48Part 9hdmapval 43077
[Baer] p. 48Part 10hdmap10 43089
[Baer] p. 48Part 11hdmapadd 43092
[Baer] p. 48Part (6)hdmap1l6h 43066  mapdh6hN 42992
[Baer] p. 48Part (7)mapdh75cN 43002  mapdh75d 43003  mapdh75e 43001  mapdh75fN 43004  mapdh7cN 42998  mapdh7dN 42999  mapdh7eN 42997  mapdh7fN 43000
[Baer] p. 48Part (8)mapdh8 43037  mapdh8a 43024  mapdh8aa 43025  mapdh8ab 43026  mapdh8ac 43027  mapdh8ad 43028  mapdh8b 43029  mapdh8c 43030  mapdh8d 43032  mapdh8d0N 43031  mapdh8e 43033  mapdh8g 43034  mapdh8i 43035  mapdh8j 43036
[Baer] p. 48Part (9)mapdh9a 43038
[Baer] p. 48Equation 10mapdhvmap 43018
[Baer] p. 49Part 12hdmap11 43097  hdmapeq0 43093  hdmapf1oN 43114  hdmapneg 43095  hdmaprnN 43113  hdmaprnlem1N 43098  hdmaprnlem3N 43099  hdmaprnlem3uN 43100  hdmaprnlem4N 43102  hdmaprnlem6N 43103  hdmaprnlem7N 43104  hdmaprnlem8N 43105  hdmaprnlem9N 43106  hdmapsub 43096
[Baer] p. 49Part 14hdmap14lem1 43117  hdmap14lem10 43126  hdmap14lem1a 43115  hdmap14lem2N 43118  hdmap14lem2a 43116  hdmap14lem3 43119  hdmap14lem8 43124  hdmap14lem9 43125
[Baer] p. 50Part 14hdmap14lem11 43127  hdmap14lem12 43128  hdmap14lem13 43129  hdmap14lem14 43130  hdmap14lem15 43131  hgmapval 43136
[Baer] p. 50Part 15hgmapadd 43143  hgmapmul 43144  hgmaprnlem2N 43146  hgmapvs 43140
[Baer] p. 50Part 16hgmaprnN 43150
[Baer] p. 110Lemma 1hdmapip0com 43166
[Baer] p. 110Line 27hdmapinvlem1 43167
[Baer] p. 110Line 28hdmapinvlem2 43168
[Baer] p. 110Line 30hdmapinvlem3 43169
[Baer] p. 110Part 1.2hdmapglem5 43171  hgmapvv 43175
[Baer] p. 110Proposition 1hdmapinvlem4 43170
[Baer] p. 111Line 10hgmapvvlem1 43172
[Baer] p. 111Line 15hdmapg 43179  hdmapglem7 43178
[Bauer], p. 483Theorem 1.22irrexpq 27089  2irrexpqALT 27158
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2597
[BellMachover] p. 460Notationdf-mo 2567
[BellMachover] p. 460Definitionmo3 2592
[BellMachover] p. 461Axiom Extax-ext 2735
[BellMachover] p. 462Theorem 1.1axextmo 2739
[BellMachover] p. 463Axiom Repaxrep5 5242
[BellMachover] p. 463Scheme Sepax-sep 5252
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 38170  sepex 5258
[BellMachover] p. 466Problemaxpow2 5333
[BellMachover] p. 466Axiom Powaxpow3 5334
[BellMachover] p. 466Axiom Unionaxun2 7777
[BellMachover] p. 468Definitiondf-ord 6383
[BellMachover] p. 469Theorem 2.2(i)ordirr 6398
[BellMachover] p. 469Theorem 2.2(iii)onelon 6405  onelond 37126
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6400
[BellMachover] p. 471Definition of Ndf-om 7902
[BellMachover] p. 471Problem 2.5(ii)uniordint 7839
[BellMachover] p. 471Definition of Limdf-lim 6385
[BellMachover] p. 472Axiom Infzfinf2 9670
[BellMachover] p. 473Theorem 2.8limom 7917
[BellMachover] p. 477Equation 3.1df-r1 9795
[BellMachover] p. 478Definitionrankval2 9854  rankval2b 9862
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9816  r1ord3g 9813
[BellMachover] p. 480Axiom Regzfreg 9617
[BellMachover] p. 488Axiom ACac5 10582  dfac4 10228
[BellMachover] p. 490Definition of alephalephval3 10216
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40568
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32985
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 33027  chirredi 33026
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 33015
[Beran] p. 3Definition of joinsshjval3 31986
[Beran] p. 39Theorem 2.3(i)cmcm2 32248  cmcm2i 32225  cmcm2ii 32230  cmt2N 40499
[Beran] p. 40Theorem 2.3(iii)lecm 32249  lecmi 32234  lecmii 32235
[Beran] p. 45Theorem 3.4cmcmlem 32223
[Beran] p. 49Theorem 4.2cm2j 32252  cm2ji 32257  cm2mi 32258
[Beran] p. 95Definitiondf-sh 31839  issh2 31841
[Beran] p. 95Lemma 3.1(S5)his5 31718
[Beran] p. 95Lemma 3.1(S6)his6 31731
[Beran] p. 95Lemma 3.1(S7)his7 31722
[Beran] p. 95Lemma 3.2(S8)ho01i 32460
[Beran] p. 95Lemma 3.2(S9)hoeq1 32462
[Beran] p. 95Lemma 3.2(S10)ho02i 32461
[Beran] p. 95Lemma 3.2(S11)hoeq2 32463
[Beran] p. 95Postulate (S1)ax-his1 31714  his1i 31732
[Beran] p. 95Postulate (S2)ax-his2 31715
[Beran] p. 95Postulate (S3)ax-his3 31716
[Beran] p. 95Postulate (S4)ax-his4 31717
[Beran] p. 96Definition of normdf-hnorm 31600  dfhnorm2 31754  normval 31756
[Beran] p. 96Definition for Cauchy sequencehcau 31816
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31605
[Beran] p. 96Definition of complete subspaceisch3 31873
[Beran] p. 96Definition of convergedf-hlim 31604  hlimi 31820
[Beran] p. 97Theorem 3.3(i)norm-i-i 31765  norm-i 31761
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31769  norm-ii 31770  normlem0 31741  normlem1 31742  normlem2 31743  normlem3 31744  normlem4 31745  normlem5 31746  normlem6 31747  normlem7 31748  normlem7tALT 31751
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31771  norm-iii 31772
[Beran] p. 98Remark 3.4bcs 31813  bcsiALT 31811  bcsiHIL 31812
[Beran] p. 98Remark 3.4(B)normlem9at 31753  normpar 31787  normpari 31786
[Beran] p. 98Remark 3.4(C)normpyc 31778  normpyth 31777  normpythi 31774
[Beran] p. 99Remarklnfn0 32679  lnfn0i 32674  lnop0 32598  lnop0i 32602
[Beran] p. 99Theorem 3.5(i)nmcexi 32658  nmcfnex 32685  nmcfnexi 32683  nmcopex 32661  nmcopexi 32659
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32686  nmcfnlbi 32684  nmcoplb 32662  nmcoplbi 32660
[Beran] p. 99Theorem 3.5(iii)lnfncon 32688  lnfnconi 32687  lnopcon 32667  lnopconi 32666
[Beran] p. 100Lemma 3.6normpar2i 31788
[Beran] p. 101Lemma 3.6norm3adifi 31785  norm3adifii 31780  norm3dif 31782  norm3difi 31779
[Beran] p. 102Theorem 3.7(i)chocunii 31933  pjhth 32025  pjhtheu 32026  pjpjhth 32057  pjpjhthi 32058  pjth 25790
[Beran] p. 102Theorem 3.7(ii)ococ 32038  ococi 32037
[Beran] p. 103Remark 3.8nlelchi 32693
[Beran] p. 104Theorem 3.9riesz3i 32694  riesz4 32696  riesz4i 32695
[Beran] p. 104Theorem 3.10cnlnadj 32711  cnlnadjeu 32710  cnlnadjeui 32709  cnlnadji 32708  cnlnadjlem1 32699  nmopadjlei 32720
[Beran] p. 106Theorem 3.11(i)adjeq0 32723
[Beran] p. 106Theorem 3.11(v)nmopadji 32722
[Beran] p. 106Theorem 3.11(ii)adjmul 32724
[Beran] p. 106Theorem 3.11(iv)adjadj 32568
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32734  nmopcoadji 32733
[Beran] p. 106Theorem 3.11(iii)adjadd 32725
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32735
[Beran] p. 106Theorem 3.11(viii)adjcoi 32732  pjadj2coi 32836  pjadjcoi 32793
[Beran] p. 107Definitiondf-ch 31853  isch2 31855
[Beran] p. 107Remark 3.12choccl 31938  isch3 31873  occl 31936  ocsh 31915  shoccl 31937  shocsh 31916
[Beran] p. 107Remark 3.12(B)ococin 32040
[Beran] p. 108Theorem 3.13chintcl 31964
[Beran] p. 109Property (i)pjadj2 32819  pjadj3 32820  pjadji 32317  pjadjii 32306
[Beran] p. 109Property (ii)pjidmco 32813  pjidmcoi 32809  pjidmi 32305
[Beran] p. 110Definition of projector orderingpjordi 32805
[Beran] p. 111Remarkho0val 32382  pjch1 32302
[Beran] p. 111Definitiondf-hfmul 32366  df-hfsum 32365  df-hodif 32364  df-homul 32363  df-hosum 32362
[Beran] p. 111Lemma 4.4(i)pjo 32303
[Beran] p. 111Lemma 4.4(ii)pjch 32326  pjchi 32064
[Beran] p. 111Lemma 4.4(iii)pjoc2 32071  pjoc2i 32070
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 32312
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32797  pjssmii 32313
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32796
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32795
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32800
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32798  pjssge0ii 32314
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32799  pjdifnormii 32315
[Bobzien] p. 116Statement T3stoic3 1809
[Bobzien] p. 117Statement T2stoic2a 1807
[Bobzien] p. 117Statement T4stoic4a 1810
[Bobzien] p. 117Conclusion the contradictorystoic1a 1805
[Bogachev] p. 16Definition 1.5df-oms 34994
[Bogachev] p. 17Lemma 1.5.4omssubadd 35002
[Bogachev] p. 17Example 1.5.2omsmon 35000
[Bogachev] p. 41Definition 1.11.2df-carsg 35004
[Bogachev] p. 42Theorem 1.11.4carsgsiga 35024
[Bogachev] p. 116Definition 2.3.1df-itgm 35055  df-sitm 35033
[Bogachev] p. 118Chapter 2.4.4df-itgm 35055
[Bogachev] p. 118Definition 2.4.1df-sitg 35032
[Bollobas] p. 1Section I.1df-edg 29656  isuhgrop 29678  isusgrop 29773  isuspgrop 29772
[Bollobas] p. 2Section I.1df-isubgr 49164  df-subgr 29879  uhgrspan1 29914  uhgrspansubgr 29902
[Bollobas] p. 3Definitiondf-gric 49184  gricuspgr 49221  isuspgrim 49199
[Bollobas] p. 3Section I.1cusgrsize 30065  df-clnbgr 49122  df-cusgr 30023  df-nbgr 29944  fusgrmaxsize 30075
[Bollobas] p. 4Definitiondf-upwlks 49437  df-wlks 30210
[Bollobas] p. 4Section I.1finsumvtxdg2size 30161  finsumvtxdgeven 30163  fusgr1th 30162  fusgrvtxdgonume 30165  vtxdgoddnumeven 30164
[Bollobas] p. 5Notationdf-pths 30329
[Bollobas] p. 5Definitiondf-crcts 30403  df-cycls 30404  df-trls 30305  df-wlkson 30211
[Bollobas] p. 7Section I.1df-ushgr 29667
[BourbakiAlg1] p. 1Definition 1df-clintop 49502  df-cllaw 49488  df-mgm 18845  df-mgm2 49521
[BourbakiAlg1] p. 4Definition 5df-assintop 49503  df-asslaw 49490  df-sgrp 18937  df-sgrp2 49523
[BourbakiAlg1] p. 7Definition 8df-cmgm2 49522  df-comlaw 49489
[BourbakiAlg1] p. 12Definition 2df-mnd 18953
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33657  mndlactf1o 33661  mndractf1 33659  mndractf1o 33662
[BourbakiAlg1] p. 92Definition 1df-ring 20491
[BourbakiAlg1] p. 93Section I.8.1df-rng 20405
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 34335
[BourbakiAlg2] p. 113Chapter 5.assafld 34339  assarrginv 34338
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34380  fldextrspunfld 34378  fldextrspunlem1 34377  fldextrspunlem2 34379  fldextrspunlsp 34376  fldextrspunlsplem 34375
[BourbakiCAlg2], p. 228Proposition 21arithidom 34139  dfufd2 34152
[BourbakiEns] p. Proposition 8fcof1 7318  fcofo 7319
[BourbakiTop1] p. Remarkxnegmnf 13367  xnegpnf 13366
[BourbakiTop1] p. Remark rexneg 13368
[BourbakiTop1] p. Remark 3ust0 24569  ustfilxp 24562
[BourbakiTop1] p. Axiom GT'tgpsubcn 24439
[BourbakiTop1] p. Criterionishmeo 24108
[BourbakiTop1] p. Example 1cstucnd 24632  iducn 24631  snfil 24213
[BourbakiTop1] p. Example 2neifil 24229
[BourbakiTop1] p. Theorem 1cnextcn 24416
[BourbakiTop1] p. Theorem 2ucnextcn 24652
[BourbakiTop1] p. Theorem 3df-hcmp 34659
[BourbakiTop1] p. Paragraph 3infil 24212
[BourbakiTop1] p. Definition 1df-ucn 24624  df-ust 24550  filintn0 24210  filn0 24211  istgp 24426  ucnprima 24630
[BourbakiTop1] p. Definition 2df-cfilu 24635
[BourbakiTop1] p. Definition 3df-cusp 24646  df-usp 24606  df-utop 24580  trust 24578
[BourbakiTop1] p. Definition 6df-pcmp 34558
[BourbakiTop1] p. Property V_issnei2 23464
[BourbakiTop1] p. Theorem 1(d)iscncl 23617
[BourbakiTop1] p. Condition F_Iustssel 24555
[BourbakiTop1] p. Condition U_Iustdiag 24558
[BourbakiTop1] p. Property V_iiinnei 23473
[BourbakiTop1] p. Property V_ivneiptopreu 23481  neissex 23475
[BourbakiTop1] p. Proposition 1neips 23461  neiss 23457  ucncn 24633  ustund 24571  ustuqtop 24595
[BourbakiTop1] p. Proposition 2cnpco 23615  neiptopreu 23481  utop2nei 24599  utop3cls 24600
[BourbakiTop1] p. Proposition 3fmucnd 24640  uspreg 24622  utopreg 24601
[BourbakiTop1] p. Proposition 4imasncld 24040  imasncls 24041  imasnopn 24039
[BourbakiTop1] p. Proposition 9cnpflf2 24349
[BourbakiTop1] p. Condition F_IIustincl 24557
[BourbakiTop1] p. Condition U_IIustinvel 24559
[BourbakiTop1] p. Property V_iiielnei 23459
[BourbakiTop1] p. Proposition 11cnextucn 24651
[BourbakiTop1] p. Condition F_IIbustbasel 24556
[BourbakiTop1] p. Condition U_IIIustexhalf 24560
[BourbakiTop1] p. Definition C'''df-cmp 23735
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 24195
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23242
[BourbakiTop2] p. 195Definition 1df-ldlf 34555
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 47277
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 47279  stoweid 47278
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 47216  stoweidlem10 47225  stoweidlem14 47229  stoweidlem15 47230  stoweidlem35 47250  stoweidlem36 47251  stoweidlem37 47252  stoweidlem38 47253  stoweidlem40 47255  stoweidlem41 47256  stoweidlem43 47258  stoweidlem44 47259  stoweidlem46 47261  stoweidlem5 47220  stoweidlem50 47265  stoweidlem52 47267  stoweidlem53 47268  stoweidlem55 47270  stoweidlem56 47271
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 47238  stoweidlem24 47239  stoweidlem27 47242  stoweidlem28 47243  stoweidlem30 47245
[BrosowskiDeutsh] p. 91Proofstoweidlem34 47249  stoweidlem59 47274  stoweidlem60 47275
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 47260  stoweidlem49 47264  stoweidlem7 47222
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 47246  stoweidlem39 47254  stoweidlem42 47257  stoweidlem48 47263  stoweidlem51 47266  stoweidlem54 47269  stoweidlem57 47272  stoweidlem58 47273
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 47240
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 47232
[BrosowskiDeutsh] p. 92Proofstoweidlem11 47226  stoweidlem13 47228  stoweidlem26 47241  stoweidlem61 47276
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 47233
[Bruck] p. 1Section I.1df-clintop 49502  df-mgm 18845  df-mgm2 49521
[Bruck] p. 23Section II.1df-sgrp 18937  df-sgrp2 49523
[Bruck] p. 28Theorem 3.2dfgrp3 19278
[ChoquetDD] p. 2Definition of mappingdf-mpt 5190
[Church] p. 129Section II.24df-ifp 1079  dfifp2 1080
[Clemente] p. 10Definition ITnatded 31034
[Clemente] p. 10Definition I` `m,nnatded 31034
[Clemente] p. 11Definition E=>m,nnatded 31034
[Clemente] p. 11Definition I=>m,nnatded 31034
[Clemente] p. 11Definition E` `(1)natded 31034
[Clemente] p. 11Definition E` `(2)natded 31034
[Clemente] p. 12Definition E` `m,n,pnatded 31034
[Clemente] p. 12Definition I` `n(1)natded 31034
[Clemente] p. 12Definition I` `n(2)natded 31034
[Clemente] p. 13Definition I` `m,n,pnatded 31034
[Clemente] p. 14Proof 5.11natded 31034
[Clemente] p. 14Definition E` `nnatded 31034
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 31036  ex-natded5.2 31035
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 31039  ex-natded5.3 31038
[Clemente] p. 18Theorem 5.5ex-natded5.5 31041
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 31043  ex-natded5.7 31042
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 31045  ex-natded5.8 31044
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 31047  ex-natded5.13 31046
[Clemente] p. 32Definition I` `nnatded 31034
[Clemente] p. 32Definition E` `m,n,p,anatded 31034
[Clemente] p. 32Definition E` `n,tnatded 31034
[Clemente] p. 32Definition I` `n,tnatded 31034
[Clemente] p. 43Theorem 9.20ex-natded9.20 31048
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 31049
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 31051  ex-natded9.26 31050
[Cohen] p. 301Remarkrelogoprlem 26949
[Cohen] p. 301Property 2relogmul 26950  relogmuld 26983
[Cohen] p. 301Property 3relogdiv 26951  relogdivd 26984
[Cohen] p. 301Property 4relogexp 26954
[Cohen] p. 301Property 1alog1 26943
[Cohen] p. 301Property 1bloge 26944
[Cohen4] p. 348Observationrelogbcxpb 27145
[Cohen4] p. 349Propertyrelogbf 27149
[Cohen4] p. 352Definitionelogb 27128
[Cohen4] p. 361Property 2relogbmul 27135
[Cohen4] p. 361Property 3logbrec 27140  relogbdiv 27137
[Cohen4] p. 361Property 4relogbreexp 27133
[Cohen4] p. 361Property 6relogbexp 27138
[Cohen4] p. 361Property 1(a)logbid1 27126
[Cohen4] p. 361Property 1(b)logb1 27127
[Cohen4] p. 367Propertylogbchbase 27129
[Cohen4] p. 377Property 2logblt 27142
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34987  sxbrsigalem4 34989
[Cohn] p. 81Section II.5acsdomd 18760  acsinfd 18759  acsinfdimd 18761  acsmap2d 18758  acsmapd 18757
[Cohn] p. 143Example 5.1.1sxbrsiga 34992
[Connell] p. 57Definitiondf-scmat 22836  df-scmatalt 49716
[Conway] p. 4Definitionlesrec 28215  lesrecd 28216
[Conway] p. 5Definitionaddsval 28378  addsval2 28379  df-adds 28376  df-muls 28523  df-negs 28437
[Conway] p. 7Theorem0lt1s 28228
[Conway] p. 12Theorem 12pw2cut2 28878
[Conway] p. 16Theorem 0(i)sltsright 28277
[Conway] p. 16Theorem 0(ii)sltsleft 28276
[Conway] p. 16Theorem 0(iii)lesid 28154
[Conway] p. 17Theorem 3addsass 28421  addsassd 28422  addscom 28382  addscomd 28383  addsrid 28380  addsridd 28381
[Conway] p. 17Definitiondf-0s 28223
[Conway] p. 17Theorem 4(ii)negnegs 28460
[Conway] p. 17Theorem 4(iii)negsid 28457  negsidd 28458
[Conway] p. 18Theorem 5leadds1 28405  leadds1d 28411
[Conway] p. 18Definitiondf-1s 28224
[Conway] p. 18Theorem 6(ii)negscl 28452  negscld 28453
[Conway] p. 18Theorem 6(iii)addscld 28396
[Conway] p. 19Notemulsunif2 28586
[Conway] p. 19Theorem 7addsdi 28571  addsdid 28572  addsdird 28573  mulnegs1d 28576  mulnegs2d 28577  mulsass 28582  mulsassd 28583  mulscom 28555  mulscomd 28556
[Conway] p. 19Theorem 8(i)mulscl 28550  mulscld 28551
[Conway] p. 19Theorem 8(iii)lemulsd 28554  ltmuls 28552  ltmulsd 28553
[Conway] p. 20Theorem 9mulsgt0 28560  mulsgt0d 28561
[Conway] p. 21Theorem 10(iv)precsex 28634
[Conway] p. 23Theorem 11eqcuts3 28220
[Conway] p. 24Definitiondf-reno 28906
[Conway] p. 24Theorem 13(ii)readdscl 28915  remulscl 28918  renegscl 28914
[Conway] p. 27Definitiondf-ons 28668  elons2 28674
[Conway] p. 27Theorem 14ltonsex 28678
[Conway] p. 28Theorem 15oncutlt 28680  onswe 28688
[Conway] p. 29Remarkmadebday 28316  newbday 28318  oldbday 28317
[Conway] p. 29Definitiondf-made 28243  df-new 28245  df-old 28244
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 14028
[Crawley] p. 1Definition of posetdf-poset 18516
[Crawley] p. 107Theorem 13.2hlsupr 40635
[Crawley] p. 110Theorem 13.3arglem1N 41439  dalaw 41135
[Crawley] p. 111Theorem 13.4hlathil 43210
[Crawley] p. 111Definition of set Wdf-watsN 41239
[Crawley] p. 111Definition of dilationdf-dilN 41355  df-ldil 41353  isldil 41359
[Crawley] p. 111Definition of translationdf-ltrn 41354  df-trnN 41356  isltrn 41368  ltrnu 41370
[Crawley] p. 112Lemma Acdlema1N 41040  cdlema2N 41041  exatleN 40653
[Crawley] p. 112Lemma B1cvrat 40725  cdlemb 41043  cdlemb2 41290  cdlemb3 41855  idltrn 41399  l1cvat 40304  lhpat 41292  lhpat2 41294  lshpat 40305  ltrnel 41388  ltrnmw 41400
[Crawley] p. 112Lemma Ccdlemc1 41440  cdlemc2 41441  ltrnnidn 41423  trlat 41418  trljat1 41415  trljat2 41416  trljat3 41417  trlne 41434  trlnidat 41422  trlnle 41435
[Crawley] p. 112Definition of automorphismdf-pautN 41240
[Crawley] p. 113Lemma Ccdlemc 41446  cdlemc3 41442  cdlemc4 41443
[Crawley] p. 113Lemma Dcdlemd 41456  cdlemd1 41447  cdlemd2 41448  cdlemd3 41449  cdlemd4 41450  cdlemd5 41451  cdlemd6 41452  cdlemd7 41453  cdlemd8 41454  cdlemd9 41455  cdleme31sde 41634  cdleme31se 41631  cdleme31se2 41632  cdleme31snd 41635  cdleme32a 41690  cdleme32b 41691  cdleme32c 41692  cdleme32d 41693  cdleme32e 41694  cdleme32f 41695  cdleme32fva 41686  cdleme32fva1 41687  cdleme32fvcl 41689  cdleme32le 41696  cdleme48fv 41748  cdleme4gfv 41756  cdleme50eq 41790  cdleme50f 41791  cdleme50f1 41792  cdleme50f1o 41795  cdleme50laut 41796  cdleme50ldil 41797  cdleme50lebi 41789  cdleme50rn 41794  cdleme50rnlem 41793  cdlemeg49le 41760  cdlemeg49lebilem 41788
[Crawley] p. 113Lemma Ecdleme 41809  cdleme00a 41458  cdleme01N 41470  cdleme02N 41471  cdleme0a 41460  cdleme0aa 41459  cdleme0b 41461  cdleme0c 41462  cdleme0cp 41463  cdleme0cq 41464  cdleme0dN 41465  cdleme0e 41466  cdleme0ex1N 41472  cdleme0ex2N 41473  cdleme0fN 41467  cdleme0gN 41468  cdleme0moN 41474  cdleme1 41476  cdleme10 41503  cdleme10tN 41507  cdleme11 41519  cdleme11a 41509  cdleme11c 41510  cdleme11dN 41511  cdleme11e 41512  cdleme11fN 41513  cdleme11g 41514  cdleme11h 41515  cdleme11j 41516  cdleme11k 41517  cdleme11l 41518  cdleme12 41520  cdleme13 41521  cdleme14 41522  cdleme15 41527  cdleme15a 41523  cdleme15b 41524  cdleme15c 41525  cdleme15d 41526  cdleme16 41534  cdleme16aN 41508  cdleme16b 41528  cdleme16c 41529  cdleme16d 41530  cdleme16e 41531  cdleme16f 41532  cdleme16g 41533  cdleme19a 41552  cdleme19b 41553  cdleme19c 41554  cdleme19d 41555  cdleme19e 41556  cdleme19f 41557  cdleme1b 41475  cdleme2 41477  cdleme20aN 41558  cdleme20bN 41559  cdleme20c 41560  cdleme20d 41561  cdleme20e 41562  cdleme20f 41563  cdleme20g 41564  cdleme20h 41565  cdleme20i 41566  cdleme20j 41567  cdleme20k 41568  cdleme20l 41571  cdleme20l1 41569  cdleme20l2 41570  cdleme20m 41572  cdleme20y 41551  cdleme20zN 41550  cdleme21 41586  cdleme21d 41579  cdleme21e 41580  cdleme22a 41589  cdleme22aa 41588  cdleme22b 41590  cdleme22cN 41591  cdleme22d 41592  cdleme22e 41593  cdleme22eALTN 41594  cdleme22f 41595  cdleme22f2 41596  cdleme22g 41597  cdleme23a 41598  cdleme23b 41599  cdleme23c 41600  cdleme26e 41608  cdleme26eALTN 41610  cdleme26ee 41609  cdleme26f 41612  cdleme26f2 41614  cdleme26f2ALTN 41613  cdleme26fALTN 41611  cdleme27N 41618  cdleme27a 41616  cdleme27cl 41615  cdleme28c 41621  cdleme3 41486  cdleme30a 41627  cdleme31fv 41639  cdleme31fv1 41640  cdleme31fv1s 41641  cdleme31fv2 41642  cdleme31id 41643  cdleme31sc 41633  cdleme31sdnN 41636  cdleme31sn 41629  cdleme31sn1 41630  cdleme31sn1c 41637  cdleme31sn2 41638  cdleme31so 41628  cdleme35a 41697  cdleme35b 41699  cdleme35c 41700  cdleme35d 41701  cdleme35e 41702  cdleme35f 41703  cdleme35fnpq 41698  cdleme35g 41704  cdleme35h 41705  cdleme35h2 41706  cdleme35sn2aw 41707  cdleme35sn3a 41708  cdleme36a 41709  cdleme36m 41710  cdleme37m 41711  cdleme38m 41712  cdleme38n 41713  cdleme39a 41714  cdleme39n 41715  cdleme3b 41478  cdleme3c 41479  cdleme3d 41480  cdleme3e 41481  cdleme3fN 41482  cdleme3fa 41485  cdleme3g 41483  cdleme3h 41484  cdleme4 41487  cdleme40m 41716  cdleme40n 41717  cdleme40v 41718  cdleme40w 41719  cdleme41fva11 41726  cdleme41sn3aw 41723  cdleme41sn4aw 41724  cdleme41snaw 41725  cdleme42a 41720  cdleme42b 41727  cdleme42c 41721  cdleme42d 41722  cdleme42e 41728  cdleme42f 41729  cdleme42g 41730  cdleme42h 41731  cdleme42i 41732  cdleme42k 41733  cdleme42ke 41734  cdleme42keg 41735  cdleme42mN 41736  cdleme42mgN 41737  cdleme43aN 41738  cdleme43bN 41739  cdleme43cN 41740  cdleme43dN 41741  cdleme5 41489  cdleme50ex 41808  cdleme50ltrn 41806  cdleme51finvN 41805  cdleme51finvfvN 41804  cdleme51finvtrN 41807  cdleme6 41490  cdleme7 41498  cdleme7a 41492  cdleme7aa 41491  cdleme7b 41493  cdleme7c 41494  cdleme7d 41495  cdleme7e 41496  cdleme7ga 41497  cdleme8 41499  cdleme8tN 41504  cdleme9 41502  cdleme9a 41500  cdleme9b 41501  cdleme9tN 41506  cdleme9taN 41505  cdlemeda 41547  cdlemedb 41546  cdlemednpq 41548  cdlemednuN 41549  cdlemefr27cl 41652  cdlemefr32fva1 41659  cdlemefr32fvaN 41658  cdlemefrs32fva 41649  cdlemefrs32fva1 41650  cdlemefs27cl 41662  cdlemefs32fva1 41672  cdlemefs32fvaN 41671  cdlemesner 41545  cdlemeulpq 41469
[Crawley] p. 114Lemma E4atex 41325  4atexlem7 41324  cdleme0nex 41539  cdleme17a 41535  cdleme17c 41537  cdleme17d 41747  cdleme17d1 41538  cdleme17d2 41744  cdleme18a 41540  cdleme18b 41541  cdleme18c 41542  cdleme18d 41544  cdleme4a 41488
[Crawley] p. 115Lemma Ecdleme21a 41574  cdleme21at 41577  cdleme21b 41575  cdleme21c 41576  cdleme21ct 41578  cdleme21f 41581  cdleme21g 41582  cdleme21h 41583  cdleme21i 41584  cdleme22gb 41543
[Crawley] p. 116Lemma Fcdlemf 41812  cdlemf1 41810  cdlemf2 41811
[Crawley] p. 116Lemma Gcdlemftr1 41816  cdlemg16 41906  cdlemg28 41953  cdlemg28a 41942  cdlemg28b 41952  cdlemg3a 41846  cdlemg42 41978  cdlemg43 41979  cdlemg44 41982  cdlemg44a 41980  cdlemg46 41984  cdlemg47 41985  cdlemg9 41883  ltrnco 41968  ltrncom 41987  tgrpabl 42000  trlco 41976
[Crawley] p. 116Definition of Gdf-tgrp 41992
[Crawley] p. 117Lemma Gcdlemg17 41926  cdlemg17b 41911
[Crawley] p. 117Definition of Edf-edring-rN 42005  df-edring 42006
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 42009
[Crawley] p. 118Remarktendopltp 42029
[Crawley] p. 118Lemma Hcdlemh 42066  cdlemh1 42064  cdlemh2 42065
[Crawley] p. 118Lemma Icdlemi 42069  cdlemi1 42067  cdlemi2 42068
[Crawley] p. 118Lemma Jcdlemj1 42070  cdlemj2 42071  cdlemj3 42072  tendocan 42073
[Crawley] p. 118Lemma Kcdlemk 42223  cdlemk1 42080  cdlemk10 42092  cdlemk11 42098  cdlemk11t 42195  cdlemk11ta 42178  cdlemk11tb 42180  cdlemk11tc 42194  cdlemk11u-2N 42138  cdlemk11u 42120  cdlemk12 42099  cdlemk12u-2N 42139  cdlemk12u 42121  cdlemk13-2N 42125  cdlemk13 42101  cdlemk14-2N 42127  cdlemk14 42103  cdlemk15-2N 42128  cdlemk15 42104  cdlemk16-2N 42129  cdlemk16 42106  cdlemk16a 42105  cdlemk17-2N 42130  cdlemk17 42107  cdlemk18-2N 42135  cdlemk18-3N 42149  cdlemk18 42117  cdlemk19-2N 42136  cdlemk19 42118  cdlemk19u 42219  cdlemk1u 42108  cdlemk2 42081  cdlemk20-2N 42141  cdlemk20 42123  cdlemk21-2N 42140  cdlemk21N 42122  cdlemk22-3 42150  cdlemk22 42142  cdlemk23-3 42151  cdlemk24-3 42152  cdlemk25-3 42153  cdlemk26-3 42155  cdlemk26b-3 42154  cdlemk27-3 42156  cdlemk28-3 42157  cdlemk29-3 42160  cdlemk3 42082  cdlemk30 42143  cdlemk31 42145  cdlemk32 42146  cdlemk33N 42158  cdlemk34 42159  cdlemk35 42161  cdlemk36 42162  cdlemk37 42163  cdlemk38 42164  cdlemk39 42165  cdlemk39u 42217  cdlemk4 42083  cdlemk41 42169  cdlemk42 42190  cdlemk42yN 42193  cdlemk43N 42212  cdlemk45 42196  cdlemk46 42197  cdlemk47 42198  cdlemk48 42199  cdlemk49 42200  cdlemk5 42085  cdlemk50 42201  cdlemk51 42202  cdlemk52 42203  cdlemk53 42206  cdlemk54 42207  cdlemk55 42210  cdlemk55u 42215  cdlemk56 42220  cdlemk5a 42084  cdlemk5auN 42109  cdlemk5u 42110  cdlemk6 42086  cdlemk6u 42111  cdlemk7 42097  cdlemk7u-2N 42137  cdlemk7u 42119  cdlemk8 42087  cdlemk9 42088  cdlemk9bN 42089  cdlemki 42090  cdlemkid 42185  cdlemkj-2N 42131  cdlemkj 42112  cdlemksat 42095  cdlemksel 42094  cdlemksv 42093  cdlemksv2 42096  cdlemkuat 42115  cdlemkuel-2N 42133  cdlemkuel-3 42147  cdlemkuel 42114  cdlemkuv-2N 42132  cdlemkuv2-2 42134  cdlemkuv2-3N 42148  cdlemkuv2 42116  cdlemkuvN 42113  cdlemkvcl 42091  cdlemky 42175  cdlemkyyN 42211  tendoex 42224
[Crawley] p. 120Remarkdva1dim 42234
[Crawley] p. 120Lemma Lcdleml1N 42225  cdleml2N 42226  cdleml3N 42227  cdleml4N 42228  cdleml5N 42229  cdleml6 42230  cdleml7 42231  cdleml8 42232  cdleml9 42233  dia1dim 42310
[Crawley] p. 120Lemma Mdia11N 42297  diaf11N 42298  dialss 42295  diaord 42296  dibf11N 42410  djajN 42386
[Crawley] p. 120Definition of isomorphism mapdiaval 42281
[Crawley] p. 121Lemma Mcdlemm10N 42367  dia2dimlem1 42313  dia2dimlem2 42314  dia2dimlem3 42315  dia2dimlem4 42316  dia2dimlem5 42317  diaf1oN 42379  diarnN 42378  dvheveccl 42361  dvhopN 42365
[Crawley] p. 121Lemma Ncdlemn 42461  cdlemn10 42455  cdlemn11 42460  cdlemn11a 42456  cdlemn11b 42457  cdlemn11c 42458  cdlemn11pre 42459  cdlemn2 42444  cdlemn2a 42445  cdlemn3 42446  cdlemn4 42447  cdlemn4a 42448  cdlemn5 42450  cdlemn5pre 42449  cdlemn6 42451  cdlemn7 42452  cdlemn8 42453  cdlemn9 42454  diclspsn 42443
[Crawley] p. 121Definition of phi(q)df-dic 42422
[Crawley] p. 122Lemma Ndih11 42514  dihf11 42516  dihjust 42466  dihjustlem 42465  dihord 42513  dihord1 42467  dihord10 42472  dihord11b 42471  dihord11c 42473  dihord2 42476  dihord2a 42468  dihord2b 42469  dihord2cN 42470  dihord2pre 42474  dihord2pre2 42475  dihordlem6 42462  dihordlem7 42463  dihordlem7b 42464
[Crawley] p. 122Definition of isomorphism mapdihffval 42479  dihfval 42480  dihval 42481
[Diestel] p. 3Definitiondf-gric 49184  df-grim 49181  isuspgrim 49199
[Diestel] p. 3Section 1.1df-cusgr 30023  df-nbgr 29944
[Diestel] p. 3Definition by df-grisom 49180
[Diestel] p. 4Section 1.1df-isubgr 49164  df-subgr 29879  uhgrspan1 29914  uhgrspansubgr 29902
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 30165  vtxdgoddnumeven 30164
[Diestel] p. 27Section 1.10df-ushgr 29667
[EGA] p. 80Notation 1.1.1rspecval 34566
[EGA] p. 80Proposition 1.1.2zartop 34578
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34570  zarcls1 34571
[EGA] p. 81Corollary 1.1.8zart0 34581
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34584
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34587
[Eisenberg] p. 67Definition 5.3df-dif 4050
[Eisenberg] p. 82Definition 6.3dfom3 9675
[Eisenberg] p. 125Definition 8.21df-map 8877
[Eisenberg] p. 216Example 13.2(4)omenps 9683
[Eisenberg] p. 310Theorem 19.8cardprc 10088
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10666
[Enderton] p. 18Axiom of Empty Setaxnul 5262
[Enderton] p. 19Definitiondf-tp 4593
[Enderton] p. 26Exercise 5unissb 4904
[Enderton] p. 26Exercise 10pwel 5347
[Enderton] p. 28Exercise 7(b)pwun 5548
[Enderton] p. 30Theorem "Distributive laws"iinin1 5042  iinin2 5041  iinun2 5034  iunin1 5033  iunin1f 33224  iunin2 5032  uniin1 5036  uniin2 5037
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5040  iundif2 5035
[Enderton] p. 32Exercise 20unineq 4236
[Enderton] p. 33Exercise 23iinuni 5061
[Enderton] p. 33Exercise 25iununi 5062
[Enderton] p. 33Exercise 24(a)iinpw 5069
[Enderton] p. 33Exercise 24(b)iunpw 7809  iunpwss 5070
[Enderton] p. 36Definitionopthwiener 5491
[Enderton] p. 38Exercise 6(a)unipw 5422
[Enderton] p. 38Exercise 6(b)pwuni 4909
[Enderton] p. 41Lemma 3Dopeluu 5443  rnex 7946  rnexg 7938
[Enderton] p. 41Exercise 8dmuni 5903  rnuni 6152
[Enderton] p. 42Definition of a functiondffun7 6587  dffun8 6588
[Enderton] p. 43Definition of function valuefunfv2 6996
[Enderton] p. 43Definition of single-rootedfuncnv 6631
[Enderton] p. 44Definition (d)dfima2 6070  dfima3 6071
[Enderton] p. 47Theorem 3Hfvco2 7005
[Enderton] p. 49Axiom of Choice (first form)ac7 10578  ac7g 10579  df-ac 10222  dfac2 10237  dfac2a 10235  dfac2b 10236  dfac3 10227  dfac7 10238
[Enderton] p. 50Theorem 3K(a)imauni 7273
[Enderton] p. 52Definitiondf-map 8877
[Enderton] p. 53Exercise 21coass 6284
[Enderton] p. 53Exercise 27dmco 6269
[Enderton] p. 53Exercise 14(a)funin 6638
[Enderton] p. 53Exercise 22(a)imass2 6067
[Enderton] p. 54Remarkixpf 8976  ixpssmap 8988
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8954
[Enderton] p. 55Axiom of Choice (second form)ac9 10588  ac9s 10598
[Enderton] p. 56Theorem 3Meqvrelref 39818  erref 8766
[Enderton] p. 57Lemma 3Neqvrelthi 39821  erthi 8802
[Enderton] p. 57Definitiondf-ec 8747
[Enderton] p. 58Definitiondf-qs 8751
[Enderton] p. 61Exercise 35df-ec 8747
[Enderton] p. 65Exercise 56(a)dmun 5899
[Enderton] p. 68Definition of successordf-suc 6386
[Enderton] p. 71Definitiondf-tr 5216  dftr4 5221
[Enderton] p. 72Theorem 4Eunisuc 6462  unisucg 6461
[Enderton] p. 73Exercise 6unisuc 6462  unisucg 6461
[Enderton] p. 73Exercise 5(a)truni 5231
[Enderton] p. 73Exercise 5(b)trint 5233  trintALT 46054
[Enderton] p. 79Theorem 4I(A1)nna0 8641
[Enderton] p. 79Theorem 4I(A2)nnasuc 8643  onasuc 8564
[Enderton] p. 79Definition of operation valuedf-ov 7446
[Enderton] p. 80Theorem 4J(A1)nnm0 8642
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8644  onmsuc 8565
[Enderton] p. 81Theorem 4K(1)nnaass 8659
[Enderton] p. 81Theorem 4K(2)nna0r 8646  nnacom 8654
[Enderton] p. 81Theorem 4K(3)nndi 8660
[Enderton] p. 81Theorem 4K(4)nnmass 8661
[Enderton] p. 81Theorem 4K(5)nnmcom 8663
[Enderton] p. 82Exercise 16nnm0r 8647  nnmsucr 8662
[Enderton] p. 88Exercise 23nnaordex 8675
[Enderton] p. 129Definitiondf-en 9002
[Enderton] p. 132Theorem 6B(b)canth 7397
[Enderton] p. 133Exercise 1xpomen 10121
[Enderton] p. 133Exercise 2qnnen 16410
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9250
[Enderton] p. 135Corollary 6Cphp3 9252
[Enderton] p. 136Corollary 6Enneneq 9249
[Enderton] p. 136Corollary 6D(a)pssinf 9281
[Enderton] p. 136Corollary 6D(b)ominf 9283
[Enderton] p. 137Lemma 6Fpssnn 9212
[Enderton] p. 138Corollary 6Gssfi 9216
[Enderton] p. 139Theorem 6H(c)mapen 9188
[Enderton] p. 142Theorem 6I(3)xpdjuen 10285
[Enderton] p. 142Theorem 6I(4)mapdjuen 10286
[Enderton] p. 143Theorem 6Jdju0en 10281  dju1en 10277
[Enderton] p. 144Exercise 13iunfi 9360  unifi 9361  unifi2 9362
[Enderton] p. 144Corollary 6Kundif2 4434  unfi 9214  unfi2 9330
[Enderton] p. 145Figure 38ffoss 7982
[Enderton] p. 145Definitiondf-dom 9003
[Enderton] p. 146Example 1domen 9016  domeng 9017
[Enderton] p. 146Example 3nndomo 9261  nnsdom 9682  nnsdomg 9319
[Enderton] p. 149Theorem 6L(a)djudom2 10289
[Enderton] p. 149Theorem 6L(c)mapdom1 9189  xpdom1 9123  xpdom1g 9121  xpdom2g 9120
[Enderton] p. 149Theorem 6L(d)mapdom2 9195
[Enderton] p. 151Theorem 6Mzorn 10612  zorng 10609
[Enderton] p. 151Theorem 6M(4)ac8 10597  dfac5 10234
[Enderton] p. 159Theorem 6Qunictb 10687
[Enderton] p. 164Exampleinfdif 10313
[Enderton] p. 168Definitiondf-po 5563
[Enderton] p. 192Theorem 7M(a)oneli 6496
[Enderton] p. 192Theorem 7M(b)ontr1 6428
[Enderton] p. 192Theorem 7M(c)onirri 6495
[Enderton] p. 193Corollary 7N(b)0elon 6436
[Enderton] p. 193Corollary 7N(c)onsuci 7874
[Enderton] p. 193Corollary 7N(d)ssonunii 7819
[Enderton] p. 194Remarkonprc 7816
[Enderton] p. 194Exercise 16suc11 6490
[Enderton] p. 197Definitiondf-card 10047
[Enderton] p. 197Theorem 7Pcarden 10662
[Enderton] p. 200Exercise 25tfis 7890
[Enderton] p. 202Lemma 7Tr1tr 9810
[Enderton] p. 202Definitiondf-r1 9795
[Enderton] p. 202Theorem 7Qr1val1 9820
[Enderton] p. 204Theorem 7V(b)rankval4 9911  rankval4b 9907
[Enderton] p. 206Theorem 7X(b)en2lp 9634
[Enderton] p. 207Exercise 30rankpr 9898  rankprb 9892  rankpw 9883  rankpwi 9859  rankuniss 9910
[Enderton] p. 207Exercise 34opthreg 9646
[Enderton] p. 208Exercise 35suc11reg 9647
[Enderton] p. 212Definition of alephalephval3 10216
[Enderton] p. 213Theorem 8A(a)alephord2 10182
[Enderton] p. 213Theorem 8A(b)cardalephex 10196
[Enderton] p. 218Theorem Schema 8Eonfununi 8377
[Enderton] p. 222Definitiondf-kard 35918
[Enderton] p. 222Definition of kardkarden 9986  kardex 9984
[Enderton] p. 238Theorem 8Roeoa 8634
[Enderton] p. 238Theorem 8Soeoe 8636
[Enderton] p. 240Exercise 25oarec 8598
[Enderton] p. 257Definition of cofinalitycflm 10354
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17845
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17787
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18756  mrieqv2d 17842  mrieqvd 17841
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17846
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17851  mreexexlem2d 17848
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18762  mreexfidimd 17853
[Frege1879] p. 11Statementdf3or2 44960
[Frege1879] p. 12Statementdf3an2 44961  dfxor4 44958  dfxor5 44959
[Frege1879] p. 26Axiom 1ax-frege1 44982
[Frege1879] p. 26Axiom 2ax-frege2 44983
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44987
[Frege1879] p. 31Proposition 4frege4 44991
[Frege1879] p. 32Proposition 5frege5 44992
[Frege1879] p. 33Proposition 6frege6 44998
[Frege1879] p. 34Proposition 7frege7 45000
[Frege1879] p. 35Axiom 8ax-frege8 45001  axfrege8 44999
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38560
[Frege1879] p. 35Proposition 9frege9 45004
[Frege1879] p. 36Proposition 10frege10 45012
[Frege1879] p. 36Proposition 11frege11 45006
[Frege1879] p. 37Proposition 12frege12 45005
[Frege1879] p. 37Proposition 13frege13 45014
[Frege1879] p. 37Proposition 14frege14 45015
[Frege1879] p. 38Proposition 15frege15 45018
[Frege1879] p. 38Proposition 16frege16 45008
[Frege1879] p. 39Proposition 17frege17 45013
[Frege1879] p. 39Proposition 18frege18 45010
[Frege1879] p. 39Proposition 19frege19 45016
[Frege1879] p. 40Proposition 20frege20 45020
[Frege1879] p. 40Proposition 21frege21 45019
[Frege1879] p. 41Proposition 22frege22 45011
[Frege1879] p. 42Proposition 23frege23 45017
[Frege1879] p. 42Proposition 24frege24 45007
[Frege1879] p. 42Proposition 25frege25 45009  rp-frege25 44997
[Frege1879] p. 42Proposition 26frege26 45002
[Frege1879] p. 43Axiom 28ax-frege28 45022
[Frege1879] p. 43Proposition 27frege27 45003
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 45023
[Frege1879] p. 44Axiom 31ax-frege31 45026  axfrege31 45025
[Frege1879] p. 44Proposition 30frege30 45024
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 45027
[Frege1879] p. 44Proposition 33frege33 45028
[Frege1879] p. 45Proposition 34frege34 45029
[Frege1879] p. 45Proposition 35frege35 45030
[Frege1879] p. 45Proposition 36frege36 45031
[Frege1879] p. 46Proposition 37frege37 45032
[Frege1879] p. 46Proposition 38frege38 45033
[Frege1879] p. 46Proposition 39frege39 45034
[Frege1879] p. 46Proposition 40frege40 45035
[Frege1879] p. 47Axiom 41ax-frege41 45037  axfrege41 45036
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 45038
[Frege1879] p. 47Proposition 43frege43 45039
[Frege1879] p. 47Proposition 44frege44 45040
[Frege1879] p. 47Proposition 45frege45 45041
[Frege1879] p. 48Proposition 46frege46 45042
[Frege1879] p. 48Proposition 47frege47 45043
[Frege1879] p. 49Proposition 48frege48 45044
[Frege1879] p. 49Proposition 49frege49 45045
[Frege1879] p. 49Proposition 50frege50 45046
[Frege1879] p. 50Axiom 52ax-frege52a 45049  ax-frege52c 45080  frege52aid 45050  frege52b 45081
[Frege1879] p. 50Axiom 54ax-frege54a 45054  ax-frege54c 45084  frege54b 45085
[Frege1879] p. 50Proposition 51frege51 45047
[Frege1879] p. 50Proposition 52dfsbcq 3744
[Frege1879] p. 50Proposition 53frege53a 45052  frege53aid 45051  frege53b 45082  frege53c 45106
[Frege1879] p. 50Proposition 54biid 264  eqid 2763
[Frege1879] p. 50Proposition 55frege55a 45060  frege55aid 45057  frege55b 45089  frege55c 45110  frege55cor1a 45061  frege55lem2a 45059  frege55lem2b 45088  frege55lem2c 45109
[Frege1879] p. 50Proposition 56frege56a 45063  frege56aid 45062  frege56b 45090  frege56c 45111
[Frege1879] p. 51Axiom 58ax-frege58a 45067  ax-frege58b 45093  frege58bid 45094  frege58c 45113
[Frege1879] p. 51Proposition 57frege57a 45065  frege57aid 45064  frege57b 45091  frege57c 45112
[Frege1879] p. 51Proposition 58spsbc 3755
[Frege1879] p. 51Proposition 59frege59a 45069  frege59b 45096  frege59c 45114
[Frege1879] p. 52Proposition 60frege60a 45070  frege60b 45097  frege60c 45115
[Frege1879] p. 52Proposition 61frege61a 45071  frege61b 45098  frege61c 45116
[Frege1879] p. 52Proposition 62frege62a 45072  frege62b 45099  frege62c 45117
[Frege1879] p. 52Proposition 63frege63a 45073  frege63b 45100  frege63c 45118
[Frege1879] p. 53Proposition 64frege64a 45074  frege64b 45101  frege64c 45119
[Frege1879] p. 53Proposition 65frege65a 45075  frege65b 45102  frege65c 45120
[Frege1879] p. 54Proposition 66frege66a 45076  frege66b 45103  frege66c 45121
[Frege1879] p. 54Proposition 67frege67a 45077  frege67b 45104  frege67c 45122
[Frege1879] p. 54Proposition 68frege68a 45078  frege68b 45105  frege68c 45123
[Frege1879] p. 55Definition 69dffrege69 45124
[Frege1879] p. 58Proposition 70frege70 45125
[Frege1879] p. 59Proposition 71frege71 45126
[Frege1879] p. 59Proposition 72frege72 45127
[Frege1879] p. 59Proposition 73frege73 45128
[Frege1879] p. 60Definition 76dffrege76 45131
[Frege1879] p. 60Proposition 74frege74 45129
[Frege1879] p. 60Proposition 75frege75 45130
[Frege1879] p. 62Proposition 77frege77 45132  frege77d 44938
[Frege1879] p. 63Proposition 78frege78 45133
[Frege1879] p. 63Proposition 79frege79 45134
[Frege1879] p. 63Proposition 80frege80 45135
[Frege1879] p. 63Proposition 81frege81 45136  frege81d 44939
[Frege1879] p. 64Proposition 82frege82 45137
[Frege1879] p. 65Proposition 83frege83 45138  frege83d 44940
[Frege1879] p. 65Proposition 84frege84 45139
[Frege1879] p. 66Proposition 85frege85 45140
[Frege1879] p. 66Proposition 86frege86 45141
[Frege1879] p. 66Proposition 87frege87 45142  frege87d 44942
[Frege1879] p. 67Proposition 88frege88 45143
[Frege1879] p. 68Proposition 89frege89 45144
[Frege1879] p. 68Proposition 90frege90 45145
[Frege1879] p. 68Proposition 91frege91 45146  frege91d 44943
[Frege1879] p. 69Proposition 92frege92 45147
[Frege1879] p. 70Proposition 93frege93 45148
[Frege1879] p. 70Proposition 94frege94 45149
[Frege1879] p. 70Proposition 95frege95 45150
[Frege1879] p. 71Definition 99dffrege99 45154
[Frege1879] p. 71Proposition 96frege96 45151  frege96d 44941
[Frege1879] p. 71Proposition 97frege97 45152  frege97d 44944
[Frege1879] p. 71Proposition 98frege98 45153  frege98d 44945
[Frege1879] p. 72Proposition 100frege100 45155
[Frege1879] p. 72Proposition 101frege101 45156
[Frege1879] p. 72Proposition 102frege102 45157  frege102d 44946
[Frege1879] p. 73Proposition 103frege103 45158
[Frege1879] p. 73Proposition 104frege104 45159
[Frege1879] p. 73Proposition 105frege105 45160
[Frege1879] p. 73Proposition 106frege106 45161  frege106d 44947
[Frege1879] p. 74Proposition 107frege107 45162
[Frege1879] p. 74Proposition 108frege108 45163  frege108d 44948
[Frege1879] p. 74Proposition 109frege109 45164  frege109d 44949
[Frege1879] p. 75Proposition 110frege110 45165
[Frege1879] p. 75Proposition 111frege111 45166  frege111d 44951
[Frege1879] p. 76Proposition 112frege112 45167
[Frege1879] p. 76Proposition 113frege113 45168
[Frege1879] p. 76Proposition 114frege114 45169  frege114d 44950
[Frege1879] p. 77Definition 115dffrege115 45170
[Frege1879] p. 77Proposition 116frege116 45171
[Frege1879] p. 78Proposition 117frege117 45172
[Frege1879] p. 78Proposition 118frege118 45173
[Frege1879] p. 78Proposition 119frege119 45174
[Frege1879] p. 78Proposition 120frege120 45175
[Frege1879] p. 79Proposition 121frege121 45176
[Frege1879] p. 79Proposition 122frege122 45177  frege122d 44952
[Frege1879] p. 79Proposition 123frege123 45178
[Frege1879] p. 80Proposition 124frege124 45179  frege124d 44953
[Frege1879] p. 81Proposition 125frege125 45180
[Frege1879] p. 81Proposition 126frege126 45181  frege126d 44954
[Frege1879] p. 82Proposition 127frege127 45182
[Frege1879] p. 83Proposition 128frege128 45183
[Frege1879] p. 83Proposition 129frege129 45184  frege129d 44955
[Frege1879] p. 84Proposition 130frege130 45185
[Frege1879] p. 85Proposition 131frege131 45186  frege131d 44956
[Frege1879] p. 86Proposition 132frege132 45187
[Frege1879] p. 86Proposition 133frege133 45188  frege133d 44957
[Fremlin1] p. 13Definition 111G (b)df-salgen 47528
[Fremlin1] p. 13Definition 111G (d)borelmbl 47851
[Fremlin1] p. 13Proposition 111G (b)salgenss 47551
[Fremlin1] p. 14Definition 112Aismea 47666
[Fremlin1] p. 15Remark 112B (d)psmeasure 47686
[Fremlin1] p. 15Property 112C (a)meadjun 47677  meadjunre 47691
[Fremlin1] p. 15Property 112C (b)meassle 47678
[Fremlin1] p. 15Property 112C (c)meaunle 47679
[Fremlin1] p. 16Property 112C (d)iundjiun 47675  meaiunle 47684  meaiunlelem 47683
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47696  meaiuninc2 47697  meaiuninc3 47700  meaiuninc3v 47699  meaiunincf 47698  meaiuninclem 47695
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47702  meaiininc2 47703  meaiininclem 47701
[Fremlin1] p. 19Theorem 113Ccaragen0 47721  caragendifcl 47729  caratheodory 47743  omelesplit 47733
[Fremlin1] p. 19Definition 113Aisome 47709  isomennd 47746  isomenndlem 47745
[Fremlin1] p. 19Remark 113B (c)omeunle 47731
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47750  voncmpl 47836
[Fremlin1] p. 19Definition 113A (ii)omessle 47713
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47738  carageniuncllem1 47736  carageniuncllem2 47737  caragenuncl 47728  caragenuncllem 47727  caragenunicl 47739
[Fremlin1] p. 21Remark 113Dcaragenel2d 47747
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47741  caratheodorylem2 47742
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47750
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47809  hoidmv1lelem1 47806  hoidmv1lelem2 47807  hoidmv1lelem3 47808
[Fremlin1] p. 25Definition 114Eisvonmbl 47853
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47809  hoidmvle 47815  hoidmvlelem1 47810  hoidmvlelem2 47811  hoidmvlelem3 47812  hoidmvlelem4 47813  hoidmvlelem5 47814  hsphoidmvle2 47800  hsphoif 47791  hsphoival 47794
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47763
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47771
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47798  hoidmvn0val 47799  hoidmvval 47792  hoidmvval0 47802  hoidmvval0b 47805
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47803  hsphoidmvle 47801
[Fremlin1] p. 30Definition 115Cdf-ovoln 47752  df-voln 47754
[Fremlin1] p. 30Proposition 115D (a)dmovn 47819  ovn0 47781  ovn0lem 47780  ovnf 47778  ovnome 47788  ovnssle 47776  ovnsslelem 47775  ovnsupge0 47772
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47818  ovnhoilem1 47816  ovnhoilem2 47817  vonhoi 47882
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47835  hoidifhspf 47833  hoidifhspval 47823  hoidifhspval2 47830  hoidifhspval3 47834  hspmbl 47844  hspmbllem1 47841  hspmbllem2 47842  hspmbllem3 47843
[Fremlin1] p. 31Definition 115Evoncmpl 47836  vonmea 47789
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47787  ovnsubadd2 47861  ovnsubadd2lem 47860  ovnsubaddlem1 47785  ovnsubaddlem2 47786
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47846  hoimbl2 47880  hoimbllem 47845  hspdifhsp 47831  opnvonmbl 47849  opnvonmbllem2 47848
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47851
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47894  iccvonmbllem 47893  ioovonmbl 47892
[Fremlin1] p. 32Proposition 115G (d)vonicc 47900  vonicclem2 47899  vonioo 47897  vonioolem2 47896  vonn0icc 47903  vonn0icc2 47907  vonn0ioo 47902  vonn0ioo2 47905
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47904  snvonmbl 47901  vonct 47908  vonsn 47906
[Fremlin1] p. 35Lemma 121Asubsalsal 47574
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47573  subsaliuncllem 47572
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47940  salpreimalegt 47924  salpreimaltle 47941
[Fremlin1] p. 35Proposition 121B (i)issmf 47943  issmff 47949  issmflem 47942
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47960  issmflelem 47959  smfpreimale 47969
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47971  issmfgtlem 47970
[Fremlin1] p. 36Definition 121Cdf-smblfn 47911  issmf 47943  issmff 47949  issmfge 47985  issmfgelem 47984  issmfgt 47971  issmfgtlem 47970  issmfle 47960  issmflelem 47959  issmflem 47942
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47922  salpreimagtlt 47945  salpreimalelt 47944
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47985  issmfgelem 47984
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47968
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47966  cnfsmf 47955
[Fremlin1] p. 36Proposition 121D (c)decsmf 47982  decsmflem 47981  incsmf 47957  incsmflem 47956
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47916  pimconstlt1 47917  smfconst 47964
[Fremlin1] p. 37Proposition 121E (b)smfadd 47980  smfaddlem1 47978  smfaddlem2 47979
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 48011
[Fremlin1] p. 37Proposition 121E (d)smfmul 48010  smfmullem1 48006  smfmullem2 48007  smfmullem3 48008  smfmullem4 48009
[Fremlin1] p. 37Proposition 121E (e)smfdiv 48012
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 48015  smfpimbor1lem2 48014
[Fremlin1] p. 37Proposition 121E (g)smfco 48017
[Fremlin1] p. 37Proposition 121E (h)smfres 48005
[Fremlin1] p. 38Proposition 121E (e)smfrec 48004
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 48013  smfresal 48003
[Fremlin1] p. 38Proposition 121F (a)smflim 47992  smflim2 48021  smflimlem1 47986  smflimlem2 47987  smflimlem3 47988  smflimlem4 47989  smflimlem5 47990  smflimlem6 47991  smflimmpt 48025
[Fremlin1] p. 38Proposition 121F (b)smfsup 48029  smfsuplem1 48026  smfsuplem2 48027  smfsuplem3 48028  smfsupmpt 48030  smfsupxr 48031
[Fremlin1] p. 38Proposition 121F (c)smfinf 48033  smfinflem 48032  smfinfmpt 48034
[Fremlin1] p. 39Remark 121Gsmflim 47992  smflim2 48021  smflimmpt 48025
[Fremlin1] p. 39Proposition 121Fsmfpimcc 48023
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 48053  smfdivdmmbl2 48056  smfinfdmmbl 48064  smfinfdmmbllem 48063  smfsupdmmbl 48060  smfsupdmmbllem 48059
[Fremlin1] p. 39Proposition 121F (d)smflimsup 48043  smflimsuplem2 48036  smflimsuplem6 48040  smflimsuplem7 48041  smflimsuplem8 48042  smflimsupmpt 48044
[Fremlin1] p. 39Proposition 121F (e)smfliminf 48046  smfliminflem 48045  smfliminfmpt 48047
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47911
[Fremlin1], p. 38Proposition 121F (b)fsupdm 48057  fsupdm2 48058
[Fremlin1], p. 39Proposition 121Hadddmmbl 48048  adddmmbl2 48049  finfdm 48061  finfdm2 48062  fsupdm 48057  fsupdm2 48058  muldmmbl 48050  muldmmbl2 48051
[Fremlin1], p. 39Proposition 121F (c)finfdm 48061  finfdm2 48062
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25887
[Fremlin5] p. 213Lemma 565Cauniioovol 25930
[Fremlin5] p. 214Lemma 565Cauniioombl 25940
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38808
[Fremlin5] p. 220Theorem 565Maftc1anc 38811
[FreydScedrov] p. 283Axiom of Infinityax-inf 9666  inf1 9650  inf2 9651
[Gleason] p. 117Proposition 9-2.1df-enq 11023  enqer 11033
[Gleason] p. 117Proposition 9-2.2df-1nq 11028  df-nq 11024
[Gleason] p. 117Proposition 9-2.3df-plpq 11020  df-plq 11026
[Gleason] p. 119Proposition 9-2.4caovmo 7682  df-mpq 11021  df-mq 11027
[Gleason] p. 119Proposition 9-2.5df-rq 11029
[Gleason] p. 119Proposition 9-2.6ltexnq 11087
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11088  ltbtwnnq 11090
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11083
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11084
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11091
[Gleason] p. 121Definition 9-3.1df-np 11093
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11105
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11107
[Gleason] p. 122Definitiondf-1p 11094
[Gleason] p. 122Remark (1)prub 11106
[Gleason] p. 122Lemma 9-3.4prlem934 11145
[Gleason] p. 122Proposition 9-3.2df-ltp 11097
[Gleason] p. 122Proposition 9-3.3ltsopr 11144  psslinpr 11143  supexpr 11166  suplem1pr 11164  suplem2pr 11165
[Gleason] p. 123Proposition 9-3.5addclpr 11130  addclprlem1 11128  addclprlem2 11129  df-plp 11095
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11134
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11133
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11146
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11155  ltexprlem1 11148  ltexprlem2 11149  ltexprlem3 11150  ltexprlem4 11151  ltexprlem5 11152  ltexprlem6 11153  ltexprlem7 11154
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11157  ltaprlem 11156
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11158
[Gleason] p. 124Lemma 9-3.6prlem936 11159
[Gleason] p. 124Proposition 9-3.7df-mp 11096  mulclpr 11132  mulclprlem 11131  reclem2pr 11160
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11141
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11136
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11135
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11140
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11163  reclem3pr 11161  reclem4pr 11162
[Gleason] p. 126Proposition 9-4.1df-enr 11167  enrer 11175
[Gleason] p. 126Proposition 9-4.2df-0r 11172  df-1r 11173  df-nr 11168
[Gleason] p. 126Proposition 9-4.3df-mr 11170  df-plr 11169  negexsr 11214  recexsr 11219  recexsrlem 11215
[Gleason] p. 127Proposition 9-4.4df-ltr 11171
[Gleason] p. 130Proposition 10-1.3creui 12342  creur 12341  cru 12339
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11300  axcnre 11276
[Gleason] p. 132Definition 10-3.1crim 15311  crimd 15428  crimi 15389  crre 15310  crred 15427  crrei 15388
[Gleason] p. 132Definition 10-3.2remim 15313  remimd 15394
[Gleason] p. 133Definition 10.36absval2 15480  absval2d 15644  absval2i 15594
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15337  cjaddd 15416  cjaddi 15384
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15338  cjmuld 15417  cjmuli 15385
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15336  cjcjd 15395  cjcji 15367
[Gleason] p. 133Proposition 10-3.4(f)cjre 15335  cjreb 15319  cjrebd 15398  cjrebi 15370  cjred 15422  rere 15318  rereb 15316  rerebd 15397  rerebi 15369  rered 15420
[Gleason] p. 133Proposition 10-3.4(h)addcj 15344  addcjd 15408  addcji 15379
[Gleason] p. 133Proposition 10-3.7(a)absval 15434
[Gleason] p. 133Proposition 10-3.7(b)abscj 15475  abscjd 15649  abscji 15598
[Gleason] p. 133Proposition 10-3.7(c)abs00 15485  abs00d 15645  abs00i 15595  absne0d 15646
[Gleason] p. 133Proposition 10-3.7(d)releabs 15518  releabsd 15650  releabsi 15599
[Gleason] p. 133Proposition 10-3.7(f)absmul 15490  absmuld 15653  absmuli 15601
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15478  sqabsaddi 15602
[Gleason] p. 133Proposition 10-3.7(h)abstri 15527  abstrid 15655  abstrii 15605
[Gleason] p. 134Definition 10-4.1df-exp 14232  exp0 14235  expp1 14238  expp1d 14317
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 27037  cxpaddd 27075  expadd 14274  expaddd 14318  expaddz 14276
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 27046  cxpmuld 27095  expmul 14277  expmuld 14319  expmulz 14278
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 27043  mulcxpd 27086  mulexp 14271  mulexpd 14331  mulexpz 14272
[Gleason] p. 140Exercise 1znnen 16409
[Gleason] p. 141Definition 11-2.1fzval 13668
[Gleason] p. 168Proposition 12-2.1(a)climadd 15828  rlimadd 15839  rlimdiv 15842
[Gleason] p. 168Proposition 12-2.1(b)climsub 15830  rlimsub 15840
[Gleason] p. 168Proposition 12-2.1(c)climmul 15829  rlimmul 15841
[Gleason] p. 171Corollary 12-2.2climmulc2 15833
[Gleason] p. 172Corollary 12-2.5climrecl 15779
[Gleason] p. 172Proposition 12-2.4(c)climabs 15800  climcj 15801  climim 15803  climre 15802  rlimabs 15805  rlimcj 15806  rlimim 15808  rlimre 15807
[Gleason] p. 173Definition 12-3.1df-ltxr 11375  df-xr 11374  ltxr 13271
[Gleason] p. 175Definition 12-4.1df-limsup 15667  limsupval 15670
[Gleason] p. 180Theorem 12-5.1climsup 15866
[Gleason] p. 180Theorem 12-5.3caucvg 15875  caucvgb 15876  caucvgbf 46704  caucvgr 15872  climcau 15867
[Gleason] p. 182Exercise 3cvgcmp 16012
[Gleason] p. 182Exercise 4cvgrat 16081
[Gleason] p. 195Theorem 13-2.12abs1m 15532
[Gleason] p. 217Lemma 13-4.1btwnzge0 13995
[Gleason] p. 223Definition 14-1.1df-met 21702
[Gleason] p. 223Definition 14-1.1(a)met0 24692  xmet0 24691
[Gleason] p. 223Definition 14-1.1(b)metgt0 24708
[Gleason] p. 223Definition 14-1.1(c)metsym 24699
[Gleason] p. 223Definition 14-1.1(d)mettri 24701  mstri 24818  xmettri 24700  xmstri 24817
[Gleason] p. 225Definition 14-1.5xpsmet 24731
[Gleason] p. 230Proposition 14-2.6txlm 23997
[Gleason] p. 240Theorem 14-4.3metcnp4 25661
[Gleason] p. 240Proposition 14-4.2metcnp3 24889
[Gleason] p. 243Proposition 14-4.16addcn 25215  addcn2 15790  mulcn 25217  mulcn2 15792  subcn 25216  subcn2 15791
[Gleason] p. 295Remarkbcval3 14477  bcval4 14478
[Gleason] p. 295Equation 2bcpasc 14492
[Gleason] p. 295Definition of binomial coefficientbcval 14475  df-bc 14474
[Gleason] p. 296Remarkbcn0 14481  bcnn 14483
[Gleason] p. 296Theorem 15-2.8binom 16028
[Gleason] p. 308Equation 2ef0 16286
[Gleason] p. 308Equation 3efcj 16287
[Gleason] p. 309Corollary 15-4.3efne0 16293
[Gleason] p. 309Corollary 15-4.4efexp 16298
[Gleason] p. 310Equation 14sinadd 16361
[Gleason] p. 310Equation 15cosadd 16362
[Gleason] p. 311Equation 17sincossq 16373
[Gleason] p. 311Equation 18cosbnd 16378  sinbnd 16377
[Gleason] p. 311Lemma 15-4.7sqeqor 14387  sqeqori 14385
[Gleason] p. 311Definition of ` `df-pi 16267
[Godowski] p. 730Equation SFgoeqi 32905
[GodowskiGreechie] p. 249Equation IV3oai 32300
[Golan] p. 1Remarksrgisid 20465
[Golan] p. 1Definitiondf-srg 20443
[Golan] p. 149Definitiondf-slmd 33832
[Gonshor] p. 7Definitiondf-cuts 28176
[Gonshor] p. 9Theorem 2.5lesrec 28215  lesrecd 28216
[Gonshor] p. 10Theorem 2.6cofcut1 28336  cofcut1d 28337
[Gonshor] p. 10Theorem 2.7cofcut2 28338  cofcut2d 28339
[Gonshor] p. 12Theorem 2.9cofcutr 28340  cofcutr1d 28341  cofcutr2d 28342
[Gonshor] p. 13Definitiondf-adds 28376
[Gonshor] p. 14Theorem 3.1addsprop 28392
[Gonshor] p. 15Theorem 3.2addsunif 28418
[Gonshor] p. 17Theorem 3.4mulsprop 28546
[Gonshor] p. 18Theorem 3.5mulsunif 28566
[Gonshor] p. 28Lemma 4.2halfcut 28874
[Gonshor] p. 28Theorem 4.2pw2cut 28876
[Gonshor] p. 30Theorem 4.2addhalfcut 28875
[Gonshor] p. 39Theorem 4.4(b)elreno2 28911
[Gonshor] p. 95Theorem 6.1addbday 28434
[GramKnuthPat], p. 47Definition 2.42df-fwddif 37102
[Gratzer] p. 23Section 0.6df-mre 17785
[Gratzer] p. 27Section 0.6df-mri 17787
[Hall] p. 1Section 1.1df-asslaw 49490  df-cllaw 49488  df-comlaw 49489
[Hall] p. 2Section 1.2df-clintop 49502
[Hall] p. 7Section 1.3df-sgrp2 49523
[Halmos] p. 28Partition ` `df-parts 39992  dfmembpart2 39997
[Halmos] p. 31Theorem 17.3riesz1 32697  riesz2 32698
[Halmos] p. 41Definition of Hermitianhmopadj2 32573
[Halmos] p. 42Definition of projector orderingpjordi 32805
[Halmos] p. 43Theorem 26.1elpjhmop 32817  elpjidm 32816  pjnmopi 32780
[Halmos] p. 44Remarkpjinormi 32319  pjinormii 32308
[Halmos] p. 44Theorem 26.2elpjch 32821  pjrn 32339  pjrni 32334  pjvec 32328
[Halmos] p. 44Theorem 26.3pjnorm2 32359
[Halmos] p. 44Theorem 26.4hmopidmpj 32786  hmopidmpji 32784
[Halmos] p. 45Theorem 27.1pjinvari 32823
[Halmos] p. 45Theorem 27.3pjoci 32812  pjocvec 32329
[Halmos] p. 45Theorem 27.4pjorthcoi 32801
[Halmos] p. 48Theorem 29.2pjssposi 32804
[Halmos] p. 48Theorem 29.3pjssdif1i 32807  pjssdif2i 32806
[Halmos] p. 50Definition of spectrumdf-spec 32487
[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 1828
[Hatcher] p. 25Definitiondf-phtpc 25343  df-phtpy 25322
[Hatcher] p. 26Definitiondf-pco 25356  df-pi1 25359
[Hatcher] p. 26Proposition 1.2phtpcer 25346
[Hatcher] p. 26Proposition 1.3pi1grp 25401
[Hefferon] p. 240Definition 3.12df-dmat 22835  df-dmatalt 49715
[Helfgott] p. 2Theoremtgoldbach 49120
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 49105
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 49117  bgoldbtbnd 49112  bgoldbtbnd 49112  tgblthelfgott 49118
[Helfgott] p. 5Proposition 1.1circlevma 35341
[Helfgott] p. 69Statement 7.49circlemethhgt 35342
[Helfgott] p. 69Statement 7.50hgt750lema 35356  hgt750lemb 35355  hgt750leme 35357  hgt750lemf 35352  hgt750lemg 35353
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 49114  tgoldbachgt 35362  tgoldbachgtALTV 49115  tgoldbachgtd 35361
[Helfgott] p. 70Statement 7.49ax-hgt749 35343
[Herstein] p. 54Exercise 28df-grpo 31125
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19184  grpoideu 31141  mndideu 18963
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19214  grpoinveu 31151
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19245  grpo2inv 31163
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19257  grpoinvop 31165
[Herstein] p. 57Exercise 1dfgrp3e 19279
[Hitchcock] p. 5Rule A3mptnan 1801
[Hitchcock] p. 5Rule A4mptxor 1802
[Hitchcock] p. 5Rule A5mtpxor 1804
[Holland] p. 1519Theorem 2sumdmdi 33052
[Holland] p. 1520Lemma 5cdj1i 33065  cdj3i 33073  cdj3lem1 33066  cdjreui 33064
[Holland] p. 1524Lemma 7mddmdin0i 33063
[Holland95] p. 13Theorem 3.6hlathil 43210
[Holland95] p. 14Line 15hgmapvs 43140
[Holland95] p. 14Line 16hdmaplkr 43162
[Holland95] p. 14Line 17hdmapellkr 43163
[Holland95] p. 14Line 19hdmapglnm2 43160
[Holland95] p. 14Line 20hdmapip0com 43166
[Holland95] p. 14Theorem 3.6hdmapevec2 43085
[Holland95] p. 14Lines 24 and 25hdmapoc 43180
[Holland95] p. 204Definition of involutiondf-srng 21127
[Holland95] p. 212Definition of subspacedf-psubsp 40752
[Holland95] p. 214Lemma 3.3lclkrlem2v 42777
[Holland95] p. 214Definition 3.2df-lpolN 42730
[Holland95] p. 214Definition of nonsingularpnonsingN 41182
[Holland95] p. 215Lemma 3.3(1)dihoml4 42626  poml4N 41202
[Holland95] p. 215Lemma 3.3(2)dochexmid 42717  pexmidALTN 41227  pexmidN 41218
[Holland95] p. 218Theorem 3.6lclkr 42782
[Holland95] p. 218Definition of dual vector spacedf-ldual 40373  ldualset 40374
[Holland95] p. 222Item 1df-lines 40750  df-pointsN 40751
[Holland95] p. 222Item 2df-polarityN 41152
[Holland95] p. 223Remarkispsubcl2N 41196  omllaw4 40495  pol1N 41159  polcon3N 41166
[Holland95] p. 223Definitiondf-psubclN 41184
[Holland95] p. 223Equation for polaritypolval2N 41155
[Holmes] p. 40Definitiondf-xrn 39504
[Hughes] p. 44Equation 1.21bax-his3 31716
[Hughes] p. 47Definition of projection operatordfpjop 32814
[Hughes] p. 49Equation 1.30eighmre 32595  eigre 32467  eigrei 32466
[Hughes] p. 49Equation 1.31eighmorth 32596  eigorth 32470  eigorthi 32469
[Hughes] p. 137Remark (ii)eigposi 32468
[Huneke] p. 1Claim 1frgrncvvdeq 30940
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30936
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30937
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30938
[Huneke] p. 2Claim 2frgrregorufr 30956  frgrregorufr0 30955  frgrregorufrg 30957
[Huneke] p. 2Claim 3frgrhash2wsp 30963  frrusgrord 30972  frrusgrord0 30971
[Huneke] p. 2Statementdf-clwwlknon 30709
[Huneke] p. 2Statement 4frgrwopreglem4 30946
[Huneke] p. 2Statement 5frgrwopreg1 30949  frgrwopreg2 30950  frgrwopregasn 30947  frgrwopregbsn 30948
[Huneke] p. 2Statement 6frgrwopreglem5 30952
[Huneke] p. 2Statement 7fusgreghash2wspv 30966
[Huneke] p. 2Statement 8fusgreghash2wsp 30969
[Huneke] p. 2Statement 9clwlksndivn 30707  numclwlk1 31002  numclwlk1lem1 31000  numclwlk1lem2 31001  numclwwlk1 30992  numclwwlk8 31023
[Huneke] p. 2Definition 3frgrwopreglem1 30943
[Huneke] p. 2Definition 4df-clwlks 30388
[Huneke] p. 2Definition 62clwwlk 30978
[Huneke] p. 2Definition 7numclwwlkovh 31004  numclwwlkovh0 31003
[Huneke] p. 2Statement 10numclwwlk2 31012
[Huneke] p. 2Statement 11rusgrnumwlkg 30599
[Huneke] p. 2Statement 12numclwwlk3 31016
[Huneke] p. 2Statement 13numclwwlk5 31019
[Huneke] p. 2Statement 14numclwwlk7 31022
[Indrzejczak] p. 33Definition ` `Enatded 31034  natded 31034
[Indrzejczak] p. 33Definition ` `Inatded 31034
[Indrzejczak] p. 34Definition ` `Enatded 31034  natded 31034
[Indrzejczak] p. 34Definition ` `Inatded 31034
[Jech] p. 4Definition of classcv 1569  cvjust 2757
[Jech] p. 42Lemma 6.1alephexp1 10691
[Jech] p. 42Equation 6.1alephadd 10689  alephmul 10690
[Jech] p. 43Lemma 6.2infmap 10688  infmap2 10322
[Jech] p. 71Lemma 9.3jech9.3 9849
[Jech] p. 72Equation 9.3df-scott 9956
[Jech] p. 72Exercise 9.1rankval4 9911  rankval4b 9907
[Jech] p. 72Scheme "Collection Principle"cp 9981
[Jech] p. 78Noteopthprc 5719
[JonesMatijasevic] p. 694Definition 2.3rmxyval 44115
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 44203
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 44204
[JonesMatijasevic] p. 695Equation 2.7rmxadd 44127
[JonesMatijasevic] p. 695Equation 2.8rmyadd 44131
[JonesMatijasevic] p. 695Equation 2.9rmxp1 44132  rmyp1 44133
[JonesMatijasevic] p. 695Equation 2.10rmxm1 44134  rmym1 44135
[JonesMatijasevic] p. 695Equation 2.11rmx0 44125  rmx1 44126  rmxluc 44136
[JonesMatijasevic] p. 695Equation 2.12rmy0 44129  rmy1 44130  rmyluc 44137
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 44139
[JonesMatijasevic] p. 695Equation 2.14rmydbl 44140
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 44160  jm2.17b 44161  jm2.17c 44162
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 44193
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 44197
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 44188
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 44163  jm2.24nn 44159
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 44202
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 44208  rmygeid 44164
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 44220
[Juillerat] p. 11Section *5etransc 47498  etransclem47 47496  etransclem48 47497
[Juillerat] p. 12Equation (7)etransclem44 47493
[Juillerat] p. 12Equation *(7)etransclem46 47495
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 47481
[Juillerat] p. 13Proofetransclem35 47484
[Juillerat] p. 13Part of case 2 proven inetransclem38 47487
[Juillerat] p. 13Part of case 2 provenetransclem24 47473
[Juillerat] p. 13Part of case 2: proven inetransclem41 47490
[Juillerat] p. 14Proofetransclem23 47472
[KalishMontague] p. 81Note 1ax-6 2002
[KalishMontague] p. 85Lemma 2equid 2047
[KalishMontague] p. 85Lemma 3equcomi 2052
[KalishMontague] p. 86Lemma 7cbvalivw 2042  cbvaliw 2041  wl-cbvmotv 38637  wl-motae 38639  wl-moteq 38638
[KalishMontague] p. 87Lemma 8spimvw 2021  spimw 2005
[KalishMontague] p. 87Lemma 9spfw 2068  spw 2069
[Kalmbach] p. 14Definition of latticechabs1 32148  chabs1i 32150  chabs2 32149  chabs2i 32151  chjass 32165  chjassi 32118  latabs1 18678  latabs2 18679
[Kalmbach] p. 15Definition of atomdf-at 32970  ela 32971
[Kalmbach] p. 15Definition of coverscvbr2 32915  cvrval2 40523
[Kalmbach] p. 16Definitiondf-ol 40427  df-oml 40428
[Kalmbach] p. 20Definition of commutescmbr 32216  cmbri 32222  cmtvalN 40460  df-cm 32215  df-cmtN 40426
[Kalmbach] p. 22Remarkomllaw5N 40496  pjoml5 32245  pjoml5i 32220
[Kalmbach] p. 22Definitionpjoml2 32243  pjoml2i 32217
[Kalmbach] p. 22Theorem 2(v)cmcm 32246  cmcmi 32224  cmcmii 32229  cmtcomN 40498
[Kalmbach] p. 22Theorem 2(ii)omllaw3 40494  omlsi 32036  pjoml 32068  pjomli 32067
[Kalmbach] p. 22Definition of OML lawomllaw2N 40493
[Kalmbach] p. 23Remarkcmbr2i 32228  cmcm3 32247  cmcm3i 32226  cmcm3ii 32231  cmcm4i 32227  cmt3N 40500  cmt4N 40501  cmtbr2N 40502
[Kalmbach] p. 23Lemma 3cmbr3 32240  cmbr3i 32232  cmtbr3N 40503
[Kalmbach] p. 25Theorem 5fh1 32250  fh1i 32253  fh2 32251  fh2i 32254  omlfh1N 40507
[Kalmbach] p. 65Remarkchjatom 32989  chslej 32130  chsleji 32090  shslej 32012  shsleji 32002
[Kalmbach] p. 65Proposition 1chocin 32127  chocini 32086  chsupcl 31972  chsupval2 32042  h0elch 31887  helch 31875  hsupval2 32041  ocin 31928  ococss 31925  shococss 31926
[Kalmbach] p. 65Definition of subspace sumshsval 31944
[Kalmbach] p. 66Remarkdf-pjh 32027  pjssmi 32797  pjssmii 32313
[Kalmbach] p. 67Lemma 3osum 32277  osumi 32274
[Kalmbach] p. 67Lemma 4pjci 32832
[Kalmbach] p. 103Exercise 6atmd2 33032
[Kalmbach] p. 103Exercise 12mdsl0 32942
[Kalmbach] p. 140Remarkhatomic 32992  hatomici 32991  hatomistici 32994
[Kalmbach] p. 140Proposition 1atlatmstc 40568
[Kalmbach] p. 140Proposition 1(i)atexch 33013  lsatexch 40292
[Kalmbach] p. 140Proposition 1(ii)chcv1 32987  cvlcvr1 40588  cvr1 40659
[Kalmbach] p. 140Proposition 1(iii)cvexch 33006  cvexchi 33001  cvrexch 40669
[Kalmbach] p. 149Remark 2chrelati 32996  hlrelat 40651  hlrelat5N 40650  lrelat 40263
[Kalmbach] p. 153Exercise 5lsmcv 21449  lsmsatcv 40259  spansncv 32285  spansncvi 32284
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 40278  spansncv2 32925
[Kalmbach] p. 266Definitiondf-st 32843
[Kalmbach2] p. 8Definition of adjointdf-adjh 32481
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10758  fpwwe2 10755
[KanamoriPincus] p. 416Corollary 1.3canth4 10759
[KanamoriPincus] p. 417Corollary 1.6canthp1 10766
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10761
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10763
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10776
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10780  gchxpidm 10781
[KanamoriPincus] p. 419Theorem 2.1gchacg 10792  gchhar 10791
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10320  unxpwdom 9610
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10782
[Kreyszig] p. 3Property M1metcl 24681  xmetcl 24680
[Kreyszig] p. 4Property M2meteq0 24688
[Kreyszig] p. 8Definition 1.1-8dscmet 24921
[Kreyszig] p. 12Equation 5conjmul 12061  muleqadd 11987
[Kreyszig] p. 18Definition 1.3-2mopnval 24787
[Kreyszig] p. 19Remarkmopntopon 24788
[Kreyszig] p. 19Theorem T1mopn0 24847  mopnm 24793
[Kreyszig] p. 19Theorem T2unimopn 24845
[Kreyszig] p. 19Definition of neighborhoodneibl 24850
[Kreyszig] p. 20Definition 1.3-3metcnp2 24891
[Kreyszig] p. 25Definition 1.4-1lmbr 23606  lmmbr 25609  lmmbr2 25610
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23728
[Kreyszig] p. 28Theorem 1.4-5lmcau 25664
[Kreyszig] p. 28Definition 1.4-3iscau 25627  iscmet2 25645
[Kreyszig] p. 30Theorem 1.4-7cmetss 25667
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23810  metelcls 25656
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25657  metcld2 25658
[Kreyszig] p. 51Equation 2clmvneg1 25450  lmodvneg1 21210  nvinv 31271  vcm 31208
[Kreyszig] p. 51Equation 1aclm0vs 25446  lmod0vs 21200  slmd0vs 33855  vc0 31206
[Kreyszig] p. 51Equation 1blmodvs0 21201  slmdvs0 33856  vcz 31207
[Kreyszig] p. 58Definition 2.2-1imsmet 31323  ngpmet 24952  nrmmetd 24923
[Kreyszig] p. 59Equation 1imsdval 31318  imsdval2 31319  ncvspds 25512  ngpds 24953
[Kreyszig] p. 63Problem 1nmval 24938  nvnd 31320
[Kreyszig] p. 64Problem 2nmeq0 24967  nmge0 24966  nvge0 31305  nvz 31301
[Kreyszig] p. 64Problem 3nmrtri 24973  nvabs 31304
[Kreyszig] p. 91Definition 2.7-1isblo3i 31433
[Kreyszig] p. 92Equation 2df-nmoo 31377
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31439  blocni 31437
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31438
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25555  ipeq0 21974  ipz 31351
[Kreyszig] p. 135Problem 2cphpyth 25567  pythi 31482
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31486
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25589
[Kreyszig] p. 144Equation 4supcvg 16054
[Kreyszig] p. 144Theorem 3.3-1minvec 25787  minveco 31516
[Kreyszig] p. 196Definition 3.9-1df-aj 31382
[Kreyszig] p. 247Theorem 4.7-2bcth 25680
[Kreyszig] p. 249Theorem 4.7-3ubth 31505
[Kreyszig] p. 470Definition of positive operator orderingleop 32755  leopg 32754
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32773
[Kreyszig] p. 525Theorem 10.1-1htth 31550
[Kulpa] p. 547Theorempoimir 38763
[Kulpa] p. 547Equation (1)poimirlem32 38762
[Kulpa] p. 547Equation (2)poimirlem31 38761
[Kulpa] p. 548Theorembroucube 38764
[Kulpa] p. 548Equation (6)poimirlem26 38756
[Kulpa] p. 548Equation (7)poimirlem27 38757
[Kunen] p. 10Axiom 0ax6e 2415  axnul 5262
[Kunen] p. 11Axiom 3axnul 5262
[Kunen] p. 12Axiom 6zfrep6 5245
[Kunen] p. 24Definition 10.24mapval 8886  mapvalg 8884
[Kunen] p. 30Lemma 10.20fodomg 10627
[Kunen] p. 31Definition 10.24mapex 7976
[Kunen] p. 95Definition 2.1df-r1 9795
[Kunen] p. 97Lemma 2.10r1elss 9841  r1elssi 9840
[Kunen] p. 107Exercise 4rankop 9899  rankopb 9893  rankuni 9906  rankxplim 9923  rankxpsuc 9926
[Kunen2] p. 47Lemma I.9.9relpfr 46139
[Kunen2] p. 53Lemma I.9.21trfr 46147
[Kunen2] p. 53Lemma I.9.24(2)wffr 46146
[Kunen2] p. 53Definition I.9.20tcfr 46148
[Kunen2] p. 95Lemma I.16.2ralabso 46153  rexabso 46154
[Kunen2] p. 96Example I.16.3disjabso 46160  n0abso 46161  ssabso 46159
[Kunen2] p. 111Lemma II.2.4(1)traxext 46162
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 46172
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 46167
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 46170
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 46171
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 46166
[Kunen2] p. 112Corollary II.2.5wfaxext 46178  wfaxpr 46183  wfaxreg 46185  wfaxrep 46179  wfaxsep 46180  wfaxun 46184
[Kunen2] p. 113Lemma II.2.8pwclaxpow 46169
[Kunen2] p. 113Corollary II.2.9wfaxpow 46182
[Kunen2] p. 114Theorem II.2.13wfaxext 46178
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 46177  omelaxinf2 46174
[Kunen2] p. 114Corollary II.2.12wfac8prim 46187  wfaxinf2 46186
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 46200  permaxext 46190  permaxinf2 46198  permaxnul 46193  permaxpow 46194  permaxpr 46195  permaxrep 46191  permaxsep 46192  permaxun 46196
[Kunen2] p. 148Definition II.9.1brpermmodel 46188
[Kunen2] p. 149Exercise II.9.3permac8prim 46199
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4967
[Lang] , p. 225Corollary 1.3finexttrb 34367
[Lang] p. Definitiondf-rn 5666
[Lang] p. 3Statementlidrideqd 18879  mndbn0 18969
[Lang] p. 3Definitiondf-mnd 18953
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18905
[Lang] p. 4Property of composites. Second formulagsumccat 19066
[Lang] p. 5Equationgsumreidx 20161
[Lang] p. 5Definition of an (infinite) productgsumfsupp 49484
[Lang] p. 6Examplenn0mnd 49481
[Lang] p. 6Equationgsumxp2 20224
[Lang] p. 6Statementcycsubm 19446
[Lang] p. 6Definitionmulgnn0gsum 19319
[Lang] p. 6Observationmndlsmidm 19914
[Lang] p. 7Definitiondfgrp2e 19203
[Lang] p. 30Definitiondf-tocyc 33738
[Lang] p. 32Property (a)cyc3genpm 33783
[Lang] p. 32Property (b)cyc3conja 33788  cycpmconjv 33773
[Lang] p. 53Definitiondf-cat 17871
[Lang] p. 53Axiom CAT 1cat1 18301  cat1lem 18300
[Lang] p. 54Definitiondf-iso 17953
[Lang] p. 57Definitiondf-inito 18188  df-termo 18189
[Lang] p. 58Exampleirinitoringc 21815
[Lang] p. 58Statementinitoeu1 18215  termoeu1 18222
[Lang] p. 62Definitiondf-func 18062
[Lang] p. 65Definitiondf-nat 18150
[Lang] p. 83Definition of "ring with unit"dfring2 20547
[Lang] p. 91Notedf-ringc 20928
[Lang] p. 92Statementmxidlprm 34065
[Lang] p. 92Definitionisprmidlc 21658
[Lang] p. 128Remarkdsmmlmod 22081
[Lang] p. 129Prooflincscm 49747  lincscmcl 49749  lincsum 49746  lincsumcl 49748
[Lang] p. 129Statementlincolss 49751
[Lang] p. 129Observationdsmmfi 22074
[Lang] p. 141Theorem 5.3dimkerim 34329  qusdimsum 34330
[Lang] p. 141Corollary 5.4lssdimle 34310
[Lang] p. 147Definitionsnlindsntor 49788
[Lang] p. 504Statementmat1 22792  matring 22788
[Lang] p. 504Definitiondf-mamu 22736
[Lang] p. 505Statementmamuass 22747  mamutpos 22803  matassa 22789  mattposvs 22800  tposmap 22802
[Lang] p. 513Definitionmdet1 22946  mdetf 22940
[Lang] p. 513Theorem 4.4cramer 23039
[Lang] p. 514Proposition 4.6mdetleib 22932
[Lang] p. 514Proposition 4.8mdettpos 22956
[Lang] p. 515Definitiondf-minmar1 22980  smadiadetr 23020
[Lang] p. 515Corollary 4.9mdetero 22955  mdetralt 22953
[Lang] p. 517Proposition 4.15mdetmul 22968
[Lang] p. 518Definitiondf-madu 22979
[Lang] p. 518Proposition 4.16madulid 22990  madurid 22989  matinv 23022
[Lang] p. 561Theorem 3.1cayleyhamilton 23238
[Lang], p. 190Chapter 6vieta 34282
[Lang], p. 224Proposition 1.1extdgfialg 34396  finextalg 34400
[Lang], p. 224Proposition 1.2extdgmul 34365  fedgmul 34333
[Lang], p. 225Proposition 1.4algextdeg 34427
[Lang], p. 561Remarkchpmatply1 23180
[Lang], p. 561Definitiondf-chpmat 23175
[Lang2] p. 3Notationsdf-ind 12348
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45510
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45505
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45511
[LeBlanc] p. 277Rule R2axnul 5262
[Levy] p. 12Axiom 4.3.1df-clab 2742  wl-df.clab 38622
[Levy] p. 59Definitiondf-ttrcl 9736
[Levy] p. 64Theorem 5.6(ii)frinsg 9782
[Levy] p. 338Axiomdf-clel 2839  df-cleq 2755  wl-df.cleq 38623
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38626
[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 38626
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2839  df-cleq 2755  wl-df.cleq 38623
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2742  wl-df.clab 38622
[Levy] p. 358Axiomdf-clab 2742  wl-df.clab 38622
[Levy58] p. 2Definition Iisfin1-3 10491
[Levy58] p. 2Definition IIdf-fin2 10391
[Levy58] p. 2Definition Iadf-fin1a 10390
[Levy58] p. 2Definition IIIdf-fin3 10393
[Levy58] p. 3Definition Vdf-fin5 10394
[Levy58] p. 3Definition IVdf-fin4 10392
[Levy58] p. 4Definition VIdf-fin6 10395
[Levy58] p. 4Definition VIIdf-fin7 10396
[Levy58], p. 3Theorem 1fin1a2 10520
[Lipparini] p. 3Lemma 2.1.1nosepssdm 28073
[Lipparini] p. 3Lemma 2.1.4noresle 28084
[Lipparini] p. 6Proposition 4.2noinfbnd1 28116  nosupbnd1 28101
[Lipparini] p. 6Proposition 4.3noinfbnd2 28118  nosupbnd2 28103
[Lipparini] p. 7Theorem 5.1noetasuplem3 28122  noetasuplem4 28123
[Lipparini] p. 7Corollary 4.4nosupinfsep 28119
[Lopez-Astorga] p. 12Rule 1mptnan 1801
[Lopez-Astorga] p. 12Rule 2mptxor 1802
[Lopez-Astorga] p. 12Rule 3mtpxor 1804
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 33040
[Maeda] p. 168Lemma 5mdsym 33044  mdsymi 33043
[Maeda] p. 168Lemma 4(i)mdsymlem4 33038  mdsymlem6 33040  mdsymlem7 33041
[Maeda] p. 168Lemma 4(ii)mdsymlem8 33042
[MaedaMaeda] p. 1Remarkssdmd1 32945  ssdmd2 32946  ssmd1 32943  ssmd2 32944
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32941
[MaedaMaeda] p. 1Definition 1.1df-dmd 32913  df-md 32912  mdbr 32926
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32963  mdslj1i 32951  mdslj2i 32952  mdslle1i 32949  mdslle2i 32950  mdslmd1i 32961  mdslmd2i 32962
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32953  mdsl2bi 32955  mdsl2i 32954
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32967
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32964
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32965
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32942
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32947  mdsl3 32948
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32966
[MaedaMaeda] p. 4Theorem 1.14mdcompli 33061
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40570  hlrelat1 40649
[MaedaMaeda] p. 31Lemma 7.5lcvexch 40288
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32968  cvmdi 32956  cvnbtwn4 32921  cvrnbtwn4 40528
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32969
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40589  cvp 33007  cvrp 40665  lcvp 40289
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 33031
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 33030
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40582  hlexch4N 40641
[MaedaMaeda] p. 34Exercise 7.1atabsi 33033
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40692
[MaedaMaeda] p. 61Definition 15.10psubN 40998  atpsubN 41002  df-pointsN 40751  pointpsubN 41000
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40753  pmap11 41011  pmaple 41010  pmapsub 41017  pmapval 41006
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 41014  pmap1N 41016
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 41019  pmapglb2N 41020  pmapglb2xN 41021  pmapglbx 41018
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 41101
[MaedaMaeda] p. 67Postulate PS1ps-1 40726
[MaedaMaeda] p. 68Lemma 16.2df-padd 41045  paddclN 41091  paddidm 41090
[MaedaMaeda] p. 68Condition PS2ps-2 40727
[MaedaMaeda] p. 68Equation 16.2.1paddass 41087
[MaedaMaeda] p. 69Lemma 16.4ps-1 40726
[MaedaMaeda] p. 69Theorem 16.4ps-2 40727
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19919  lsmmod2 19920  lssats 40261  shatomici 32990  shatomistici 32993  shmodi 32022  shmodsi 32021
[MaedaMaeda] p. 130Remark 29.6dmdmd 32932  mdsymlem7 33041
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 32221
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 32125
[MaedaMaeda] p. 139Remarksumdmdii 33047
[Margaris] p. 40Rule Cexlimiv 1965
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 402  df-ex 1813  df-or 862  dfbi2 480
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 31031
[Margaris] p. 59Section 14notnotrALTVD 46088
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 46089
[Margaris] p. 79Rule Cexinst01 45799  exinst11 45800
[Margaris] p. 89Theorem 19.219.2 2011  19.2g 2228  r19.2z 4458
[Margaris] p. 89Theorem 19.319.3 2242  rr19.3v 3624
[Margaris] p. 89Theorem 19.5alcom 2199
[Margaris] p. 89Theorem 19.6alex 1859
[Margaris] p. 89Theorem 19.7alnex 1814
[Margaris] p. 89Theorem 19.819.8a 2221
[Margaris] p. 89Theorem 19.919.9 2245  19.9h 2323  exlimd 2258  exlimdh 2327
[Margaris] p. 89Theorem 19.11excom 2202  excomim 2203
[Margaris] p. 89Theorem 19.1219.12 2361
[Margaris] p. 90Section 19conventions-labels 31032  conventions-labels 31032  conventions-labels 31032  conventions-labels 31032
[Margaris] p. 90Theorem 19.14exnal 1860
[Margaris] p. 90Theorem 19.152albi 45554  albi 1851
[Margaris] p. 90Theorem 19.1619.16 2265
[Margaris] p. 90Theorem 19.1719.17 2266
[Margaris] p. 90Theorem 19.182exbi 45556  exbi 1880
[Margaris] p. 90Theorem 19.1919.19 2269
[Margaris] p. 90Theorem 19.202alim 45553  2alimdv 1953  alimd 2252  alimdh 1850  alimdv 1951  ax-4 1842  ralimdaa 3267  ralimdv 3180  ralimdva 3178  ralimdvva 3213  sbcimdv 3810
[Margaris] p. 90Theorem 19.2119.21 2247  19.21h 2324  19.21t 2246  19.21vv 45552  alrimd 2255  alrimdd 2254  alrimdh 1896  alrimdv 1964  alrimi 2253  alrimih 1857  alrimiv 1962  alrimivv 1963  bj-alrimdh 37672  hbralrimi 3156  r19.21be 3259  r19.21bi 3258  ralrimd 3271  ralrimdv 3164  ralrimdva 3166  ralrimdvv 3210  ralrimdvva 3221  ralrimi 3264  ralrimia 3265  ralrimiv 3157  ralrimiva 3158  ralrimivv 3207  ralrimivva 3209  ralrimivvva 3212  ralrimivw 3162
[Margaris] p. 90Theorem 19.222exim 45555  2eximdv 1954  bj-exim 37687  exim 1867  eximd 2256  eximdh 1897  eximdv 1952  rexim 3107  reximd2a 3276  reximdai 3268  reximdd 46368  reximddv 3182  reximddv2 3225  reximddv3 3183  reximdv 3181  reximdv2 3176  reximdva 3179  reximdvai 3177  reximdvva 3214  reximi2 3099
[Margaris] p. 90Theorem 19.2319.23 2251  19.23bi 2231  19.23h 2325  19.23t 2250  exlimdv 1968  exlimdvv 1969  exlimexi 45698  exlimiv 1965  exlimivv 1967  rexlimd3 46364  rexlimdv 3165  rexlimdv3a 3171  rexlimdva 3167  rexlimdva2 3169  rexlimdvaa 3168  rexlimdvv 3222  rexlimdvva 3223  rexlimdvvva 3224  rexlimdvw 3172  rexlimiv 3160  rexlimiva 3159  rexlimivv 3208
[Margaris] p. 90Theorem 19.2419.24 2026
[Margaris] p. 90Theorem 19.2519.25 1915
[Margaris] p. 90Theorem 19.2619.26 1903
[Margaris] p. 90Theorem 19.2719.27 2267  r19.27z 4469  r19.27zv 4470
[Margaris] p. 90Theorem 19.2819.28 2268  19.28vv 45562  r19.28z 4461  r19.28zf 46379  r19.28zv 4465  rr19.28v 3625
[Margaris] p. 90Theorem 19.2919.29 1908  r19.29d2r 3153  r19.29imd 3131
[Margaris] p. 90Theorem 19.3019.30 1916
[Margaris] p. 90Theorem 19.3119.31 2274  19.31vv 45560
[Margaris] p. 90Theorem 19.3219.32 2273  r19.32 48374
[Margaris] p. 90Theorem 19.3319.33-2 45558  19.33 1919
[Margaris] p. 90Theorem 19.3419.34 2027
[Margaris] p. 90Theorem 19.3519.35 1912
[Margaris] p. 90Theorem 19.3619.36 2270  19.36vv 45559  r19.36zv 4471
[Margaris] p. 90Theorem 19.3719.37 2272  19.37vv 45561  r19.37zv 4466
[Margaris] p. 90Theorem 19.3819.38 1872
[Margaris] p. 90Theorem 19.3919.39 2025
[Margaris] p. 90Theorem 19.4019.40-2 1922  19.40 1921  r19.40 3132
[Margaris] p. 90Theorem 19.4119.41 2275  19.41rg 45724
[Margaris] p. 90Theorem 19.4219.42 2276
[Margaris] p. 90Theorem 19.4319.43 1917
[Margaris] p. 90Theorem 19.4419.44 2277  r19.44zv 4468
[Margaris] p. 90Theorem 19.4519.45 2278  r19.45zv 4467
[Margaris] p. 110Exercise 2(b)eu1 2638
[Mayet] p. 370Remarkjpi 32902  largei 32899  stri 32889
[Mayet3] p. 9Definition of CH-statesdf-hst 32844  ishst 32846
[Mayet3] p. 10Theoremhstrbi 32898  hstri 32897
[Mayet3] p. 1223Theorem 4.1mayete3i 32360
[Mayet3] p. 1240Theorem 7.1mayetes3i 32361
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32910
[MegPav2000] p. 2345Definition 3.4-1chintcl 31964  chsupcl 31972
[MegPav2000] p. 2345Definition 3.4-2hatomic 32992
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32986
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 33013
[MegPav2000] p. 2366Figure 7pl42N 41232
[MegPav2002] p. 362Lemma 2.2latj31 18690  latj32 18688  latjass 18686
[Megill] p. 444Axiom C5ax-5 1945  ax5ALT 40156
[Megill] p. 444Section 7conventions 31031
[Megill] p. 445Lemma L12aecom-o 40150  ax-c11n 40137  axc11n 2458
[Megill] p. 446Lemma L17equtrr 2057
[Megill] p. 446Lemma L18ax6fromc10 40145
[Megill] p. 446Lemma L19hbnae-o 40177  hbnae 2464
[Megill] p. 447Remark 9.1dfsb1 2513  sbid 2294  sbidd-misc 51092  sbidd 51091
[Megill] p. 448Remark 9.6axc14 2495
[Megill] p. 448Scheme C4'ax-c4 40133
[Megill] p. 448Scheme C5'ax-c5 40132  sp 2223
[Megill] p. 448Scheme C6'ax-11 2197
[Megill] p. 448Scheme C7'ax-c7 40134
[Megill] p. 448Scheme C8'ax-7 2043
[Megill] p. 448Scheme C9'ax-c9 40139
[Megill] p. 448Scheme C10'ax-6 2002  ax-c10 40135
[Megill] p. 448Scheme C11'ax-c11 40136
[Megill] p. 448Scheme C12'ax-8 2149
[Megill] p. 448Scheme C13'ax-9 2157
[Megill] p. 448Scheme C14'ax-c14 40140
[Megill] p. 448Scheme C15'ax-c15 40138
[Megill] p. 448Scheme C16'ax-c16 40141
[Megill] p. 448Theorem 9.4dral1-o 40153  dral1 2471  dral2-o 40179  dral2 2470  drex1 2473  drex2 2474  drsb1 2527  drsb2 2304
[Megill] p. 449Theorem 9.7sbcom2 2212  sbequ 2122  sbid2v 2541
[Megill] p. 450Example in Appendixhba1-o 40146  hba1 2330
[Mendelson] p. 35Axiom A3hirstL-ax3 48167
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3830  rspsbca 3831  stdpc4 2107
[Mendelson] p. 69Axiom 5ax-c4 40133  ra4 3837  stdpc5 2248
[Mendelson] p. 81Rule Cexlimiv 1965
[Mendelson] p. 95Axiom 6stdpc6 2063
[Mendelson] p. 95Axiom 7stdpc7 2289
[Mendelson] p. 225Axiom system NBGru 3741
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5491
[Mendelson] p. 231Exercise 4.10(k)inv1 4351
[Mendelson] p. 231Exercise 4.10(l)unv 4352
[Mendelson] p. 231Exercise 4.10(n)dfin3 4225
[Mendelson] p. 231Exercise 4.10(o)df-nul 4282
[Mendelson] p. 231Exercise 4.10(q)dfin4 4226
[Mendelson] p. 231Exercise 4.10(s)ddif 4080
[Mendelson] p. 231Definition of uniondfun3 4224
[Mendelson] p. 235Exercise 4.12(c)univ 5423
[Mendelson] p. 235Exercise 4.12(d)pwv 4578
[Mendelson] p. 235Exercise 4.12(j)pwin 5546
[Mendelson] p. 235Exercise 4.12(k)pwunss 4579
[Mendelson] p. 235Exercise 4.12(l)pwssun 5547
[Mendelson] p. 235Exercise 4.12(n)uniin 4894
[Mendelson] p. 235Exercise 4.12(p)reli 5810
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6289
[Mendelson] p. 244Proposition 4.8(g)epweon 7813
[Mendelson] p. 246Definition of successordf-suc 6386
[Mendelson] p. 250Exercise 4.36oelim2 8632
[Mendelson] p. 254Proposition 4.22(b)xpen 9187
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9108  xpsneng 9109
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9115  xpcomeng 9116
[Mendelson] p. 254Proposition 4.22(e)xpassen 9118
[Mendelson] p. 255Definitionbrsdom 9029
[Mendelson] p. 255Exercise 4.39endisj 9111
[Mendelson] p. 255Exercise 4.41mapprc 8879
[Mendelson] p. 255Exercise 4.43mapsnen 9093  mapsnend 9092
[Mendelson] p. 255Exercise 4.45mapunen 9193
[Mendelson] p. 255Exercise 4.47xpmapen 9192
[Mendelson] p. 255Exercise 4.42(a)map0e 8938
[Mendelson] p. 255Exercise 4.42(b)map1 9096
[Mendelson] p. 257Proposition 4.24(a)undom 9112
[Mendelson] p. 258Exercise 4.56(c)djuassen 10284  djucomen 10283
[Mendelson] p. 258Exercise 4.56(f)djudom1 10288
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10282
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8567
[Mendelson] p. 266Proposition 4.34(f)oaordex 8594
[Mendelson] p. 275Proposition 4.42(d)entri3 10670
[Mendelson] p. 281Definitiondf-r1 9795
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9848
[Mendelson] p. 287Axiom system MKru 3741
[MertziosUnger] p. 152Definitiondf-frgr 30890
[MertziosUnger] p. 153Remark 1frgrconngr 30925
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30927  vdgn1frgrv3 30928
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30929
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30922
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30915  2pthfrgrrn 30913  2pthfrgrrn2 30914
[Mittelstaedt] p. 9Definitiondf-oc 31884
[Monk1] p. 22Remarkconventions 31031
[Monk1] p. 22Theorem 3.1conventions 31031
[Monk1] p. 26Theorem 2.8(vii)ssin 4138
[Monk1] p. 33Theorem 3.2(i)ssrel 5764  ssrelf 33281
[Monk1] p. 33Theorem 3.2(ii)eqrel 5765
[Monk1] p. 34Definition 3.3df-opab 5171
[Monk1] p. 36Theorem 3.7(i)bj-coi1 38152  coi1 6279  coi2 6280
[Monk1] p. 36Theorem 3.8(v)dm0 5909  rn0 5915
[Monk1] p. 36Theorem 3.7(ii)cnvi 5870
[Monk1] p. 37Theorem 3.13(i)relxp 5673
[Monk1] p. 37Theorem 3.13(x)dmxp 5918  rnxp 6174
[Monk1] p. 37Theorem 3.13(ii)0xp 5755  xp0 5756
[Monk1] p. 38Theorem 3.16(ii)ima0 6087
[Monk1] p. 38Theorem 3.16(viii)imai 6084
[Monk1] p. 39Theorem 3.17imaex 7950  imaexg 7949
[Monk1] p. 39Theorem 3.16(xi)imassrn 6210
[Monk1] p. 41Theorem 4.3(i)fnopfv 7099  funfvop 7072
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6962
[Monk1] p. 42Theorem 4.4(iii)fvelima 6973
[Monk1] p. 43Theorem 4.6funun 6606
[Monk1] p. 43Theorem 4.8(iv)dff13 7281  dff13f 7282
[Monk1] p. 46Theorem 4.15(v)funex 7248  funrnex 7990
[Monk1] p. 50Definition 5.4fniunfv 7274
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6241
[Monk1] p. 52Theorem 5.11(viii)ssint 4927
[Monk1] p. 52Definition 5.13 (i)1stval2 8042  df-1st 8025
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8043  df-2nd 8026
[Monk1] p. 112Theorem 15.17(v)ranksn 9895  ranksnb 9864
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9896
[Monk1] p. 112Theorem 15.17(iii)rankun 9897  rankunb 9891
[Monk1] p. 113Theorem 15.18r1val3 9877
[Monk1] p. 113Definition 15.19df-r1 9795  r1val2 9876
[Monk1] p. 117Lemmazorn2 10611  zorn2g 10608
[Monk1] p. 133Theorem 18.11cardom 10094
[Monk1] p. 133Theorem 18.12canth3 10672
[Monk1] p. 133Theorem 18.14carduni 10089
[Monk2] p. 105Axiom C4ax-4 1842
[Monk2] p. 105Axiom C7ax-7 2043
[Monk2] p. 105Axiom C8ax-12 2216  ax-c15 40138  ax12v2 2218
[Monk2] p. 108Lemma 5ax-c4 40133
[Monk2] p. 109Lemma 12ax-11 2197
[Monk2] p. 109Lemma 15equvini 2487  equvinv 2064  eqvinop 5460
[Monk2] p. 113Axiom C5-1ax-5 1945  ax5ALT 40156
[Monk2] p. 113Axiom C5-2ax-10 2180
[Monk2] p. 113Axiom C5-3ax-11 2197
[Monk2] p. 114Lemma 21sp 2223
[Monk2] p. 114Lemma 22axc4 2355  hba1-o 40146  hba1 2330
[Monk2] p. 114Lemma 23nfia1 2193
[Monk2] p. 114Lemma 24nfa2 2213  nfra2 3365  nfra2w 3302
[Moore] p. 53Part Idf-mre 17785
[Munkres] p. 77Example 2distop 23343  indistop 23350  indistopon 23349
[Munkres] p. 77Example 3fctop 23352  fctop2 23353
[Munkres] p. 77Example 4cctop 23354
[Munkres] p. 78Definition of basisdf-bases 23294  isbasis3g 23297
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17643  tgval2 23304
[Munkres] p. 79Remarktgcl 23317
[Munkres] p. 80Lemma 2.1tgval3 23311
[Munkres] p. 80Lemma 2.2tgss2 23335  tgss3 23334
[Munkres] p. 81Lemma 2.3basgen 23336  basgen2 23337
[Munkres] p. 83Exercise 3topdifinf 38464  topdifinfeq 38465  topdifinffin 38463  topdifinfindis 38461
[Munkres] p. 89Definition of subspace topologyresttop 23508
[Munkres] p. 93Theorem 6.1(1)0cld 23386  topcld 23383
[Munkres] p. 93Theorem 6.1(2)iincld 23387
[Munkres] p. 93Theorem 6.1(3)uncld 23389
[Munkres] p. 94Definition of closureclsval 23385
[Munkres] p. 94Definition of interiorntrval 23384
[Munkres] p. 95Theorem 6.5(a)clsndisj 23423  elcls 23421
[Munkres] p. 95Theorem 6.5(b)elcls3 23431
[Munkres] p. 97Theorem 6.6clslp 23496  neindisj 23465
[Munkres] p. 97Corollary 6.7cldlp 23498
[Munkres] p. 97Definition of limit pointislp2 23493  lpval 23487
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23663
[Munkres] p. 102Definition of continuous functiondf-cn 23575  iscn 23583  iscn2 23586
[Munkres] p. 107Theorem 7.2(g)cncnp 23628  cncnp2 23629  cncnpi 23626  df-cnp 23576  iscnp 23585  iscnp2 23587
[Munkres] p. 127Theorem 10.1metcn 24892
[Munkres] p. 128Theorem 10.3metcn4 25662
[Nathanson] p. 123Remarkreprgt 35320  reprinfz1 35321  reprlt 35318
[Nathanson] p. 123Definitiondf-repr 35308
[Nathanson] p. 123Chapter 5.1circlemethnat 35340
[Nathanson] p. 123Propositionbreprexp 35332  breprexpnat 35333  itgexpif 35305
[NielsenChuang] p. 195Equation 4.73unierri 32736
[OeSilva] p. 2042Section 2ax-bgbltosilva 49113
[Pfenning] p. 17Definition XMnatded 31034
[Pfenning] p. 17Definition NNCnatded 31034  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 31034
[Pfenning] p. 18Rule"natded 31034
[Pfenning] p. 18Definition /\Inatded 31034
[Pfenning] p. 18Definition ` `Enatded 31034  natded 31034  natded 31034  natded 31034  natded 31034
[Pfenning] p. 18Definition ` `Inatded 31034  natded 31034  natded 31034  natded 31034  natded 31034
[Pfenning] p. 18Definition ` `ELnatded 31034
[Pfenning] p. 18Definition ` `ERnatded 31034
[Pfenning] p. 18Definition ` `Ea,unatded 31034
[Pfenning] p. 18Definition ` `IRnatded 31034
[Pfenning] p. 18Definition ` `Ianatded 31034
[Pfenning] p. 127Definition =Enatded 31034
[Pfenning] p. 127Definition =Inatded 31034
[Ponnusamy] p. 361Theorem 6.44cphip0l 25553  df-dip 31333  dip0l 31350  ip0l 21972
[Ponnusamy] p. 361Equation 6.45cphipval 25594  ipval 31335
[Ponnusamy] p. 362Equation I1dipcj 31346  ipcj 21970
[Ponnusamy] p. 362Equation I3cphdir 25556  dipdir 31474  ipdir 21975  ipdiri 31462
[Ponnusamy] p. 362Equation I4ipidsq 31342  nmsq 25545
[Ponnusamy] p. 362Equation 6.46ip0i 31457
[Ponnusamy] p. 362Equation 6.47ip1i 31459
[Ponnusamy] p. 362Equation 6.48ip2i 31460
[Ponnusamy] p. 363Equation I2cphass 25562  dipass 31477  ipass 21981  ipassi 31473
[Prugovecki] p. 186Definition of brabraval 32576  df-bra 32482
[Prugovecki] p. 376Equation 8.1df-kb 32483  kbval 32586
[PtakPulmannova] p. 66Proposition 3.2.17atomli 33014
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 41137
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 33028  atcvat4i 33029  cvrat3 40691  cvrat4 40692  lsatcvat3 40301
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32914  cvrval 40518  df-cv 32911  df-lcv 40268  lspsncv0 21454
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 41149
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 41150
[Quine] p. 16Definition 2.1df-clab 2742  rabid 3436  rabidd 46375  wl-df.clab 38622
[Quine] p. 17Definition 2.1''dfsb7 2316
[Quine] p. 18Definition 2.7df-cleq 2755  wl-df.cleq 38623
[Quine] p. 19Definition 2.9conventions 31031  df-v 3456
[Quine] p. 34Theorem 5.1eqabb 2903
[Quine] p. 35Theorem 5.2abid1 2900  abid2f 2956
[Quine] p. 37Paragraph 1mirimanoff 36628
[Quine] p. 40Theorem 6.1sb5 2313
[Quine] p. 40Theorem 6.2sb6 2124  sbalex 2282
[Quine] p. 41Theorem 6.3df-clel 2839  wl-df.clel 38626
[Quine] p. 41Theorem 6.4eqid 2763  eqid1 31098
[Quine] p. 41Theorem 6.5eqcom 2770
[Quine] p. 42Theorem 6.6df-sbc 3743
[Quine] p. 42Theorem 6.7dfsbcq 3744  dfsbcq2 3745
[Quine] p. 43Theorem 6.8vex 3458
[Quine] p. 43Theorem 6.9isset 3468
[Quine] p. 44Theorem 7.3spcgf 3549  spcgv 3554  spcimgf 3517
[Quine] p. 44Theorem 6.11spsbc 3755  spsbcd 3756
[Quine] p. 44Theorem 6.12elex 3475
[Quine] p. 44Theorem 6.13elab 3636  elabg 3633  elabgf 3631
[Quine] p. 44Theorem 6.14noel 4286
[Quine] p. 48Theorem 7.2snprc 4678
[Quine] p. 48Definition 7.1df-pr 4591  df-sn 4589
[Quine] p. 49Theorem 7.4snss 4745  snssg 4744
[Quine] p. 49Theorem 7.5prss 4779  prssg 4778
[Quine] p. 49Theorem 7.6prid1 4723  prid1g 4721  prid2 4724  prid2g 4722  snid 4623  snidg 4621
[Quine] p. 51Theorem 7.12snex 5401
[Quine] p. 51Theorem 7.13prex 5400
[Quine] p. 53Theorem 8.2unisn 4889  unisnALT 46099  unisng 4888
[Quine] p. 53Theorem 8.3uniun 4893
[Quine] p. 54Theorem 8.6elssuni 4902
[Quine] p. 54Theorem 8.7uni0 4899
[Quine] p. 56Theorem 8.17uniabio 6526
[Quine] p. 56Definition 8.18dfaiota2 48361  dfiota2 6513
[Quine] p. 57Theorem 8.19aiotaval 48370  iotaval 6530
[Quine] p. 57Theorem 8.22iotanul 6537
[Quine] p. 58Theorem 8.23iotaex 6533
[Quine] p. 58Definition 9.1df-op 4839
[Quine] p. 61Theorem 9.5opabid 5503  opabidw 5502  opelopab 5521  opelopaba 5514  opelopabaf 5523  opelopabf 5524  opelopabg 5517  opelopabga 5511  opelopabgf 5519  oprabid 7475  oprabidw 7474
[Quine] p. 64Definition 9.11df-xp 5661
[Quine] p. 64Definition 9.12df-cnv 5663
[Quine] p. 64Definition 9.15df-id 5550
[Quine] p. 65Theorem 10.3fun0 6627
[Quine] p. 65Theorem 10.4funi 6592
[Quine] p. 65Theorem 10.5funsn 6615  funsng 6613
[Quine] p. 65Definition 10.1df-fun 6560
[Quine] p. 65Definition 10.2args 6102  dffv4 6905
[Quine] p. 68Definition 10.11conventions 31031  df-fv 6566  fv2 6903
[Quine] p. 124Theorem 17.3nn0opth2 14443  nn0opth2i 14442  nn0opthi 14441  omopthi 8698
[Quine] p. 177Definition 25.2df-rdg 8446
[Quine] p. 232Equation icarddom 10665
[Quine] p. 284Axiom 39(vi)funimaex 6649  funimaexg 6648
[Quine] p. 331Axiom system NFru 3741
[ReedSimon] p. 36Definition (iii)ax-his3 31716
[ReedSimon] p. 63Exercise 4(a)df-dip 31333  polid 31791  polid2i 31789  polidi 31790
[ReedSimon] p. 63Exercise 4(b)df-ph 31445
[ReedSimon] p. 195Remarklnophm 32651  lnophmi 32650
[Retherford] p. 49Exercise 1(i)leopadd 32764
[Retherford] p. 49Exercise 1(ii)leopmul 32766  leopmuli 32765
[Retherford] p. 49Exercise 1(iv)leoptr 32769
[Retherford] p. 49Definition VI.1df-leop 32484  leoppos 32758
[Retherford] p. 49Exercise 1(iii)leoptri 32768
[Retherford] p. 49Definition of operator orderingleop3 32757
[Ribenboim] p. 181Remarknprmdvdsfacm1 48914
[Ribenboim], p. 181Statementppivalnn 48922
[Roman] p. 4Definitiondf-dmat 22835  df-dmatalt 49715
[Roman] p. 18Part Preliminariesdf-rng 20405
[Roman] p. 19Part Preliminariesdf-ring 20491
[Roman] p. 46Theorem 1.6isldepslvec2 49802
[Roman] p. 112Noteisldepslvec2 49802  ldepsnlinc 49825  zlmodzxznm 49814
[Roman] p. 112Examplezlmodzxzequa 49813  zlmodzxzequap 49816  zlmodzxzldep 49821
[Roman] p. 170Theorem 7.8cayleyhamilton 23238
[Rosenlicht] p. 80Theoremheicant 38765
[Rosser] p. 281Definitiondf-op 4839
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 35344
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 35345
[Rotman] p. 28Remarkpgrpgt2nabl 49683  pmtr3ncom 19719
[Rotman] p. 31Theorem 3.4symggen2 19715
[Rotman] p. 42Theorem 3.15cayley 19658  cayleyth 19659
[Rudin] p. 164Equation 27efcan 16291
[Rudin] p. 164Equation 30efzval 16299
[Rudin] p. 167Equation 48absefi 16393
[Russell1905] p. 482Example of "the fatherdfalseu2 51212
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1804
[Sanford] p. 39Rule 4mptxor 1802
[Sanford] p. 40Rule 1mptnan 1801
[Schechter] p. 51Definition of antisymmetryintasym 6121
[Schechter] p. 51Definition of irreflexivityintirr 6124
[Schechter] p. 51Definition of symmetrycnvsym 6120
[Schechter] p. 51Definition of transitivitycotr 6118
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17785
[Schechter] p. 79Definition of Moore closuredf-mrc 17786
[Schechter] p. 82Section 4.5df-mrc 17786
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17788
[Schechter] p. 139Definition AC3dfac9 10242
[Schechter] p. 141Definition (MC)dfac11 44257
[Schechter] p. 149Axiom DC1ax-dc 10551  axdc3 10559
[Schechter] p. 187Definition of "ring with unit"isring 20493  isrngo 39023
[Schechter] p. 276Remark 11.6.espan0 32174
[Schechter] p. 276Definition of spandf-span 31941  spanval 31965
[Schechter] p. 428Definition 15.35bastop1 23341
[Schloeder] p. 1Lemma 1.3onelon 6405  onelond 37126  onelord 44445  ordelon 6404  ordelord 6402
[Schloeder] p. 1Lemma 1.7onepsuc 44446  sucidg 6464
[Schloeder] p. 1Remark 1.50elon 6436  onsuc 7848  ord0 6435  ordsuci 7846
[Schloeder] p. 1Theorem 1.9epsoon 44447
[Schloeder] p. 1Definition 1.1dftr5 5219
[Schloeder] p. 1Definition 1.2dford3 44228  elon2 6391
[Schloeder] p. 1Definition 1.4df-suc 6386
[Schloeder] p. 1Definition 1.6epel 5558  epelg 5556
[Schloeder] p. 1Theorem 1.9(i)elirr 9621  epirron 44448  ordirr 6398
[Schloeder] p. 1Theorem 1.9(ii)oneltr 44450  oneptr 44449  ontr1 6428
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6424  oneptri 44451  ordtri3or 6413
[Schloeder] p. 2Lemma 1.10ondif1 8537  ord0eln0 6437
[Schloeder] p. 2Lemma 1.13elsuci 6450  onsucss 44460  trsucss 6471
[Schloeder] p. 2Lemma 1.14ordsucss 7853
[Schloeder] p. 2Lemma 1.15onnbtwn 6477  ordnbtwn 6476
[Schloeder] p. 2Lemma 1.16orddif0suc 44462  ordnexbtwnsuc 44461
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10506  onsucf1lem 44463  onsucf1o 44466  onsucf1olem 44464  onsucrn 44465
[Schloeder] p. 2Lemma 1.18dflim7 44467
[Schloeder] p. 2Remark 1.12ordzsl 7880
[Schloeder] p. 2Theorem 1.10ondif1i 44456  ordne0gt0 44455
[Schloeder] p. 2Definition 1.11dflim6 44458  limnsuc 44459  onsucelab 44457
[Schloeder] p. 3Remark 1.21omex 9671
[Schloeder] p. 3Theorem 1.19tfinds 7895
[Schloeder] p. 3Theorem 1.22omelon 9674  ordom 7911
[Schloeder] p. 3Definition 1.20dfom3 9675
[Schloeder] p. 4Lemma 2.21onn 8677
[Schloeder] p. 4Lemma 2.7ssonuni 7818  ssorduni 7817
[Schloeder] p. 4Remark 2.4oa1suc 8567
[Schloeder] p. 4Theorem 1.23dfom5 9678  limom 7917
[Schloeder] p. 4Definition 2.1df-1o 8504  df1o2 8511
[Schloeder] p. 4Definition 2.3oa0 8552  oa0suclim 44469  oalim 8568  oasuc 8560
[Schloeder] p. 4Definition 2.5om0 8553  om0suclim 44470  omlim 8569  omsuc 8562
[Schloeder] p. 4Definition 2.6oe0 8558  oe0m1 8557  oe0suclim 44471  oelim 8570  oesuc 8563
[Schloeder] p. 5Lemma 2.10onsupuni 44423
[Schloeder] p. 5Lemma 2.11onsupsucismax 44473
[Schloeder] p. 5Lemma 2.12onsssupeqcond 44474
[Schloeder] p. 5Lemma 2.13limexissup 44475  limexissupab 44477  limiun 44476  limuni 6443
[Schloeder] p. 5Lemma 2.14oa0r 8574
[Schloeder] p. 5Lemma 2.15om1 8578  om1om1r 44478  om1r 8579
[Schloeder] p. 5Remark 2.8oacl 8571  oaomoecl 44472  oecl 8573  omcl 8572
[Schloeder] p. 5Definition 2.9onsupintrab 44425
[Schloeder] p. 6Lemma 2.16oe1 8580
[Schloeder] p. 6Lemma 2.17oe1m 8581
[Schloeder] p. 6Lemma 2.18oe0rif 44479
[Schloeder] p. 6Theorem 2.19oasubex 44480
[Schloeder] p. 6Theorem 2.20nnacl 8648  nnamecl 44481  nnecl 8650  nnmcl 8649
[Schloeder] p. 7Lemma 3.1onsucwordi 44482
[Schloeder] p. 7Lemma 3.2oaword1 8588
[Schloeder] p. 7Lemma 3.3oaword2 8589
[Schloeder] p. 7Lemma 3.4oalimcl 8596
[Schloeder] p. 7Lemma 3.5oaltublim 44484
[Schloeder] p. 8Lemma 3.6oaordi3 44485
[Schloeder] p. 8Lemma 3.81oaomeqom 44487
[Schloeder] p. 8Lemma 3.10oa00 8595
[Schloeder] p. 8Lemma 3.11omge1 44491  omword1 8609
[Schloeder] p. 8Remark 3.9oaordnr 44490  oaordnrex 44489
[Schloeder] p. 8Theorem 3.7oaord3 44486
[Schloeder] p. 9Lemma 3.12omge2 44492  omword2 8610
[Schloeder] p. 9Lemma 3.13omlim2 44493
[Schloeder] p. 9Lemma 3.14omord2lim 44494
[Schloeder] p. 9Lemma 3.15omord2i 44495  omordi 8602
[Schloeder] p. 9Theorem 3.16omord 8604  omord2com 44496
[Schloeder] p. 10Lemma 3.172omomeqom 44497  df-2o 8505
[Schloeder] p. 10Lemma 3.19oege1 44500  oewordi 8628
[Schloeder] p. 10Lemma 3.20oege2 44501  oeworde 8630
[Schloeder] p. 10Lemma 3.21rp-oelim2 44502
[Schloeder] p. 10Lemma 3.22oeord2lim 44503
[Schloeder] p. 10Remark 3.18omnord1 44499  omnord1ex 44498
[Schloeder] p. 11Lemma 3.23oeord2i 44504
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44506
[Schloeder] p. 11Remark 3.26oenord1 44510  oenord1ex 44509
[Schloeder] p. 11Theorem 4.1oaomoencom 44511
[Schloeder] p. 11Theorem 4.2oaass 8597
[Schloeder] p. 11Theorem 3.24oeord2com 44505
[Schloeder] p. 12Theorem 4.3odi 8615
[Schloeder] p. 13Theorem 4.4omass 8616
[Schloeder] p. 14Remark 4.6oenass 44513
[Schloeder] p. 14Theorem 4.7oeoa 8634
[Schloeder] p. 15Lemma 5.1cantnftermord 44514
[Schloeder] p. 15Lemma 5.2cantnfub 44515  cantnfub2 44516
[Schloeder] p. 16Theorem 5.3cantnf2 44519
[Schwabhauser] p. 10Axiom A1axcgrrflx 29522  axtgcgrrflx 28954
[Schwabhauser] p. 10Axiom A2axcgrtr 29523
[Schwabhauser] p. 10Axiom A3axcgrid 29524  axtgcgrid 28955
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28940
[Schwabhauser] p. 11Axiom A4axsegcon 29535  axtgsegcon 28956  df-trkgcb 28942
[Schwabhauser] p. 11Axiom A5ax5seg 29546  axtg5seg 28957  df-trkgcb 28942
[Schwabhauser] p. 11Axiom A6axbtwnid 29547  axtgbtwnid 28958  df-trkgb 28941
[Schwabhauser] p. 12Axiom A7axpasch 29549  axtgpasch 28959  df-trkgb 28941
[Schwabhauser] p. 12Axiom A8axlowdim2 29568  df-trkg2d 35364
[Schwabhauser] p. 13Axiom A8axtglowdim2 28962
[Schwabhauser] p. 13Axiom A9axtgupdim2 28963  df-trkg2d 35364
[Schwabhauser] p. 13Axiom A10axeuclid 29571  axtgeucl 28964  df-trkge 28943
[Schwabhauser] p. 13Axiom A11axcont 29584  axtgcont 28961  axtgcont1 28960  df-trkgb 28941
[Schwabhauser] p. 24Theorem A10prlngmo 29462
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36930
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36932
[Schwabhauser] p. 27Theorem 2.3cgrtr 36935
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36939
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36940  tgcgrcomimp 28969  tgcgrcoml 28971  tgcgrcomr 28970
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36945  tgcgrtriv 28976
[Schwabhauser] p. 28Theorem 2.105segofs 36949  tg5segofs 35375
[Schwabhauser] p. 28Definition 2.10df-afs 35372  df-ofs 36926
[Schwabhauser] p. 29Theorem 2.11cgrextend 36951  tgcgrextend 28977
[Schwabhauser] p. 29Theorem 2.12segconeq 36953  tgsegconeq 28978
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36965  btwntriv2 36955  tgbtwntriv2 28980
[Schwabhauser] p. 30Theorem 3.2btwncomim 36956  tgbtwncom 28981
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36959  tgbtwntriv1 28984
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36960  tgbtwnswapid 28985
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36966  btwnintr 36962  tgbtwnexch2 28989  tgbtwnintr 28986
[Schwabhauser] p. 30Theorem 3.6btwnexch 36968  btwnexch3 36963  tgbtwnexch 28991  tgbtwnexch3 28987
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36967  tgbtwnouttr 28990  tgbtwnouttr2 28988
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29567
[Schwabhauser] p. 32Theorem 3.14btwndiff 36970  tgbtwndiff 28999
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28992  trisegint 36971
[Schwabhauser] p. 34Theorem 4.2ifscgr 36987  tgifscgr 29001
[Schwabhauser] p. 34Theorem 4.11colcom 29051  colrot1 29052  colrot2 29053  lncom 29120  lnrot1 29121  lnrot2 29122
[Schwabhauser] p. 34Definition 4.1df-ifs 36983
[Schwabhauser] p. 35Theorem 4.3cgrsub 36988  tgcgrsub 29002
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36998  tgcgrxfr 29011
[Schwabhauser] p. 35Statement 4.4ercgrg 29010
[Schwabhauser] p. 35Definition 4.4df-cgr3 36984  df-cgrg 29004
[Schwabhauser] p. 35Definition instead (givendf-cgrg 29004
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36999  tgbtwnxfr 29023
[Schwabhauser] p. 36Theorem 4.11colinearperm1 37005  colinearperm2 37007  colinearperm3 37006  colinearperm4 37008  colinearperm5 37009
[Schwabhauser] p. 36Definition 4.8df-ismt 29026
[Schwabhauser] p. 36Definition 4.10df-colinear 36982  tgellng 29046  tglng 29039
[Schwabhauser] p. 37Theorem 4.12colineartriv1 37010
[Schwabhauser] p. 37Theorem 4.13colinearxfr 37018  lnxfr 29059
[Schwabhauser] p. 37Theorem 4.14lineext 37019  lnext 29060
[Schwabhauser] p. 37Theorem 4.16fscgr 37023  tgfscgr 29061
[Schwabhauser] p. 37Theorem 4.17linecgr 37024  lncgr 29062
[Schwabhauser] p. 37Definition 4.15df-fs 36985
[Schwabhauser] p. 38Theorem 4.18lineid 37026  lnid 29063
[Schwabhauser] p. 38Theorem 4.19idinside 37027  tgidinside 29064
[Schwabhauser] p. 39Theorem 5.1btwnconn1 37044  tgbtwnconn1 29068
[Schwabhauser] p. 41Theorem 5.2btwnconn2 37045  tgbtwnconn2 29069
[Schwabhauser] p. 41Theorem 5.3btwnconn3 37046  tgbtwnconn3 29070
[Schwabhauser] p. 41Theorem 5.5brsegle2 37052
[Schwabhauser] p. 41Definition 5.4df-segle 37050  legov 29078
[Schwabhauser] p. 41Definition 5.5legov2 29079
[Schwabhauser] p. 42Remark 5.13legso 29092
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 37053
[Schwabhauser] p. 42Theorem 5.7seglerflx 37055
[Schwabhauser] p. 42Theorem 5.8segletr 37057
[Schwabhauser] p. 42Theorem 5.9segleantisym 37058
[Schwabhauser] p. 42Theorem 5.10seglelin 37059
[Schwabhauser] p. 42Theorem 5.11seglemin 37056
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 37061
[Schwabhauser] p. 42Proposition 5.7legid 29080
[Schwabhauser] p. 42Proposition 5.8legtrd 29082
[Schwabhauser] p. 42Proposition 5.9legtri3 29083
[Schwabhauser] p. 42Proposition 5.10legtrid 29084
[Schwabhauser] p. 42Proposition 5.11leg0 29085
[Schwabhauser] p. 43Theorem 6.2btwnoutside 37068
[Schwabhauser] p. 43Theorem 6.3broutsideof3 37069
[Schwabhauser] p. 43Theorem 6.4broutsideof 37064  df-outsideof 37063
[Schwabhauser] p. 43Definition 6.1broutsideof2 37065  ishlg 29098
[Schwabhauser] p. 44Theorem 6.4hlln 29103
[Schwabhauser] p. 44Theorem 6.5hlid 29105  outsideofrflx 37070
[Schwabhauser] p. 44Theorem 6.6hlcomb 29099  hlcomd 29100  outsideofcom 37071
[Schwabhauser] p. 44Theorem 6.7hltr 29106  outsideoftr 37072
[Schwabhauser] p. 44Theorem 6.11hlcgreq 29115  hlcgreu 29114  outsideofeu 37074
[Schwabhauser] p. 44Definition 6.8df-ray 37081
[Schwabhauser] p. 45Part 2df-lines2 37082
[Schwabhauser] p. 45Theorem 6.13outsidele 37075
[Schwabhauser] p. 45Theorem 6.15lineunray 37090
[Schwabhauser] p. 45Theorem 6.16lineelsb2 37091  tglineelsb2 29130
[Schwabhauser] p. 45Theorem 6.17linecom 37093  linerflx1 37092  linerflx2 37094  tglinecom 29133  tglinerflx1 29131  tglinerflx2 29132
[Schwabhauser] p. 45Theorem 6.18linethru 37096  tglinethru 29134
[Schwabhauser] p. 45Definition 6.14df-line2 37080  tglng 29039
[Schwabhauser] p. 45Proposition 6.13legbtwn 29087
[Schwabhauser] p. 46Theorem 6.19linethrueu 37099  tglinethrueu 29137
[Schwabhauser] p. 46Theorem 6.21lineintmo 37100  tglineineq 29141  tglineinsn 29142  tglineinteq 29144  tglineintmo 29140
[Schwabhauser] p. 46Theorem 6.23colline 29148
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 29149
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 29150
[Schwabhauser] p. 49Theorem 7.3mirinv 29168
[Schwabhauser] p. 49Theorem 7.7mirmir 29164
[Schwabhauser] p. 49Theorem 7.8mirreu3 29156
[Schwabhauser] p. 49Definition 7.5df-mir 29155  ismir 29161  mirbtwn 29160  mircgr 29159  mirfv 29158  mirval 29157
[Schwabhauser] p. 50Theorem 7.8mirreu 29166
[Schwabhauser] p. 50Theorem 7.9mireq 29167
[Schwabhauser] p. 50Theorem 7.10mirinv 29168
[Schwabhauser] p. 50Theorem 7.11mirf1o 29171
[Schwabhauser] p. 50Theorem 7.13miriso 29172
[Schwabhauser] p. 51Theorem 7.14mirmot 29177
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 29174  mirbtwni 29173
[Schwabhauser] p. 51Theorem 7.16mircgrs 29175
[Schwabhauser] p. 51Theorem 7.17miduniq 29187
[Schwabhauser] p. 52Lemma 7.21symquadlem 29191  symquadmid 29334
[Schwabhauser] p. 52Theorem 7.18miduniq1 29188
[Schwabhauser] p. 52Theorem 7.19miduniq2 29189
[Schwabhauser] p. 52Theorem 7.20colmid 29190
[Schwabhauser] p. 53Lemma 7.22krippen 29193
[Schwabhauser] p. 55Lemma 7.25midexlem 29194
[Schwabhauser] p. 57Theorem 8.2ragcom 29203
[Schwabhauser] p. 57Definition 8.1df-rag 29199  israg 29202
[Schwabhauser] p. 58Theorem 8.3ragcol 29204
[Schwabhauser] p. 58Theorem 8.4ragmir 29205
[Schwabhauser] p. 58Theorem 8.5ragtrivb 29207
[Schwabhauser] p. 58Theorem 8.6ragflat2 29208
[Schwabhauser] p. 58Theorem 8.7ragflat 29209
[Schwabhauser] p. 58Theorem 8.8ragtriva 29210
[Schwabhauser] p. 58Theorem 8.9ragflat3 29211  ragncol 29214
[Schwabhauser] p. 58Theorem 8.10ragcgr 29212
[Schwabhauser] p. 59Theorem 8.12perpcom 29218
[Schwabhauser] p. 59Theorem 8.13ragperp 29222
[Schwabhauser] p. 59Theorem 8.14perpneq 29219
[Schwabhauser] p. 59Definition 8.11df-perpg 29201  isperp 29217
[Schwabhauser] p. 59Definition 8.13isperp2 29220
[Schwabhauser] p. 60Theorem 8.18foot 29227
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 29236  colperpexlem2 29237
[Schwabhauser] p. 63Theorem 8.21colperpex 29239  colperpexlem3 29238
[Schwabhauser] p. 64Theorem 8.22mideu 29244  midex 29243
[Schwabhauser] p. 66Lemma 8.24opphllem 29241
[Schwabhauser] p. 67Theorem 9.2oppcom 29250
[Schwabhauser] p. 67Definition 9.1islnopp 29245
[Schwabhauser] p. 68Lemma 9.3opphllem2 29254
[Schwabhauser] p. 68Lemma 9.4opphllem5 29257  opphllem6 29258
[Schwabhauser] p. 69Theorem 9.5opphl 29260
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28959
[Schwabhauser] p. 70Theorem 9.6outpasch 29263
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29271
[Schwabhauser] p. 71Definition 9.7df-hpg 29266  hpgbr 29268
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29273
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29272
[Schwabhauser] p. 72Theorem 9.11hpgid 29274
[Schwabhauser] p. 72Theorem 9.12hpgcom 29275
[Schwabhauser] p. 72Theorem 9.13hpgtr 29276
[Schwabhauser] p. 73Theorem 9.18colopp 29277
[Schwabhauser] p. 73Theorem 9.19colhp 29278
[Schwabhauser] p. 74Lemma 9.22lnincplng 29292
[Schwabhauser] p. 74Theorem 9.21plngcp 29294
[Schwabhauser] p. 74Theorem 9.24plngrot 29298
[Schwabhauser] p. 74Definition 9.20df-plng 29282  elplng 29288
[Schwabhauser] p. 75Theorem 9.25lnssplng 29300  lnssplng1 29301
[Schwabhauser] p. 76Theorem 9.26plng3p 29305
[Schwabhauser] p. 88Theorem 10.2lmieu 29319
[Schwabhauser] p. 88Definition 10.1df-mid 29309
[Schwabhauser] p. 89Theorem 10.4lmicom 29323
[Schwabhauser] p. 89Theorem 10.5lmilmi 29324
[Schwabhauser] p. 89Theorem 10.6lmireu 29325
[Schwabhauser] p. 89Theorem 10.7lmieq 29326
[Schwabhauser] p. 89Theorem 10.8lmiinv 29327
[Schwabhauser] p. 89Theorem 10.9lmif1o 29330
[Schwabhauser] p. 89Theorem 10.10lmiiso 29332
[Schwabhauser] p. 89Definition 10.3df-lmi 29310
[Schwabhauser] p. 90Theorem 10.11lmimot 29333
[Schwabhauser] p. 91Theorem 10.12hypcgr 29337
[Schwabhauser] p. 92Theorem 10.14lmiopp 29338
[Schwabhauser] p. 92Theorem 10.15lnperpex 29339  lnperpexs 29340
[Schwabhauser] p. 92Theorem 10.16trgcopy 29341  trgcopyeu 29343
[Schwabhauser] p. 95Definition 11.2dfcgra2 29368
[Schwabhauser] p. 95Definition 11.3iscgra 29346
[Schwabhauser] p. 95Proposition 11.4cgracgr 29355
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29353  cgrahl2 29354
[Schwabhauser] p. 96Theorem 11.6cgraid 29356
[Schwabhauser] p. 96Theorem 11.9cgraswap 29357
[Schwabhauser] p. 97Theorem 11.7cgracom 29359
[Schwabhauser] p. 97Theorem 11.8cgratr 29360
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29364  cgrahl 29365
[Schwabhauser] p. 98Theorem 11.13sacgr 29369
[Schwabhauser] p. 98Theorem 11.14oacgr 29370
[Schwabhauser] p. 98Theorem 11.15acopy 29371  acopyeu 29372
[Schwabhauser] p. 98Theorem 11.16ragcgra 29373
[Schwabhauser] p. 98Theorem 11.17cgrarag 29374
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29375
[Schwabhauser] p. 99Theorem 11.19ragraghl 29376
[Schwabhauser] p. 99Theorem 11.20perpeq 29378
[Schwabhauser] p. 99Theorem 11.22tgaaddcpbl 29382
[Schwabhauser] p. 101Theorem 11.24inagswap 29390
[Schwabhauser] p. 101Theorem 11.25inaghl 29394
[Schwabhauser] p. 101Definition 11.23isinag 29387
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29402
[Schwabhauser] p. 102Definition 11.27df-leag 29395  isleag 29396
[Schwabhauser] p. 107Theorem 11.49tgsas 29430  tgsas1 29429  tgsas2 29431  tgsas3 29432
[Schwabhauser] p. 108Theorem 11.50tgasa 29434  tgasa1 29433
[Schwabhauser] p. 109Theorem 11.51tgsss1 29435  tgsss2 29436  tgsss3 29437
[Schwabhauser] p. 121Definition 12.2df-prlng 29445
[Schwabhauser] p. 122Theorem 12.4prlngref 29448
[Schwabhauser] p. 122Theorem 12.5prlngsym 29449
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29454
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29455  dfprlng3 29456
[Schwabhauser] p. 122Theorem 12.9perpprlng 29458
[Schwabhauser] p. 122Theorem 12.10prlngex 29459
[Schwabhauser] p. 123Theorem 12.11prlngmo 29462  prlngmo2 29464
[Schwabhauser] p. 124Theorem 12.13prlngeu 29463
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29466
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29467
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29468
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29469
[Schwabhauser] p. 126Theorem 12.18symquadprlng 29470
[Schwabhauser] p. 126Theorem 12.19prlngsymquad 29472  prlngsymquadopp 29473
[Schwabhauser] p. 126Theorem 12.20quadcgrprlng 29474
[Schwabhauser] p. 126Theorem 12.21tgaltai 29475
[Shapiro] p. 230Theorem 6.5.1dchrhash 27628  dchrsum 27626  dchrsum2 27625  sumdchr 27629
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27630  sum2dchr 27631
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20312  ablfacrp2 20313
[Shapiro], p. 328Equation 9.2.4vmasum 27573
[Shapiro], p. 329Equation 9.2.7logfac2 27574
[Shapiro], p. 329Equation 9.2.9logfacrlim 27581
[Shapiro], p. 331Equation 9.2.13vmadivsum 27839
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27842
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27896  vmalogdivsum2 27895
[Shapiro], p. 375Theorem 9.4.1dirith 27886  dirith2 27885
[Shapiro], p. 375Equation 9.4.3rplogsum 27884  rpvmasum 27883  rpvmasum2 27869
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27844
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27882
[Shapiro], p. 377Lemma 9.4.1dchrisum 27849  dchrisumlem1 27846  dchrisumlem2 27847  dchrisumlem3 27848  dchrisumlema 27845
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27852
[Shapiro], p. 379Equation 9.4.16dchrmusum 27881  dchrmusumlem 27879  dchrvmasumlem 27880
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27851
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27853
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27877  dchrisum0re 27870  dchrisumn0 27878
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27863
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27867
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27868
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27923  pntrsumbnd2 27924  pntrsumo1 27922
[Shapiro], p. 405Equation 10.2.1mudivsum 27887
[Shapiro], p. 406Equation 10.2.6mulogsum 27889
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27891
[Shapiro], p. 407Equation 10.2.8mulog2sum 27894
[Shapiro], p. 418Equation 10.4.6logsqvma 27899
[Shapiro], p. 418Equation 10.4.8logsqvma2 27900
[Shapiro], p. 419Equation 10.4.10selberg 27905
[Shapiro], p. 420Equation 10.4.12selberg2lem 27907
[Shapiro], p. 420Equation 10.4.14selberg2 27908
[Shapiro], p. 422Equation 10.6.7selberg3 27916
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27917
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27914  selberg3lem2 27915
[Shapiro], p. 422Equation 10.4.23selberg4 27918
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27912
[Shapiro], p. 428Equation 10.6.2selbergr 27925
[Shapiro], p. 429Equation 10.6.8selberg3r 27926
[Shapiro], p. 430Equation 10.6.11selberg4r 27927
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27941
[Shapiro], p. 434Equation 10.6.27pntlema 27953  pntlemb 27954  pntlemc 27952  pntlemd 27951  pntlemg 27955
[Shapiro], p. 435Equation 10.6.29pntlema 27953
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27945
[Shapiro], p. 436Lemma 10.6.2pntibnd 27950
[Shapiro], p. 436Equation 10.6.34pntlema 27953
[Shapiro], p. 436Equation 10.6.35pntlem3 27966  pntleml 27968
[Stewart] p. 91Lemma 7.3constrss 34445
[Stewart] p. 92Definition 7.4.df-constr 34432
[Stewart] p. 96Theorem 7.10constraddcl 34464  constrinvcl 34475  constrmulcl 34473  constrnegcl 34465  constrsqrtcl 34481
[Stewart] p. 97Theorem 7.11constrextdg2 34451
[Stewart] p. 98Theorem 7.12constrext2chn 34461
[Stewart] p. 99Theorem 7.132sqr3nconstr 34483
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34493
[Stoll] p. 13Definition corresponds to dfsymdif3 4254
[Stoll] p. 16Exercise 4.40dif 4359  dif0 4330
[Stoll] p. 16Exercise 4.8difdifdir 4450
[Stoll] p. 17Theorem 5.1(5)unvdif 4432
[Stoll] p. 19Theorem 5.2(13)undm 4245
[Stoll] p. 19Theorem 5.2(13')indm 4246
[Stoll] p. 20Remarkinvdif 4227
[Stoll] p. 25Definition of ordered tripledf-ot 4862
[Stoll] p. 43Definitionuniiun 5020
[Stoll] p. 44Definitionintiin 5021
[Stoll] p. 45Definitiondf-iin 4957
[Stoll] p. 45Definition indexed uniondf-iun 4956
[Stoll] p. 176Theorem 3.4(27)iman 407
[Stoll] p. 262Example 4.1dfsymdif3 4254
[Strang] p. 242Section 6.3expgrowth 45511
[Suppes] p. 22Theorem 2eq0 4300  eq0f 4297
[Suppes] p. 22Theorem 4eqss 3928  eqssd 3930  eqssi 3929
[Suppes] p. 23Theorem 5ss0 4355  ss0b 4354
[Suppes] p. 23Theorem 6sstr 3921  sstrALT2 46008
[Suppes] p. 23Theorem 7pssirr 4033
[Suppes] p. 23Theorem 8pssn2lp 4035
[Suppes] p. 23Theorem 9psstr 4038
[Suppes] p. 23Theorem 10pssss 4028
[Suppes] p. 25Theorem 12elin 4096  elun 4155
[Suppes] p. 26Theorem 15inidm 4126
[Suppes] p. 26Theorem 16in0 4348
[Suppes] p. 27Theorem 23unidm 4159
[Suppes] p. 27Theorem 24un0 4347
[Suppes] p. 27Theorem 25ssun1 4179
[Suppes] p. 27Theorem 26ssequn1 4187
[Suppes] p. 27Theorem 27unss 4191
[Suppes] p. 27Theorem 28indir 4234
[Suppes] p. 27Theorem 29undir 4235
[Suppes] p. 28Theorem 32difid 4328
[Suppes] p. 29Theorem 33difin 4220
[Suppes] p. 29Theorem 34indif 4228
[Suppes] p. 29Theorem 35undif1 4433
[Suppes] p. 29Theorem 36difun2 4440
[Suppes] p. 29Theorem 37difin0 4431
[Suppes] p. 29Theorem 38disjdif 4429
[Suppes] p. 29Theorem 39difundi 4238
[Suppes] p. 29Theorem 40difindi 4240
[Suppes] p. 30Theorem 41nalset 5271
[Suppes] p. 39Theorem 61uniss 4878
[Suppes] p. 39Theorem 65uniop 5492
[Suppes] p. 41Theorem 70intsn 4947
[Suppes] p. 42Theorem 71intpr 4945  intprg 4944
[Suppes] p. 42Theorem 73op1stb 5444
[Suppes] p. 42Theorem 78intun 4943
[Suppes] p. 44Definition 15(a)dfiun2 4993  dfiun2g 4991
[Suppes] p. 44Definition 15(b)dfiin2 4994
[Suppes] p. 47Theorem 86elpw 4564  elpw2 5300  elpw2g 5299  elpwg 4563  elpwgdedVD 46090
[Suppes] p. 47Theorem 87pwid 4584
[Suppes] p. 47Theorem 89pw0 4833
[Suppes] p. 48Theorem 90pwpw0 4834
[Suppes] p. 52Theorem 101xpss12 5670
[Suppes] p. 52Theorem 102xpindi 5816  xpindir 5817
[Suppes] p. 52Theorem 103xpundi 5724  xpundir 5725
[Suppes] p. 54Theorem 105elirrv 9618
[Suppes] p. 58Theorem 2relss 5763
[Suppes] p. 59Theorem 4eldm 5889  eldm2 5890  eldm2g 5888  eldmg 5887
[Suppes] p. 59Definition 3df-dm 5665
[Suppes] p. 60Theorem 6dmin 5900
[Suppes] p. 60Theorem 8rnun 6148
[Suppes] p. 60Theorem 9rnin 6149
[Suppes] p. 60Definition 4dfrn2 5877
[Suppes] p. 61Theorem 11brcnv 5867  brcnvg 5864
[Suppes] p. 62Equation 5elcnv 5861  elcnv2 5862
[Suppes] p. 62Theorem 12relcnv 6112
[Suppes] p. 62Theorem 15cnvin 6147
[Suppes] p. 62Theorem 16cnvun 6145
[Suppes] p. 63Definitiondftrrels2 39783
[Suppes] p. 63Theorem 20co02 6277
[Suppes] p. 63Theorem 21dmcoss 5964
[Suppes] p. 63Definition 7df-co 5664
[Suppes] p. 64Theorem 26cnvco 5874
[Suppes] p. 64Theorem 27coass 6284
[Suppes] p. 65Theorem 31resundi 5995
[Suppes] p. 65Theorem 34elima 6073  elima2 6074  elima3 6075  elimag 6072
[Suppes] p. 65Theorem 35imaundi 6153
[Suppes] p. 66Theorem 40dminss 6155
[Suppes] p. 66Theorem 41imainss 6156
[Suppes] p. 67Exercise 11cnvxp 6159
[Suppes] p. 81Definition 34dfec2 8748
[Suppes] p. 82Theorem 72elec 8792  elecALTV 39395  elecg 8790
[Suppes] p. 82Theorem 73eqvrelth 39819  erth 8800  erth2 8801
[Suppes] p. 83Theorem 74eqvreldisj 39822  erdisj 8803
[Suppes] p. 83Definition 35, df-parts 39992  dfmembpart2 39997
[Suppes] p. 89Theorem 96map0b 8939
[Suppes] p. 89Theorem 97map0 8943  map0g 8940
[Suppes] p. 89Theorem 98mapsn 8944  mapsnd 8942
[Suppes] p. 89Theorem 99mapss 8945
[Suppes] p. 91Definition 12(ii)alephsuc 10174
[Suppes] p. 91Definition 12(iii)alephlim 10173
[Suppes] p. 92Theorem 1enref 9040  enrefg 9039
[Suppes] p. 92Theorem 2ensym 9058  ensymb 9057  ensymi 9059
[Suppes] p. 92Theorem 3entr 9061
[Suppes] p. 92Theorem 4unen 9101
[Suppes] p. 94Theorem 15endom 9034
[Suppes] p. 94Theorem 16ssdomg 9055
[Suppes] p. 94Theorem 17domtr 9062
[Suppes] p. 95Theorem 18sbth 9144
[Suppes] p. 97Theorem 23canth2 9177  canth2g 9178
[Suppes] p. 97Definition 3brsdom2 9148  df-sdom 9004  dfsdom2 9147
[Suppes] p. 97Theorem 21(i)sdomirr 9161
[Suppes] p. 97Theorem 22(i)domnsym 9150
[Suppes] p. 97Theorem 21(ii)sdomnsym 9149
[Suppes] p. 97Theorem 22(ii)domsdomtr 9159
[Suppes] p. 97Theorem 22(iv)brdom2 9037
[Suppes] p. 97Theorem 21(iii)sdomtr 9162
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9157
[Suppes] p. 98Exercise 4fundmen 9087  fundmeng 9088
[Suppes] p. 98Exercise 6xpdom3 9122
[Suppes] p. 98Exercise 11sdomentr 9158
[Suppes] p. 104Theorem 37fofi 9333
[Suppes] p. 104Theorem 38pwfi 9338
[Suppes] p. 105Theorem 40pwfi 9338
[Suppes] p. 111Axiom for cardinal numberscarden 10662
[Suppes] p. 130Definition 3df-tr 5216
[Suppes] p. 132Theorem 9ssonuni 7818
[Suppes] p. 134Definition 6df-suc 6386
[Suppes] p. 136Theorem Schema 22findes 7936  finds 7932  finds1 7935  finds2 7934
[Suppes] p. 151Theorem 42isfinite 9680  isfinite2 9318  isfiniteg 9320  unbnn 9316
[Suppes] p. 162Definition 5df-ltnq 11030  df-ltpq 11022
[Suppes] p. 197Theorem Schema 4tfindes 7898  tfinds 7895  tfinds2 7899
[Suppes] p. 209Theorem 18oaord1 8587
[Suppes] p. 209Theorem 21oaword2 8589
[Suppes] p. 211Theorem 25oaass 8597
[Suppes] p. 225Definition 8iscard2 10084
[Suppes] p. 227Theorem 56ondomon 10674
[Suppes] p. 228Theorem 59harcard 10086
[Suppes] p. 228Definition 12(i)aleph0 10172
[Suppes] p. 228Theorem Schema 61onintss 6433
[Suppes] p. 228Theorem Schema 62onminesb 7831  onminsb 7832
[Suppes] p. 229Theorem 64alephval2 10684
[Suppes] p. 229Theorem 65alephcard 10176
[Suppes] p. 229Theorem 66alephord2i 10183
[Suppes] p. 229Theorem 67alephnbtwn 10177
[Suppes] p. 229Definition 12df-aleph 10048
[Suppes] p. 242Theorem 6weth 10600
[Suppes] p. 242Theorem 8entric 10668
[Suppes] p. 242Theorem 9carden 10662
[Szendrei] p. 11Line 6df-cloneop 36639
[Szendrei] p. 11Paragraph 3df-suppos 36643
[TakeutiZaring] p. 8Axiom 1ax-ext 2735
[TakeutiZaring] p. 13Definition 4.5df-cleq 2755  wl-df.cleq 38623
[TakeutiZaring] p. 13Proposition 4.6df-clel 2839  wl-df.clel 38626
[TakeutiZaring] p. 13Proposition 4.9cvjust 2757
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2783
[TakeutiZaring] p. 14Definition 4.16df-oprab 7447
[TakeutiZaring] p. 14Proposition 4.14ru 3741
[TakeutiZaring] p. 15Axiom 2zfpair 5387
[TakeutiZaring] p. 15Exercise 1elpr 4609  elpr2 4611  elpr2g 4610  elprg 4607
[TakeutiZaring] p. 15Exercise 2elsn 4599  elsn2 4626  elsn2g 4625  elsng 4598  velsn 4600
[TakeutiZaring] p. 15Exercise 3elop 5440
[TakeutiZaring] p. 15Exercise 4sneq 4594  sneqr 4798
[TakeutiZaring] p. 15Definition 5.1dfpr2 4605  dfsn2 4597  dfsn2ALT 4606
[TakeutiZaring] p. 16Axiom 3uniex 7782
[TakeutiZaring] p. 16Exercise 6opth 5449
[TakeutiZaring] p. 16Exercise 7opex 5436
[TakeutiZaring] p. 16Exercise 8rext 5420
[TakeutiZaring] p. 16Corollary 5.8unex 7785  unexg 7784
[TakeutiZaring] p. 16Definition 5.3dftp2 4652
[TakeutiZaring] p. 16Definition 5.5df-uni 4871
[TakeutiZaring] p. 16Definition 5.6df-in 4094  df-un 4154
[TakeutiZaring] p. 16Proposition 5.7unipr 4887  uniprg 4886
[TakeutiZaring] p. 17Axiom 4vpwex 5343
[TakeutiZaring] p. 17Exercise 1eltp 4650
[TakeutiZaring] p. 17Exercise 5elsuc 6453  elsucg 6451  sstr2 3920
[TakeutiZaring] p. 17Exercise 6uncom 4160
[TakeutiZaring] p. 17Exercise 7incom 4109
[TakeutiZaring] p. 17Exercise 8unass 4173
[TakeutiZaring] p. 17Exercise 9inass 4127
[TakeutiZaring] p. 17Exercise 10indi 4232
[TakeutiZaring] p. 17Exercise 11undi 4233
[TakeutiZaring] p. 17Definition 5.9df-pss 4017  df-ss 3901
[TakeutiZaring] p. 17Definition 5.10df-pw 4562
[TakeutiZaring] p. 18Exercise 7unss2 4188
[TakeutiZaring] p. 18Exercise 9dfss2 4097  sseqin2 4123
[TakeutiZaring] p. 18Exercise 10ssid 3935
[TakeutiZaring] p. 18Exercise 12inss1 4136  inss2 4137
[TakeutiZaring] p. 18Exercise 13nss 3977
[TakeutiZaring] p. 18Exercise 15unieq 4881
[TakeutiZaring] p. 18Exercise 18sspwb 5421  sspwimp 46091  sspwimpALT 46098  sspwimpALT2 46101  sspwimpcf 46093
[TakeutiZaring] p. 18Exercise 19pweqb 5428
[TakeutiZaring] p. 19Axiom 5ax-rep 5235
[TakeutiZaring] p. 20Definitiondf-rab 3417
[TakeutiZaring] p. 20Corollary 5.160ex 5264
[TakeutiZaring] p. 20Definition 5.12df-dif 4050
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37618  dfnul2 4284
[TakeutiZaring] p. 20Proposition 5.15difid 4328
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4303  n0f 4299  neq0 4302  neq0f 4298
[TakeutiZaring] p. 21Axiom 6zfreg 9617
[TakeutiZaring] p. 21Axiom 6'zfregs 9760
[TakeutiZaring] p. 21Theorem 5.22setind 9775
[TakeutiZaring] p. 21Definition 5.20df-v 3456
[TakeutiZaring] p. 21Proposition 5.21vprc 5278
[TakeutiZaring] p. 22Exercise 10ss 4353
[TakeutiZaring] p. 22Exercise 3ssex 5286  ssexg 5285
[TakeutiZaring] p. 22Exercise 4inex1 5281
[TakeutiZaring] p. 22Exercise 5ruv 9629
[TakeutiZaring] p. 22Exercise 6elirr 9621
[TakeutiZaring] p. 22Exercise 7ssdif0 4317
[TakeutiZaring] p. 22Exercise 11difdif 4074
[TakeutiZaring] p. 22Exercise 13undif3 4248  undif3VD 46055
[TakeutiZaring] p. 22Exercise 14difss 4075
[TakeutiZaring] p. 22Exercise 15sscon 4082
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3081
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3091
[TakeutiZaring] p. 23Proposition 6.2xpex 7791  xpexg 7788
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5662
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6633
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6811  fun11 6636
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6571  svrelfun 6634
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5876
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5878
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5667
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5668
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5664
[TakeutiZaring] p. 25Exercise 2bj-dfrel2 38147  cnvcnvss 6198  dfrel2 6193
[TakeutiZaring] p. 25Exercise 3xpss 5671
[TakeutiZaring] p. 25Exercise 5relun 5794
[TakeutiZaring] p. 25Exercise 6reluni 5801
[TakeutiZaring] p. 25Exercise 9inxp 5815
[TakeutiZaring] p. 25Exercise 12relres 6007
[TakeutiZaring] p. 25Exercise 13opelres 5987  opelresi 5989
[TakeutiZaring] p. 25Exercise 14dmres 6015
[TakeutiZaring] p. 25Exercise 15resss 6003
[TakeutiZaring] p. 25Exercise 17resabs1 6009
[TakeutiZaring] p. 25Exercise 18funres 6602
[TakeutiZaring] p. 25Exercise 24relco 6116
[TakeutiZaring] p. 25Exercise 29funco 6600
[TakeutiZaring] p. 25Exercise 30f1co 6813
[TakeutiZaring] p. 26Definition 6.10eu2 2637
[TakeutiZaring] p. 26Definition 6.11conventions 31031  df-fv 6566  fv3 6926
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7961  cnvexg 7960
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7945  dmexg 7937
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7946  rnexg 7938
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45627
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7956
[TakeutiZaring] p. 27Corollary 6.13fvex 6921
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 48449  tz6.12-1-afv2 48516  tz6.12-1 6931  tz6.12-afv 48448  tz6.12-afv2 48515  tz6.12 6932  tz6.12c-afv2 48517  tz6.12c 6930
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 48512  tz6.12-2 6895  tz6.12i-afv2 48518  tz6.12i 6934
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6561
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6562
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6564  wfo 6556
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6563  wf1 6555
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6565  wf1o 6557
[TakeutiZaring] p. 28Exercise 4eqfnfv 7052  eqfnfv2 7053  eqfnfv2f 7056
[TakeutiZaring] p. 28Exercise 5fvco 7006
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7246
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7244
[TakeutiZaring] p. 29Exercise 9funimaex 6649  funimaexg 6648
[TakeutiZaring] p. 29Definition 6.18df-br 5107
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5564
[TakeutiZaring] p. 30Definition 6.21dffr2 5616  dffr3 6109  eliniseg 6104  iniseg 6107
[TakeutiZaring] p. 30Definition 6.22df-eprel 5555
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5632  fr3nr 7810  frirr 5631
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5608
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7812
[TakeutiZaring] p. 31Exercise 1frss 5619
[TakeutiZaring] p. 31Exercise 4wess 5641
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6368  tz6.26i 6369  wefrc 5649  wereu2 5652
[TakeutiZaring] p. 32Theorem 6.27wfi 6370  wfii 6371
[TakeutiZaring] p. 32Definition 6.28df-isom 6567
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7360
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7361
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7367
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7368
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7369
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7373
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7380
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7382
[TakeutiZaring] p. 35Notationwtr 5215
[TakeutiZaring] p. 35Theorem 7.2trelpss 45628  tz7.2 5638
[TakeutiZaring] p. 35Definition 7.1dftr3 5220
[TakeutiZaring] p. 36Proposition 7.4ordwe 6393
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6401
[TakeutiZaring] p. 36Proposition 7.6ordelord 6402  ordelordALT 45711  ordelordALTVD 46040
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6408  ordelssne 6407
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6406
[TakeutiZaring] p. 37Proposition 7.9ordin 6411
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7820
[TakeutiZaring] p. 38Corollary 7.15ordsson 7821
[TakeutiZaring] p. 38Definition 7.11df-on 6384
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6413
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45723  ordon 7815
[TakeutiZaring] p. 38Proposition 7.13onprc 7816
[TakeutiZaring] p. 39Theorem 7.17tfi 7888
[TakeutiZaring] p. 40Exercise 3ontr2 6429  ontr2d 37127
[TakeutiZaring] p. 40Exercise 7dftr2 5217
[TakeutiZaring] p. 40Exercise 9onssmin 7830
[TakeutiZaring] p. 40Exercise 11unon 7866
[TakeutiZaring] p. 40Exercise 12ordun 6487
[TakeutiZaring] p. 40Exercise 14ordequn 6486
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7817
[TakeutiZaring] p. 40Proposition 7.20elssuni 4902
[TakeutiZaring] p. 41Definition 7.22df-suc 6386
[TakeutiZaring] p. 41Proposition 7.23sssucid 6463  sucidg 6464
[TakeutiZaring] p. 41Proposition 7.24onsuc 7848
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6477  ordnbtwn 6476
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7863
[TakeutiZaring] p. 42Exercise 1df-lim 6385
[TakeutiZaring] p. 42Exercise 4omssnlim 7916
[TakeutiZaring] p. 42Exercise 7ssnlim 7921
[TakeutiZaring] p. 42Exercise 8onsucssi 7876  ordelsuc 7855
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7857
[TakeutiZaring] p. 42Definition 7.27nlimon 7886
[TakeutiZaring] p. 42Definition 7.28dfom2 7903
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7924
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7925
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7926
[TakeutiZaring] p. 43Remarkomon 7913
[TakeutiZaring] p. 43Axiom 7inf3 9663  omex 9671
[TakeutiZaring] p. 43Theorem 7.32ordom 7911
[TakeutiZaring] p. 43Corollary 7.31find 7931
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7928
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7929
[TakeutiZaring] p. 44Exercise 1limomss 7906
[TakeutiZaring] p. 44Exercise 2int0 4925
[TakeutiZaring] p. 44Exercise 3trintss 5234
[TakeutiZaring] p. 44Exercise 4intss1 4926
[TakeutiZaring] p. 44Exercise 5intex 5309
[TakeutiZaring] p. 44Exercise 6oninton 7833
[TakeutiZaring] p. 44Exercise 11ordintdif 6432
[TakeutiZaring] p. 44Definition 7.35df-int 4911
[TakeutiZaring] p. 44Proposition 7.34noinfep 9688
[TakeutiZaring] p. 45Exercise 4onint 7828
[TakeutiZaring] p. 47Lemma 1tfrlem1 8411
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8433
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8434
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8435
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8442  tz7.44-2 8443  tz7.44-3 8444
[TakeutiZaring] p. 50Exercise 1smogt 8403
[TakeutiZaring] p. 50Exercise 3smoiso 8398
[TakeutiZaring] p. 50Definition 7.46df-smo 8382
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8483  tz7.49c 8484
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8481
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8480
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8482
[TakeutiZaring] p. 53Proposition 7.532eu5 2683
[TakeutiZaring] p. 54Definition 7.55df-lexo 35989
[TakeutiZaring] p. 54Definition 7.57df-r0 35990
[TakeutiZaring] p. 54Proposition 7.58r0weseon 36000
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10117  lexoweon 35998
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10118
[TakeutiZaring] p. 55Definition 7.59df-j0 35991  j0iso 36004
[TakeutiZaring] p. 56Definition 8.1oalim 8568  oasuc 8560
[TakeutiZaring] p. 57Remarktfindsg 7896
[TakeutiZaring] p. 57Proposition 8.2oacl 8571
[TakeutiZaring] p. 57Proposition 8.3oa0 8552  oa0r 8574
[TakeutiZaring] p. 57Proposition 8.16omcl 8572
[TakeutiZaring] p. 58Corollary 8.5oacan 8584
[TakeutiZaring] p. 58Proposition 8.4nnaord 8656  nnaordi 8655  oaord 8583  oaordi 8582
[TakeutiZaring] p. 59Proposition 8.6iunss2 5011  uniss2 4905
[TakeutiZaring] p. 59Proposition 8.7oawordri 8586
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8591  oawordex 8593
[TakeutiZaring] p. 59Proposition 8.9nnacl 8648
[TakeutiZaring] p. 59Proposition 8.10oaabs 8685
[TakeutiZaring] p. 60Remarkoancom 9679
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8596
[TakeutiZaring] p. 62Exercise 1nnarcl 8653
[TakeutiZaring] p. 62Exercise 5oaword1 8588
[TakeutiZaring] p. 62Definition 8.15om0x 8555  omlim 8569  omsuc 8562
[TakeutiZaring] p. 62Definition 8.15(a)om0 8553
[TakeutiZaring] p. 63Proposition 8.17nnecl 8650  nnmcl 8649
[TakeutiZaring] p. 63Proposition 8.19nnmord 8669  nnmordi 8668  omord 8604  omordi 8602
[TakeutiZaring] p. 63Proposition 8.20omcan 8605
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8673  omwordri 8608
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8575
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8578  om1r 8579
[TakeutiZaring] p. 64Proposition 8.22om00 8611
[TakeutiZaring] p. 64Proposition 8.23omordlim 8613
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8614
[TakeutiZaring] p. 64Proposition 8.25odi 8615
[TakeutiZaring] p. 65Theorem 8.26omass 8616
[TakeutiZaring] p. 67Definition 8.30nnesuc 8645  oe0 8558  oelim 8570  oesuc 8563  onesuc 8566
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8556
[TakeutiZaring] p. 67Proposition 8.32oen0 8623
[TakeutiZaring] p. 67Proposition 8.33oeordi 8624
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8557
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8581
[TakeutiZaring] p. 68Corollary 8.34oeord 8625
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8631
[TakeutiZaring] p. 68Proposition 8.35oewordri 8629
[TakeutiZaring] p. 68Proposition 8.37oeworde 8630
[TakeutiZaring] p. 69Proposition 8.41oeoa 8634
[TakeutiZaring] p. 70Proposition 8.42oeoe 8636
[TakeutiZaring] p. 73Theorem 9.1trcl 9756  tz9.1 9757
[TakeutiZaring] p. 76Definition 9.9df-r1 9795  r10 9802  r1lim 9806  r1limg 9805  r1suc 9804  r1sucg 9803
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9814  r1ord2 9815  r1ordg 9812
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9824
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9851  tz9.13 9825  tz9.13g 9826
[TakeutiZaring] p. 79Definition 9.14df-rank 9796  rankval 9852  rankvalb 9832  rankvalg 9853
[TakeutiZaring] p. 79Proposition 9.16rankel 9878  rankelb 9860
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9894  rankval3 9880  rankval3b 9863
[TakeutiZaring] p. 79Proposition 9.18rankonid 9866
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9830
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9873  rankr1c 9857  rankr1g 9871
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9874
[TakeutiZaring] p. 80Exercise 1rankss 9890  rankssb 9889
[TakeutiZaring] p. 80Exercise 2unbndrank 9882
[TakeutiZaring] p. 80Proposition 9.19bndrank 9881
[TakeutiZaring] p. 83Axiom of Choiceac4 10580  dfac3 10227
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10136  numth 10577  numth2 10576
[TakeutiZaring] p. 85Definition 10.4cardval 10657
[TakeutiZaring] p. 85Proposition 10.5cardid 10658  cardid2 10061
[TakeutiZaring] p. 85Proposition 10.9oncard 10068
[TakeutiZaring] p. 85Proposition 10.10carden 10662
[TakeutiZaring] p. 85Proposition 10.11cardidm 10067
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 10052
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10073
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 10065
[TakeutiZaring] p. 87Proposition 10.15pwen 9197
[TakeutiZaring] p. 88Exercise 1en0 9073
[TakeutiZaring] p. 88Exercise 7infensuc 9202
[TakeutiZaring] p. 89Exercise 10omxpen 9126
[TakeutiZaring] p. 90Corollary 10.23cardnn 10071
[TakeutiZaring] p. 90Definition 10.27alephiso 10204
[TakeutiZaring] p. 90Proposition 10.20nneneq 9249
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9257
[TakeutiZaring] p. 90Proposition 10.26alephprc 10205
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9254
[TakeutiZaring] p. 91Exercise 2alephle 10194
[TakeutiZaring] p. 91Exercise 3aleph0 10172
[TakeutiZaring] p. 91Exercise 4cardlim 10080
[TakeutiZaring] p. 91Exercise 7infpss 10321
[TakeutiZaring] p. 91Exercise 8infcntss 9342
[TakeutiZaring] p. 91Definition 10.29df-fin 9005  isfi 9030
[TakeutiZaring] p. 92Proposition 10.32onfin 9258
[TakeutiZaring] p. 92Proposition 10.34imadomg 10640
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9119
[TakeutiZaring] p. 93Proposition 10.35fodomb 10632
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10291  unxpdom 9278
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10082  cardsdomelir 10081
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9280
[TakeutiZaring] p. 94Proposition 10.39infxpen 10120
[TakeutiZaring] p. 95Definition 10.42df-map 8877
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10673  infxpidm2 10123
[TakeutiZaring] p. 95Proposition 10.41infdju 10312  infxp 10319
[TakeutiZaring] p. 96Proposition 10.44pw2en 9131  pw2f1o 9129
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9190
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10592
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10587  ac6s5 10596
[TakeutiZaring] p. 98Theorem 10.47unidom 10654
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10655  uniimadomf 10656
[TakeutiZaring] p. 100Definition 11.1cfcof 10379
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10374
[TakeutiZaring] p. 102Exercise 1cfle 10358
[TakeutiZaring] p. 102Exercise 2cf0 10355
[TakeutiZaring] p. 102Exercise 3cfsuc 10362
[TakeutiZaring] p. 102Exercise 4cfom 10369
[TakeutiZaring] p. 102Proposition 11.9coftr 10378
[TakeutiZaring] p. 103Theorem 11.15alephreg 10694
[TakeutiZaring] p. 103Proposition 11.11cardcf 10356
[TakeutiZaring] p. 103Proposition 11.13alephsing 10381
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10203
[TakeutiZaring] p. 104Proposition 11.16carduniima 10202
[TakeutiZaring] p. 104Proposition 11.18alephfp 10214  alephfp2 10215
[TakeutiZaring] p. 106Theorem 11.20gchina 10811
[TakeutiZaring] p. 106Theorem 11.21mappwen 10218
[TakeutiZaring] p. 107Theorem 11.26konigth 10681
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10695
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10696
[TakeutiZaring] p. 143Definition 14.1(1)df-cnv2 35952
[TakeutiZaring] p. 143Definition 14.1(2)df-cnv3 35953
[TakeutiZaring] p. 144Definition 14.2df-gdlop1 35954  df-gdlop2 35955  df-gdlop3 35956  df-gdlop4 35957  df-gdlop5 35958  df-gdlop6 35959  df-gdlop7 35960  df-gdlop8 35961  df-gdlopc 35962
[TakeutiZaring] p. 154Proposition 15.1(1)maxssj0 36006
[TakeutiZaring] p. 154Proposition 15.1(2)j0ltaleph 36008
[TakeutiZaring] p. 155Definition 15.2df-j 35992
[TakeutiZaring] p. 155Proposition 15.3jf1 36010  jf1o 36011
[TakeutiZaring] p. 156Definition 15.7df-k1 35993  df-k2 35994  df-k3 35995
[TakeutiZaring] p. 156Proposition 15.8jk1k2k3 36018
[TakeutiZaring] p. 156Proposition 15.11jltaleph 36026
[TakeutiZaring] p. 156Proposition 15.10(1)k1le 36021  k2le 36022
[TakeutiZaring] p. 156Proposition 15.10(2)k3n0k1lt 36023  k3n0k2lt 36024
[TakeutiZaring] p. 158Definition 15.13df-fnl 35996
[TakeutiZaring] p. 158Definition 15.15df-l 35997
[TakeutiZaring] p. 158Proposition 15.14fnlfvk30 36027  fnlfvk3n0 36028
[Tarski] p. 67Axiom B5ax-c5 40132
[Tarski] p. 67Scheme B5sp 2223
[Tarski] p. 68Lemma 6avril1 31094  equid 2047
[Tarski] p. 69Lemma 7equcomi 2052
[Tarski] p. 70Lemma 14spim 2419  spime 2421  spimew 2006
[Tarski] p. 70Lemma 16ax-12 2216  ax-c15 40138  ax12i 2001
[Tarski] p. 70Lemmas 16 and 17sb6 2124
[Tarski] p. 75Axiom B7ax6v 2003
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1945  ax5ALT 40156
[Tarski], p. 75Scheme B8 of system S2ax-7 2043  ax-8 2149  ax-9 2157
[Tarski1999] p. 178Axiom 4axtgsegcon 28956
[Tarski1999] p. 178Axiom 5axtg5seg 28957
[Tarski1999] p. 179Axiom 7axtgpasch 28959
[Tarski1999] p. 180Axiom 7.1axtgpasch 28959
[Tarski1999] p. 185Axiom 11axtgcont1 28960
[Truss] p. 114Theorem 5.18ruc 16440
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38769
[Viaclovsky8] p. 3Proposition 7ismblfin 38771
[Weierstrass] p. 272Definitiondf-mdet 22930  mdetuni 22967
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 917
[WhiteheadRussell] p. 96Axiom *1.3olc 882
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 883
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 933
[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 38560
[WhiteheadRussell] p. 100Theorem *2.05frege5 44992  imim2 59  wl-luk-imim2 38555
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 48294  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 910
[WhiteheadRussell] p. 101Theorem *2.06barbara 2690  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 916
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38558
[WhiteheadRussell] p. 101Theorem *2.11exmid 908
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 911
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 46100  wl-luk-notnotr 38559
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 45022  axfrege28 45021  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 881
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 938
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 38552
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 903
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 954
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 31032  pm2.27 43  wl-luk-pm2.27 38550
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 936
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 39495
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 937
[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 1104
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 920
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 921
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 957
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 895
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 896
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 897
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 898
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 899
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 865
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 866
[WhiteheadRussell] p. 107Theorem *2.55orel1 902
[WhiteheadRussell] p. 107Theorem *2.56orel2 904
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 913
[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 905  pm2.67 906
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 912
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 988
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 914
[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 947
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 945
[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 946
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1007
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 475  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 477
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 465
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 408
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 815
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 454
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 455
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 488  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 490  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 777
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 778
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 820
[WhiteheadRussell] p. 113Fact)pm3.45 634
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 822
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 498
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 499
[WhiteheadRussell] p. 113Theorem *3.44jao 975  pm3.44 974
[WhiteheadRussell] p. 113Theorem *3.47anim12 821
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 479
[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 819
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 846
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 818  bitr 817
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 574
[WhiteheadRussell] p. 117Theorem *4.25oridm 918  pm4.25 919
[WhiteheadRussell] p. 118Theorem *4.3ancom 466
[WhiteheadRussell] p. 118Theorem *4.4andi 1025
[WhiteheadRussell] p. 118Theorem *4.31orcom 884
[WhiteheadRussell] p. 118Theorem *4.32anass 474
[WhiteheadRussell] p. 118Theorem *4.33orass 935
[WhiteheadRussell] p. 118Theorem *4.36anbi1 645
[WhiteheadRussell] p. 118Theorem *4.37orbi1 931
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 649
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 992
[WhiteheadRussell] p. 118Definition *4.34df-3an 1105
[WhiteheadRussell] p. 119Theorem *4.41ordi 1023
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1069
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1040
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1012
[WhiteheadRussell] p. 119Theorem *4.45orabs 1014  pm4.45 1013  pm4.45im 841
[WhiteheadRussell] p. 120Theorem *4.5anor 998
[WhiteheadRussell] p. 120Theorem *4.6imor 867
[WhiteheadRussell] p. 120Theorem *4.7anclb 555
[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 410
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 870
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 403
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 863
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 411
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 864
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 404
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 567  pm4.71d 571  pm4.71i 569  pm4.71r 568  pm4.71rd 572  pm4.71ri 570
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 964
[WhiteheadRussell] p. 121Theorem *4.73iba 537
[WhiteheadRussell] p. 121Theorem *4.74biorf 950
[WhiteheadRussell] p. 121Theorem *4.76jcab 527  pm4.76 528
[WhiteheadRussell] p. 121Theorem *4.77jaob 976  pm4.77 977
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 948
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1021
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 398
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 399
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1041
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1042
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 392  impexp 456  pm4.87 857
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 836
[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 1030
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1031
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1029
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 391
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 837
[WhiteheadRussell] p. 124Theorem *5.22xor 1032
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1065
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1066
[WhiteheadRussell] p. 124Theorem *5.25dfor2 915
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 583
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 393
[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 844
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 584
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 849
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 838
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 847
[WhiteheadRussell] p. 125Theorem *5.41imdi 394  pm5.41 395
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 553
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 552
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1022
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1035
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 963
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1016
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1036
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1037
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1045
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1046
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37669
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45534
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45535
[WhiteheadRussell] p. 147Theorem *10.2219.26 1903
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45536
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45537
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45538
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1928
[WhiteheadRussell] p. 151Theorem *10.301albitr 45539
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45540
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45541
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45542
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45543
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45545
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45546
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45547
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45544
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2129
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45550
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45551
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2109
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2200
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1862
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1863
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45552
[WhiteheadRussell] p. 162Theorem *11.322alim 45553
[WhiteheadRussell] p. 162Theorem *11.332albi 45554
[WhiteheadRussell] p. 162Theorem *11.342exim 45555
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45557
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45556
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1922
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45559
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45560
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45558
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1861
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45561
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45562
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1879
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45563
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2379
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1893
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45568
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45564
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45565
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45566
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45567
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45572
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45569
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45570
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45571
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45573
[WhiteheadRussell] p. 175Definition *14.02df-eu 2597
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45583  pm13.13b 45584
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45585
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3040
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3041
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3623
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45591
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45592
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45586
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45726  pm13.193 45587
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45588
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45589
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45590
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45596
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45595
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45594
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3804
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45597  pm14.122b 45598  pm14.122c 45599
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45600  pm14.123b 45601  pm14.123c 45602
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45604
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45603
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45605
[WhiteheadRussell] p. 190Theorem *14.22iota4 6538
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45606
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6539
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45607
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45609
[WhiteheadRussell] p. 192Theorem *14.26eupick 2661  eupickbi 2664  sbaniota 45610
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45608
[WhiteheadRussell] p. 192Theorem *14.271eubi 2612
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45611
[WhiteheadRussell] p. 235Definition *30.01conventions 31031  df-fv 6566
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10109  pm54.43lem 10108
[Young] p. 141Definition of operator orderingleop2 32756
[Young] p. 142Example 12.2(i)0leop 32762  idleop 32763
[vandenDries] p. 42Lemma 61irrapx1 44028
[vandenDries] p. 43Theorem 62pellex 44035  pellexlem1 44029

This page was last updated on 6-Nov-2026.
Copyright terms: Public domain