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 17843
[Adamek] p. 21Condition 3.1(b)df-cat 17843
[Adamek] p. 22Example 3.3(1)df-setc 18252
[Adamek] p. 24Example 3.3(4.c)0cat 17864  0funcg 50269  df-termc 50657
[Adamek] p. 24Example 3.3(4.d)df-prstc 50734  prsthinc 50648
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50762  df-mndtc 50762
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50758
[Adamek] p. 25Definition 3.5df-oppc 17887
[Adamek] p. 25Example 3.6(1)oduoppcciso 50750
[Adamek] p. 25Example 3.6(2)oppgoppcco 50775  oppgoppchom 50774  oppgoppcid 50776
[Adamek] p. 28Remark 3.9oppciso 17957
[Adamek] p. 28Remark 3.12invf1o 17945  invisoinvl 17966
[Adamek] p. 28Example 3.13idinv 17965  idiso 17964
[Adamek] p. 28Corollary 3.11inveq 17950
[Adamek] p. 28Definition 3.8df-inv 17924  df-iso 17925  dfiso2 17948
[Adamek] p. 28Proposition 3.10sectcan 17931
[Adamek] p. 29Remark 3.16cicer 17982  cicerALT 50230
[Adamek] p. 29Definition 3.15cic 17975  df-cic 17972
[Adamek] p. 29Definition 3.17df-func 18034
[Adamek] p. 29Proposition 3.14(1)invinv 17946
[Adamek] p. 29Proposition 3.14(2)invco 17947  isoco 17953
[Adamek] p. 30Remark 3.19df-func 18034
[Adamek] p. 30Example 3.20(1)idfucl 18057
[Adamek] p. 30Example 3.20(2)diag1 50488
[Adamek] p. 32Proposition 3.21funciso 18050
[Adamek] p. 33Example 3.26(1)discsnterm 50758  discthing 50645
[Adamek] p. 33Example 3.26(2)df-thinc 50602  prsthinc 50648  thincciso 50637  thincciso2 50639  thincciso3 50640  thinccisod 50638
[Adamek] p. 33Example 3.26(3)df-mndtc 50762
[Adamek] p. 33Proposition 3.23cofucl 18064  cofucla 50280
[Adamek] p. 34Remark 3.28(1)cofidfth 50346
[Adamek] p. 34Remark 3.28(2)catciso 18287  catcisoi 50584
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18342
[Adamek] p. 34Definition 3.27(2)df-fth 18083
[Adamek] p. 34Definition 3.27(3)df-full 18082
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18342
[Adamek] p. 35Corollary 3.32ffthiso 18107
[Adamek] p. 35Proposition 3.30(c)cofth 18113
[Adamek] p. 35Proposition 3.30(d)cofull 18112
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18327
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18327
[Adamek] p. 39Remark 3.422oppf 50316
[Adamek] p. 39Definition 3.41df-oppf 50307  funcoppc 18051
[Adamek] p. 39Definition 3.44.df-catc 18275  elcatchom 50581
[Adamek] p. 39Proposition 3.43(c)fthoppc 18101  fthoppf 50348
[Adamek] p. 39Proposition 3.43(d)fulloppc 18100  fulloppf 50347
[Adamek] p. 40Remark 3.48catccat 18284
[Adamek] p. 40Definition 3.470funcg 50269  df-catc 18275
[Adamek] p. 45Exercise 3Gincat 50785
[Adamek] p. 48Remark 4.2(2)cnelsubc 50788  nelsubc3 50255
[Adamek] p. 48Remark 4.2(3)imasubc 50335  imasubc2 50336  imasubc3 50340
[Adamek] p. 48Example 4.3(1.a)0subcat 18014
[Adamek] p. 48Example 4.3(1.b)catsubcat 18015
[Adamek] p. 48Definition 4.1(1)nelsubc3 50255
[Adamek] p. 48Definition 4.1(2)fullsubc 18026
[Adamek] p. 48Definition 4.1(a)df-subc 17988
[Adamek] p. 49Remark 4.4idsubc 50344
[Adamek] p. 49Remark 4.4(1)idemb 50343
[Adamek] p. 49Remark 4.4(2)idfullsubc 50345  ressffth 18116
[Adamek] p. 58Exercise 4Asetc1onsubc 50786
[Adamek] p. 83Definition 6.1df-nat 18122
[Adamek] p. 87Remark 6.14(a)fuccocl 18143
[Adamek] p. 87Remark 6.14(b)fucass 18147
[Adamek] p. 87Definition 6.15df-fuc 18123
[Adamek] p. 88Remark 6.16fuccat 18149
[Adamek] p. 101Definition 7.10funcg 50269  df-inito 18160
[Adamek] p. 101Example 7.2(3)0funcg 50269  df-termc 50657  initc 50275
[Adamek] p. 101Example 7.2 (6)irinitoringc 21786
[Adamek] p. 102Definition 7.4df-termo 18161  oppctermo 50420
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18188
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18192
[Adamek] p. 103Remark 7.8oppczeroo 50421
[Adamek] p. 103Definition 7.7df-zeroo 18162
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21787
[Adamek] p. 103Proposition 7.6termoeu1w 18195
[Adamek] p. 106Definition 7.19df-sect 17923
[Adamek] p. 107Example 7.20(7)thincinv 50653
[Adamek] p. 108Example 7.25(4)thincsect2 50652
[Adamek] p. 110Example 7.33(9)thincmon 50617
[Adamek] p. 110Proposition 7.35sectmon 17958
[Adamek] p. 112Proposition 7.42sectepi 17960
[Adamek] p. 185Section 10.67updjud 10016
[Adamek] p. 193Definition 11.1(1)df-lmd 50829
[Adamek] p. 193Definition 11.3(1)df-lmd 50829
[Adamek] p. 194Definition 11.3(2)df-lmd 50829
[Adamek] p. 202Definition 11.27(1)df-cmd 50830
[Adamek] p. 202Definition 11.27(2)df-cmd 50830
[Adamek] p. 478Item Rngdf-ringc 20899
[AhoHopUll] p. 2Section 1.1df-bigo 49736
[AhoHopUll] p. 12Section 1.3df-blen 49758
[AhoHopUll] p. 318Section 9.1df-concat 14717  df-pfx 14822  df-substr 14790  df-word 14660  lencl 14679  wrd0 14685
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 25028  df-nmoo 31348
[AkhiezerGlazman] p. 64Theoremhmopidmch 32756  hmopidmchi 32754
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32804  pjcmul2i 32805
[AkhiezerGlazman] p. 72Theoremcnvunop 32521  unoplin 32523
[AkhiezerGlazman] p. 72Equation 2unopadj 32522  unopadj2 32541
[AkhiezerGlazman] p. 73Theoremelunop2 32616  lnopunii 32615
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32689
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28314
[Alling] p. 184Axiom Bbdayfo 28035
[Alling] p. 184Axiom Oltsso 28034
[Alling] p. 184Axiom SDnodense 28050
[Alling] p. 185Lemma 0nocvxmin 28142
[Alling] p. 185Theoremconway 28166
[Alling] p. 185Axiom FEnoeta 28101
[Alling] p. 186Theorem 4lesrec 28186  lesrecd 28187
[Alling], p. 2Definitionrp-brsslt 44500
[Alling], p. 3Notenla0001 44503  nla0002 44501  nla0003 44502
[Apostol] p. 18Theorem I.1addcan 11495  addcan2d 11515  addcan2i 11505  addcand 11514  addcani 11504
[Apostol] p. 18Theorem I.2negeu 11548
[Apostol] p. 18Theorem I.3negsub 11607  negsubd 11676  negsubi 11637
[Apostol] p. 18Theorem I.4negneg 11609  negnegd 11661  negnegi 11629
[Apostol] p. 18Theorem I.5subdi 11750  subdid 11773  subdii 11766  subdir 11751  subdird 11774  subdiri 11767
[Apostol] p. 18Theorem I.6mul01 11490  mul01d 11510  mul01i 11501  mul02 11489  mul02d 11509  mul02i 11500
[Apostol] p. 18Theorem I.7mulcan 11954  mulcan2d 11951  mulcand 11950  mulcani 11956
[Apostol] p. 18Theorem I.8receu 11962  xreceu 33531
[Apostol] p. 18Theorem I.9divrec 11991  divrecd 12097  divreci 12063  divreczi 12056
[Apostol] p. 18Theorem I.10recrec 12015  recreci 12050
[Apostol] p. 18Theorem I.11mul0or 11957  mul0ord 11965  mul0ori 11964
[Apostol] p. 18Theorem I.12mul2neg 11756  mul2negd 11772  mul2negi 11765  mulneg1 11753  mulneg1d 11770  mulneg1i 11763
[Apostol] p. 18Theorem I.13divadddiv 12033  divadddivd 12138  divadddivi 12080
[Apostol] p. 18Theorem I.14divmuldiv 12018  divmuldivd 12135  divmuldivi 12078  rdivmuldivd 20644
[Apostol] p. 18Theorem I.15divdivdiv 12019  divdivdivd 12141  divdivdivi 12081
[Apostol] p. 20Axiom 7rpaddcl 13145  rpaddcld 13180  rpmulcl 13146  rpmulcld 13181
[Apostol] p. 20Axiom 8rpneg 13155
[Apostol] p. 20Axiom 90nrp 13158
[Apostol] p. 20Theorem I.17lttri 11437
[Apostol] p. 20Theorem I.18ltadd1d 11910  ltadd1dd 11928  ltadd1i 11871
[Apostol] p. 20Theorem I.19ltmul1 12168  ltmul1a 12167  ltmul1i 12236  ltmul1ii 12246  ltmul2 12169  ltmul2d 13207  ltmul2dd 13221  ltmul2i 12239
[Apostol] p. 20Theorem I.20msqgt0 11837  msqgt0d 11884  msqgt0i 11854
[Apostol] p. 20Theorem I.210lt1 11839
[Apostol] p. 20Theorem I.23lt0neg1 11823  lt0neg1d 11886  ltneg 11817  ltnegd 11895  ltnegi 11861
[Apostol] p. 20Theorem I.25lt2add 11802  lt2addd 11940  lt2addi 11879
[Apostol] p. 20Definition of positive numbersdf-rp 13122
[Apostol] p. 21Exercise 4recgt0 12164  recgt0d 12252  recgt0i 12223  recgt0ii 12224
[Apostol] p. 22Definition of integersdf-z 12695
[Apostol] p. 22Definition of positive integersdfnn3 12350
[Apostol] p. 22Definition of rationalsdf-q 13077
[Apostol] p. 24Theorem I.26supeu 9447
[Apostol] p. 26Theorem I.28nnunb 12603
[Apostol] p. 26Theorem I.29arch 12604  archd 46253
[Apostol] p. 28Exercise 2btwnz 12803
[Apostol] p. 28Exercise 3nnrecl 12605
[Apostol] p. 28Exercise 4rebtwnz 13075
[Apostol] p. 28Exercise 5zbtwnre 13074
[Apostol] p. 28Exercise 6qbtwnre 13330
[Apostol] p. 28Exercise 10(a)zeneo 16510  zneo 12783  zneoALTV 48843
[Apostol] p. 29Theorem I.35cxpsqrtth 27059  msqsqrtd 15611  resqrtth 15423  sqrtth 15533  sqrtthi 15539  sqsqrtd 15610
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12339
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 13041
[Apostol] p. 361Remarkcrreczi 14373
[Apostol] p. 363Remarkabsgt0i 15568
[Apostol] p. 363Exampleabssubd 15624  abssubi 15572
[ApostolNT] p. 7Remarkfmtno0 48701  fmtno1 48702  fmtno2 48711  fmtno3 48712  fmtno4 48713  fmtno5fac 48743  fmtnofz04prm 48738
[ApostolNT] p. 7Definitiondf-fmtno 48689
[ApostolNT] p. 8Definitiondf-ppi 27428
[ApostolNT] p. 14Definitiondf-dvds 16424
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16440
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16465
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16460
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16453
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16455
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16441
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16442
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16447
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16482
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16484
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16486
[ApostolNT] p. 15Definitiondf-gcd 16666  dfgcd2 16720
[ApostolNT] p. 16Definitionisprm2 16858
[ApostolNT] p. 16Theorem 1.5coprmdvds 16829
[ApostolNT] p. 16Theorem 1.7prminf 17094
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16686
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16721
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16723
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16702
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16693
[ApostolNT] p. 17Theorem 1.8coprm 16888
[ApostolNT] p. 17Theorem 1.9euclemma 16890
[ApostolNT] p. 17Theorem 1.101arith2 17107
[ApostolNT] p. 18Theorem 1.13prmrec 17101
[ApostolNT] p. 19Theorem 1.14divalg 16574
[ApostolNT] p. 20Theorem 1.15eucalg 16763
[ApostolNT] p. 24Definitiondf-mu 27429
[ApostolNT] p. 25Definitiondf-phi 16944
[ApostolNT] p. 25Theorem 2.1musum 27519
[ApostolNT] p. 26Theorem 2.2phisum 16969
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16954
[ApostolNT] p. 28Theorem 2.5(c)phimul 16958
[ApostolNT] p. 32Definitiondf-vma 27426
[ApostolNT] p. 32Theorem 2.9muinv 27521
[ApostolNT] p. 32Theorem 2.10vmasum 27544
[ApostolNT] p. 38Remarkdf-sgm 27430
[ApostolNT] p. 38Definitiondf-sgm 27430
[ApostolNT] p. 75Definitiondf-chp 27427  df-cht 27425
[ApostolNT] p. 104Definitioncongr 16840
[ApostolNT] p. 106Remarkdvdsval3 16427
[ApostolNT] p. 106Definitionmoddvds 16434
[ApostolNT] p. 107Example 2mod2eq0even 16517
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16518
[ApostolNT] p. 107Example 4zmod1congr 14029
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 14069
[ApostolNT] p. 107Theorem 5.2(c)modexp 14383
[ApostolNT] p. 108Theorem 5.3modmulconst 16459
[ApostolNT] p. 109Theorem 5.4cncongr1 16843
[ApostolNT] p. 109Theorem 5.6gcdmodi 17253
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16845
[ApostolNT] p. 113Theorem 5.17eulerth 16961
[ApostolNT] p. 113Theorem 5.18vfermltl 16980
[ApostolNT] p. 114Theorem 5.19fermltl 16962
[ApostolNT] p. 116Theorem 5.24wilthimp 27400
[ApostolNT] p. 179Definitiondf-lgs 27623  lgsprme0 27667
[ApostolNT] p. 180Example 11lgs 27668
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27644
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27659
[ApostolNT] p. 181Theorem 9.4m1lgs 27716
[ApostolNT] p. 181Theorem 9.52lgs 27735  2lgsoddprm 27744
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27702
[ApostolNT] p. 185Theorem 9.8lgsquad 27711
[ApostolNT] p. 188Definitiondf-lgs 27623  lgs1 27669
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27660
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27662
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27670
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27671
[Baer] p. 40Property (b)mapdord 42771
[Baer] p. 40Property (c)mapd11 42772
[Baer] p. 40Property (e)mapdin 42795  mapdlsm 42797
[Baer] p. 40Property (f)mapd0 42798
[Baer] p. 40Definition of projectivitydf-mapd 42758  mapd1o 42781
[Baer] p. 41Property (g)mapdat 42800
[Baer] p. 44Part (1)mapdpg 42839
[Baer] p. 45Part (2)hdmap1eq 42934  mapdheq 42861  mapdheq2 42862  mapdheq2biN 42863
[Baer] p. 45Part (3)baerlem3 42846
[Baer] p. 46Part (4)mapdheq4 42865  mapdheq4lem 42864
[Baer] p. 46Part (5)baerlem5a 42847  baerlem5abmN 42851  baerlem5amN 42849  baerlem5b 42848  baerlem5bmN 42850
[Baer] p. 47Part (6)hdmap1l6 42954  hdmap1l6a 42942  hdmap1l6e 42947  hdmap1l6f 42948  hdmap1l6g 42949  hdmap1l6lem1 42940  hdmap1l6lem2 42941  mapdh6N 42880  mapdh6aN 42868  mapdh6eN 42873  mapdh6fN 42874  mapdh6gN 42875  mapdh6lem1N 42866  mapdh6lem2N 42867
[Baer] p. 48Part 9hdmapval 42961
[Baer] p. 48Part 10hdmap10 42973
[Baer] p. 48Part 11hdmapadd 42976
[Baer] p. 48Part (6)hdmap1l6h 42950  mapdh6hN 42876
[Baer] p. 48Part (7)mapdh75cN 42886  mapdh75d 42887  mapdh75e 42885  mapdh75fN 42888  mapdh7cN 42882  mapdh7dN 42883  mapdh7eN 42881  mapdh7fN 42884
[Baer] p. 48Part (8)mapdh8 42921  mapdh8a 42908  mapdh8aa 42909  mapdh8ab 42910  mapdh8ac 42911  mapdh8ad 42912  mapdh8b 42913  mapdh8c 42914  mapdh8d 42916  mapdh8d0N 42915  mapdh8e 42917  mapdh8g 42918  mapdh8i 42919  mapdh8j 42920
[Baer] p. 48Part (9)mapdh9a 42922
[Baer] p. 48Equation 10mapdhvmap 42902
[Baer] p. 49Part 12hdmap11 42981  hdmapeq0 42977  hdmapf1oN 42998  hdmapneg 42979  hdmaprnN 42997  hdmaprnlem1N 42982  hdmaprnlem3N 42983  hdmaprnlem3uN 42984  hdmaprnlem4N 42986  hdmaprnlem6N 42987  hdmaprnlem7N 42988  hdmaprnlem8N 42989  hdmaprnlem9N 42990  hdmapsub 42980
[Baer] p. 49Part 14hdmap14lem1 43001  hdmap14lem10 43010  hdmap14lem1a 42999  hdmap14lem2N 43002  hdmap14lem2a 43000  hdmap14lem3 43003  hdmap14lem8 43008  hdmap14lem9 43009
[Baer] p. 50Part 14hdmap14lem11 43011  hdmap14lem12 43012  hdmap14lem13 43013  hdmap14lem14 43014  hdmap14lem15 43015  hgmapval 43020
[Baer] p. 50Part 15hgmapadd 43027  hgmapmul 43028  hgmaprnlem2N 43030  hgmapvs 43024
[Baer] p. 50Part 16hgmaprnN 43034
[Baer] p. 110Lemma 1hdmapip0com 43050
[Baer] p. 110Line 27hdmapinvlem1 43051
[Baer] p. 110Line 28hdmapinvlem2 43052
[Baer] p. 110Line 30hdmapinvlem3 43053
[Baer] p. 110Part 1.2hdmapglem5 43055  hgmapvv 43059
[Baer] p. 110Proposition 1hdmapinvlem4 43054
[Baer] p. 111Line 10hgmapvvlem1 43056
[Baer] p. 111Line 15hdmapg 43063  hdmapglem7 43062
[Bauer], p. 483Theorem 1.22irrexpq 27060  2irrexpqALT 27129
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2594
[BellMachover] p. 460Notationdf-mo 2564
[BellMachover] p. 460Definitionmo3 2589
[BellMachover] p. 461Axiom Extax-ext 2732
[BellMachover] p. 462Theorem 1.1axextmo 2736
[BellMachover] p. 463Axiom Repaxrep5 5238
[BellMachover] p. 463Scheme Sepax-sep 5248
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 38054  sepex 5254
[BellMachover] p. 466Problemaxpow2 5328
[BellMachover] p. 466Axiom Powaxpow3 5329
[BellMachover] p. 466Axiom Unionaxun2 7753
[BellMachover] p. 468Definitiondf-ord 6365
[BellMachover] p. 469Theorem 2.2(i)ordirr 6380
[BellMachover] p. 469Theorem 2.2(iii)onelon 6387  onelond 37023
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6382
[BellMachover] p. 471Definition of Ndf-om 7878
[BellMachover] p. 471Problem 2.5(ii)uniordint 7815
[BellMachover] p. 471Definition of Limdf-lim 6367
[BellMachover] p. 472Axiom Infzfinf2 9644
[BellMachover] p. 473Theorem 2.8limom 7893
[BellMachover] p. 477Equation 3.1df-r1 9769
[BellMachover] p. 478Definitionrankval2 9828  rankval2b 9836
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9790  r1ord3g 9787
[BellMachover] p. 480Axiom Regzfreg 9591
[BellMachover] p. 488Axiom ACac5 10556  dfac4 10202
[BellMachover] p. 490Definition of alephalephval3 10190
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40452
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32956
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32998  chirredi 32997
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32986
[Beran] p. 3Definition of joinsshjval3 31957
[Beran] p. 39Theorem 2.3(i)cmcm2 32219  cmcm2i 32196  cmcm2ii 32201  cmt2N 40383
[Beran] p. 40Theorem 2.3(iii)lecm 32220  lecmi 32205  lecmii 32206
[Beran] p. 45Theorem 3.4cmcmlem 32194
[Beran] p. 49Theorem 4.2cm2j 32223  cm2ji 32228  cm2mi 32229
[Beran] p. 95Definitiondf-sh 31810  issh2 31812
[Beran] p. 95Lemma 3.1(S5)his5 31689
[Beran] p. 95Lemma 3.1(S6)his6 31702
[Beran] p. 95Lemma 3.1(S7)his7 31693
[Beran] p. 95Lemma 3.2(S8)ho01i 32431
[Beran] p. 95Lemma 3.2(S9)hoeq1 32433
[Beran] p. 95Lemma 3.2(S10)ho02i 32432
[Beran] p. 95Lemma 3.2(S11)hoeq2 32434
[Beran] p. 95Postulate (S1)ax-his1 31685  his1i 31703
[Beran] p. 95Postulate (S2)ax-his2 31686
[Beran] p. 95Postulate (S3)ax-his3 31687
[Beran] p. 95Postulate (S4)ax-his4 31688
[Beran] p. 96Definition of normdf-hnorm 31571  dfhnorm2 31725  normval 31727
[Beran] p. 96Definition for Cauchy sequencehcau 31787
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31576
[Beran] p. 96Definition of complete subspaceisch3 31844
[Beran] p. 96Definition of convergedf-hlim 31575  hlimi 31791
[Beran] p. 97Theorem 3.3(i)norm-i-i 31736  norm-i 31732
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31740  norm-ii 31741  normlem0 31712  normlem1 31713  normlem2 31714  normlem3 31715  normlem4 31716  normlem5 31717  normlem6 31718  normlem7 31719  normlem7tALT 31722
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31742  norm-iii 31743
[Beran] p. 98Remark 3.4bcs 31784  bcsiALT 31782  bcsiHIL 31783
[Beran] p. 98Remark 3.4(B)normlem9at 31724  normpar 31758  normpari 31757
[Beran] p. 98Remark 3.4(C)normpyc 31749  normpyth 31748  normpythi 31745
[Beran] p. 99Remarklnfn0 32650  lnfn0i 32645  lnop0 32569  lnop0i 32573
[Beran] p. 99Theorem 3.5(i)nmcexi 32629  nmcfnex 32656  nmcfnexi 32654  nmcopex 32632  nmcopexi 32630
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32657  nmcfnlbi 32655  nmcoplb 32633  nmcoplbi 32631
[Beran] p. 99Theorem 3.5(iii)lnfncon 32659  lnfnconi 32658  lnopcon 32638  lnopconi 32637
[Beran] p. 100Lemma 3.6normpar2i 31759
[Beran] p. 101Lemma 3.6norm3adifi 31756  norm3adifii 31751  norm3dif 31753  norm3difi 31750
[Beran] p. 102Theorem 3.7(i)chocunii 31904  pjhth 31996  pjhtheu 31997  pjpjhth 32028  pjpjhthi 32029  pjth 25761
[Beran] p. 102Theorem 3.7(ii)ococ 32009  ococi 32008
[Beran] p. 103Remark 3.8nlelchi 32664
[Beran] p. 104Theorem 3.9riesz3i 32665  riesz4 32667  riesz4i 32666
[Beran] p. 104Theorem 3.10cnlnadj 32682  cnlnadjeu 32681  cnlnadjeui 32680  cnlnadji 32679  cnlnadjlem1 32670  nmopadjlei 32691
[Beran] p. 106Theorem 3.11(i)adjeq0 32694
[Beran] p. 106Theorem 3.11(v)nmopadji 32693
[Beran] p. 106Theorem 3.11(ii)adjmul 32695
[Beran] p. 106Theorem 3.11(iv)adjadj 32539
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32705  nmopcoadji 32704
[Beran] p. 106Theorem 3.11(iii)adjadd 32696
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32706
[Beran] p. 106Theorem 3.11(viii)adjcoi 32703  pjadj2coi 32807  pjadjcoi 32764
[Beran] p. 107Definitiondf-ch 31824  isch2 31826
[Beran] p. 107Remark 3.12choccl 31909  isch3 31844  occl 31907  ocsh 31886  shoccl 31908  shocsh 31887
[Beran] p. 107Remark 3.12(B)ococin 32011
[Beran] p. 108Theorem 3.13chintcl 31935
[Beran] p. 109Property (i)pjadj2 32790  pjadj3 32791  pjadji 32288  pjadjii 32277
[Beran] p. 109Property (ii)pjidmco 32784  pjidmcoi 32780  pjidmi 32276
[Beran] p. 110Definition of projector orderingpjordi 32776
[Beran] p. 111Remarkho0val 32353  pjch1 32273
[Beran] p. 111Definitiondf-hfmul 32337  df-hfsum 32336  df-hodif 32335  df-homul 32334  df-hosum 32333
[Beran] p. 111Lemma 4.4(i)pjo 32274
[Beran] p. 111Lemma 4.4(ii)pjch 32297  pjchi 32035
[Beran] p. 111Lemma 4.4(iii)pjoc2 32042  pjoc2i 32041
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 32283
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32768  pjssmii 32284
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32767
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32766
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32771
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32769  pjssge0ii 32285
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32770  pjdifnormii 32286
[Bobzien] p. 116Statement T3stoic3 1808
[Bobzien] p. 117Statement T2stoic2a 1806
[Bobzien] p. 117Statement T4stoic4a 1809
[Bobzien] p. 117Conclusion the contradictorystoic1a 1804
[Bogachev] p. 16Definition 1.5df-oms 34967
[Bogachev] p. 17Lemma 1.5.4omssubadd 34975
[Bogachev] p. 17Example 1.5.2omsmon 34973
[Bogachev] p. 41Definition 1.11.2df-carsg 34977
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34997
[Bogachev] p. 116Definition 2.3.1df-itgm 35028  df-sitm 35006
[Bogachev] p. 118Chapter 2.4.4df-itgm 35028
[Bogachev] p. 118Definition 2.4.1df-sitg 35005
[Bollobas] p. 1Section I.1df-edg 29627  isuhgrop 29649  isusgrop 29744  isuspgrop 29743
[Bollobas] p. 2Section I.1df-isubgr 49035  df-subgr 29850  uhgrspan1 29885  uhgrspansubgr 29873
[Bollobas] p. 3Definitiondf-gric 49055  gricuspgr 49092  isuspgrim 49070
[Bollobas] p. 3Section I.1cusgrsize 30036  df-clnbgr 48993  df-cusgr 29994  df-nbgr 29915  fusgrmaxsize 30046
[Bollobas] p. 4Definitiondf-upwlks 49308  df-wlks 30181
[Bollobas] p. 4Section I.1finsumvtxdg2size 30132  finsumvtxdgeven 30134  fusgr1th 30133  fusgrvtxdgonume 30136  vtxdgoddnumeven 30135
[Bollobas] p. 5Notationdf-pths 30300
[Bollobas] p. 5Definitiondf-crcts 30374  df-cycls 30375  df-trls 30276  df-wlkson 30182
[Bollobas] p. 7Section I.1df-ushgr 29638
[BourbakiAlg1] p. 1Definition 1df-clintop 49373  df-cllaw 49359  df-mgm 18817  df-mgm2 49392
[BourbakiAlg1] p. 4Definition 5df-assintop 49374  df-asslaw 49361  df-sgrp 18909  df-sgrp2 49394
[BourbakiAlg1] p. 7Definition 8df-cmgm2 49393  df-comlaw 49360
[BourbakiAlg1] p. 12Definition 2df-mnd 18925
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33630  mndlactf1o 33634  mndractf1 33632  mndractf1o 33635
[BourbakiAlg1] p. 92Definition 1df-ring 20462
[BourbakiAlg1] p. 93Section I.8.1df-rng 20376
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 34308
[BourbakiAlg2] p. 113Chapter 5.assafld 34312  assarrginv 34311
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34353  fldextrspunfld 34351  fldextrspunlem1 34350  fldextrspunlem2 34352  fldextrspunlsp 34349  fldextrspunlsplem 34348
[BourbakiCAlg2], p. 228Proposition 21arithidom 34112  dfufd2 34125
[BourbakiEns] p. Proposition 8fcof1 7295  fcofo 7296
[BourbakiTop1] p. Remarkxnegmnf 13341  xnegpnf 13340
[BourbakiTop1] p. Remark rexneg 13342
[BourbakiTop1] p. Remark 3ust0 24540  ustfilxp 24533
[BourbakiTop1] p. Axiom GT'tgpsubcn 24410
[BourbakiTop1] p. Criterionishmeo 24079
[BourbakiTop1] p. Example 1cstucnd 24603  iducn 24602  snfil 24184
[BourbakiTop1] p. Example 2neifil 24200
[BourbakiTop1] p. Theorem 1cnextcn 24387
[BourbakiTop1] p. Theorem 2ucnextcn 24623
[BourbakiTop1] p. Theorem 3df-hcmp 34632
[BourbakiTop1] p. Paragraph 3infil 24183
[BourbakiTop1] p. Definition 1df-ucn 24595  df-ust 24521  filintn0 24181  filn0 24182  istgp 24397  ucnprima 24601
[BourbakiTop1] p. Definition 2df-cfilu 24606
[BourbakiTop1] p. Definition 3df-cusp 24617  df-usp 24577  df-utop 24551  trust 24549
[BourbakiTop1] p. Definition 6df-pcmp 34531
[BourbakiTop1] p. Property V_issnei2 23435
[BourbakiTop1] p. Theorem 1(d)iscncl 23588
[BourbakiTop1] p. Condition F_Iustssel 24526
[BourbakiTop1] p. Condition U_Iustdiag 24529
[BourbakiTop1] p. Property V_iiinnei 23444
[BourbakiTop1] p. Property V_ivneiptopreu 23452  neissex 23446
[BourbakiTop1] p. Proposition 1neips 23432  neiss 23428  ucncn 24604  ustund 24542  ustuqtop 24566
[BourbakiTop1] p. Proposition 2cnpco 23586  neiptopreu 23452  utop2nei 24570  utop3cls 24571
[BourbakiTop1] p. Proposition 3fmucnd 24611  uspreg 24593  utopreg 24572
[BourbakiTop1] p. Proposition 4imasncld 24011  imasncls 24012  imasnopn 24010
[BourbakiTop1] p. Proposition 9cnpflf2 24320
[BourbakiTop1] p. Condition F_IIustincl 24528
[BourbakiTop1] p. Condition U_IIustinvel 24530
[BourbakiTop1] p. Property V_iiielnei 23430
[BourbakiTop1] p. Proposition 11cnextucn 24622
[BourbakiTop1] p. Condition F_IIbustbasel 24527
[BourbakiTop1] p. Condition U_IIIustexhalf 24531
[BourbakiTop1] p. Definition C'''df-cmp 23706
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 24166
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23213
[BourbakiTop2] p. 195Definition 1df-ldlf 34528
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 47148
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 47150  stoweid 47149
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 47087  stoweidlem10 47096  stoweidlem14 47100  stoweidlem15 47101  stoweidlem35 47121  stoweidlem36 47122  stoweidlem37 47123  stoweidlem38 47124  stoweidlem40 47126  stoweidlem41 47127  stoweidlem43 47129  stoweidlem44 47130  stoweidlem46 47132  stoweidlem5 47091  stoweidlem50 47136  stoweidlem52 47138  stoweidlem53 47139  stoweidlem55 47141  stoweidlem56 47142
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 47109  stoweidlem24 47110  stoweidlem27 47113  stoweidlem28 47114  stoweidlem30 47116
[BrosowskiDeutsh] p. 91Proofstoweidlem34 47120  stoweidlem59 47145  stoweidlem60 47146
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 47131  stoweidlem49 47135  stoweidlem7 47093
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 47117  stoweidlem39 47125  stoweidlem42 47128  stoweidlem48 47134  stoweidlem51 47137  stoweidlem54 47140  stoweidlem57 47143  stoweidlem58 47144
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 47111
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 47103
[BrosowskiDeutsh] p. 92Proofstoweidlem11 47097  stoweidlem13 47099  stoweidlem26 47112  stoweidlem61 47147
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 47104
[Bruck] p. 1Section I.1df-clintop 49373  df-mgm 18817  df-mgm2 49392
[Bruck] p. 23Section II.1df-sgrp 18909  df-sgrp2 49394
[Bruck] p. 28Theorem 3.2dfgrp3 19250
[ChoquetDD] p. 2Definition of mappingdf-mpt 5186
[Church] p. 129Section II.24df-ifp 1079  dfifp2 1080
[Clemente] p. 10Definition ITnatded 31005
[Clemente] p. 10Definition I` `m,nnatded 31005
[Clemente] p. 11Definition E=>m,nnatded 31005
[Clemente] p. 11Definition I=>m,nnatded 31005
[Clemente] p. 11Definition E` `(1)natded 31005
[Clemente] p. 11Definition E` `(2)natded 31005
[Clemente] p. 12Definition E` `m,n,pnatded 31005
[Clemente] p. 12Definition I` `n(1)natded 31005
[Clemente] p. 12Definition I` `n(2)natded 31005
[Clemente] p. 13Definition I` `m,n,pnatded 31005
[Clemente] p. 14Proof 5.11natded 31005
[Clemente] p. 14Definition E` `nnatded 31005
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 31007  ex-natded5.2 31006
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 31010  ex-natded5.3 31009
[Clemente] p. 18Theorem 5.5ex-natded5.5 31012
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 31014  ex-natded5.7 31013
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 31016  ex-natded5.8 31015
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 31018  ex-natded5.13 31017
[Clemente] p. 32Definition I` `nnatded 31005
[Clemente] p. 32Definition E` `m,n,p,anatded 31005
[Clemente] p. 32Definition E` `n,tnatded 31005
[Clemente] p. 32Definition I` `n,tnatded 31005
[Clemente] p. 43Theorem 9.20ex-natded9.20 31019
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 31020
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 31022  ex-natded9.26 31021
[Cohen] p. 301Remarkrelogoprlem 26920
[Cohen] p. 301Property 2relogmul 26921  relogmuld 26954
[Cohen] p. 301Property 3relogdiv 26922  relogdivd 26955
[Cohen] p. 301Property 4relogexp 26925
[Cohen] p. 301Property 1alog1 26914
[Cohen] p. 301Property 1bloge 26915
[Cohen4] p. 348Observationrelogbcxpb 27116
[Cohen4] p. 349Propertyrelogbf 27120
[Cohen4] p. 352Definitionelogb 27099
[Cohen4] p. 361Property 2relogbmul 27106
[Cohen4] p. 361Property 3logbrec 27111  relogbdiv 27108
[Cohen4] p. 361Property 4relogbreexp 27104
[Cohen4] p. 361Property 6relogbexp 27109
[Cohen4] p. 361Property 1(a)logbid1 27097
[Cohen4] p. 361Property 1(b)logb1 27098
[Cohen4] p. 367Propertylogbchbase 27100
[Cohen4] p. 377Property 2logblt 27113
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34960  sxbrsigalem4 34962
[Cohn] p. 81Section II.5acsdomd 18732  acsinfd 18731  acsinfdimd 18733  acsmap2d 18730  acsmapd 18729
[Cohn] p. 143Example 5.1.1sxbrsiga 34965
[Connell] p. 57Definitiondf-scmat 22807  df-scmatalt 49587
[Conway] p. 4Definitionlesrec 28186  lesrecd 28187
[Conway] p. 5Definitionaddsval 28349  addsval2 28350  df-adds 28347  df-muls 28494  df-negs 28408
[Conway] p. 7Theorem0lt1s 28199
[Conway] p. 12Theorem 12pw2cut2 28849
[Conway] p. 16Theorem 0(i)sltsright 28248
[Conway] p. 16Theorem 0(ii)sltsleft 28247
[Conway] p. 16Theorem 0(iii)lesid 28125
[Conway] p. 17Theorem 3addsass 28392  addsassd 28393  addscom 28353  addscomd 28354  addsrid 28351  addsridd 28352
[Conway] p. 17Definitiondf-0s 28194
[Conway] p. 17Theorem 4(ii)negnegs 28431
[Conway] p. 17Theorem 4(iii)negsid 28428  negsidd 28429
[Conway] p. 18Theorem 5leadds1 28376  leadds1d 28382
[Conway] p. 18Definitiondf-1s 28195
[Conway] p. 18Theorem 6(ii)negscl 28423  negscld 28424
[Conway] p. 18Theorem 6(iii)addscld 28367
[Conway] p. 19Notemulsunif2 28557
[Conway] p. 19Theorem 7addsdi 28542  addsdid 28543  addsdird 28544  mulnegs1d 28547  mulnegs2d 28548  mulsass 28553  mulsassd 28554  mulscom 28526  mulscomd 28527
[Conway] p. 19Theorem 8(i)mulscl 28521  mulscld 28522
[Conway] p. 19Theorem 8(iii)lemulsd 28525  ltmuls 28523  ltmulsd 28524
[Conway] p. 20Theorem 9mulsgt0 28531  mulsgt0d 28532
[Conway] p. 21Theorem 10(iv)precsex 28605
[Conway] p. 23Theorem 11eqcuts3 28191
[Conway] p. 24Definitiondf-reno 28877
[Conway] p. 24Theorem 13(ii)readdscl 28886  remulscl 28889  renegscl 28885
[Conway] p. 27Definitiondf-ons 28639  elons2 28645
[Conway] p. 27Theorem 14ltonsex 28649
[Conway] p. 28Theorem 15oncutlt 28651  onswe 28659
[Conway] p. 29Remarkmadebday 28287  newbday 28289  oldbday 28288
[Conway] p. 29Definitiondf-made 28214  df-new 28216  df-old 28215
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 14002
[Crawley] p. 1Definition of posetdf-poset 18488
[Crawley] p. 107Theorem 13.2hlsupr 40519
[Crawley] p. 110Theorem 13.3arglem1N 41323  dalaw 41019
[Crawley] p. 111Theorem 13.4hlathil 43094
[Crawley] p. 111Definition of set Wdf-watsN 41123
[Crawley] p. 111Definition of dilationdf-dilN 41239  df-ldil 41237  isldil 41243
[Crawley] p. 111Definition of translationdf-ltrn 41238  df-trnN 41240  isltrn 41252  ltrnu 41254
[Crawley] p. 112Lemma Acdlema1N 40924  cdlema2N 40925  exatleN 40537
[Crawley] p. 112Lemma B1cvrat 40609  cdlemb 40927  cdlemb2 41174  cdlemb3 41739  idltrn 41283  l1cvat 40188  lhpat 41176  lhpat2 41178  lshpat 40189  ltrnel 41272  ltrnmw 41284
[Crawley] p. 112Lemma Ccdlemc1 41324  cdlemc2 41325  ltrnnidn 41307  trlat 41302  trljat1 41299  trljat2 41300  trljat3 41301  trlne 41318  trlnidat 41306  trlnle 41319
[Crawley] p. 112Definition of automorphismdf-pautN 41124
[Crawley] p. 113Lemma Ccdlemc 41330  cdlemc3 41326  cdlemc4 41327
[Crawley] p. 113Lemma Dcdlemd 41340  cdlemd1 41331  cdlemd2 41332  cdlemd3 41333  cdlemd4 41334  cdlemd5 41335  cdlemd6 41336  cdlemd7 41337  cdlemd8 41338  cdlemd9 41339  cdleme31sde 41518  cdleme31se 41515  cdleme31se2 41516  cdleme31snd 41519  cdleme32a 41574  cdleme32b 41575  cdleme32c 41576  cdleme32d 41577  cdleme32e 41578  cdleme32f 41579  cdleme32fva 41570  cdleme32fva1 41571  cdleme32fvcl 41573  cdleme32le 41580  cdleme48fv 41632  cdleme4gfv 41640  cdleme50eq 41674  cdleme50f 41675  cdleme50f1 41676  cdleme50f1o 41679  cdleme50laut 41680  cdleme50ldil 41681  cdleme50lebi 41673  cdleme50rn 41678  cdleme50rnlem 41677  cdlemeg49le 41644  cdlemeg49lebilem 41672
[Crawley] p. 113Lemma Ecdleme 41693  cdleme00a 41342  cdleme01N 41354  cdleme02N 41355  cdleme0a 41344  cdleme0aa 41343  cdleme0b 41345  cdleme0c 41346  cdleme0cp 41347  cdleme0cq 41348  cdleme0dN 41349  cdleme0e 41350  cdleme0ex1N 41356  cdleme0ex2N 41357  cdleme0fN 41351  cdleme0gN 41352  cdleme0moN 41358  cdleme1 41360  cdleme10 41387  cdleme10tN 41391  cdleme11 41403  cdleme11a 41393  cdleme11c 41394  cdleme11dN 41395  cdleme11e 41396  cdleme11fN 41397  cdleme11g 41398  cdleme11h 41399  cdleme11j 41400  cdleme11k 41401  cdleme11l 41402  cdleme12 41404  cdleme13 41405  cdleme14 41406  cdleme15 41411  cdleme15a 41407  cdleme15b 41408  cdleme15c 41409  cdleme15d 41410  cdleme16 41418  cdleme16aN 41392  cdleme16b 41412  cdleme16c 41413  cdleme16d 41414  cdleme16e 41415  cdleme16f 41416  cdleme16g 41417  cdleme19a 41436  cdleme19b 41437  cdleme19c 41438  cdleme19d 41439  cdleme19e 41440  cdleme19f 41441  cdleme1b 41359  cdleme2 41361  cdleme20aN 41442  cdleme20bN 41443  cdleme20c 41444  cdleme20d 41445  cdleme20e 41446  cdleme20f 41447  cdleme20g 41448  cdleme20h 41449  cdleme20i 41450  cdleme20j 41451  cdleme20k 41452  cdleme20l 41455  cdleme20l1 41453  cdleme20l2 41454  cdleme20m 41456  cdleme20y 41435  cdleme20zN 41434  cdleme21 41470  cdleme21d 41463  cdleme21e 41464  cdleme22a 41473  cdleme22aa 41472  cdleme22b 41474  cdleme22cN 41475  cdleme22d 41476  cdleme22e 41477  cdleme22eALTN 41478  cdleme22f 41479  cdleme22f2 41480  cdleme22g 41481  cdleme23a 41482  cdleme23b 41483  cdleme23c 41484  cdleme26e 41492  cdleme26eALTN 41494  cdleme26ee 41493  cdleme26f 41496  cdleme26f2 41498  cdleme26f2ALTN 41497  cdleme26fALTN 41495  cdleme27N 41502  cdleme27a 41500  cdleme27cl 41499  cdleme28c 41505  cdleme3 41370  cdleme30a 41511  cdleme31fv 41523  cdleme31fv1 41524  cdleme31fv1s 41525  cdleme31fv2 41526  cdleme31id 41527  cdleme31sc 41517  cdleme31sdnN 41520  cdleme31sn 41513  cdleme31sn1 41514  cdleme31sn1c 41521  cdleme31sn2 41522  cdleme31so 41512  cdleme35a 41581  cdleme35b 41583  cdleme35c 41584  cdleme35d 41585  cdleme35e 41586  cdleme35f 41587  cdleme35fnpq 41582  cdleme35g 41588  cdleme35h 41589  cdleme35h2 41590  cdleme35sn2aw 41591  cdleme35sn3a 41592  cdleme36a 41593  cdleme36m 41594  cdleme37m 41595  cdleme38m 41596  cdleme38n 41597  cdleme39a 41598  cdleme39n 41599  cdleme3b 41362  cdleme3c 41363  cdleme3d 41364  cdleme3e 41365  cdleme3fN 41366  cdleme3fa 41369  cdleme3g 41367  cdleme3h 41368  cdleme4 41371  cdleme40m 41600  cdleme40n 41601  cdleme40v 41602  cdleme40w 41603  cdleme41fva11 41610  cdleme41sn3aw 41607  cdleme41sn4aw 41608  cdleme41snaw 41609  cdleme42a 41604  cdleme42b 41611  cdleme42c 41605  cdleme42d 41606  cdleme42e 41612  cdleme42f 41613  cdleme42g 41614  cdleme42h 41615  cdleme42i 41616  cdleme42k 41617  cdleme42ke 41618  cdleme42keg 41619  cdleme42mN 41620  cdleme42mgN 41621  cdleme43aN 41622  cdleme43bN 41623  cdleme43cN 41624  cdleme43dN 41625  cdleme5 41373  cdleme50ex 41692  cdleme50ltrn 41690  cdleme51finvN 41689  cdleme51finvfvN 41688  cdleme51finvtrN 41691  cdleme6 41374  cdleme7 41382  cdleme7a 41376  cdleme7aa 41375  cdleme7b 41377  cdleme7c 41378  cdleme7d 41379  cdleme7e 41380  cdleme7ga 41381  cdleme8 41383  cdleme8tN 41388  cdleme9 41386  cdleme9a 41384  cdleme9b 41385  cdleme9tN 41390  cdleme9taN 41389  cdlemeda 41431  cdlemedb 41430  cdlemednpq 41432  cdlemednuN 41433  cdlemefr27cl 41536  cdlemefr32fva1 41543  cdlemefr32fvaN 41542  cdlemefrs32fva 41533  cdlemefrs32fva1 41534  cdlemefs27cl 41546  cdlemefs32fva1 41556  cdlemefs32fvaN 41555  cdlemesner 41429  cdlemeulpq 41353
[Crawley] p. 114Lemma E4atex 41209  4atexlem7 41208  cdleme0nex 41423  cdleme17a 41419  cdleme17c 41421  cdleme17d 41631  cdleme17d1 41422  cdleme17d2 41628  cdleme18a 41424  cdleme18b 41425  cdleme18c 41426  cdleme18d 41428  cdleme4a 41372
[Crawley] p. 115Lemma Ecdleme21a 41458  cdleme21at 41461  cdleme21b 41459  cdleme21c 41460  cdleme21ct 41462  cdleme21f 41465  cdleme21g 41466  cdleme21h 41467  cdleme21i 41468  cdleme22gb 41427
[Crawley] p. 116Lemma Fcdlemf 41696  cdlemf1 41694  cdlemf2 41695
[Crawley] p. 116Lemma Gcdlemftr1 41700  cdlemg16 41790  cdlemg28 41837  cdlemg28a 41826  cdlemg28b 41836  cdlemg3a 41730  cdlemg42 41862  cdlemg43 41863  cdlemg44 41866  cdlemg44a 41864  cdlemg46 41868  cdlemg47 41869  cdlemg9 41767  ltrnco 41852  ltrncom 41871  tgrpabl 41884  trlco 41860
[Crawley] p. 116Definition of Gdf-tgrp 41876
[Crawley] p. 117Lemma Gcdlemg17 41810  cdlemg17b 41795
[Crawley] p. 117Definition of Edf-edring-rN 41889  df-edring 41890
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41893
[Crawley] p. 118Remarktendopltp 41913
[Crawley] p. 118Lemma Hcdlemh 41950  cdlemh1 41948  cdlemh2 41949
[Crawley] p. 118Lemma Icdlemi 41953  cdlemi1 41951  cdlemi2 41952
[Crawley] p. 118Lemma Jcdlemj1 41954  cdlemj2 41955  cdlemj3 41956  tendocan 41957
[Crawley] p. 118Lemma Kcdlemk 42107  cdlemk1 41964  cdlemk10 41976  cdlemk11 41982  cdlemk11t 42079  cdlemk11ta 42062  cdlemk11tb 42064  cdlemk11tc 42078  cdlemk11u-2N 42022  cdlemk11u 42004  cdlemk12 41983  cdlemk12u-2N 42023  cdlemk12u 42005  cdlemk13-2N 42009  cdlemk13 41985  cdlemk14-2N 42011  cdlemk14 41987  cdlemk15-2N 42012  cdlemk15 41988  cdlemk16-2N 42013  cdlemk16 41990  cdlemk16a 41989  cdlemk17-2N 42014  cdlemk17 41991  cdlemk18-2N 42019  cdlemk18-3N 42033  cdlemk18 42001  cdlemk19-2N 42020  cdlemk19 42002  cdlemk19u 42103  cdlemk1u 41992  cdlemk2 41965  cdlemk20-2N 42025  cdlemk20 42007  cdlemk21-2N 42024  cdlemk21N 42006  cdlemk22-3 42034  cdlemk22 42026  cdlemk23-3 42035  cdlemk24-3 42036  cdlemk25-3 42037  cdlemk26-3 42039  cdlemk26b-3 42038  cdlemk27-3 42040  cdlemk28-3 42041  cdlemk29-3 42044  cdlemk3 41966  cdlemk30 42027  cdlemk31 42029  cdlemk32 42030  cdlemk33N 42042  cdlemk34 42043  cdlemk35 42045  cdlemk36 42046  cdlemk37 42047  cdlemk38 42048  cdlemk39 42049  cdlemk39u 42101  cdlemk4 41967  cdlemk41 42053  cdlemk42 42074  cdlemk42yN 42077  cdlemk43N 42096  cdlemk45 42080  cdlemk46 42081  cdlemk47 42082  cdlemk48 42083  cdlemk49 42084  cdlemk5 41969  cdlemk50 42085  cdlemk51 42086  cdlemk52 42087  cdlemk53 42090  cdlemk54 42091  cdlemk55 42094  cdlemk55u 42099  cdlemk56 42104  cdlemk5a 41968  cdlemk5auN 41993  cdlemk5u 41994  cdlemk6 41970  cdlemk6u 41995  cdlemk7 41981  cdlemk7u-2N 42021  cdlemk7u 42003  cdlemk8 41971  cdlemk9 41972  cdlemk9bN 41973  cdlemki 41974  cdlemkid 42069  cdlemkj-2N 42015  cdlemkj 41996  cdlemksat 41979  cdlemksel 41978  cdlemksv 41977  cdlemksv2 41980  cdlemkuat 41999  cdlemkuel-2N 42017  cdlemkuel-3 42031  cdlemkuel 41998  cdlemkuv-2N 42016  cdlemkuv2-2 42018  cdlemkuv2-3N 42032  cdlemkuv2 42000  cdlemkuvN 41997  cdlemkvcl 41975  cdlemky 42059  cdlemkyyN 42095  tendoex 42108
[Crawley] p. 120Remarkdva1dim 42118
[Crawley] p. 120Lemma Lcdleml1N 42109  cdleml2N 42110  cdleml3N 42111  cdleml4N 42112  cdleml5N 42113  cdleml6 42114  cdleml7 42115  cdleml8 42116  cdleml9 42117  dia1dim 42194
[Crawley] p. 120Lemma Mdia11N 42181  diaf11N 42182  dialss 42179  diaord 42180  dibf11N 42294  djajN 42270
[Crawley] p. 120Definition of isomorphism mapdiaval 42165
[Crawley] p. 121Lemma Mcdlemm10N 42251  dia2dimlem1 42197  dia2dimlem2 42198  dia2dimlem3 42199  dia2dimlem4 42200  dia2dimlem5 42201  diaf1oN 42263  diarnN 42262  dvheveccl 42245  dvhopN 42249
[Crawley] p. 121Lemma Ncdlemn 42345  cdlemn10 42339  cdlemn11 42344  cdlemn11a 42340  cdlemn11b 42341  cdlemn11c 42342  cdlemn11pre 42343  cdlemn2 42328  cdlemn2a 42329  cdlemn3 42330  cdlemn4 42331  cdlemn4a 42332  cdlemn5 42334  cdlemn5pre 42333  cdlemn6 42335  cdlemn7 42336  cdlemn8 42337  cdlemn9 42338  diclspsn 42327
[Crawley] p. 121Definition of phi(q)df-dic 42306
[Crawley] p. 122Lemma Ndih11 42398  dihf11 42400  dihjust 42350  dihjustlem 42349  dihord 42397  dihord1 42351  dihord10 42356  dihord11b 42355  dihord11c 42357  dihord2 42360  dihord2a 42352  dihord2b 42353  dihord2cN 42354  dihord2pre 42358  dihord2pre2 42359  dihordlem6 42346  dihordlem7 42347  dihordlem7b 42348
[Crawley] p. 122Definition of isomorphism mapdihffval 42363  dihfval 42364  dihval 42365
[Diestel] p. 3Definitiondf-gric 49055  df-grim 49052  isuspgrim 49070
[Diestel] p. 3Section 1.1df-cusgr 29994  df-nbgr 29915
[Diestel] p. 3Definition by df-grisom 49051
[Diestel] p. 4Section 1.1df-isubgr 49035  df-subgr 29850  uhgrspan1 29885  uhgrspansubgr 29873
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 30136  vtxdgoddnumeven 30135
[Diestel] p. 27Section 1.10df-ushgr 29638
[EGA] p. 80Notation 1.1.1rspecval 34539
[EGA] p. 80Proposition 1.1.2zartop 34551
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34543  zarcls1 34544
[EGA] p. 81Corollary 1.1.8zart0 34554
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34557
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34560
[Eisenberg] p. 67Definition 5.3df-dif 4047
[Eisenberg] p. 82Definition 6.3dfom3 9649
[Eisenberg] p. 125Definition 8.21df-map 8850
[Eisenberg] p. 216Example 13.2(4)omenps 9657
[Eisenberg] p. 310Theorem 19.8cardprc 10062
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10640
[Enderton] p. 18Axiom of Empty Setaxnul 5258
[Enderton] p. 19Definitiondf-tp 4588
[Enderton] p. 26Exercise 5unissb 4900
[Enderton] p. 26Exercise 10pwel 5342
[Enderton] p. 28Exercise 7(b)pwun 5543
[Enderton] p. 30Theorem "Distributive laws"iinin1 5038  iinin2 5037  iinun2 5030  iunin1 5029  iunin1f 33195  iunin2 5028  uniin1 5032  uniin2 5033
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5036  iundif2 5031
[Enderton] p. 32Exercise 20unineq 4233
[Enderton] p. 33Exercise 23iinuni 5057
[Enderton] p. 33Exercise 25iununi 5058
[Enderton] p. 33Exercise 24(a)iinpw 5065
[Enderton] p. 33Exercise 24(b)iunpw 7785  iunpwss 5066
[Enderton] p. 36Definitionopthwiener 5486
[Enderton] p. 38Exercise 6(a)unipw 5417
[Enderton] p. 38Exercise 6(b)pwuni 4905
[Enderton] p. 41Lemma 3Dopeluu 5438  rnex 7922  rnexg 7914
[Enderton] p. 41Exercise 8dmuni 5895  rnuni 6139
[Enderton] p. 42Definition of a functiondffun7 6567  dffun8 6568
[Enderton] p. 43Definition of function valuefunfv2 6973
[Enderton] p. 43Definition of single-rootedfuncnv 6609
[Enderton] p. 44Definition (d)dfima2 6057  dfima3 6058
[Enderton] p. 47Theorem 3Hfvco2 6982
[Enderton] p. 49Axiom of Choice (first form)ac7 10552  ac7g 10553  df-ac 10196  dfac2 10211  dfac2a 10209  dfac2b 10210  dfac3 10201  dfac7 10212
[Enderton] p. 50Theorem 3K(a)imauni 7250
[Enderton] p. 52Definitiondf-map 8850
[Enderton] p. 53Exercise 21coass 6267
[Enderton] p. 53Exercise 27dmco 6256
[Enderton] p. 53Exercise 14(a)funin 6616
[Enderton] p. 53Exercise 22(a)imass2 6054
[Enderton] p. 54Remarkixpf 8949  ixpssmap 8961
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8927
[Enderton] p. 55Axiom of Choice (second form)ac9 10562  ac9s 10572
[Enderton] p. 56Theorem 3Meqvrelref 39702  erref 8739
[Enderton] p. 57Lemma 3Neqvrelthi 39705  erthi 8775
[Enderton] p. 57Definitiondf-ec 8720
[Enderton] p. 58Definitiondf-qs 8724
[Enderton] p. 61Exercise 35df-ec 8720
[Enderton] p. 65Exercise 56(a)dmun 5891
[Enderton] p. 68Definition of successordf-suc 6368
[Enderton] p. 71Definitiondf-tr 5212  dftr4 5217
[Enderton] p. 72Theorem 4Eunisuc 6444  unisucg 6443
[Enderton] p. 73Exercise 6unisuc 6444  unisucg 6443
[Enderton] p. 73Exercise 5(a)truni 5227
[Enderton] p. 73Exercise 5(b)trint 5229  trintALT 45939
[Enderton] p. 79Theorem 4I(A1)nna0 8614
[Enderton] p. 79Theorem 4I(A2)nnasuc 8616  onasuc 8537
[Enderton] p. 79Definition of operation valuedf-ov 7423
[Enderton] p. 80Theorem 4J(A1)nnm0 8615
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8617  onmsuc 8538
[Enderton] p. 81Theorem 4K(1)nnaass 8632
[Enderton] p. 81Theorem 4K(2)nna0r 8619  nnacom 8627
[Enderton] p. 81Theorem 4K(3)nndi 8633
[Enderton] p. 81Theorem 4K(4)nnmass 8634
[Enderton] p. 81Theorem 4K(5)nnmcom 8636
[Enderton] p. 82Exercise 16nnm0r 8620  nnmsucr 8635
[Enderton] p. 88Exercise 23nnaordex 8648
[Enderton] p. 129Definitiondf-en 8975
[Enderton] p. 132Theorem 6B(b)canth 7374
[Enderton] p. 133Exercise 1xpomen 10095
[Enderton] p. 133Exercise 2qnnen 16382
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9223
[Enderton] p. 135Corollary 6Cphp3 9225
[Enderton] p. 136Corollary 6Enneneq 9222
[Enderton] p. 136Corollary 6D(a)pssinf 9254
[Enderton] p. 136Corollary 6D(b)ominf 9256
[Enderton] p. 137Lemma 6Fpssnn 9185
[Enderton] p. 138Corollary 6Gssfi 9189
[Enderton] p. 139Theorem 6H(c)mapen 9161
[Enderton] p. 142Theorem 6I(3)xpdjuen 10259
[Enderton] p. 142Theorem 6I(4)mapdjuen 10260
[Enderton] p. 143Theorem 6Jdju0en 10255  dju1en 10251
[Enderton] p. 144Exercise 13iunfi 9333  unifi 9334  unifi2 9335
[Enderton] p. 144Corollary 6Kundif2 4430  unfi 9187  unfi2 9303
[Enderton] p. 145Figure 38ffoss 7958
[Enderton] p. 145Definitiondf-dom 8976
[Enderton] p. 146Example 1domen 8989  domeng 8990
[Enderton] p. 146Example 3nndomo 9234  nnsdom 9656  nnsdomg 9292
[Enderton] p. 149Theorem 6L(a)djudom2 10263
[Enderton] p. 149Theorem 6L(c)mapdom1 9162  xpdom1 9096  xpdom1g 9094  xpdom2g 9093
[Enderton] p. 149Theorem 6L(d)mapdom2 9168
[Enderton] p. 151Theorem 6Mzorn 10586  zorng 10583
[Enderton] p. 151Theorem 6M(4)ac8 10571  dfac5 10208
[Enderton] p. 159Theorem 6Qunictb 10661
[Enderton] p. 164Exampleinfdif 10287
[Enderton] p. 168Definitiondf-po 5558
[Enderton] p. 192Theorem 7M(a)oneli 6478
[Enderton] p. 192Theorem 7M(b)ontr1 6410
[Enderton] p. 192Theorem 7M(c)onirri 6477
[Enderton] p. 193Corollary 7N(b)0elon 6418
[Enderton] p. 193Corollary 7N(c)onsuci 7850
[Enderton] p. 193Corollary 7N(d)ssonunii 7795
[Enderton] p. 194Remarkonprc 7792
[Enderton] p. 194Exercise 16suc11 6472
[Enderton] p. 197Definitiondf-card 10021
[Enderton] p. 197Theorem 7Pcarden 10636
[Enderton] p. 200Exercise 25tfis 7866
[Enderton] p. 202Lemma 7Tr1tr 9784
[Enderton] p. 202Definitiondf-r1 9769
[Enderton] p. 202Theorem 7Qr1val1 9794
[Enderton] p. 204Theorem 7V(b)rankval4 9885  rankval4b 9881
[Enderton] p. 206Theorem 7X(b)en2lp 9608
[Enderton] p. 207Exercise 30rankpr 9872  rankprb 9866  rankpw 9857  rankpwi 9833  rankuniss 9884
[Enderton] p. 207Exercise 34opthreg 9620
[Enderton] p. 208Exercise 35suc11reg 9621
[Enderton] p. 212Definition of alephalephval3 10190
[Enderton] p. 213Theorem 8A(a)alephord2 10156
[Enderton] p. 213Theorem 8A(b)cardalephex 10170
[Enderton] p. 218Theorem Schema 8Eonfununi 8350
[Enderton] p. 222Definitiondf-kard 35867
[Enderton] p. 222Definition of kardkarden 9960  kardex 9958
[Enderton] p. 238Theorem 8Roeoa 8607
[Enderton] p. 238Theorem 8Soeoe 8609
[Enderton] p. 240Exercise 25oarec 8571
[Enderton] p. 257Definition of cofinalitycflm 10328
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17817
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17759
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18728  mrieqv2d 17814  mrieqvd 17813
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17818
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17823  mreexexlem2d 17820
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18734  mreexfidimd 17825
[Frege1879] p. 11Statementdf3or2 44844
[Frege1879] p. 12Statementdf3an2 44845  dfxor4 44842  dfxor5 44843
[Frege1879] p. 26Axiom 1ax-frege1 44866
[Frege1879] p. 26Axiom 2ax-frege2 44867
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44871
[Frege1879] p. 31Proposition 4frege4 44875
[Frege1879] p. 32Proposition 5frege5 44876
[Frege1879] p. 33Proposition 6frege6 44882
[Frege1879] p. 34Proposition 7frege7 44884
[Frege1879] p. 35Axiom 8ax-frege8 44885  axfrege8 44883
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38444
[Frege1879] p. 35Proposition 9frege9 44888
[Frege1879] p. 36Proposition 10frege10 44896
[Frege1879] p. 36Proposition 11frege11 44890
[Frege1879] p. 37Proposition 12frege12 44889
[Frege1879] p. 37Proposition 13frege13 44898
[Frege1879] p. 37Proposition 14frege14 44899
[Frege1879] p. 38Proposition 15frege15 44902
[Frege1879] p. 38Proposition 16frege16 44892
[Frege1879] p. 39Proposition 17frege17 44897
[Frege1879] p. 39Proposition 18frege18 44894
[Frege1879] p. 39Proposition 19frege19 44900
[Frege1879] p. 40Proposition 20frege20 44904
[Frege1879] p. 40Proposition 21frege21 44903
[Frege1879] p. 41Proposition 22frege22 44895
[Frege1879] p. 42Proposition 23frege23 44901
[Frege1879] p. 42Proposition 24frege24 44891
[Frege1879] p. 42Proposition 25frege25 44893  rp-frege25 44881
[Frege1879] p. 42Proposition 26frege26 44886
[Frege1879] p. 43Axiom 28ax-frege28 44906
[Frege1879] p. 43Proposition 27frege27 44887
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44907
[Frege1879] p. 44Axiom 31ax-frege31 44910  axfrege31 44909
[Frege1879] p. 44Proposition 30frege30 44908
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44911
[Frege1879] p. 44Proposition 33frege33 44912
[Frege1879] p. 45Proposition 34frege34 44913
[Frege1879] p. 45Proposition 35frege35 44914
[Frege1879] p. 45Proposition 36frege36 44915
[Frege1879] p. 46Proposition 37frege37 44916
[Frege1879] p. 46Proposition 38frege38 44917
[Frege1879] p. 46Proposition 39frege39 44918
[Frege1879] p. 46Proposition 40frege40 44919
[Frege1879] p. 47Axiom 41ax-frege41 44921  axfrege41 44920
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44922
[Frege1879] p. 47Proposition 43frege43 44923
[Frege1879] p. 47Proposition 44frege44 44924
[Frege1879] p. 47Proposition 45frege45 44925
[Frege1879] p. 48Proposition 46frege46 44926
[Frege1879] p. 48Proposition 47frege47 44927
[Frege1879] p. 49Proposition 48frege48 44928
[Frege1879] p. 49Proposition 49frege49 44929
[Frege1879] p. 49Proposition 50frege50 44930
[Frege1879] p. 50Axiom 52ax-frege52a 44933  ax-frege52c 44964  frege52aid 44934  frege52b 44965
[Frege1879] p. 50Axiom 54ax-frege54a 44938  ax-frege54c 44968  frege54b 44969
[Frege1879] p. 50Proposition 51frege51 44931
[Frege1879] p. 50Proposition 52dfsbcq 3740
[Frege1879] p. 50Proposition 53frege53a 44936  frege53aid 44935  frege53b 44966  frege53c 44990
[Frege1879] p. 50Proposition 54biid 264  eqid 2760
[Frege1879] p. 50Proposition 55frege55a 44944  frege55aid 44941  frege55b 44973  frege55c 44994  frege55cor1a 44945  frege55lem2a 44943  frege55lem2b 44972  frege55lem2c 44993
[Frege1879] p. 50Proposition 56frege56a 44947  frege56aid 44946  frege56b 44974  frege56c 44995
[Frege1879] p. 51Axiom 58ax-frege58a 44951  ax-frege58b 44977  frege58bid 44978  frege58c 44997
[Frege1879] p. 51Proposition 57frege57a 44949  frege57aid 44948  frege57b 44975  frege57c 44996
[Frege1879] p. 51Proposition 58spsbc 3751
[Frege1879] p. 51Proposition 59frege59a 44953  frege59b 44980  frege59c 44998
[Frege1879] p. 52Proposition 60frege60a 44954  frege60b 44981  frege60c 44999
[Frege1879] p. 52Proposition 61frege61a 44955  frege61b 44982  frege61c 45000
[Frege1879] p. 52Proposition 62frege62a 44956  frege62b 44983  frege62c 45001
[Frege1879] p. 52Proposition 63frege63a 44957  frege63b 44984  frege63c 45002
[Frege1879] p. 53Proposition 64frege64a 44958  frege64b 44985  frege64c 45003
[Frege1879] p. 53Proposition 65frege65a 44959  frege65b 44986  frege65c 45004
[Frege1879] p. 54Proposition 66frege66a 44960  frege66b 44987  frege66c 45005
[Frege1879] p. 54Proposition 67frege67a 44961  frege67b 44988  frege67c 45006
[Frege1879] p. 54Proposition 68frege68a 44962  frege68b 44989  frege68c 45007
[Frege1879] p. 55Definition 69dffrege69 45008
[Frege1879] p. 58Proposition 70frege70 45009
[Frege1879] p. 59Proposition 71frege71 45010
[Frege1879] p. 59Proposition 72frege72 45011
[Frege1879] p. 59Proposition 73frege73 45012
[Frege1879] p. 60Definition 76dffrege76 45015
[Frege1879] p. 60Proposition 74frege74 45013
[Frege1879] p. 60Proposition 75frege75 45014
[Frege1879] p. 62Proposition 77frege77 45016  frege77d 44822
[Frege1879] p. 63Proposition 78frege78 45017
[Frege1879] p. 63Proposition 79frege79 45018
[Frege1879] p. 63Proposition 80frege80 45019
[Frege1879] p. 63Proposition 81frege81 45020  frege81d 44823
[Frege1879] p. 64Proposition 82frege82 45021
[Frege1879] p. 65Proposition 83frege83 45022  frege83d 44824
[Frege1879] p. 65Proposition 84frege84 45023
[Frege1879] p. 66Proposition 85frege85 45024
[Frege1879] p. 66Proposition 86frege86 45025
[Frege1879] p. 66Proposition 87frege87 45026  frege87d 44826
[Frege1879] p. 67Proposition 88frege88 45027
[Frege1879] p. 68Proposition 89frege89 45028
[Frege1879] p. 68Proposition 90frege90 45029
[Frege1879] p. 68Proposition 91frege91 45030  frege91d 44827
[Frege1879] p. 69Proposition 92frege92 45031
[Frege1879] p. 70Proposition 93frege93 45032
[Frege1879] p. 70Proposition 94frege94 45033
[Frege1879] p. 70Proposition 95frege95 45034
[Frege1879] p. 71Definition 99dffrege99 45038
[Frege1879] p. 71Proposition 96frege96 45035  frege96d 44825
[Frege1879] p. 71Proposition 97frege97 45036  frege97d 44828
[Frege1879] p. 71Proposition 98frege98 45037  frege98d 44829
[Frege1879] p. 72Proposition 100frege100 45039
[Frege1879] p. 72Proposition 101frege101 45040
[Frege1879] p. 72Proposition 102frege102 45041  frege102d 44830
[Frege1879] p. 73Proposition 103frege103 45042
[Frege1879] p. 73Proposition 104frege104 45043
[Frege1879] p. 73Proposition 105frege105 45044
[Frege1879] p. 73Proposition 106frege106 45045  frege106d 44831
[Frege1879] p. 74Proposition 107frege107 45046
[Frege1879] p. 74Proposition 108frege108 45047  frege108d 44832
[Frege1879] p. 74Proposition 109frege109 45048  frege109d 44833
[Frege1879] p. 75Proposition 110frege110 45049
[Frege1879] p. 75Proposition 111frege111 45050  frege111d 44835
[Frege1879] p. 76Proposition 112frege112 45051
[Frege1879] p. 76Proposition 113frege113 45052
[Frege1879] p. 76Proposition 114frege114 45053  frege114d 44834
[Frege1879] p. 77Definition 115dffrege115 45054
[Frege1879] p. 77Proposition 116frege116 45055
[Frege1879] p. 78Proposition 117frege117 45056
[Frege1879] p. 78Proposition 118frege118 45057
[Frege1879] p. 78Proposition 119frege119 45058
[Frege1879] p. 78Proposition 120frege120 45059
[Frege1879] p. 79Proposition 121frege121 45060
[Frege1879] p. 79Proposition 122frege122 45061  frege122d 44836
[Frege1879] p. 79Proposition 123frege123 45062
[Frege1879] p. 80Proposition 124frege124 45063  frege124d 44837
[Frege1879] p. 81Proposition 125frege125 45064
[Frege1879] p. 81Proposition 126frege126 45065  frege126d 44838
[Frege1879] p. 82Proposition 127frege127 45066
[Frege1879] p. 83Proposition 128frege128 45067
[Frege1879] p. 83Proposition 129frege129 45068  frege129d 44839
[Frege1879] p. 84Proposition 130frege130 45069
[Frege1879] p. 85Proposition 131frege131 45070  frege131d 44840
[Frege1879] p. 86Proposition 132frege132 45071
[Frege1879] p. 86Proposition 133frege133 45072  frege133d 44841
[Fremlin1] p. 13Definition 111G (b)df-salgen 47399
[Fremlin1] p. 13Definition 111G (d)borelmbl 47722
[Fremlin1] p. 13Proposition 111G (b)salgenss 47422
[Fremlin1] p. 14Definition 112Aismea 47537
[Fremlin1] p. 15Remark 112B (d)psmeasure 47557
[Fremlin1] p. 15Property 112C (a)meadjun 47548  meadjunre 47562
[Fremlin1] p. 15Property 112C (b)meassle 47549
[Fremlin1] p. 15Property 112C (c)meaunle 47550
[Fremlin1] p. 16Property 112C (d)iundjiun 47546  meaiunle 47555  meaiunlelem 47554
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47567  meaiuninc2 47568  meaiuninc3 47571  meaiuninc3v 47570  meaiunincf 47569  meaiuninclem 47566
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47573  meaiininc2 47574  meaiininclem 47572
[Fremlin1] p. 19Theorem 113Ccaragen0 47592  caragendifcl 47600  caratheodory 47614  omelesplit 47604
[Fremlin1] p. 19Definition 113Aisome 47580  isomennd 47617  isomenndlem 47616
[Fremlin1] p. 19Remark 113B (c)omeunle 47602
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47621  voncmpl 47707
[Fremlin1] p. 19Definition 113A (ii)omessle 47584
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47609  carageniuncllem1 47607  carageniuncllem2 47608  caragenuncl 47599  caragenuncllem 47598  caragenunicl 47610
[Fremlin1] p. 21Remark 113Dcaragenel2d 47618
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47612  caratheodorylem2 47613
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47621
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47680  hoidmv1lelem1 47677  hoidmv1lelem2 47678  hoidmv1lelem3 47679
[Fremlin1] p. 25Definition 114Eisvonmbl 47724
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47680  hoidmvle 47686  hoidmvlelem1 47681  hoidmvlelem2 47682  hoidmvlelem3 47683  hoidmvlelem4 47684  hoidmvlelem5 47685  hsphoidmvle2 47671  hsphoif 47662  hsphoival 47665
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47634
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47642
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47669  hoidmvn0val 47670  hoidmvval 47663  hoidmvval0 47673  hoidmvval0b 47676
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47674  hsphoidmvle 47672
[Fremlin1] p. 30Definition 115Cdf-ovoln 47623  df-voln 47625
[Fremlin1] p. 30Proposition 115D (a)dmovn 47690  ovn0 47652  ovn0lem 47651  ovnf 47649  ovnome 47659  ovnssle 47647  ovnsslelem 47646  ovnsupge0 47643
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47689  ovnhoilem1 47687  ovnhoilem2 47688  vonhoi 47753
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47706  hoidifhspf 47704  hoidifhspval 47694  hoidifhspval2 47701  hoidifhspval3 47705  hspmbl 47715  hspmbllem1 47712  hspmbllem2 47713  hspmbllem3 47714
[Fremlin1] p. 31Definition 115Evoncmpl 47707  vonmea 47660
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47658  ovnsubadd2 47732  ovnsubadd2lem 47731  ovnsubaddlem1 47656  ovnsubaddlem2 47657
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47717  hoimbl2 47751  hoimbllem 47716  hspdifhsp 47702  opnvonmbl 47720  opnvonmbllem2 47719
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47722
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47765  iccvonmbllem 47764  ioovonmbl 47763
[Fremlin1] p. 32Proposition 115G (d)vonicc 47771  vonicclem2 47770  vonioo 47768  vonioolem2 47767  vonn0icc 47774  vonn0icc2 47778  vonn0ioo 47773  vonn0ioo2 47776
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47775  snvonmbl 47772  vonct 47779  vonsn 47777
[Fremlin1] p. 35Lemma 121Asubsalsal 47445
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47444  subsaliuncllem 47443
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47811  salpreimalegt 47795  salpreimaltle 47812
[Fremlin1] p. 35Proposition 121B (i)issmf 47814  issmff 47820  issmflem 47813
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47831  issmflelem 47830  smfpreimale 47840
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47842  issmfgtlem 47841
[Fremlin1] p. 36Definition 121Cdf-smblfn 47782  issmf 47814  issmff 47820  issmfge 47856  issmfgelem 47855  issmfgt 47842  issmfgtlem 47841  issmfle 47831  issmflelem 47830  issmflem 47813
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47793  salpreimagtlt 47816  salpreimalelt 47815
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47856  issmfgelem 47855
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47839
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47837  cnfsmf 47826
[Fremlin1] p. 36Proposition 121D (c)decsmf 47853  decsmflem 47852  incsmf 47828  incsmflem 47827
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47787  pimconstlt1 47788  smfconst 47835
[Fremlin1] p. 37Proposition 121E (b)smfadd 47851  smfaddlem1 47849  smfaddlem2 47850
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47882
[Fremlin1] p. 37Proposition 121E (d)smfmul 47881  smfmullem1 47877  smfmullem2 47878  smfmullem3 47879  smfmullem4 47880
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47883
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47886  smfpimbor1lem2 47885
[Fremlin1] p. 37Proposition 121E (g)smfco 47888
[Fremlin1] p. 37Proposition 121E (h)smfres 47876
[Fremlin1] p. 38Proposition 121E (e)smfrec 47875
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47884  smfresal 47874
[Fremlin1] p. 38Proposition 121F (a)smflim 47863  smflim2 47892  smflimlem1 47857  smflimlem2 47858  smflimlem3 47859  smflimlem4 47860  smflimlem5 47861  smflimlem6 47862  smflimmpt 47896
[Fremlin1] p. 38Proposition 121F (b)smfsup 47900  smfsuplem1 47897  smfsuplem2 47898  smfsuplem3 47899  smfsupmpt 47901  smfsupxr 47902
[Fremlin1] p. 38Proposition 121F (c)smfinf 47904  smfinflem 47903  smfinfmpt 47905
[Fremlin1] p. 39Remark 121Gsmflim 47863  smflim2 47892  smflimmpt 47896
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47894
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47924  smfdivdmmbl2 47927  smfinfdmmbl 47935  smfinfdmmbllem 47934  smfsupdmmbl 47931  smfsupdmmbllem 47930
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47914  smflimsuplem2 47907  smflimsuplem6 47911  smflimsuplem7 47912  smflimsuplem8 47913  smflimsupmpt 47915
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47917  smfliminflem 47916  smfliminfmpt 47918
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47782
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47928  fsupdm2 47929
[Fremlin1], p. 39Proposition 121Hadddmmbl 47919  adddmmbl2 47920  finfdm 47932  finfdm2 47933  fsupdm 47928  fsupdm2 47929  muldmmbl 47921  muldmmbl2 47922
[Fremlin1], p. 39Proposition 121F (c)finfdm 47932  finfdm2 47933
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25858
[Fremlin5] p. 213Lemma 565Cauniioovol 25901
[Fremlin5] p. 214Lemma 565Cauniioombl 25911
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38692
[Fremlin5] p. 220Theorem 565Maftc1anc 38695
[FreydScedrov] p. 283Axiom of Infinityax-inf 9640  inf1 9624  inf2 9625
[Gleason] p. 117Proposition 9-2.1df-enq 10997  enqer 11007
[Gleason] p. 117Proposition 9-2.2df-1nq 11002  df-nq 10998
[Gleason] p. 117Proposition 9-2.3df-plpq 10994  df-plq 11000
[Gleason] p. 119Proposition 9-2.4caovmo 7658  df-mpq 10995  df-mq 11001
[Gleason] p. 119Proposition 9-2.5df-rq 11003
[Gleason] p. 119Proposition 9-2.6ltexnq 11061
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11062  ltbtwnnq 11064
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11057
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11058
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11065
[Gleason] p. 121Definition 9-3.1df-np 11067
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11079
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11081
[Gleason] p. 122Definitiondf-1p 11068
[Gleason] p. 122Remark (1)prub 11080
[Gleason] p. 122Lemma 9-3.4prlem934 11119
[Gleason] p. 122Proposition 9-3.2df-ltp 11071
[Gleason] p. 122Proposition 9-3.3ltsopr 11118  psslinpr 11117  supexpr 11140  suplem1pr 11138  suplem2pr 11139
[Gleason] p. 123Proposition 9-3.5addclpr 11104  addclprlem1 11102  addclprlem2 11103  df-plp 11069
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11108
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11107
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11120
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11129  ltexprlem1 11122  ltexprlem2 11123  ltexprlem3 11124  ltexprlem4 11125  ltexprlem5 11126  ltexprlem6 11127  ltexprlem7 11128
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11131  ltaprlem 11130
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11132
[Gleason] p. 124Lemma 9-3.6prlem936 11133
[Gleason] p. 124Proposition 9-3.7df-mp 11070  mulclpr 11106  mulclprlem 11105  reclem2pr 11134
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11115
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11110
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11109
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11114
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11137  reclem3pr 11135  reclem4pr 11136
[Gleason] p. 126Proposition 9-4.1df-enr 11141  enrer 11149
[Gleason] p. 126Proposition 9-4.2df-0r 11146  df-1r 11147  df-nr 11142
[Gleason] p. 126Proposition 9-4.3df-mr 11144  df-plr 11143  negexsr 11188  recexsr 11193  recexsrlem 11189
[Gleason] p. 127Proposition 9-4.4df-ltr 11145
[Gleason] p. 130Proposition 10-1.3creui 12316  creur 12315  cru 12313
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11274  axcnre 11250
[Gleason] p. 132Definition 10-3.1crim 15283  crimd 15400  crimi 15361  crre 15282  crred 15399  crrei 15360
[Gleason] p. 132Definition 10-3.2remim 15285  remimd 15366
[Gleason] p. 133Definition 10.36absval2 15452  absval2d 15616  absval2i 15566
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15309  cjaddd 15388  cjaddi 15356
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15310  cjmuld 15389  cjmuli 15357
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15308  cjcjd 15367  cjcji 15339
[Gleason] p. 133Proposition 10-3.4(f)cjre 15307  cjreb 15291  cjrebd 15370  cjrebi 15342  cjred 15394  rere 15290  rereb 15288  rerebd 15369  rerebi 15341  rered 15392
[Gleason] p. 133Proposition 10-3.4(h)addcj 15316  addcjd 15380  addcji 15351
[Gleason] p. 133Proposition 10-3.7(a)absval 15406
[Gleason] p. 133Proposition 10-3.7(b)abscj 15447  abscjd 15621  abscji 15570
[Gleason] p. 133Proposition 10-3.7(c)abs00 15457  abs00d 15617  abs00i 15567  absne0d 15618
[Gleason] p. 133Proposition 10-3.7(d)releabs 15490  releabsd 15622  releabsi 15571
[Gleason] p. 133Proposition 10-3.7(f)absmul 15462  absmuld 15625  absmuli 15573
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15450  sqabsaddi 15574
[Gleason] p. 133Proposition 10-3.7(h)abstri 15499  abstrid 15627  abstrii 15577
[Gleason] p. 134Definition 10-4.1df-exp 14206  exp0 14209  expp1 14212  expp1d 14291
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 27008  cxpaddd 27046  expadd 14248  expaddd 14292  expaddz 14250
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 27017  cxpmuld 27066  expmul 14251  expmuld 14293  expmulz 14252
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 27014  mulcxpd 27057  mulexp 14245  mulexpd 14305  mulexpz 14246
[Gleason] p. 140Exercise 1znnen 16381
[Gleason] p. 141Definition 11-2.1fzval 13642
[Gleason] p. 168Proposition 12-2.1(a)climadd 15800  rlimadd 15811  rlimdiv 15814
[Gleason] p. 168Proposition 12-2.1(b)climsub 15802  rlimsub 15812
[Gleason] p. 168Proposition 12-2.1(c)climmul 15801  rlimmul 15813
[Gleason] p. 171Corollary 12-2.2climmulc2 15805
[Gleason] p. 172Corollary 12-2.5climrecl 15751
[Gleason] p. 172Proposition 12-2.4(c)climabs 15772  climcj 15773  climim 15775  climre 15774  rlimabs 15777  rlimcj 15778  rlimim 15780  rlimre 15779
[Gleason] p. 173Definition 12-3.1df-ltxr 11349  df-xr 11348  ltxr 13245
[Gleason] p. 175Definition 12-4.1df-limsup 15639  limsupval 15642
[Gleason] p. 180Theorem 12-5.1climsup 15838
[Gleason] p. 180Theorem 12-5.3caucvg 15847  caucvgb 15848  caucvgbf 46575  caucvgr 15844  climcau 15839
[Gleason] p. 182Exercise 3cvgcmp 15984
[Gleason] p. 182Exercise 4cvgrat 16053
[Gleason] p. 195Theorem 13-2.12abs1m 15504
[Gleason] p. 217Lemma 13-4.1btwnzge0 13969
[Gleason] p. 223Definition 14-1.1df-met 21673
[Gleason] p. 223Definition 14-1.1(a)met0 24663  xmet0 24662
[Gleason] p. 223Definition 14-1.1(b)metgt0 24679
[Gleason] p. 223Definition 14-1.1(c)metsym 24670
[Gleason] p. 223Definition 14-1.1(d)mettri 24672  mstri 24789  xmettri 24671  xmstri 24788
[Gleason] p. 225Definition 14-1.5xpsmet 24702
[Gleason] p. 230Proposition 14-2.6txlm 23968
[Gleason] p. 240Theorem 14-4.3metcnp4 25632
[Gleason] p. 240Proposition 14-4.2metcnp3 24860
[Gleason] p. 243Proposition 14-4.16addcn 25186  addcn2 15762  mulcn 25188  mulcn2 15764  subcn 25187  subcn2 15763
[Gleason] p. 295Remarkbcval3 14451  bcval4 14452
[Gleason] p. 295Equation 2bcpasc 14466
[Gleason] p. 295Definition of binomial coefficientbcval 14449  df-bc 14448
[Gleason] p. 296Remarkbcn0 14455  bcnn 14457
[Gleason] p. 296Theorem 15-2.8binom 16000
[Gleason] p. 308Equation 2ef0 16258
[Gleason] p. 308Equation 3efcj 16259
[Gleason] p. 309Corollary 15-4.3efne0 16265
[Gleason] p. 309Corollary 15-4.4efexp 16270
[Gleason] p. 310Equation 14sinadd 16333
[Gleason] p. 310Equation 15cosadd 16334
[Gleason] p. 311Equation 17sincossq 16345
[Gleason] p. 311Equation 18cosbnd 16350  sinbnd 16349
[Gleason] p. 311Lemma 15-4.7sqeqor 14361  sqeqori 14359
[Gleason] p. 311Definition of ` `df-pi 16239
[Godowski] p. 730Equation SFgoeqi 32876
[GodowskiGreechie] p. 249Equation IV3oai 32271
[Golan] p. 1Remarksrgisid 20436
[Golan] p. 1Definitiondf-srg 20414
[Golan] p. 149Definitiondf-slmd 33805
[Gonshor] p. 7Definitiondf-cuts 28147
[Gonshor] p. 9Theorem 2.5lesrec 28186  lesrecd 28187
[Gonshor] p. 10Theorem 2.6cofcut1 28307  cofcut1d 28308
[Gonshor] p. 10Theorem 2.7cofcut2 28309  cofcut2d 28310
[Gonshor] p. 12Theorem 2.9cofcutr 28311  cofcutr1d 28312  cofcutr2d 28313
[Gonshor] p. 13Definitiondf-adds 28347
[Gonshor] p. 14Theorem 3.1addsprop 28363
[Gonshor] p. 15Theorem 3.2addsunif 28389
[Gonshor] p. 17Theorem 3.4mulsprop 28517
[Gonshor] p. 18Theorem 3.5mulsunif 28537
[Gonshor] p. 28Lemma 4.2halfcut 28845
[Gonshor] p. 28Theorem 4.2pw2cut 28847
[Gonshor] p. 30Theorem 4.2addhalfcut 28846
[Gonshor] p. 39Theorem 4.4(b)elreno2 28882
[Gonshor] p. 95Theorem 6.1addbday 28405
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36999
[Gratzer] p. 23Section 0.6df-mre 17757
[Gratzer] p. 27Section 0.6df-mri 17759
[Hall] p. 1Section 1.1df-asslaw 49361  df-cllaw 49359  df-comlaw 49360
[Hall] p. 2Section 1.2df-clintop 49373
[Hall] p. 7Section 1.3df-sgrp2 49394
[Halmos] p. 28Partition ` `df-parts 39876  dfmembpart2 39881
[Halmos] p. 31Theorem 17.3riesz1 32668  riesz2 32669
[Halmos] p. 41Definition of Hermitianhmopadj2 32544
[Halmos] p. 42Definition of projector orderingpjordi 32776
[Halmos] p. 43Theorem 26.1elpjhmop 32788  elpjidm 32787  pjnmopi 32751
[Halmos] p. 44Remarkpjinormi 32290  pjinormii 32279
[Halmos] p. 44Theorem 26.2elpjch 32792  pjrn 32310  pjrni 32305  pjvec 32299
[Halmos] p. 44Theorem 26.3pjnorm2 32330
[Halmos] p. 44Theorem 26.4hmopidmpj 32757  hmopidmpji 32755
[Halmos] p. 45Theorem 27.1pjinvari 32794
[Halmos] p. 45Theorem 27.3pjoci 32783  pjocvec 32300
[Halmos] p. 45Theorem 27.4pjorthcoi 32772
[Halmos] p. 48Theorem 29.2pjssposi 32775
[Halmos] p. 48Theorem 29.3pjssdif1i 32778  pjssdif2i 32777
[Halmos] p. 50Definition of spectrumdf-spec 32458
[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 1827
[Hatcher] p. 25Definitiondf-phtpc 25314  df-phtpy 25293
[Hatcher] p. 26Definitiondf-pco 25327  df-pi1 25330
[Hatcher] p. 26Proposition 1.2phtpcer 25317
[Hatcher] p. 26Proposition 1.3pi1grp 25372
[Hefferon] p. 240Definition 3.12df-dmat 22806  df-dmatalt 49586
[Helfgott] p. 2Theoremtgoldbach 48991
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48976
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48988  bgoldbtbnd 48983  bgoldbtbnd 48983  tgblthelfgott 48989
[Helfgott] p. 5Proposition 1.1circlevma 35314
[Helfgott] p. 69Statement 7.49circlemethhgt 35315
[Helfgott] p. 69Statement 7.50hgt750lema 35329  hgt750lemb 35328  hgt750leme 35330  hgt750lemf 35325  hgt750lemg 35326
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48985  tgoldbachgt 35335  tgoldbachgtALTV 48986  tgoldbachgtd 35334
[Helfgott] p. 70Statement 7.49ax-hgt749 35316
[Herstein] p. 54Exercise 28df-grpo 31096
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19156  grpoideu 31112  mndideu 18935
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19186  grpoinveu 31122
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19217  grpo2inv 31134
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19229  grpoinvop 31136
[Herstein] p. 57Exercise 1dfgrp3e 19251
[Hitchcock] p. 5Rule A3mptnan 1800
[Hitchcock] p. 5Rule A4mptxor 1801
[Hitchcock] p. 5Rule A5mtpxor 1803
[Holland] p. 1519Theorem 2sumdmdi 33023
[Holland] p. 1520Lemma 5cdj1i 33036  cdj3i 33044  cdj3lem1 33037  cdjreui 33035
[Holland] p. 1524Lemma 7mddmdin0i 33034
[Holland95] p. 13Theorem 3.6hlathil 43094
[Holland95] p. 14Line 15hgmapvs 43024
[Holland95] p. 14Line 16hdmaplkr 43046
[Holland95] p. 14Line 17hdmapellkr 43047
[Holland95] p. 14Line 19hdmapglnm2 43044
[Holland95] p. 14Line 20hdmapip0com 43050
[Holland95] p. 14Theorem 3.6hdmapevec2 42969
[Holland95] p. 14Lines 24 and 25hdmapoc 43064
[Holland95] p. 204Definition of involutiondf-srng 21098
[Holland95] p. 212Definition of subspacedf-psubsp 40636
[Holland95] p. 214Lemma 3.3lclkrlem2v 42661
[Holland95] p. 214Definition 3.2df-lpolN 42614
[Holland95] p. 214Definition of nonsingularpnonsingN 41066
[Holland95] p. 215Lemma 3.3(1)dihoml4 42510  poml4N 41086
[Holland95] p. 215Lemma 3.3(2)dochexmid 42601  pexmidALTN 41111  pexmidN 41102
[Holland95] p. 218Theorem 3.6lclkr 42666
[Holland95] p. 218Definition of dual vector spacedf-ldual 40257  ldualset 40258
[Holland95] p. 222Item 1df-lines 40634  df-pointsN 40635
[Holland95] p. 222Item 2df-polarityN 41036
[Holland95] p. 223Remarkispsubcl2N 41080  omllaw4 40379  pol1N 41043  polcon3N 41050
[Holland95] p. 223Definitiondf-psubclN 41068
[Holland95] p. 223Equation for polaritypolval2N 41039
[Holmes] p. 40Definitiondf-xrn 39388
[Hughes] p. 44Equation 1.21bax-his3 31687
[Hughes] p. 47Definition of projection operatordfpjop 32785
[Hughes] p. 49Equation 1.30eighmre 32566  eigre 32438  eigrei 32437
[Hughes] p. 49Equation 1.31eighmorth 32567  eigorth 32441  eigorthi 32440
[Hughes] p. 137Remark (ii)eigposi 32439
[Huneke] p. 1Claim 1frgrncvvdeq 30911
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30907
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30908
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30909
[Huneke] p. 2Claim 2frgrregorufr 30927  frgrregorufr0 30926  frgrregorufrg 30928
[Huneke] p. 2Claim 3frgrhash2wsp 30934  frrusgrord 30943  frrusgrord0 30942
[Huneke] p. 2Statementdf-clwwlknon 30680
[Huneke] p. 2Statement 4frgrwopreglem4 30917
[Huneke] p. 2Statement 5frgrwopreg1 30920  frgrwopreg2 30921  frgrwopregasn 30918  frgrwopregbsn 30919
[Huneke] p. 2Statement 6frgrwopreglem5 30923
[Huneke] p. 2Statement 7fusgreghash2wspv 30937
[Huneke] p. 2Statement 8fusgreghash2wsp 30940
[Huneke] p. 2Statement 9clwlksndivn 30678  numclwlk1 30973  numclwlk1lem1 30971  numclwlk1lem2 30972  numclwwlk1 30963  numclwwlk8 30994
[Huneke] p. 2Definition 3frgrwopreglem1 30914
[Huneke] p. 2Definition 4df-clwlks 30359
[Huneke] p. 2Definition 62clwwlk 30949
[Huneke] p. 2Definition 7numclwwlkovh 30975  numclwwlkovh0 30974
[Huneke] p. 2Statement 10numclwwlk2 30983
[Huneke] p. 2Statement 11rusgrnumwlkg 30570
[Huneke] p. 2Statement 12numclwwlk3 30987
[Huneke] p. 2Statement 13numclwwlk5 30990
[Huneke] p. 2Statement 14numclwwlk7 30993
[Indrzejczak] p. 33Definition ` `Enatded 31005  natded 31005
[Indrzejczak] p. 33Definition ` `Inatded 31005
[Indrzejczak] p. 34Definition ` `Enatded 31005  natded 31005
[Indrzejczak] p. 34Definition ` `Inatded 31005
[Jech] p. 4Definition of classcv 1568  cvjust 2754
[Jech] p. 42Lemma 6.1alephexp1 10665
[Jech] p. 42Equation 6.1alephadd 10663  alephmul 10664
[Jech] p. 43Lemma 6.2infmap 10662  infmap2 10296
[Jech] p. 71Lemma 9.3jech9.3 9823
[Jech] p. 72Equation 9.3df-scott 9930
[Jech] p. 72Exercise 9.1rankval4 9885  rankval4b 9881
[Jech] p. 72Scheme "Collection Principle"cp 9955
[Jech] p. 78Noteopthprc 5714
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43998
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 44086
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 44087
[JonesMatijasevic] p. 695Equation 2.7rmxadd 44010
[JonesMatijasevic] p. 695Equation 2.8rmyadd 44014
[JonesMatijasevic] p. 695Equation 2.9rmxp1 44015  rmyp1 44016
[JonesMatijasevic] p. 695Equation 2.10rmxm1 44017  rmym1 44018
[JonesMatijasevic] p. 695Equation 2.11rmx0 44008  rmx1 44009  rmxluc 44019
[JonesMatijasevic] p. 695Equation 2.12rmy0 44012  rmy1 44013  rmyluc 44020
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 44022
[JonesMatijasevic] p. 695Equation 2.14rmydbl 44023
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 44043  jm2.17b 44044  jm2.17c 44045
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 44076
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 44080
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 44071
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 44046  jm2.24nn 44042
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 44085
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 44091  rmygeid 44047
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 44103
[Juillerat] p. 11Section *5etransc 47369  etransclem47 47367  etransclem48 47368
[Juillerat] p. 12Equation (7)etransclem44 47364
[Juillerat] p. 12Equation *(7)etransclem46 47366
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 47352
[Juillerat] p. 13Proofetransclem35 47355
[Juillerat] p. 13Part of case 2 proven inetransclem38 47358
[Juillerat] p. 13Part of case 2 provenetransclem24 47344
[Juillerat] p. 13Part of case 2: proven inetransclem41 47361
[Juillerat] p. 14Proofetransclem23 47343
[KalishMontague] p. 81Note 1ax-6 1999
[KalishMontague] p. 85Lemma 2equid 2044
[KalishMontague] p. 85Lemma 3equcomi 2049
[KalishMontague] p. 86Lemma 7cbvalivw 2039  cbvaliw 2038  wl-cbvmotv 38521  wl-motae 38523  wl-moteq 38522
[KalishMontague] p. 87Lemma 8spimvw 2018  spimw 2002
[KalishMontague] p. 87Lemma 9spfw 2065  spw 2066
[Kalmbach] p. 14Definition of latticechabs1 32119  chabs1i 32121  chabs2 32120  chabs2i 32122  chjass 32136  chjassi 32089  latabs1 18650  latabs2 18651
[Kalmbach] p. 15Definition of atomdf-at 32941  ela 32942
[Kalmbach] p. 15Definition of coverscvbr2 32886  cvrval2 40407
[Kalmbach] p. 16Definitiondf-ol 40311  df-oml 40312
[Kalmbach] p. 20Definition of commutescmbr 32187  cmbri 32193  cmtvalN 40344  df-cm 32186  df-cmtN 40310
[Kalmbach] p. 22Remarkomllaw5N 40380  pjoml5 32216  pjoml5i 32191
[Kalmbach] p. 22Definitionpjoml2 32214  pjoml2i 32188
[Kalmbach] p. 22Theorem 2(v)cmcm 32217  cmcmi 32195  cmcmii 32200  cmtcomN 40382
[Kalmbach] p. 22Theorem 2(ii)omllaw3 40378  omlsi 32007  pjoml 32039  pjomli 32038
[Kalmbach] p. 22Definition of OML lawomllaw2N 40377
[Kalmbach] p. 23Remarkcmbr2i 32199  cmcm3 32218  cmcm3i 32197  cmcm3ii 32202  cmcm4i 32198  cmt3N 40384  cmt4N 40385  cmtbr2N 40386
[Kalmbach] p. 23Lemma 3cmbr3 32211  cmbr3i 32203  cmtbr3N 40387
[Kalmbach] p. 25Theorem 5fh1 32221  fh1i 32224  fh2 32222  fh2i 32225  omlfh1N 40391
[Kalmbach] p. 65Remarkchjatom 32960  chslej 32101  chsleji 32061  shslej 31983  shsleji 31973
[Kalmbach] p. 65Proposition 1chocin 32098  chocini 32057  chsupcl 31943  chsupval2 32013  h0elch 31858  helch 31846  hsupval2 32012  ocin 31899  ococss 31896  shococss 31897
[Kalmbach] p. 65Definition of subspace sumshsval 31915
[Kalmbach] p. 66Remarkdf-pjh 31998  pjssmi 32768  pjssmii 32284
[Kalmbach] p. 67Lemma 3osum 32248  osumi 32245
[Kalmbach] p. 67Lemma 4pjci 32803
[Kalmbach] p. 103Exercise 6atmd2 33003
[Kalmbach] p. 103Exercise 12mdsl0 32913
[Kalmbach] p. 140Remarkhatomic 32963  hatomici 32962  hatomistici 32965
[Kalmbach] p. 140Proposition 1atlatmstc 40452
[Kalmbach] p. 140Proposition 1(i)atexch 32984  lsatexch 40176
[Kalmbach] p. 140Proposition 1(ii)chcv1 32958  cvlcvr1 40472  cvr1 40543
[Kalmbach] p. 140Proposition 1(iii)cvexch 32977  cvexchi 32972  cvrexch 40553
[Kalmbach] p. 149Remark 2chrelati 32967  hlrelat 40535  hlrelat5N 40534  lrelat 40147
[Kalmbach] p. 153Exercise 5lsmcv 21420  lsmsatcv 40143  spansncv 32256  spansncvi 32255
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 40162  spansncv2 32896
[Kalmbach] p. 266Definitiondf-st 32814
[Kalmbach2] p. 8Definition of adjointdf-adjh 32452
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10732  fpwwe2 10729
[KanamoriPincus] p. 416Corollary 1.3canth4 10733
[KanamoriPincus] p. 417Corollary 1.6canthp1 10740
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10735
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10737
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10750
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10754  gchxpidm 10755
[KanamoriPincus] p. 419Theorem 2.1gchacg 10766  gchhar 10765
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10294  unxpwdom 9584
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10756
[Kreyszig] p. 3Property M1metcl 24652  xmetcl 24651
[Kreyszig] p. 4Property M2meteq0 24659
[Kreyszig] p. 8Definition 1.1-8dscmet 24892
[Kreyszig] p. 12Equation 5conjmul 12035  muleqadd 11961
[Kreyszig] p. 18Definition 1.3-2mopnval 24758
[Kreyszig] p. 19Remarkmopntopon 24759
[Kreyszig] p. 19Theorem T1mopn0 24818  mopnm 24764
[Kreyszig] p. 19Theorem T2unimopn 24816
[Kreyszig] p. 19Definition of neighborhoodneibl 24821
[Kreyszig] p. 20Definition 1.3-3metcnp2 24862
[Kreyszig] p. 25Definition 1.4-1lmbr 23577  lmmbr 25580  lmmbr2 25581
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23699
[Kreyszig] p. 28Theorem 1.4-5lmcau 25635
[Kreyszig] p. 28Definition 1.4-3iscau 25598  iscmet2 25616
[Kreyszig] p. 30Theorem 1.4-7cmetss 25638
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23781  metelcls 25627
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25628  metcld2 25629
[Kreyszig] p. 51Equation 2clmvneg1 25421  lmodvneg1 21181  nvinv 31242  vcm 31179
[Kreyszig] p. 51Equation 1aclm0vs 25417  lmod0vs 21171  slmd0vs 33828  vc0 31177
[Kreyszig] p. 51Equation 1blmodvs0 21172  slmdvs0 33829  vcz 31178
[Kreyszig] p. 58Definition 2.2-1imsmet 31294  ngpmet 24923  nrmmetd 24894
[Kreyszig] p. 59Equation 1imsdval 31289  imsdval2 31290  ncvspds 25483  ngpds 24924
[Kreyszig] p. 63Problem 1nmval 24909  nvnd 31291
[Kreyszig] p. 64Problem 2nmeq0 24938  nmge0 24937  nvge0 31276  nvz 31272
[Kreyszig] p. 64Problem 3nmrtri 24944  nvabs 31275
[Kreyszig] p. 91Definition 2.7-1isblo3i 31404
[Kreyszig] p. 92Equation 2df-nmoo 31348
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31410  blocni 31408
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31409
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25526  ipeq0 21945  ipz 31322
[Kreyszig] p. 135Problem 2cphpyth 25538  pythi 31453
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31457
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25560
[Kreyszig] p. 144Equation 4supcvg 16026
[Kreyszig] p. 144Theorem 3.3-1minvec 25758  minveco 31487
[Kreyszig] p. 196Definition 3.9-1df-aj 31353
[Kreyszig] p. 247Theorem 4.7-2bcth 25651
[Kreyszig] p. 249Theorem 4.7-3ubth 31476
[Kreyszig] p. 470Definition of positive operator orderingleop 32726  leopg 32725
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32744
[Kreyszig] p. 525Theorem 10.1-1htth 31521
[Kulpa] p. 547Theorempoimir 38647
[Kulpa] p. 547Equation (1)poimirlem32 38646
[Kulpa] p. 547Equation (2)poimirlem31 38645
[Kulpa] p. 548Theorembroucube 38648
[Kulpa] p. 548Equation (6)poimirlem26 38640
[Kulpa] p. 548Equation (7)poimirlem27 38641
[Kunen] p. 10Axiom 0ax6e 2412  axnul 5258
[Kunen] p. 11Axiom 3axnul 5258
[Kunen] p. 12Axiom 6zfrep6 5241
[Kunen] p. 24Definition 10.24mapval 8859  mapvalg 8857
[Kunen] p. 30Lemma 10.20fodomg 10601
[Kunen] p. 31Definition 10.24mapex 7952
[Kunen] p. 95Definition 2.1df-r1 9769
[Kunen] p. 97Lemma 2.10r1elss 9815  r1elssi 9814
[Kunen] p. 107Exercise 4rankop 9873  rankopb 9867  rankuni 9880  rankxplim 9897  rankxpsuc 9900
[Kunen2] p. 47Lemma I.9.9relpfr 46020
[Kunen2] p. 53Lemma I.9.21trfr 46028
[Kunen2] p. 53Lemma I.9.24(2)wffr 46027
[Kunen2] p. 53Definition I.9.20tcfr 46029
[Kunen2] p. 95Lemma I.16.2ralabso 46034  rexabso 46035
[Kunen2] p. 96Example I.16.3disjabso 46041  n0abso 46042  ssabso 46040
[Kunen2] p. 111Lemma II.2.4(1)traxext 46043
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 46053
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 46048
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 46051
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 46052
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 46047
[Kunen2] p. 112Corollary II.2.5wfaxext 46059  wfaxpr 46064  wfaxreg 46066  wfaxrep 46060  wfaxsep 46061  wfaxun 46065
[Kunen2] p. 113Lemma II.2.8pwclaxpow 46050
[Kunen2] p. 113Corollary II.2.9wfaxpow 46063
[Kunen2] p. 114Theorem II.2.13wfaxext 46059
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 46058  omelaxinf2 46055
[Kunen2] p. 114Corollary II.2.12wfac8prim 46068  wfaxinf2 46067
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 46081  permaxext 46071  permaxinf2 46079  permaxnul 46074  permaxpow 46075  permaxpr 46076  permaxrep 46072  permaxsep 46073  permaxun 46077
[Kunen2] p. 148Definition II.9.1brpermmodel 46069
[Kunen2] p. 149Exercise II.9.3permac8prim 46080
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4963
[Lang] , p. 225Corollary 1.3finexttrb 34340
[Lang] p. Definitiondf-rn 5661
[Lang] p. 3Statementlidrideqd 18851  mndbn0 18941
[Lang] p. 3Definitiondf-mnd 18925
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18877
[Lang] p. 4Property of composites. Second formulagsumccat 19038
[Lang] p. 5Equationgsumreidx 20132
[Lang] p. 5Definition of an (infinite) productgsumfsupp 49355
[Lang] p. 6Examplenn0mnd 49352
[Lang] p. 6Equationgsumxp2 20195
[Lang] p. 6Statementcycsubm 19418
[Lang] p. 6Definitionmulgnn0gsum 19291
[Lang] p. 6Observationmndlsmidm 19885
[Lang] p. 7Definitiondfgrp2e 19175
[Lang] p. 30Definitiondf-tocyc 33711
[Lang] p. 32Property (a)cyc3genpm 33756
[Lang] p. 32Property (b)cyc3conja 33761  cycpmconjv 33746
[Lang] p. 53Definitiondf-cat 17843
[Lang] p. 53Axiom CAT 1cat1 18273  cat1lem 18272
[Lang] p. 54Definitiondf-iso 17925
[Lang] p. 57Definitiondf-inito 18160  df-termo 18161
[Lang] p. 58Exampleirinitoringc 21786
[Lang] p. 58Statementinitoeu1 18187  termoeu1 18194
[Lang] p. 62Definitiondf-func 18034
[Lang] p. 65Definitiondf-nat 18122
[Lang] p. 83Definition of "ring with unit"dfring2 20518
[Lang] p. 91Notedf-ringc 20899
[Lang] p. 92Statementmxidlprm 34038
[Lang] p. 92Definitionisprmidlc 21629
[Lang] p. 128Remarkdsmmlmod 22052
[Lang] p. 129Prooflincscm 49618  lincscmcl 49620  lincsum 49617  lincsumcl 49619
[Lang] p. 129Statementlincolss 49622
[Lang] p. 129Observationdsmmfi 22045
[Lang] p. 141Theorem 5.3dimkerim 34302  qusdimsum 34303
[Lang] p. 141Corollary 5.4lssdimle 34283
[Lang] p. 147Definitionsnlindsntor 49659
[Lang] p. 504Statementmat1 22763  matring 22759
[Lang] p. 504Definitiondf-mamu 22707
[Lang] p. 505Statementmamuass 22718  mamutpos 22774  matassa 22760  mattposvs 22771  tposmap 22773
[Lang] p. 513Definitionmdet1 22917  mdetf 22911
[Lang] p. 513Theorem 4.4cramer 23010
[Lang] p. 514Proposition 4.6mdetleib 22903
[Lang] p. 514Proposition 4.8mdettpos 22927
[Lang] p. 515Definitiondf-minmar1 22951  smadiadetr 22991
[Lang] p. 515Corollary 4.9mdetero 22926  mdetralt 22924
[Lang] p. 517Proposition 4.15mdetmul 22939
[Lang] p. 518Definitiondf-madu 22950
[Lang] p. 518Proposition 4.16madulid 22961  madurid 22960  matinv 22993
[Lang] p. 561Theorem 3.1cayleyhamilton 23209
[Lang], p. 190Chapter 6vieta 34255
[Lang], p. 224Proposition 1.1extdgfialg 34369  finextalg 34373
[Lang], p. 224Proposition 1.2extdgmul 34338  fedgmul 34306
[Lang], p. 225Proposition 1.4algextdeg 34400
[Lang], p. 561Remarkchpmatply1 23151
[Lang], p. 561Definitiondf-chpmat 23146
[Lang2] p. 3Notationsdf-ind 12322
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45394
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45389
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45395
[LeBlanc] p. 277Rule R2axnul 5258
[Levy] p. 12Axiom 4.3.1df-clab 2739  wl-df.clab 38506
[Levy] p. 59Definitiondf-ttrcl 9710
[Levy] p. 64Theorem 5.6(ii)frinsg 9756
[Levy] p. 338Axiomdf-clel 2835  df-cleq 2752  wl-df.cleq 38507
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38510
[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 38510
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2835  df-cleq 2752  wl-df.cleq 38507
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2739  wl-df.clab 38506
[Levy] p. 358Axiomdf-clab 2739  wl-df.clab 38506
[Levy58] p. 2Definition Iisfin1-3 10465
[Levy58] p. 2Definition IIdf-fin2 10365
[Levy58] p. 2Definition Iadf-fin1a 10364
[Levy58] p. 2Definition IIIdf-fin3 10367
[Levy58] p. 3Definition Vdf-fin5 10368
[Levy58] p. 3Definition IVdf-fin4 10366
[Levy58] p. 4Definition VIdf-fin6 10369
[Levy58] p. 4Definition VIIdf-fin7 10370
[Levy58], p. 3Theorem 1fin1a2 10494
[Lipparini] p. 3Lemma 2.1.1nosepssdm 28044
[Lipparini] p. 3Lemma 2.1.4noresle 28055
[Lipparini] p. 6Proposition 4.2noinfbnd1 28087  nosupbnd1 28072
[Lipparini] p. 6Proposition 4.3noinfbnd2 28089  nosupbnd2 28074
[Lipparini] p. 7Theorem 5.1noetasuplem3 28093  noetasuplem4 28094
[Lipparini] p. 7Corollary 4.4nosupinfsep 28090
[Lopez-Astorga] p. 12Rule 1mptnan 1800
[Lopez-Astorga] p. 12Rule 2mptxor 1801
[Lopez-Astorga] p. 12Rule 3mtpxor 1803
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 33011
[Maeda] p. 168Lemma 5mdsym 33015  mdsymi 33014
[Maeda] p. 168Lemma 4(i)mdsymlem4 33009  mdsymlem6 33011  mdsymlem7 33012
[Maeda] p. 168Lemma 4(ii)mdsymlem8 33013
[MaedaMaeda] p. 1Remarkssdmd1 32916  ssdmd2 32917  ssmd1 32914  ssmd2 32915
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32912
[MaedaMaeda] p. 1Definition 1.1df-dmd 32884  df-md 32883  mdbr 32897
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32934  mdslj1i 32922  mdslj2i 32923  mdslle1i 32920  mdslle2i 32921  mdslmd1i 32932  mdslmd2i 32933
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32924  mdsl2bi 32926  mdsl2i 32925
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32938
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32935
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32936
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32913
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32918  mdsl3 32919
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32937
[MaedaMaeda] p. 4Theorem 1.14mdcompli 33032
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40454  hlrelat1 40533
[MaedaMaeda] p. 31Lemma 7.5lcvexch 40172
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32939  cvmdi 32927  cvnbtwn4 32892  cvrnbtwn4 40412
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32940
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40473  cvp 32978  cvrp 40549  lcvp 40173
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 33002
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 33001
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40466  hlexch4N 40525
[MaedaMaeda] p. 34Exercise 7.1atabsi 33004
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40576
[MaedaMaeda] p. 61Definition 15.10psubN 40882  atpsubN 40886  df-pointsN 40635  pointpsubN 40884
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40637  pmap11 40895  pmaple 40894  pmapsub 40901  pmapval 40890
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40898  pmap1N 40900
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40903  pmapglb2N 40904  pmapglb2xN 40905  pmapglbx 40902
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40985
[MaedaMaeda] p. 67Postulate PS1ps-1 40610
[MaedaMaeda] p. 68Lemma 16.2df-padd 40929  paddclN 40975  paddidm 40974
[MaedaMaeda] p. 68Condition PS2ps-2 40611
[MaedaMaeda] p. 68Equation 16.2.1paddass 40971
[MaedaMaeda] p. 69Lemma 16.4ps-1 40610
[MaedaMaeda] p. 69Theorem 16.4ps-2 40611
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19890  lsmmod2 19891  lssats 40145  shatomici 32961  shatomistici 32964  shmodi 31993  shmodsi 31992
[MaedaMaeda] p. 130Remark 29.6dmdmd 32903  mdsymlem7 33012
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 32192
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 32096
[MaedaMaeda] p. 139Remarksumdmdii 33018
[Margaris] p. 40Rule Cexlimiv 1962
[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 1812  df-or 862  dfbi2 480
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 31002
[Margaris] p. 59Section 14notnotrALTVD 45973
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45974
[Margaris] p. 79Rule Cexinst01 45684  exinst11 45685
[Margaris] p. 89Theorem 19.219.2 2008  19.2g 2224  r19.2z 4454
[Margaris] p. 89Theorem 19.319.3 2238  rr19.3v 3620
[Margaris] p. 89Theorem 19.5alcom 2195
[Margaris] p. 89Theorem 19.6alex 1858
[Margaris] p. 89Theorem 19.7alnex 1813
[Margaris] p. 89Theorem 19.819.8a 2217
[Margaris] p. 89Theorem 19.919.9 2241  19.9h 2319  exlimd 2254  exlimdh 2323
[Margaris] p. 89Theorem 19.11excom 2198  excomim 2199
[Margaris] p. 89Theorem 19.1219.12 2357
[Margaris] p. 90Section 19conventions-labels 31003  conventions-labels 31003  conventions-labels 31003  conventions-labels 31003
[Margaris] p. 90Theorem 19.14exnal 1859
[Margaris] p. 90Theorem 19.152albi 45438  albi 1850
[Margaris] p. 90Theorem 19.1619.16 2261
[Margaris] p. 90Theorem 19.1719.17 2262
[Margaris] p. 90Theorem 19.182exbi 45440  exbi 1879
[Margaris] p. 90Theorem 19.1919.19 2265
[Margaris] p. 90Theorem 19.202alim 45437  2alimdv 1950  alimd 2248  alimdh 1849  alimdv 1948  ax-4 1841  ralimdaa 3263  ralimdv 3176  ralimdva 3174  ralimdvva 3209  sbcimdv 3806
[Margaris] p. 90Theorem 19.2119.21 2243  19.21h 2320  19.21t 2242  19.21vv 45436  alrimd 2251  alrimdd 2250  alrimdh 1895  alrimdv 1961  alrimi 2249  alrimih 1856  alrimiv 1959  alrimivv 1960  bj-alrimdh 37569  hbralrimi 3152  r19.21be 3255  r19.21bi 3254  ralrimd 3267  ralrimdv 3160  ralrimdva 3162  ralrimdvv 3206  ralrimdvva 3217  ralrimi 3260  ralrimia 3261  ralrimiv 3153  ralrimiva 3154  ralrimivv 3203  ralrimivva 3205  ralrimivvva 3208  ralrimivw 3158
[Margaris] p. 90Theorem 19.222exim 45439  2eximdv 1951  bj-exim 37584  exim 1866  eximd 2252  eximdh 1896  eximdv 1949  rexim 3103  reximd2a 3272  reximdai 3264  reximdd 46239  reximddv 3178  reximddv2 3221  reximddv3 3179  reximdv 3177  reximdv2 3172  reximdva 3175  reximdvai 3173  reximdvva 3210  reximi2 3095
[Margaris] p. 90Theorem 19.2319.23 2247  19.23bi 2227  19.23h 2321  19.23t 2246  exlimdv 1965  exlimdvv 1966  exlimexi 45583  exlimiv 1962  exlimivv 1964  rexlimd3 46235  rexlimdv 3161  rexlimdv3a 3167  rexlimdva 3163  rexlimdva2 3165  rexlimdvaa 3164  rexlimdvv 3218  rexlimdvva 3219  rexlimdvvva 3220  rexlimdvw 3168  rexlimiv 3156  rexlimiva 3155  rexlimivv 3204
[Margaris] p. 90Theorem 19.2419.24 2023
[Margaris] p. 90Theorem 19.2519.25 1912
[Margaris] p. 90Theorem 19.2619.26 1902
[Margaris] p. 90Theorem 19.2719.27 2263  r19.27z 4465  r19.27zv 4466
[Margaris] p. 90Theorem 19.2819.28 2264  19.28vv 45446  r19.28z 4457  r19.28zf 46250  r19.28zv 4461  rr19.28v 3621
[Margaris] p. 90Theorem 19.2919.29 1905  r19.29d2r 3149  r19.29imd 3127
[Margaris] p. 90Theorem 19.3019.30 1913
[Margaris] p. 90Theorem 19.3119.31 2270  19.31vv 45444
[Margaris] p. 90Theorem 19.3219.32 2269  r19.32 48244
[Margaris] p. 90Theorem 19.3319.33-2 45442  19.33 1916
[Margaris] p. 90Theorem 19.3419.34 2024
[Margaris] p. 90Theorem 19.3519.35 1909
[Margaris] p. 90Theorem 19.3619.36 2266  19.36vv 45443  r19.36zv 4467
[Margaris] p. 90Theorem 19.3719.37 2268  19.37vv 45445  r19.37zv 4462
[Margaris] p. 90Theorem 19.3819.38 1871
[Margaris] p. 90Theorem 19.3919.39 2022
[Margaris] p. 90Theorem 19.4019.40-2 1919  19.40 1918  r19.40 3128
[Margaris] p. 90Theorem 19.4119.41 2271  19.41rg 45609
[Margaris] p. 90Theorem 19.4219.42 2272
[Margaris] p. 90Theorem 19.4319.43 1914
[Margaris] p. 90Theorem 19.4419.44 2273  r19.44zv 4464
[Margaris] p. 90Theorem 19.4519.45 2274  r19.45zv 4463
[Margaris] p. 110Exercise 2(b)eu1 2635
[Mayet] p. 370Remarkjpi 32873  largei 32870  stri 32860
[Mayet3] p. 9Definition of CH-statesdf-hst 32815  ishst 32817
[Mayet3] p. 10Theoremhstrbi 32869  hstri 32868
[Mayet3] p. 1223Theorem 4.1mayete3i 32331
[Mayet3] p. 1240Theorem 7.1mayetes3i 32332
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32881
[MegPav2000] p. 2345Definition 3.4-1chintcl 31935  chsupcl 31943
[MegPav2000] p. 2345Definition 3.4-2hatomic 32963
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32957
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32984
[MegPav2000] p. 2366Figure 7pl42N 41116
[MegPav2002] p. 362Lemma 2.2latj31 18662  latj32 18660  latjass 18658
[Megill] p. 444Axiom C5ax-5 1942  ax5ALT 40040
[Megill] p. 444Section 7conventions 31002
[Megill] p. 445Lemma L12aecom-o 40034  ax-c11n 40021  axc11n 2455
[Megill] p. 446Lemma L17equtrr 2054
[Megill] p. 446Lemma L18ax6fromc10 40029
[Megill] p. 446Lemma L19hbnae-o 40061  hbnae 2461
[Megill] p. 447Remark 9.1dfsb1 2510  sbid 2290  sbidd-misc 50888  sbidd 50887
[Megill] p. 448Remark 9.6axc14 2492
[Megill] p. 448Scheme C4'ax-c4 40017
[Megill] p. 448Scheme C5'ax-c5 40016  sp 2219
[Megill] p. 448Scheme C6'ax-11 2193
[Megill] p. 448Scheme C7'ax-c7 40018
[Megill] p. 448Scheme C8'ax-7 2040
[Megill] p. 448Scheme C9'ax-c9 40023
[Megill] p. 448Scheme C10'ax-6 1999  ax-c10 40019
[Megill] p. 448Scheme C11'ax-c11 40020
[Megill] p. 448Scheme C12'ax-8 2146
[Megill] p. 448Scheme C13'ax-9 2154
[Megill] p. 448Scheme C14'ax-c14 40024
[Megill] p. 448Scheme C15'ax-c15 40022
[Megill] p. 448Scheme C16'ax-c16 40025
[Megill] p. 448Theorem 9.4dral1-o 40037  dral1 2468  dral2-o 40063  dral2 2467  drex1 2470  drex2 2471  drsb1 2524  drsb2 2300
[Megill] p. 449Theorem 9.7sbcom2 2208  sbequ 2119  sbid2v 2538
[Megill] p. 450Example in Appendixhba1-o 40030  hba1 2326
[Mendelson] p. 35Axiom A3hirstL-ax3 48038
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3825  rspsbca 3826  stdpc4 2104
[Mendelson] p. 69Axiom 5ax-c4 40017  ra4 3832  stdpc5 2244
[Mendelson] p. 81Rule Cexlimiv 1962
[Mendelson] p. 95Axiom 6stdpc6 2060
[Mendelson] p. 95Axiom 7stdpc7 2285
[Mendelson] p. 225Axiom system NBGru 3737
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5486
[Mendelson] p. 231Exercise 4.10(k)inv1 4347
[Mendelson] p. 231Exercise 4.10(l)unv 4348
[Mendelson] p. 231Exercise 4.10(n)dfin3 4222
[Mendelson] p. 231Exercise 4.10(o)df-nul 4279
[Mendelson] p. 231Exercise 4.10(q)dfin4 4223
[Mendelson] p. 231Exercise 4.10(s)ddif 4077
[Mendelson] p. 231Definition of uniondfun3 4221
[Mendelson] p. 235Exercise 4.12(c)univ 5418
[Mendelson] p. 235Exercise 4.12(d)pwv 4863
[Mendelson] p. 235Exercise 4.12(j)pwin 5541
[Mendelson] p. 235Exercise 4.12(k)pwunss 4574
[Mendelson] p. 235Exercise 4.12(l)pwssun 5542
[Mendelson] p. 235Exercise 4.12(n)uniin 4890
[Mendelson] p. 235Exercise 4.12(p)reli 5803
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6271
[Mendelson] p. 244Proposition 4.8(g)epweon 7789
[Mendelson] p. 246Definition of successordf-suc 6368
[Mendelson] p. 250Exercise 4.36oelim2 8605
[Mendelson] p. 254Proposition 4.22(b)xpen 9160
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9081  xpsneng 9082
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9088  xpcomeng 9089
[Mendelson] p. 254Proposition 4.22(e)xpassen 9091
[Mendelson] p. 255Definitionbrsdom 9002
[Mendelson] p. 255Exercise 4.39endisj 9084
[Mendelson] p. 255Exercise 4.41mapprc 8852
[Mendelson] p. 255Exercise 4.43mapsnen 9066  mapsnend 9065
[Mendelson] p. 255Exercise 4.45mapunen 9166
[Mendelson] p. 255Exercise 4.47xpmapen 9165
[Mendelson] p. 255Exercise 4.42(a)map0e 8911
[Mendelson] p. 255Exercise 4.42(b)map1 9069
[Mendelson] p. 257Proposition 4.24(a)undom 9085
[Mendelson] p. 258Exercise 4.56(c)djuassen 10258  djucomen 10257
[Mendelson] p. 258Exercise 4.56(f)djudom1 10262
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10256
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8540
[Mendelson] p. 266Proposition 4.34(f)oaordex 8567
[Mendelson] p. 275Proposition 4.42(d)entri3 10644
[Mendelson] p. 281Definitiondf-r1 9769
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9822
[Mendelson] p. 287Axiom system MKru 3737
[MertziosUnger] p. 152Definitiondf-frgr 30861
[MertziosUnger] p. 153Remark 1frgrconngr 30896
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30898  vdgn1frgrv3 30899
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30900
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30893
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30886  2pthfrgrrn 30884  2pthfrgrrn2 30885
[Mittelstaedt] p. 9Definitiondf-oc 31855
[Monk1] p. 22Remarkconventions 31002
[Monk1] p. 22Theorem 3.1conventions 31002
[Monk1] p. 26Theorem 2.8(vii)ssin 4135
[Monk1] p. 33Theorem 3.2(i)ssrel 5758  ssrelf 33252
[Monk1] p. 33Theorem 3.2(ii)eqrel 5759
[Monk1] p. 34Definition 3.3df-opab 5167
[Monk1] p. 36Theorem 3.7(i)coi1 6264  coi2 6265
[Monk1] p. 36Theorem 3.8(v)dm0 5901  rn0 5907
[Monk1] p. 36Theorem 3.7(ii)cnvi 5862
[Monk1] p. 37Theorem 3.13(i)relxp 5668
[Monk1] p. 37Theorem 3.13(x)dmxp 5910  rnxp 6161
[Monk1] p. 37Theorem 3.13(ii)0xp 5749  xp0 5750
[Monk1] p. 38Theorem 3.16(ii)ima0 6074
[Monk1] p. 38Theorem 3.16(viii)imai 6071
[Monk1] p. 39Theorem 3.17imaex 7926  imaexg 7925
[Monk1] p. 39Theorem 3.16(xi)imassrn 6197
[Monk1] p. 41Theorem 4.3(i)fnopfv 7075  funfvop 7049
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6939
[Monk1] p. 42Theorem 4.4(iii)fvelima 6950
[Monk1] p. 43Theorem 4.6funun 6586
[Monk1] p. 43Theorem 4.8(iv)dff13 7258  dff13f 7259
[Monk1] p. 46Theorem 4.15(v)funex 7225  funrnex 7966
[Monk1] p. 50Definition 5.4fniunfv 7251
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6228
[Monk1] p. 52Theorem 5.11(viii)ssint 4923
[Monk1] p. 52Definition 5.13 (i)1stval2 8018  df-1st 8001
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8019  df-2nd 8002
[Monk1] p. 112Theorem 15.17(v)ranksn 9869  ranksnb 9838
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9870
[Monk1] p. 112Theorem 15.17(iii)rankun 9871  rankunb 9865
[Monk1] p. 113Theorem 15.18r1val3 9851
[Monk1] p. 113Definition 15.19df-r1 9769  r1val2 9850
[Monk1] p. 117Lemmazorn2 10585  zorn2g 10582
[Monk1] p. 133Theorem 18.11cardom 10068
[Monk1] p. 133Theorem 18.12canth3 10646
[Monk1] p. 133Theorem 18.14carduni 10063
[Monk2] p. 105Axiom C4ax-4 1841
[Monk2] p. 105Axiom C7ax-7 2040
[Monk2] p. 105Axiom C8ax-12 2212  ax-c15 40022  ax12v2 2214
[Monk2] p. 108Lemma 5ax-c4 40017
[Monk2] p. 109Lemma 12ax-11 2193
[Monk2] p. 109Lemma 15equvini 2484  equvinv 2061  eqvinop 5455
[Monk2] p. 113Axiom C5-1ax-5 1942  ax5ALT 40040
[Monk2] p. 113Axiom C5-2ax-10 2177
[Monk2] p. 113Axiom C5-3ax-11 2193
[Monk2] p. 114Lemma 21sp 2219
[Monk2] p. 114Lemma 22axc4 2351  hba1-o 40030  hba1 2326
[Monk2] p. 114Lemma 23nfia1 2189
[Monk2] p. 114Lemma 24nfa2 2209  nfra2 3361  nfra2w 3298
[Moore] p. 53Part Idf-mre 17757
[Munkres] p. 77Example 2distop 23314  indistop 23321  indistopon 23320
[Munkres] p. 77Example 3fctop 23323  fctop2 23324
[Munkres] p. 77Example 4cctop 23325
[Munkres] p. 78Definition of basisdf-bases 23265  isbasis3g 23268
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17615  tgval2 23275
[Munkres] p. 79Remarktgcl 23288
[Munkres] p. 80Lemma 2.1tgval3 23282
[Munkres] p. 80Lemma 2.2tgss2 23306  tgss3 23305
[Munkres] p. 81Lemma 2.3basgen 23307  basgen2 23308
[Munkres] p. 83Exercise 3topdifinf 38348  topdifinfeq 38349  topdifinffin 38347  topdifinfindis 38345
[Munkres] p. 89Definition of subspace topologyresttop 23479
[Munkres] p. 93Theorem 6.1(1)0cld 23357  topcld 23354
[Munkres] p. 93Theorem 6.1(2)iincld 23358
[Munkres] p. 93Theorem 6.1(3)uncld 23360
[Munkres] p. 94Definition of closureclsval 23356
[Munkres] p. 94Definition of interiorntrval 23355
[Munkres] p. 95Theorem 6.5(a)clsndisj 23394  elcls 23392
[Munkres] p. 95Theorem 6.5(b)elcls3 23402
[Munkres] p. 97Theorem 6.6clslp 23467  neindisj 23436
[Munkres] p. 97Corollary 6.7cldlp 23469
[Munkres] p. 97Definition of limit pointislp2 23464  lpval 23458
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23634
[Munkres] p. 102Definition of continuous functiondf-cn 23546  iscn 23554  iscn2 23557
[Munkres] p. 107Theorem 7.2(g)cncnp 23599  cncnp2 23600  cncnpi 23597  df-cnp 23547  iscnp 23556  iscnp2 23558
[Munkres] p. 127Theorem 10.1metcn 24863
[Munkres] p. 128Theorem 10.3metcn4 25633
[Nathanson] p. 123Remarkreprgt 35293  reprinfz1 35294  reprlt 35291
[Nathanson] p. 123Definitiondf-repr 35281
[Nathanson] p. 123Chapter 5.1circlemethnat 35313
[Nathanson] p. 123Propositionbreprexp 35305  breprexpnat 35306  itgexpif 35278
[NielsenChuang] p. 195Equation 4.73unierri 32707
[OeSilva] p. 2042Section 2ax-bgbltosilva 48984
[Pfenning] p. 17Definition XMnatded 31005
[Pfenning] p. 17Definition NNCnatded 31005  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 31005
[Pfenning] p. 18Rule"natded 31005
[Pfenning] p. 18Definition /\Inatded 31005
[Pfenning] p. 18Definition ` `Enatded 31005  natded 31005  natded 31005  natded 31005  natded 31005
[Pfenning] p. 18Definition ` `Inatded 31005  natded 31005  natded 31005  natded 31005  natded 31005
[Pfenning] p. 18Definition ` `ELnatded 31005
[Pfenning] p. 18Definition ` `ERnatded 31005
[Pfenning] p. 18Definition ` `Ea,unatded 31005
[Pfenning] p. 18Definition ` `IRnatded 31005
[Pfenning] p. 18Definition ` `Ianatded 31005
[Pfenning] p. 127Definition =Enatded 31005
[Pfenning] p. 127Definition =Inatded 31005
[Ponnusamy] p. 361Theorem 6.44cphip0l 25524  df-dip 31304  dip0l 31321  ip0l 21943
[Ponnusamy] p. 361Equation 6.45cphipval 25565  ipval 31306
[Ponnusamy] p. 362Equation I1dipcj 31317  ipcj 21941
[Ponnusamy] p. 362Equation I3cphdir 25527  dipdir 31445  ipdir 21946  ipdiri 31433
[Ponnusamy] p. 362Equation I4ipidsq 31313  nmsq 25516
[Ponnusamy] p. 362Equation 6.46ip0i 31428
[Ponnusamy] p. 362Equation 6.47ip1i 31430
[Ponnusamy] p. 362Equation 6.48ip2i 31431
[Ponnusamy] p. 363Equation I2cphass 25533  dipass 31448  ipass 21952  ipassi 31444
[Prugovecki] p. 186Definition of brabraval 32547  df-bra 32453
[Prugovecki] p. 376Equation 8.1df-kb 32454  kbval 32557
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32985
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 41021
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32999  atcvat4i 33000  cvrat3 40575  cvrat4 40576  lsatcvat3 40185
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32885  cvrval 40402  df-cv 32882  df-lcv 40152  lspsncv0 21425
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 41033
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 41034
[Quine] p. 16Definition 2.1df-clab 2739  rabid 3432  rabidd 46246  wl-df.clab 38506
[Quine] p. 17Definition 2.1''dfsb7 2312
[Quine] p. 18Definition 2.7df-cleq 2752  wl-df.cleq 38507
[Quine] p. 19Definition 2.9conventions 31002  df-v 3452
[Quine] p. 34Theorem 5.1eqabb 2899
[Quine] p. 35Theorem 5.2abid1 2896  abid2f 2952
[Quine] p. 37Paragraph 1mirimanoff 36530
[Quine] p. 40Theorem 6.1sb5 2309
[Quine] p. 40Theorem 6.2sb6 2121  sbalex 2278
[Quine] p. 41Theorem 6.3df-clel 2835  wl-df.clel 38510
[Quine] p. 41Theorem 6.4eqid 2760  eqid1 31069
[Quine] p. 41Theorem 6.5eqcom 2767
[Quine] p. 42Theorem 6.6df-sbc 3739
[Quine] p. 42Theorem 6.7dfsbcq 3740  dfsbcq2 3741
[Quine] p. 43Theorem 6.8vex 3454
[Quine] p. 43Theorem 6.9isset 3464
[Quine] p. 44Theorem 7.3spcgf 3545  spcgv 3550  spcimgf 3513
[Quine] p. 44Theorem 6.11spsbc 3751  spsbcd 3752
[Quine] p. 44Theorem 6.12elex 3471
[Quine] p. 44Theorem 6.13elab 3632  elabg 3629  elabgf 3627
[Quine] p. 44Theorem 6.14noel 4283
[Quine] p. 48Theorem 7.2snprc 4677
[Quine] p. 48Definition 7.1df-pr 4586  df-sn 4584
[Quine] p. 49Theorem 7.4snss 4744  snssg 4743
[Quine] p. 49Theorem 7.5prss 4780  prssg 4779
[Quine] p. 49Theorem 7.6prid1 4722  prid1g 4720  prid2 4723  prid2g 4721  snid 4622  snidg 4620
[Quine] p. 51Theorem 7.12snex 5396
[Quine] p. 51Theorem 7.13prex 5395
[Quine] p. 53Theorem 8.2unisn 4885  unisnALT 45984  unisng 4884
[Quine] p. 53Theorem 8.3uniun 4889
[Quine] p. 54Theorem 8.6elssuni 4898
[Quine] p. 54Theorem 8.7uni0 4895
[Quine] p. 56Theorem 8.17uniabio 6508
[Quine] p. 56Definition 8.18dfaiota2 48232  dfiota2 6495
[Quine] p. 57Theorem 8.19aiotaval 48241  iotaval 6512
[Quine] p. 57Theorem 8.22iotanul 6518
[Quine] p. 58Theorem 8.23iotaex 6514
[Quine] p. 58Definition 9.1df-op 4590
[Quine] p. 61Theorem 9.5opabid 5498  opabidw 5497  opelopab 5516  opelopaba 5509  opelopabaf 5518  opelopabf 5519  opelopabg 5512  opelopabga 5506  opelopabgf 5514  oprabid 7452  oprabidw 7451
[Quine] p. 64Definition 9.11df-xp 5656
[Quine] p. 64Definition 9.12df-cnv 5658
[Quine] p. 64Definition 9.15df-id 5545
[Quine] p. 65Theorem 10.3fun0 6605
[Quine] p. 65Theorem 10.4funi 6572
[Quine] p. 65Theorem 10.5funsn 6593  funsng 6591
[Quine] p. 65Definition 10.1df-fun 6540
[Quine] p. 65Definition 10.2args 6089  dffv4 6882
[Quine] p. 68Definition 10.11conventions 31002  df-fv 6546  fv2 6880
[Quine] p. 124Theorem 17.3nn0opth2 14417  nn0opth2i 14416  nn0opthi 14415  omopthi 8671
[Quine] p. 177Definition 25.2df-rdg 8419
[Quine] p. 232Equation icarddom 10639
[Quine] p. 284Axiom 39(vi)funimaex 6627  funimaexg 6626
[Quine] p. 331Axiom system NFru 3737
[ReedSimon] p. 36Definition (iii)ax-his3 31687
[ReedSimon] p. 63Exercise 4(a)df-dip 31304  polid 31762  polid2i 31760  polidi 31761
[ReedSimon] p. 63Exercise 4(b)df-ph 31416
[ReedSimon] p. 195Remarklnophm 32622  lnophmi 32621
[Retherford] p. 49Exercise 1(i)leopadd 32735
[Retherford] p. 49Exercise 1(ii)leopmul 32737  leopmuli 32736
[Retherford] p. 49Exercise 1(iv)leoptr 32740
[Retherford] p. 49Definition VI.1df-leop 32455  leoppos 32729
[Retherford] p. 49Exercise 1(iii)leoptri 32739
[Retherford] p. 49Definition of operator orderingleop3 32728
[Ribenboim] p. 181Remarknprmdvdsfacm1 48785
[Ribenboim], p. 181Statementppivalnn 48793
[Roman] p. 4Definitiondf-dmat 22806  df-dmatalt 49586
[Roman] p. 18Part Preliminariesdf-rng 20376
[Roman] p. 19Part Preliminariesdf-ring 20462
[Roman] p. 46Theorem 1.6isldepslvec2 49673
[Roman] p. 112Noteisldepslvec2 49673  ldepsnlinc 49696  zlmodzxznm 49685
[Roman] p. 112Examplezlmodzxzequa 49684  zlmodzxzequap 49687  zlmodzxzldep 49692
[Roman] p. 170Theorem 7.8cayleyhamilton 23209
[Rosenlicht] p. 80Theoremheicant 38649
[Rosser] p. 281Definitiondf-op 4590
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 35317
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 35318
[Rotman] p. 28Remarkpgrpgt2nabl 49554  pmtr3ncom 19690
[Rotman] p. 31Theorem 3.4symggen2 19686
[Rotman] p. 42Theorem 3.15cayley 19629  cayleyth 19630
[Rudin] p. 164Equation 27efcan 16263
[Rudin] p. 164Equation 30efzval 16271
[Rudin] p. 167Equation 48absefi 16365
[Russell1905] p. 482Example of "the fatherdfalseu2 51008
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1803
[Sanford] p. 39Rule 4mptxor 1801
[Sanford] p. 40Rule 1mptnan 1800
[Schechter] p. 51Definition of antisymmetryintasym 6108
[Schechter] p. 51Definition of irreflexivityintirr 6111
[Schechter] p. 51Definition of symmetrycnvsym 6107
[Schechter] p. 51Definition of transitivitycotr 6105
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17757
[Schechter] p. 79Definition of Moore closuredf-mrc 17758
[Schechter] p. 82Section 4.5df-mrc 17758
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17760
[Schechter] p. 139Definition AC3dfac9 10216
[Schechter] p. 141Definition (MC)dfac11 44140
[Schechter] p. 149Axiom DC1ax-dc 10525  axdc3 10533
[Schechter] p. 187Definition of "ring with unit"isring 20464  isrngo 38907
[Schechter] p. 276Remark 11.6.espan0 32145
[Schechter] p. 276Definition of spandf-span 31912  spanval 31936
[Schechter] p. 428Definition 15.35bastop1 23312
[Schloeder] p. 1Lemma 1.3onelon 6387  onelond 37023  onelord 44329  ordelon 6386  ordelord 6384
[Schloeder] p. 1Lemma 1.7onepsuc 44330  sucidg 6446
[Schloeder] p. 1Remark 1.50elon 6418  onsuc 7824  ord0 6417  ordsuci 7822
[Schloeder] p. 1Theorem 1.9epsoon 44331
[Schloeder] p. 1Definition 1.1dftr5 5215
[Schloeder] p. 1Definition 1.2dford3 44111  elon2 6373
[Schloeder] p. 1Definition 1.4df-suc 6368
[Schloeder] p. 1Definition 1.6epel 5553  epelg 5551
[Schloeder] p. 1Theorem 1.9(i)elirr 9595  epirron 44332  ordirr 6380
[Schloeder] p. 1Theorem 1.9(ii)oneltr 44334  oneptr 44333  ontr1 6410
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6406  oneptri 44335  ordtri3or 6395
[Schloeder] p. 2Lemma 1.10ondif1 8510  ord0eln0 6419
[Schloeder] p. 2Lemma 1.13elsuci 6432  onsucss 44344  trsucss 6453
[Schloeder] p. 2Lemma 1.14ordsucss 7829
[Schloeder] p. 2Lemma 1.15onnbtwn 6459  ordnbtwn 6458
[Schloeder] p. 2Lemma 1.16orddif0suc 44346  ordnexbtwnsuc 44345
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10480  onsucf1lem 44347  onsucf1o 44350  onsucf1olem 44348  onsucrn 44349
[Schloeder] p. 2Lemma 1.18dflim7 44351
[Schloeder] p. 2Remark 1.12ordzsl 7856
[Schloeder] p. 2Theorem 1.10ondif1i 44340  ordne0gt0 44339
[Schloeder] p. 2Definition 1.11dflim6 44342  limnsuc 44343  onsucelab 44341
[Schloeder] p. 3Remark 1.21omex 9645
[Schloeder] p. 3Theorem 1.19tfinds 7871
[Schloeder] p. 3Theorem 1.22omelon 9648  ordom 7887
[Schloeder] p. 3Definition 1.20dfom3 9649
[Schloeder] p. 4Lemma 2.21onn 8650
[Schloeder] p. 4Lemma 2.7ssonuni 7794  ssorduni 7793
[Schloeder] p. 4Remark 2.4oa1suc 8540
[Schloeder] p. 4Theorem 1.23dfom5 9652  limom 7893
[Schloeder] p. 4Definition 2.1df-1o 8477  df1o2 8484
[Schloeder] p. 4Definition 2.3oa0 8525  oa0suclim 44353  oalim 8541  oasuc 8533
[Schloeder] p. 4Definition 2.5om0 8526  om0suclim 44354  omlim 8542  omsuc 8535
[Schloeder] p. 4Definition 2.6oe0 8531  oe0m1 8530  oe0suclim 44355  oelim 8543  oesuc 8536
[Schloeder] p. 5Lemma 2.10onsupuni 44307
[Schloeder] p. 5Lemma 2.11onsupsucismax 44357
[Schloeder] p. 5Lemma 2.12onsssupeqcond 44358
[Schloeder] p. 5Lemma 2.13limexissup 44359  limexissupab 44361  limiun 44360  limuni 6425
[Schloeder] p. 5Lemma 2.14oa0r 8547
[Schloeder] p. 5Lemma 2.15om1 8551  om1om1r 44362  om1r 8552
[Schloeder] p. 5Remark 2.8oacl 8544  oaomoecl 44356  oecl 8546  omcl 8545
[Schloeder] p. 5Definition 2.9onsupintrab 44309
[Schloeder] p. 6Lemma 2.16oe1 8553
[Schloeder] p. 6Lemma 2.17oe1m 8554
[Schloeder] p. 6Lemma 2.18oe0rif 44363
[Schloeder] p. 6Theorem 2.19oasubex 44364
[Schloeder] p. 6Theorem 2.20nnacl 8621  nnamecl 44365  nnecl 8623  nnmcl 8622
[Schloeder] p. 7Lemma 3.1onsucwordi 44366
[Schloeder] p. 7Lemma 3.2oaword1 8561
[Schloeder] p. 7Lemma 3.3oaword2 8562
[Schloeder] p. 7Lemma 3.4oalimcl 8569
[Schloeder] p. 7Lemma 3.5oaltublim 44368
[Schloeder] p. 8Lemma 3.6oaordi3 44369
[Schloeder] p. 8Lemma 3.81oaomeqom 44371
[Schloeder] p. 8Lemma 3.10oa00 8568
[Schloeder] p. 8Lemma 3.11omge1 44375  omword1 8582
[Schloeder] p. 8Remark 3.9oaordnr 44374  oaordnrex 44373
[Schloeder] p. 8Theorem 3.7oaord3 44370
[Schloeder] p. 9Lemma 3.12omge2 44376  omword2 8583
[Schloeder] p. 9Lemma 3.13omlim2 44377
[Schloeder] p. 9Lemma 3.14omord2lim 44378
[Schloeder] p. 9Lemma 3.15omord2i 44379  omordi 8575
[Schloeder] p. 9Theorem 3.16omord 8577  omord2com 44380
[Schloeder] p. 10Lemma 3.172omomeqom 44381  df-2o 8478
[Schloeder] p. 10Lemma 3.19oege1 44384  oewordi 8601
[Schloeder] p. 10Lemma 3.20oege2 44385  oeworde 8603
[Schloeder] p. 10Lemma 3.21rp-oelim2 44386
[Schloeder] p. 10Lemma 3.22oeord2lim 44387
[Schloeder] p. 10Remark 3.18omnord1 44383  omnord1ex 44382
[Schloeder] p. 11Lemma 3.23oeord2i 44388
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44390
[Schloeder] p. 11Remark 3.26oenord1 44394  oenord1ex 44393
[Schloeder] p. 11Theorem 4.1oaomoencom 44395
[Schloeder] p. 11Theorem 4.2oaass 8570
[Schloeder] p. 11Theorem 3.24oeord2com 44389
[Schloeder] p. 12Theorem 4.3odi 8588
[Schloeder] p. 13Theorem 4.4omass 8589
[Schloeder] p. 14Remark 4.6oenass 44397
[Schloeder] p. 14Theorem 4.7oeoa 8607
[Schloeder] p. 15Lemma 5.1cantnftermord 44398
[Schloeder] p. 15Lemma 5.2cantnfub 44399  cantnfub2 44400
[Schloeder] p. 16Theorem 5.3cantnf2 44403
[Schwabhauser] p. 10Axiom A1axcgrrflx 29493  axtgcgrrflx 28925
[Schwabhauser] p. 10Axiom A2axcgrtr 29494
[Schwabhauser] p. 10Axiom A3axcgrid 29495  axtgcgrid 28926
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28911
[Schwabhauser] p. 11Axiom A4axsegcon 29506  axtgsegcon 28927  df-trkgcb 28913
[Schwabhauser] p. 11Axiom A5ax5seg 29517  axtg5seg 28928  df-trkgcb 28913
[Schwabhauser] p. 11Axiom A6axbtwnid 29518  axtgbtwnid 28929  df-trkgb 28912
[Schwabhauser] p. 12Axiom A7axpasch 29520  axtgpasch 28930  df-trkgb 28912
[Schwabhauser] p. 12Axiom A8axlowdim2 29539  df-trkg2d 35337
[Schwabhauser] p. 13Axiom A8axtglowdim2 28933
[Schwabhauser] p. 13Axiom A9axtgupdim2 28934  df-trkg2d 35337
[Schwabhauser] p. 13Axiom A10axeuclid 29542  axtgeucl 28935  df-trkge 28914
[Schwabhauser] p. 13Axiom A11axcont 29555  axtgcont 28932  axtgcont1 28931  df-trkgb 28912
[Schwabhauser] p. 24Theorem A10prlngmo 29433
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36827
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36829
[Schwabhauser] p. 27Theorem 2.3cgrtr 36832
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36836
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36837  tgcgrcomimp 28940  tgcgrcoml 28942  tgcgrcomr 28941
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36842  tgcgrtriv 28947
[Schwabhauser] p. 28Theorem 2.105segofs 36846  tg5segofs 35348
[Schwabhauser] p. 28Definition 2.10df-afs 35345  df-ofs 36823
[Schwabhauser] p. 29Theorem 2.11cgrextend 36848  tgcgrextend 28948
[Schwabhauser] p. 29Theorem 2.12segconeq 36850  tgsegconeq 28949
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36862  btwntriv2 36852  tgbtwntriv2 28951
[Schwabhauser] p. 30Theorem 3.2btwncomim 36853  tgbtwncom 28952
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36856  tgbtwntriv1 28955
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36857  tgbtwnswapid 28956
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36863  btwnintr 36859  tgbtwnexch2 28960  tgbtwnintr 28957
[Schwabhauser] p. 30Theorem 3.6btwnexch 36865  btwnexch3 36860  tgbtwnexch 28962  tgbtwnexch3 28958
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36864  tgbtwnouttr 28961  tgbtwnouttr2 28959
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29538
[Schwabhauser] p. 32Theorem 3.14btwndiff 36867  tgbtwndiff 28970
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28963  trisegint 36868
[Schwabhauser] p. 34Theorem 4.2ifscgr 36884  tgifscgr 28972
[Schwabhauser] p. 34Theorem 4.11colcom 29022  colrot1 29023  colrot2 29024  lncom 29091  lnrot1 29092  lnrot2 29093
[Schwabhauser] p. 34Definition 4.1df-ifs 36880
[Schwabhauser] p. 35Theorem 4.3cgrsub 36885  tgcgrsub 28973
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36895  tgcgrxfr 28982
[Schwabhauser] p. 35Statement 4.4ercgrg 28981
[Schwabhauser] p. 35Definition 4.4df-cgr3 36881  df-cgrg 28975
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28975
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36896  tgbtwnxfr 28994
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36902  colinearperm2 36904  colinearperm3 36903  colinearperm4 36905  colinearperm5 36906
[Schwabhauser] p. 36Definition 4.8df-ismt 28997
[Schwabhauser] p. 36Definition 4.10df-colinear 36879  tgellng 29017  tglng 29010
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36907
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36915  lnxfr 29030
[Schwabhauser] p. 37Theorem 4.14lineext 36916  lnext 29031
[Schwabhauser] p. 37Theorem 4.16fscgr 36920  tgfscgr 29032
[Schwabhauser] p. 37Theorem 4.17linecgr 36921  lncgr 29033
[Schwabhauser] p. 37Definition 4.15df-fs 36882
[Schwabhauser] p. 38Theorem 4.18lineid 36923  lnid 29034
[Schwabhauser] p. 38Theorem 4.19idinside 36924  tgidinside 29035
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36941  tgbtwnconn1 29039
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36942  tgbtwnconn2 29040
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36943  tgbtwnconn3 29041
[Schwabhauser] p. 41Theorem 5.5brsegle2 36949
[Schwabhauser] p. 41Definition 5.4df-segle 36947  legov 29049
[Schwabhauser] p. 41Definition 5.5legov2 29050
[Schwabhauser] p. 42Remark 5.13legso 29063
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36950
[Schwabhauser] p. 42Theorem 5.7seglerflx 36952
[Schwabhauser] p. 42Theorem 5.8segletr 36954
[Schwabhauser] p. 42Theorem 5.9segleantisym 36955
[Schwabhauser] p. 42Theorem 5.10seglelin 36956
[Schwabhauser] p. 42Theorem 5.11seglemin 36953
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36958
[Schwabhauser] p. 42Proposition 5.7legid 29051
[Schwabhauser] p. 42Proposition 5.8legtrd 29053
[Schwabhauser] p. 42Proposition 5.9legtri3 29054
[Schwabhauser] p. 42Proposition 5.10legtrid 29055
[Schwabhauser] p. 42Proposition 5.11leg0 29056
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36965
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36966
[Schwabhauser] p. 43Theorem 6.4broutsideof 36961  df-outsideof 36960
[Schwabhauser] p. 43Definition 6.1broutsideof2 36962  ishlg 29069
[Schwabhauser] p. 44Theorem 6.4hlln 29074
[Schwabhauser] p. 44Theorem 6.5hlid 29076  outsideofrflx 36967
[Schwabhauser] p. 44Theorem 6.6hlcomb 29070  hlcomd 29071  outsideofcom 36968
[Schwabhauser] p. 44Theorem 6.7hltr 29077  outsideoftr 36969
[Schwabhauser] p. 44Theorem 6.11hlcgreq 29086  hlcgreu 29085  outsideofeu 36971
[Schwabhauser] p. 44Definition 6.8df-ray 36978
[Schwabhauser] p. 45Part 2df-lines2 36979
[Schwabhauser] p. 45Theorem 6.13outsidele 36972
[Schwabhauser] p. 45Theorem 6.15lineunray 36987
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36988  tglineelsb2 29101
[Schwabhauser] p. 45Theorem 6.17linecom 36990  linerflx1 36989  linerflx2 36991  tglinecom 29104  tglinerflx1 29102  tglinerflx2 29103
[Schwabhauser] p. 45Theorem 6.18linethru 36993  tglinethru 29105
[Schwabhauser] p. 45Definition 6.14df-line2 36977  tglng 29010
[Schwabhauser] p. 45Proposition 6.13legbtwn 29058
[Schwabhauser] p. 46Theorem 6.19linethrueu 36996  tglinethrueu 29108
[Schwabhauser] p. 46Theorem 6.21lineintmo 36997  tglineineq 29112  tglineinsn 29113  tglineinteq 29115  tglineintmo 29111
[Schwabhauser] p. 46Theorem 6.23colline 29119
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 29120
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 29121
[Schwabhauser] p. 49Theorem 7.3mirinv 29139
[Schwabhauser] p. 49Theorem 7.7mirmir 29135
[Schwabhauser] p. 49Theorem 7.8mirreu3 29127
[Schwabhauser] p. 49Definition 7.5df-mir 29126  ismir 29132  mirbtwn 29131  mircgr 29130  mirfv 29129  mirval 29128
[Schwabhauser] p. 50Theorem 7.8mirreu 29137
[Schwabhauser] p. 50Theorem 7.9mireq 29138
[Schwabhauser] p. 50Theorem 7.10mirinv 29139
[Schwabhauser] p. 50Theorem 7.11mirf1o 29142
[Schwabhauser] p. 50Theorem 7.13miriso 29143
[Schwabhauser] p. 51Theorem 7.14mirmot 29148
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 29145  mirbtwni 29144
[Schwabhauser] p. 51Theorem 7.16mircgrs 29146
[Schwabhauser] p. 51Theorem 7.17miduniq 29158
[Schwabhauser] p. 52Lemma 7.21symquadlem 29162  symquadmid 29305
[Schwabhauser] p. 52Theorem 7.18miduniq1 29159
[Schwabhauser] p. 52Theorem 7.19miduniq2 29160
[Schwabhauser] p. 52Theorem 7.20colmid 29161
[Schwabhauser] p. 53Lemma 7.22krippen 29164
[Schwabhauser] p. 55Lemma 7.25midexlem 29165
[Schwabhauser] p. 57Theorem 8.2ragcom 29174
[Schwabhauser] p. 57Definition 8.1df-rag 29170  israg 29173
[Schwabhauser] p. 58Theorem 8.3ragcol 29175
[Schwabhauser] p. 58Theorem 8.4ragmir 29176
[Schwabhauser] p. 58Theorem 8.5ragtrivb 29178
[Schwabhauser] p. 58Theorem 8.6ragflat2 29179
[Schwabhauser] p. 58Theorem 8.7ragflat 29180
[Schwabhauser] p. 58Theorem 8.8ragtriva 29181
[Schwabhauser] p. 58Theorem 8.9ragflat3 29182  ragncol 29185
[Schwabhauser] p. 58Theorem 8.10ragcgr 29183
[Schwabhauser] p. 59Theorem 8.12perpcom 29189
[Schwabhauser] p. 59Theorem 8.13ragperp 29193
[Schwabhauser] p. 59Theorem 8.14perpneq 29190
[Schwabhauser] p. 59Definition 8.11df-perpg 29172  isperp 29188
[Schwabhauser] p. 59Definition 8.13isperp2 29191
[Schwabhauser] p. 60Theorem 8.18foot 29198
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 29207  colperpexlem2 29208
[Schwabhauser] p. 63Theorem 8.21colperpex 29210  colperpexlem3 29209
[Schwabhauser] p. 64Theorem 8.22mideu 29215  midex 29214
[Schwabhauser] p. 66Lemma 8.24opphllem 29212
[Schwabhauser] p. 67Theorem 9.2oppcom 29221
[Schwabhauser] p. 67Definition 9.1islnopp 29216
[Schwabhauser] p. 68Lemma 9.3opphllem2 29225
[Schwabhauser] p. 68Lemma 9.4opphllem5 29228  opphllem6 29229
[Schwabhauser] p. 69Theorem 9.5opphl 29231
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28930
[Schwabhauser] p. 70Theorem 9.6outpasch 29234
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29242
[Schwabhauser] p. 71Definition 9.7df-hpg 29237  hpgbr 29239
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29244
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29243
[Schwabhauser] p. 72Theorem 9.11hpgid 29245
[Schwabhauser] p. 72Theorem 9.12hpgcom 29246
[Schwabhauser] p. 72Theorem 9.13hpgtr 29247
[Schwabhauser] p. 73Theorem 9.18colopp 29248
[Schwabhauser] p. 73Theorem 9.19colhp 29249
[Schwabhauser] p. 74Lemma 9.22lnincplng 29263
[Schwabhauser] p. 74Theorem 9.21plngcp 29265
[Schwabhauser] p. 74Theorem 9.24plngrot 29269
[Schwabhauser] p. 74Definition 9.20df-plng 29253  elplng 29259
[Schwabhauser] p. 75Theorem 9.25lnssplng 29271  lnssplng1 29272
[Schwabhauser] p. 76Theorem 9.26plng3p 29276
[Schwabhauser] p. 88Theorem 10.2lmieu 29290
[Schwabhauser] p. 88Definition 10.1df-mid 29280
[Schwabhauser] p. 89Theorem 10.4lmicom 29294
[Schwabhauser] p. 89Theorem 10.5lmilmi 29295
[Schwabhauser] p. 89Theorem 10.6lmireu 29296
[Schwabhauser] p. 89Theorem 10.7lmieq 29297
[Schwabhauser] p. 89Theorem 10.8lmiinv 29298
[Schwabhauser] p. 89Theorem 10.9lmif1o 29301
[Schwabhauser] p. 89Theorem 10.10lmiiso 29303
[Schwabhauser] p. 89Definition 10.3df-lmi 29281
[Schwabhauser] p. 90Theorem 10.11lmimot 29304
[Schwabhauser] p. 91Theorem 10.12hypcgr 29308
[Schwabhauser] p. 92Theorem 10.14lmiopp 29309
[Schwabhauser] p. 92Theorem 10.15lnperpex 29310  lnperpexs 29311
[Schwabhauser] p. 92Theorem 10.16trgcopy 29312  trgcopyeu 29314
[Schwabhauser] p. 95Definition 11.2dfcgra2 29339
[Schwabhauser] p. 95Definition 11.3iscgra 29317
[Schwabhauser] p. 95Proposition 11.4cgracgr 29326
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29324  cgrahl2 29325
[Schwabhauser] p. 96Theorem 11.6cgraid 29327
[Schwabhauser] p. 96Theorem 11.9cgraswap 29328
[Schwabhauser] p. 97Theorem 11.7cgracom 29330
[Schwabhauser] p. 97Theorem 11.8cgratr 29331
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29335  cgrahl 29336
[Schwabhauser] p. 98Theorem 11.13sacgr 29340
[Schwabhauser] p. 98Theorem 11.14oacgr 29341
[Schwabhauser] p. 98Theorem 11.15acopy 29342  acopyeu 29343
[Schwabhauser] p. 98Theorem 11.16ragcgra 29344
[Schwabhauser] p. 98Theorem 11.17cgrarag 29345
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29346
[Schwabhauser] p. 99Theorem 11.19ragraghl 29347
[Schwabhauser] p. 99Theorem 11.20perpeq 29349
[Schwabhauser] p. 99Theorem 11.22tgaaddcpbl 29353
[Schwabhauser] p. 101Theorem 11.24inagswap 29361
[Schwabhauser] p. 101Theorem 11.25inaghl 29365
[Schwabhauser] p. 101Definition 11.23isinag 29358
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29373
[Schwabhauser] p. 102Definition 11.27df-leag 29366  isleag 29367
[Schwabhauser] p. 107Theorem 11.49tgsas 29401  tgsas1 29400  tgsas2 29402  tgsas3 29403
[Schwabhauser] p. 108Theorem 11.50tgasa 29405  tgasa1 29404
[Schwabhauser] p. 109Theorem 11.51tgsss1 29406  tgsss2 29407  tgsss3 29408
[Schwabhauser] p. 121Definition 12.2df-prlng 29416
[Schwabhauser] p. 122Theorem 12.4prlngref 29419
[Schwabhauser] p. 122Theorem 12.5prlngsym 29420
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29425
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29426  dfprlng3 29427
[Schwabhauser] p. 122Theorem 12.9perpprlng 29429
[Schwabhauser] p. 122Theorem 12.10prlngex 29430
[Schwabhauser] p. 123Theorem 12.11prlngmo 29433  prlngmo2 29435
[Schwabhauser] p. 124Theorem 12.13prlngeu 29434
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29437
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29438
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29439
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29440
[Schwabhauser] p. 126Theorem 12.18symquadprlng 29441
[Schwabhauser] p. 126Theorem 12.19prlngsymquad 29443  prlngsymquadopp 29444
[Schwabhauser] p. 126Theorem 12.20quadcgrprlng 29445
[Schwabhauser] p. 126Theorem 12.21tgaltai 29446
[Shapiro] p. 230Theorem 6.5.1dchrhash 27599  dchrsum 27597  dchrsum2 27596  sumdchr 27600
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27601  sum2dchr 27602
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20283  ablfacrp2 20284
[Shapiro], p. 328Equation 9.2.4vmasum 27544
[Shapiro], p. 329Equation 9.2.7logfac2 27545
[Shapiro], p. 329Equation 9.2.9logfacrlim 27552
[Shapiro], p. 331Equation 9.2.13vmadivsum 27810
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27813
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27867  vmalogdivsum2 27866
[Shapiro], p. 375Theorem 9.4.1dirith 27857  dirith2 27856
[Shapiro], p. 375Equation 9.4.3rplogsum 27855  rpvmasum 27854  rpvmasum2 27840
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27815
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27853
[Shapiro], p. 377Lemma 9.4.1dchrisum 27820  dchrisumlem1 27817  dchrisumlem2 27818  dchrisumlem3 27819  dchrisumlema 27816
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27823
[Shapiro], p. 379Equation 9.4.16dchrmusum 27852  dchrmusumlem 27850  dchrvmasumlem 27851
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27822
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27824
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27848  dchrisum0re 27841  dchrisumn0 27849
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27834
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27838
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27839
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27894  pntrsumbnd2 27895  pntrsumo1 27893
[Shapiro], p. 405Equation 10.2.1mudivsum 27858
[Shapiro], p. 406Equation 10.2.6mulogsum 27860
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27862
[Shapiro], p. 407Equation 10.2.8mulog2sum 27865
[Shapiro], p. 418Equation 10.4.6logsqvma 27870
[Shapiro], p. 418Equation 10.4.8logsqvma2 27871
[Shapiro], p. 419Equation 10.4.10selberg 27876
[Shapiro], p. 420Equation 10.4.12selberg2lem 27878
[Shapiro], p. 420Equation 10.4.14selberg2 27879
[Shapiro], p. 422Equation 10.6.7selberg3 27887
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27888
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27885  selberg3lem2 27886
[Shapiro], p. 422Equation 10.4.23selberg4 27889
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27883
[Shapiro], p. 428Equation 10.6.2selbergr 27896
[Shapiro], p. 429Equation 10.6.8selberg3r 27897
[Shapiro], p. 430Equation 10.6.11selberg4r 27898
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27912
[Shapiro], p. 434Equation 10.6.27pntlema 27924  pntlemb 27925  pntlemc 27923  pntlemd 27922  pntlemg 27926
[Shapiro], p. 435Equation 10.6.29pntlema 27924
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27916
[Shapiro], p. 436Lemma 10.6.2pntibnd 27921
[Shapiro], p. 436Equation 10.6.34pntlema 27924
[Shapiro], p. 436Equation 10.6.35pntlem3 27937  pntleml 27939
[Stewart] p. 91Lemma 7.3constrss 34418
[Stewart] p. 92Definition 7.4.df-constr 34405
[Stewart] p. 96Theorem 7.10constraddcl 34437  constrinvcl 34448  constrmulcl 34446  constrnegcl 34438  constrsqrtcl 34454
[Stewart] p. 97Theorem 7.11constrextdg2 34424
[Stewart] p. 98Theorem 7.12constrext2chn 34434
[Stewart] p. 99Theorem 7.132sqr3nconstr 34456
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34466
[Stoll] p. 13Definition corresponds to dfsymdif3 4251
[Stoll] p. 16Exercise 4.40dif 4355  dif0 4326
[Stoll] p. 16Exercise 4.8difdifdir 4446
[Stoll] p. 17Theorem 5.1(5)unvdif 4428
[Stoll] p. 19Theorem 5.2(13)undm 4242
[Stoll] p. 19Theorem 5.2(13')indm 4243
[Stoll] p. 20Remarkinvdif 4224
[Stoll] p. 25Definition of ordered tripledf-ot 4592
[Stoll] p. 43Definitionuniiun 5016
[Stoll] p. 44Definitionintiin 5017
[Stoll] p. 45Definitiondf-iin 4953
[Stoll] p. 45Definition indexed uniondf-iun 4952
[Stoll] p. 176Theorem 3.4(27)iman 407
[Stoll] p. 262Example 4.1dfsymdif3 4251
[Strang] p. 242Section 6.3expgrowth 45395
[Suppes] p. 22Theorem 2eq0 4296  eq0f 4293
[Suppes] p. 22Theorem 4eqss 3923  eqssd 3925  eqssi 3924
[Suppes] p. 23Theorem 5ss0 4351  ss0b 4350
[Suppes] p. 23Theorem 6sstr 3916  sstrALT2 45893
[Suppes] p. 23Theorem 7pssirr 4030
[Suppes] p. 23Theorem 8pssn2lp 4032
[Suppes] p. 23Theorem 9psstr 4035
[Suppes] p. 23Theorem 10pssss 4025
[Suppes] p. 25Theorem 12elin 4093  elun 4152
[Suppes] p. 26Theorem 15inidm 4123
[Suppes] p. 26Theorem 16in0 4344
[Suppes] p. 27Theorem 23unidm 4156
[Suppes] p. 27Theorem 24un0 4343
[Suppes] p. 27Theorem 25ssun1 4176
[Suppes] p. 27Theorem 26ssequn1 4184
[Suppes] p. 27Theorem 27unss 4188
[Suppes] p. 27Theorem 28indir 4231
[Suppes] p. 27Theorem 29undir 4232
[Suppes] p. 28Theorem 32difid 4324
[Suppes] p. 29Theorem 33difin 4217
[Suppes] p. 29Theorem 34indif 4225
[Suppes] p. 29Theorem 35undif1 4429
[Suppes] p. 29Theorem 36difun2 4436
[Suppes] p. 29Theorem 37difin0 4427
[Suppes] p. 29Theorem 38disjdif 4425
[Suppes] p. 29Theorem 39difundi 4235
[Suppes] p. 29Theorem 40difindi 4237
[Suppes] p. 30Theorem 41nalset 5267
[Suppes] p. 39Theorem 61uniss 4874
[Suppes] p. 39Theorem 65uniop 5487
[Suppes] p. 41Theorem 70intsn 4943
[Suppes] p. 42Theorem 71intpr 4941  intprg 4940
[Suppes] p. 42Theorem 73op1stb 5439
[Suppes] p. 42Theorem 78intun 4939
[Suppes] p. 44Definition 15(a)dfiun2 4989  dfiun2g 4987
[Suppes] p. 44Definition 15(b)dfiin2 4990
[Suppes] p. 47Theorem 86elpw 4560  elpw2 5295  elpw2g 5294  elpwg 4559  elpwgdedVD 45975
[Suppes] p. 47Theorem 87pwid 4579
[Suppes] p. 47Theorem 89pw0 4772
[Suppes] p. 48Theorem 90pwpw0 4773
[Suppes] p. 52Theorem 101xpss12 5665
[Suppes] p. 52Theorem 102xpindi 5809  xpindir 5810
[Suppes] p. 52Theorem 103xpundi 5719  xpundir 5720
[Suppes] p. 54Theorem 105elirrv 9592
[Suppes] p. 58Theorem 2relss 5757
[Suppes] p. 59Theorem 4eldm 5881  eldm2 5882  eldm2g 5880  eldmg 5879
[Suppes] p. 59Definition 3df-dm 5660
[Suppes] p. 60Theorem 6dmin 5892
[Suppes] p. 60Theorem 8rnun 6135
[Suppes] p. 60Theorem 9rnin 6136
[Suppes] p. 60Definition 4dfrn2 5869
[Suppes] p. 61Theorem 11brcnv 5859  brcnvg 5856
[Suppes] p. 62Equation 5elcnv 5853  elcnv2 5854
[Suppes] p. 62Theorem 12relcnv 6099
[Suppes] p. 62Theorem 15cnvin 6134
[Suppes] p. 62Theorem 16cnvun 6132
[Suppes] p. 63Definitiondftrrels2 39667
[Suppes] p. 63Theorem 20co02 6262
[Suppes] p. 63Theorem 21dmcoss 5956
[Suppes] p. 63Definition 7df-co 5659
[Suppes] p. 64Theorem 26cnvco 5866
[Suppes] p. 64Theorem 27coass 6267
[Suppes] p. 65Theorem 31resundi 5983
[Suppes] p. 65Theorem 34elima 6060  elima2 6061  elima3 6062  elimag 6059
[Suppes] p. 65Theorem 35imaundi 6140
[Suppes] p. 66Theorem 40dminss 6142
[Suppes] p. 66Theorem 41imainss 6143
[Suppes] p. 67Exercise 11cnvxp 6146
[Suppes] p. 81Definition 34dfec2 8721
[Suppes] p. 82Theorem 72elec 8765  elecALTV 39279  elecg 8763
[Suppes] p. 82Theorem 73eqvrelth 39703  erth 8773  erth2 8774
[Suppes] p. 83Theorem 74eqvreldisj 39706  erdisj 8776
[Suppes] p. 83Definition 35, df-parts 39876  dfmembpart2 39881
[Suppes] p. 89Theorem 96map0b 8912
[Suppes] p. 89Theorem 97map0 8916  map0g 8913
[Suppes] p. 89Theorem 98mapsn 8917  mapsnd 8915
[Suppes] p. 89Theorem 99mapss 8918
[Suppes] p. 91Definition 12(ii)alephsuc 10148
[Suppes] p. 91Definition 12(iii)alephlim 10147
[Suppes] p. 92Theorem 1enref 9013  enrefg 9012
[Suppes] p. 92Theorem 2ensym 9031  ensymb 9030  ensymi 9032
[Suppes] p. 92Theorem 3entr 9034
[Suppes] p. 92Theorem 4unen 9074
[Suppes] p. 94Theorem 15endom 9007
[Suppes] p. 94Theorem 16ssdomg 9028
[Suppes] p. 94Theorem 17domtr 9035
[Suppes] p. 95Theorem 18sbth 9117
[Suppes] p. 97Theorem 23canth2 9150  canth2g 9151
[Suppes] p. 97Definition 3brsdom2 9121  df-sdom 8977  dfsdom2 9120
[Suppes] p. 97Theorem 21(i)sdomirr 9134
[Suppes] p. 97Theorem 22(i)domnsym 9123
[Suppes] p. 97Theorem 21(ii)sdomnsym 9122
[Suppes] p. 97Theorem 22(ii)domsdomtr 9132
[Suppes] p. 97Theorem 22(iv)brdom2 9010
[Suppes] p. 97Theorem 21(iii)sdomtr 9135
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9130
[Suppes] p. 98Exercise 4fundmen 9060  fundmeng 9061
[Suppes] p. 98Exercise 6xpdom3 9095
[Suppes] p. 98Exercise 11sdomentr 9131
[Suppes] p. 104Theorem 37fofi 9306
[Suppes] p. 104Theorem 38pwfi 9311
[Suppes] p. 105Theorem 40pwfi 9311
[Suppes] p. 111Axiom for cardinal numberscarden 10636
[Suppes] p. 130Definition 3df-tr 5212
[Suppes] p. 132Theorem 9ssonuni 7794
[Suppes] p. 134Definition 6df-suc 6368
[Suppes] p. 136Theorem Schema 22findes 7912  finds 7908  finds1 7911  finds2 7910
[Suppes] p. 151Theorem 42isfinite 9654  isfinite2 9291  isfiniteg 9293  unbnn 9289
[Suppes] p. 162Definition 5df-ltnq 11004  df-ltpq 10996
[Suppes] p. 197Theorem Schema 4tfindes 7874  tfinds 7871  tfinds2 7875
[Suppes] p. 209Theorem 18oaord1 8560
[Suppes] p. 209Theorem 21oaword2 8562
[Suppes] p. 211Theorem 25oaass 8570
[Suppes] p. 225Definition 8iscard2 10058
[Suppes] p. 227Theorem 56ondomon 10648
[Suppes] p. 228Theorem 59harcard 10060
[Suppes] p. 228Definition 12(i)aleph0 10146
[Suppes] p. 228Theorem Schema 61onintss 6415
[Suppes] p. 228Theorem Schema 62onminesb 7807  onminsb 7808
[Suppes] p. 229Theorem 64alephval2 10658
[Suppes] p. 229Theorem 65alephcard 10150
[Suppes] p. 229Theorem 66alephord2i 10157
[Suppes] p. 229Theorem 67alephnbtwn 10151
[Suppes] p. 229Definition 12df-aleph 10022
[Suppes] p. 242Theorem 6weth 10574
[Suppes] p. 242Theorem 8entric 10642
[Suppes] p. 242Theorem 9carden 10636
[Szendrei] p. 11Line 6df-cloneop 36536
[Szendrei] p. 11Paragraph 3df-suppos 36540
[TakeutiZaring] p. 8Axiom 1ax-ext 2732
[TakeutiZaring] p. 13Definition 4.5df-cleq 2752  wl-df.cleq 38507
[TakeutiZaring] p. 13Proposition 4.6df-clel 2835  wl-df.clel 38510
[TakeutiZaring] p. 13Proposition 4.9cvjust 2754
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2780
[TakeutiZaring] p. 14Definition 4.16df-oprab 7424
[TakeutiZaring] p. 14Proposition 4.14ru 3737
[TakeutiZaring] p. 15Axiom 2zfpair 5382
[TakeutiZaring] p. 15Exercise 1elpr 4608  elpr2 4610  elpr2g 4609  elprg 4606
[TakeutiZaring] p. 15Exercise 2elsn 4598  elsn2 4625  elsn2g 4624  elsng 4597  velsn 4599
[TakeutiZaring] p. 15Exercise 3elop 5435
[TakeutiZaring] p. 15Exercise 4sneq 4593  sneqr 4799
[TakeutiZaring] p. 15Definition 5.1dfpr2 4604  dfsn2 4596  dfsn2ALT 4605
[TakeutiZaring] p. 16Axiom 3uniex 7758
[TakeutiZaring] p. 16Exercise 6opth 5444
[TakeutiZaring] p. 16Exercise 7opex 5431
[TakeutiZaring] p. 16Exercise 8rext 5415
[TakeutiZaring] p. 16Corollary 5.8unex 7761  unexg 7760
[TakeutiZaring] p. 16Definition 5.3dftp2 4651
[TakeutiZaring] p. 16Definition 5.5df-uni 4867
[TakeutiZaring] p. 16Definition 5.6df-in 4091  df-un 4151
[TakeutiZaring] p. 16Proposition 5.7unipr 4883  uniprg 4882
[TakeutiZaring] p. 17Axiom 4vpwex 5338
[TakeutiZaring] p. 17Exercise 1eltp 4649
[TakeutiZaring] p. 17Exercise 5elsuc 6435  elsucg 6433  sstr2 3915
[TakeutiZaring] p. 17Exercise 6uncom 4157
[TakeutiZaring] p. 17Exercise 7incom 4106
[TakeutiZaring] p. 17Exercise 8unass 4170
[TakeutiZaring] p. 17Exercise 9inass 4124
[TakeutiZaring] p. 17Exercise 10indi 4229
[TakeutiZaring] p. 17Exercise 11undi 4230
[TakeutiZaring] p. 17Definition 5.9df-pss 4014  df-ss 3896
[TakeutiZaring] p. 17Definition 5.10df-pw 4558
[TakeutiZaring] p. 18Exercise 7unss2 4185
[TakeutiZaring] p. 18Exercise 9dfss2 4094  sseqin2 4120
[TakeutiZaring] p. 18Exercise 10ssid 3930
[TakeutiZaring] p. 18Exercise 12inss1 4133  inss2 4134
[TakeutiZaring] p. 18Exercise 13nss 3972
[TakeutiZaring] p. 18Exercise 15unieq 4877
[TakeutiZaring] p. 18Exercise 18sspwb 5416  sspwimp 45976  sspwimpALT 45983  sspwimpALT2 45986  sspwimpcf 45978
[TakeutiZaring] p. 18Exercise 19pweqb 5423
[TakeutiZaring] p. 19Axiom 5ax-rep 5231
[TakeutiZaring] p. 20Definitiondf-rab 3413
[TakeutiZaring] p. 20Corollary 5.160ex 5260
[TakeutiZaring] p. 20Definition 5.12df-dif 4047
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37515  dfnul2 4281
[TakeutiZaring] p. 20Proposition 5.15difid 4324
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4299  n0f 4295  neq0 4298  neq0f 4294
[TakeutiZaring] p. 21Axiom 6zfreg 9591
[TakeutiZaring] p. 21Axiom 6'zfregs 9734
[TakeutiZaring] p. 21Theorem 5.22setind 9749
[TakeutiZaring] p. 21Definition 5.20df-v 3452
[TakeutiZaring] p. 21Proposition 5.21vprc 5273
[TakeutiZaring] p. 22Exercise 10ss 4349
[TakeutiZaring] p. 22Exercise 3ssex 5281  ssexg 5280
[TakeutiZaring] p. 22Exercise 4inex1 5276
[TakeutiZaring] p. 22Exercise 5ruv 9603
[TakeutiZaring] p. 22Exercise 6elirr 9595
[TakeutiZaring] p. 22Exercise 7ssdif0 4313
[TakeutiZaring] p. 22Exercise 11difdif 4071
[TakeutiZaring] p. 22Exercise 13undif3 4245  undif3VD 45940
[TakeutiZaring] p. 22Exercise 14difss 4072
[TakeutiZaring] p. 22Exercise 15sscon 4079
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3077
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3087
[TakeutiZaring] p. 23Proposition 6.2xpex 7767  xpexg 7764
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5657
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6611
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6789  fun11 6614
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6551  svrelfun 6612
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5868
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5870
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5662
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5663
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5659
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6185  dfrel2 6180
[TakeutiZaring] p. 25Exercise 3xpss 5666
[TakeutiZaring] p. 25Exercise 5relun 5788
[TakeutiZaring] p. 25Exercise 6reluni 5795
[TakeutiZaring] p. 25Exercise 9inxp 5808
[TakeutiZaring] p. 25Exercise 12relres 5995
[TakeutiZaring] p. 25Exercise 13opelres 5975  opelresi 5977
[TakeutiZaring] p. 25Exercise 14dmres 6002
[TakeutiZaring] p. 25Exercise 15resss 5991
[TakeutiZaring] p. 25Exercise 17resabs1 5996
[TakeutiZaring] p. 25Exercise 18funres 6582
[TakeutiZaring] p. 25Exercise 24relco 6103
[TakeutiZaring] p. 25Exercise 29funco 6580
[TakeutiZaring] p. 25Exercise 30f1co 6791
[TakeutiZaring] p. 26Definition 6.10eu2 2634
[TakeutiZaring] p. 26Definition 6.11conventions 31002  df-fv 6546  fv3 6903
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7937  cnvexg 7936
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7921  dmexg 7913
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7922  rnexg 7914
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45512
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7932
[TakeutiZaring] p. 27Corollary 6.13fvex 6898
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 48320  tz6.12-1-afv2 48387  tz6.12-1 6908  tz6.12-afv 48319  tz6.12-afv2 48386  tz6.12 6909  tz6.12c-afv2 48388  tz6.12c 6907
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 48383  tz6.12-2 6872  tz6.12i-afv2 48389  tz6.12i 6911
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6541
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6542
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6544  wfo 6536
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6543  wf1 6535
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6545  wf1o 6537
[TakeutiZaring] p. 28Exercise 4eqfnfv 7029  eqfnfv2 7030  eqfnfv2f 7033
[TakeutiZaring] p. 28Exercise 5fvco 6983
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7223
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7221
[TakeutiZaring] p. 29Exercise 9funimaex 6627  funimaexg 6626
[TakeutiZaring] p. 29Definition 6.18df-br 5103
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5559
[TakeutiZaring] p. 30Definition 6.21dffr2 5611  dffr3 6096  eliniseg 6091  iniseg 6094
[TakeutiZaring] p. 30Definition 6.22df-eprel 5550
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5627  fr3nr 7786  frirr 5626
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5603
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7788
[TakeutiZaring] p. 31Exercise 1frss 5614
[TakeutiZaring] p. 31Exercise 4wess 5636
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6350  tz6.26i 6351  wefrc 5644  wereu2 5647
[TakeutiZaring] p. 32Theorem 6.27wfi 6352  wfii 6353
[TakeutiZaring] p. 32Definition 6.28df-isom 6547
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7337
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7338
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7344
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7345
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7346
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7350
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7357
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7359
[TakeutiZaring] p. 35Notationwtr 5211
[TakeutiZaring] p. 35Theorem 7.2trelpss 45513  tz7.2 5633
[TakeutiZaring] p. 35Definition 7.1dftr3 5216
[TakeutiZaring] p. 36Proposition 7.4ordwe 6375
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6383
[TakeutiZaring] p. 36Proposition 7.6ordelord 6384  ordelordALT 45596  ordelordALTVD 45925
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6390  ordelssne 6389
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6388
[TakeutiZaring] p. 37Proposition 7.9ordin 6393
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7796
[TakeutiZaring] p. 38Corollary 7.15ordsson 7797
[TakeutiZaring] p. 38Definition 7.11df-on 6366
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6395
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45608  ordon 7791
[TakeutiZaring] p. 38Proposition 7.13onprc 7792
[TakeutiZaring] p. 39Theorem 7.17tfi 7864
[TakeutiZaring] p. 40Exercise 3ontr2 6411  ontr2d 37024
[TakeutiZaring] p. 40Exercise 7dftr2 5213
[TakeutiZaring] p. 40Exercise 9onssmin 7806
[TakeutiZaring] p. 40Exercise 11unon 7842
[TakeutiZaring] p. 40Exercise 12ordun 6469
[TakeutiZaring] p. 40Exercise 14ordequn 6468
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7793
[TakeutiZaring] p. 40Proposition 7.20elssuni 4898
[TakeutiZaring] p. 41Definition 7.22df-suc 6368
[TakeutiZaring] p. 41Proposition 7.23sssucid 6445  sucidg 6446
[TakeutiZaring] p. 41Proposition 7.24onsuc 7824
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6459  ordnbtwn 6458
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7839
[TakeutiZaring] p. 42Exercise 1df-lim 6367
[TakeutiZaring] p. 42Exercise 4omssnlim 7892
[TakeutiZaring] p. 42Exercise 7ssnlim 7897
[TakeutiZaring] p. 42Exercise 8onsucssi 7852  ordelsuc 7831
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7833
[TakeutiZaring] p. 42Definition 7.27nlimon 7862
[TakeutiZaring] p. 42Definition 7.28dfom2 7879
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7900
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7901
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7902
[TakeutiZaring] p. 43Remarkomon 7889
[TakeutiZaring] p. 43Axiom 7inf3 9637  omex 9645
[TakeutiZaring] p. 43Theorem 7.32ordom 7887
[TakeutiZaring] p. 43Corollary 7.31find 7907
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7904
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7905
[TakeutiZaring] p. 44Exercise 1limomss 7882
[TakeutiZaring] p. 44Exercise 2int0 4921
[TakeutiZaring] p. 44Exercise 3trintss 5230
[TakeutiZaring] p. 44Exercise 4intss1 4922
[TakeutiZaring] p. 44Exercise 5intex 5304
[TakeutiZaring] p. 44Exercise 6oninton 7809
[TakeutiZaring] p. 44Exercise 11ordintdif 6414
[TakeutiZaring] p. 44Definition 7.35df-int 4907
[TakeutiZaring] p. 44Proposition 7.34noinfep 9662
[TakeutiZaring] p. 45Exercise 4onint 7804
[TakeutiZaring] p. 47Lemma 1tfrlem1 8384
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8406
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8407
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8408
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8415  tz7.44-2 8416  tz7.44-3 8417
[TakeutiZaring] p. 50Exercise 1smogt 8376
[TakeutiZaring] p. 50Exercise 3smoiso 8371
[TakeutiZaring] p. 50Definition 7.46df-smo 8355
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8456  tz7.49c 8457
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8454
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8453
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8455
[TakeutiZaring] p. 53Proposition 7.532eu5 2680
[TakeutiZaring] p. 54Definition 7.55df-lexo 35921
[TakeutiZaring] p. 54Definition 7.57df-r0 35922
[TakeutiZaring] p. 54Proposition 7.58r0weseon 35932
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10091  lexoweon 35930
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10092
[TakeutiZaring] p. 55Definition 7.59df-j0 35923  j0iso 35936
[TakeutiZaring] p. 56Definition 8.1oalim 8541  oasuc 8533
[TakeutiZaring] p. 57Remarktfindsg 7872
[TakeutiZaring] p. 57Proposition 8.2oacl 8544
[TakeutiZaring] p. 57Proposition 8.3oa0 8525  oa0r 8547
[TakeutiZaring] p. 57Proposition 8.16omcl 8545
[TakeutiZaring] p. 58Corollary 8.5oacan 8557
[TakeutiZaring] p. 58Proposition 8.4nnaord 8629  nnaordi 8628  oaord 8556  oaordi 8555
[TakeutiZaring] p. 59Proposition 8.6iunss2 5007  uniss2 4901
[TakeutiZaring] p. 59Proposition 8.7oawordri 8559
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8564  oawordex 8566
[TakeutiZaring] p. 59Proposition 8.9nnacl 8621
[TakeutiZaring] p. 59Proposition 8.10oaabs 8658
[TakeutiZaring] p. 60Remarkoancom 9653
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8569
[TakeutiZaring] p. 62Exercise 1nnarcl 8626
[TakeutiZaring] p. 62Exercise 5oaword1 8561
[TakeutiZaring] p. 62Definition 8.15om0x 8528  omlim 8542  omsuc 8535
[TakeutiZaring] p. 62Definition 8.15(a)om0 8526
[TakeutiZaring] p. 63Proposition 8.17nnecl 8623  nnmcl 8622
[TakeutiZaring] p. 63Proposition 8.19nnmord 8642  nnmordi 8641  omord 8577  omordi 8575
[TakeutiZaring] p. 63Proposition 8.20omcan 8578
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8646  omwordri 8581
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8548
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8551  om1r 8552
[TakeutiZaring] p. 64Proposition 8.22om00 8584
[TakeutiZaring] p. 64Proposition 8.23omordlim 8586
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8587
[TakeutiZaring] p. 64Proposition 8.25odi 8588
[TakeutiZaring] p. 65Theorem 8.26omass 8589
[TakeutiZaring] p. 67Definition 8.30nnesuc 8618  oe0 8531  oelim 8543  oesuc 8536  onesuc 8539
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8529
[TakeutiZaring] p. 67Proposition 8.32oen0 8596
[TakeutiZaring] p. 67Proposition 8.33oeordi 8597
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8530
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8554
[TakeutiZaring] p. 68Corollary 8.34oeord 8598
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8604
[TakeutiZaring] p. 68Proposition 8.35oewordri 8602
[TakeutiZaring] p. 68Proposition 8.37oeworde 8603
[TakeutiZaring] p. 69Proposition 8.41oeoa 8607
[TakeutiZaring] p. 70Proposition 8.42oeoe 8609
[TakeutiZaring] p. 73Theorem 9.1trcl 9730  tz9.1 9731
[TakeutiZaring] p. 76Definition 9.9df-r1 9769  r10 9776  r1lim 9780  r1limg 9779  r1suc 9778  r1sucg 9777
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9788  r1ord2 9789  r1ordg 9786
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9798
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9825  tz9.13 9799  tz9.13g 9800
[TakeutiZaring] p. 79Definition 9.14df-rank 9770  rankval 9826  rankvalb 9806  rankvalg 9827
[TakeutiZaring] p. 79Proposition 9.16rankel 9852  rankelb 9834
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9868  rankval3 9854  rankval3b 9837
[TakeutiZaring] p. 79Proposition 9.18rankonid 9840
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9804
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9847  rankr1c 9831  rankr1g 9845
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9848
[TakeutiZaring] p. 80Exercise 1rankss 9864  rankssb 9863
[TakeutiZaring] p. 80Exercise 2unbndrank 9856
[TakeutiZaring] p. 80Proposition 9.19bndrank 9855
[TakeutiZaring] p. 83Axiom of Choiceac4 10554  dfac3 10201
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10110  numth 10551  numth2 10550
[TakeutiZaring] p. 85Definition 10.4cardval 10631
[TakeutiZaring] p. 85Proposition 10.5cardid 10632  cardid2 10035
[TakeutiZaring] p. 85Proposition 10.9oncard 10042
[TakeutiZaring] p. 85Proposition 10.10carden 10636
[TakeutiZaring] p. 85Proposition 10.11cardidm 10041
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 10026
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10047
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 10039
[TakeutiZaring] p. 87Proposition 10.15pwen 9170
[TakeutiZaring] p. 88Exercise 1en0 9046
[TakeutiZaring] p. 88Exercise 7infensuc 9175
[TakeutiZaring] p. 89Exercise 10omxpen 9099
[TakeutiZaring] p. 90Corollary 10.23cardnn 10045
[TakeutiZaring] p. 90Definition 10.27alephiso 10178
[TakeutiZaring] p. 90Proposition 10.20nneneq 9222
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9230
[TakeutiZaring] p. 90Proposition 10.26alephprc 10179
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9227
[TakeutiZaring] p. 91Exercise 2alephle 10168
[TakeutiZaring] p. 91Exercise 3aleph0 10146
[TakeutiZaring] p. 91Exercise 4cardlim 10054
[TakeutiZaring] p. 91Exercise 7infpss 10295
[TakeutiZaring] p. 91Exercise 8infcntss 9315
[TakeutiZaring] p. 91Definition 10.29df-fin 8978  isfi 9003
[TakeutiZaring] p. 92Proposition 10.32onfin 9231
[TakeutiZaring] p. 92Proposition 10.34imadomg 10614
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9092
[TakeutiZaring] p. 93Proposition 10.35fodomb 10606
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10265  unxpdom 9251
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10056  cardsdomelir 10055
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9253
[TakeutiZaring] p. 94Proposition 10.39infxpen 10094
[TakeutiZaring] p. 95Definition 10.42df-map 8850
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10647  infxpidm2 10097
[TakeutiZaring] p. 95Proposition 10.41infdju 10286  infxp 10293
[TakeutiZaring] p. 96Proposition 10.44pw2en 9104  pw2f1o 9102
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9163
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10566
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10561  ac6s5 10570
[TakeutiZaring] p. 98Theorem 10.47unidom 10628
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10629  uniimadomf 10630
[TakeutiZaring] p. 100Definition 11.1cfcof 10353
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10348
[TakeutiZaring] p. 102Exercise 1cfle 10332
[TakeutiZaring] p. 102Exercise 2cf0 10329
[TakeutiZaring] p. 102Exercise 3cfsuc 10336
[TakeutiZaring] p. 102Exercise 4cfom 10343
[TakeutiZaring] p. 102Proposition 11.9coftr 10352
[TakeutiZaring] p. 103Theorem 11.15alephreg 10668
[TakeutiZaring] p. 103Proposition 11.11cardcf 10330
[TakeutiZaring] p. 103Proposition 11.13alephsing 10355
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10177
[TakeutiZaring] p. 104Proposition 11.16carduniima 10176
[TakeutiZaring] p. 104Proposition 11.18alephfp 10188  alephfp2 10189
[TakeutiZaring] p. 106Theorem 11.20gchina 10785
[TakeutiZaring] p. 106Theorem 11.21mappwen 10192
[TakeutiZaring] p. 107Theorem 11.26konigth 10655
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10669
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10670
[TakeutiZaring] p. 143Definition 14.1(1)df-cnv2 35901
[TakeutiZaring] p. 143Definition 14.1(2)df-cnv3 35902
[TakeutiZaring] p. 144Definition 14.2df-gdlop1 35903  df-gdlop2 35904  df-gdlop3 35905  df-gdlop4 35906  df-gdlop5 35907  df-gdlop6 35908  df-gdlop7 35909  df-gdlop8 35910  df-gdlopc 35911
[TakeutiZaring] p. 154Proposition 15.1(1)maxssj0 35938
[TakeutiZaring] p. 154Proposition 15.1(2)j0ltaleph 35940
[TakeutiZaring] p. 155Definition 15.2df-j 35924
[TakeutiZaring] p. 156Definition 15.7df-k1 35925  df-k2 35926  df-k3 35927
[TakeutiZaring] p. 158Definition 15.13df-fnl 35928
[TakeutiZaring] p. 158Definition 15.15df-l 35929
[Tarski] p. 67Axiom B5ax-c5 40016
[Tarski] p. 67Scheme B5sp 2219
[Tarski] p. 68Lemma 6avril1 31065  equid 2044
[Tarski] p. 69Lemma 7equcomi 2049
[Tarski] p. 70Lemma 14spim 2416  spime 2418  spimew 2003
[Tarski] p. 70Lemma 16ax-12 2212  ax-c15 40022  ax12i 1998
[Tarski] p. 70Lemmas 16 and 17sb6 2121
[Tarski] p. 75Axiom B7ax6v 2000
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1942  ax5ALT 40040
[Tarski], p. 75Scheme B8 of system S2ax-7 2040  ax-8 2146  ax-9 2154
[Tarski1999] p. 178Axiom 4axtgsegcon 28927
[Tarski1999] p. 178Axiom 5axtg5seg 28928
[Tarski1999] p. 179Axiom 7axtgpasch 28930
[Tarski1999] p. 180Axiom 7.1axtgpasch 28930
[Tarski1999] p. 185Axiom 11axtgcont1 28931
[Truss] p. 114Theorem 5.18ruc 16412
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38653
[Viaclovsky8] p. 3Proposition 7ismblfin 38655
[Weierstrass] p. 272Definitiondf-mdet 22901  mdetuni 22938
[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 38444
[WhiteheadRussell] p. 100Theorem *2.05frege5 44876  imim2 59  wl-luk-imim2 38439
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 48165  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 910
[WhiteheadRussell] p. 101Theorem *2.06barbara 2687  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 916
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38442
[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 45985  wl-luk-notnotr 38443
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44906  axfrege28 44905  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 38436
[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 31003  pm2.27 43  wl-luk-pm2.27 38434
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 936
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 39379
[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 37566
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45418
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45419
[WhiteheadRussell] p. 147Theorem *10.2219.26 1902
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45420
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45421
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45422
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1925
[WhiteheadRussell] p. 151Theorem *10.301albitr 45423
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45424
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45425
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45426
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45427
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45429
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45430
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45431
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45428
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2126
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45434
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45435
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2106
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2196
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1861
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1862
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45436
[WhiteheadRussell] p. 162Theorem *11.322alim 45437
[WhiteheadRussell] p. 162Theorem *11.332albi 45438
[WhiteheadRussell] p. 162Theorem *11.342exim 45439
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45441
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45440
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1919
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45443
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45444
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45442
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1860
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45445
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45446
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1878
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45447
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2375
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1892
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45452
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45448
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45449
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45450
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45451
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45456
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45453
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45454
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45455
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45457
[WhiteheadRussell] p. 175Definition *14.02df-eu 2594
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45467  pm13.13b 45468
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45469
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3036
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3037
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3619
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45475
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45476
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45470
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45611  pm13.193 45471
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45472
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45473
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45474
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45481
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45480
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45479
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3800
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45482  pm14.122b 45483  pm14.122c 45484
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45485  pm14.123b 45486  pm14.123c 45487
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45489
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45488
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45490
[WhiteheadRussell] p. 190Theorem *14.22iota4 6519
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45491
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6520
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45492
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45494
[WhiteheadRussell] p. 192Theorem *14.26eupick 2658  eupickbi 2661  sbaniota 45495
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45493
[WhiteheadRussell] p. 192Theorem *14.271eubi 2609
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45496
[WhiteheadRussell] p. 235Definition *30.01conventions 31002  df-fv 6546
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10083  pm54.43lem 10082
[Young] p. 141Definition of operator orderingleop2 32727
[Young] p. 142Example 12.2(i)0leop 32733  idleop 32734
[vandenDries] p. 42Lemma 61irrapx1 43911
[vandenDries] p. 43Theorem 62pellex 43918  pellexlem1 43912

This page was last updated on 17-Oct-2026.
Copyright terms: Public domain