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 17634
[Adamek] p. 21Condition 3.1(b)df-cat 17634
[Adamek] p. 22Example 3.3(1)df-setc 18043
[Adamek] p. 24Example 3.3(4.c)0cat 17655  0funcg 49554  df-termc 49942
[Adamek] p. 24Example 3.3(4.d)df-prstc 50019  prsthinc 49933
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50047  df-mndtc 50047
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50043
[Adamek] p. 25Definition 3.5df-oppc 17678
[Adamek] p. 25Example 3.6(1)oduoppcciso 50035
[Adamek] p. 25Example 3.6(2)oppgoppcco 50060  oppgoppchom 50059  oppgoppcid 50061
[Adamek] p. 28Remark 3.9oppciso 17748
[Adamek] p. 28Remark 3.12invf1o 17736  invisoinvl 17757
[Adamek] p. 28Example 3.13idinv 17756  idiso 17755
[Adamek] p. 28Corollary 3.11inveq 17741
[Adamek] p. 28Definition 3.8df-inv 17715  df-iso 17716  dfiso2 17739
[Adamek] p. 28Proposition 3.10sectcan 17722
[Adamek] p. 29Remark 3.16cicer 17773  cicerALT 49515
[Adamek] p. 29Definition 3.15cic 17766  df-cic 17763
[Adamek] p. 29Definition 3.17df-func 17825
[Adamek] p. 29Proposition 3.14(1)invinv 17737
[Adamek] p. 29Proposition 3.14(2)invco 17738  isoco 17744
[Adamek] p. 30Remark 3.19df-func 17825
[Adamek] p. 30Example 3.20(1)idfucl 17848
[Adamek] p. 30Example 3.20(2)diag1 49773
[Adamek] p. 32Proposition 3.21funciso 17841
[Adamek] p. 33Example 3.26(1)discsnterm 50043  discthing 49930
[Adamek] p. 33Example 3.26(2)df-thinc 49887  prsthinc 49933  thincciso 49922  thincciso2 49924  thincciso3 49925  thinccisod 49923
[Adamek] p. 33Example 3.26(3)df-mndtc 50047
[Adamek] p. 33Proposition 3.23cofucl 17855  cofucla 49565
[Adamek] p. 34Remark 3.28(1)cofidfth 49631
[Adamek] p. 34Remark 3.28(2)catciso 18078  catcisoi 49869
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18133
[Adamek] p. 34Definition 3.27(2)df-fth 17874
[Adamek] p. 34Definition 3.27(3)df-full 17873
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18133
[Adamek] p. 35Corollary 3.32ffthiso 17898
[Adamek] p. 35Proposition 3.30(c)cofth 17904
[Adamek] p. 35Proposition 3.30(d)cofull 17903
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18118
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18118
[Adamek] p. 39Remark 3.422oppf 49601
[Adamek] p. 39Definition 3.41df-oppf 49592  funcoppc 17842
[Adamek] p. 39Definition 3.44.df-catc 18066  elcatchom 49866
[Adamek] p. 39Proposition 3.43(c)fthoppc 17892  fthoppf 49633
[Adamek] p. 39Proposition 3.43(d)fulloppc 17891  fulloppf 49632
[Adamek] p. 40Remark 3.48catccat 18075
[Adamek] p. 40Definition 3.470funcg 49554  df-catc 18066
[Adamek] p. 45Exercise 3Gincat 50070
[Adamek] p. 48Remark 4.2(2)cnelsubc 50073  nelsubc3 49540
[Adamek] p. 48Remark 4.2(3)imasubc 49620  imasubc2 49621  imasubc3 49625
[Adamek] p. 48Example 4.3(1.a)0subcat 17805
[Adamek] p. 48Example 4.3(1.b)catsubcat 17806
[Adamek] p. 48Definition 4.1(1)nelsubc3 49540
[Adamek] p. 48Definition 4.1(2)fullsubc 17817
[Adamek] p. 48Definition 4.1(a)df-subc 17779
[Adamek] p. 49Remark 4.4idsubc 49629
[Adamek] p. 49Remark 4.4(1)idemb 49628
[Adamek] p. 49Remark 4.4(2)idfullsubc 49630  ressffth 17907
[Adamek] p. 58Exercise 4Asetc1onsubc 50071
[Adamek] p. 83Definition 6.1df-nat 17913
[Adamek] p. 87Remark 6.14(a)fuccocl 17934
[Adamek] p. 87Remark 6.14(b)fucass 17938
[Adamek] p. 87Definition 6.15df-fuc 17914
[Adamek] p. 88Remark 6.16fuccat 17940
[Adamek] p. 101Definition 7.10funcg 49554  df-inito 17951
[Adamek] p. 101Example 7.2(3)0funcg 49554  df-termc 49942  initc 49560
[Adamek] p. 101Example 7.2 (6)irinitoringc 21459
[Adamek] p. 102Definition 7.4df-termo 17952  oppctermo 49705
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17979
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17983
[Adamek] p. 103Remark 7.8oppczeroo 49706
[Adamek] p. 103Definition 7.7df-zeroo 17953
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21460
[Adamek] p. 103Proposition 7.6termoeu1w 17986
[Adamek] p. 106Definition 7.19df-sect 17714
[Adamek] p. 107Example 7.20(7)thincinv 49938
[Adamek] p. 108Example 7.25(4)thincsect2 49937
[Adamek] p. 110Example 7.33(9)thincmon 49902
[Adamek] p. 110Proposition 7.35sectmon 17749
[Adamek] p. 112Proposition 7.42sectepi 17751
[Adamek] p. 185Section 10.67updjud 9858
[Adamek] p. 193Definition 11.1(1)df-lmd 50114
[Adamek] p. 193Definition 11.3(1)df-lmd 50114
[Adamek] p. 194Definition 11.3(2)df-lmd 50114
[Adamek] p. 202Definition 11.27(1)df-cmd 50115
[Adamek] p. 202Definition 11.27(2)df-cmd 50115
[Adamek] p. 478Item Rngdf-ringc 20623
[AhoHopUll] p. 2Section 1.1df-bigo 49018
[AhoHopUll] p. 12Section 1.3df-blen 49040
[AhoHopUll] p. 318Section 9.1df-concat 14533  df-pfx 14634  df-substr 14604  df-word 14476  lencl 14495  wrd0 14501
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24673  df-nmoo 30816
[AkhiezerGlazman] p. 64Theoremhmopidmch 32224  hmopidmchi 32222
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32272  pjcmul2i 32273
[AkhiezerGlazman] p. 72Theoremcnvunop 31989  unoplin 31991
[AkhiezerGlazman] p. 72Equation 2unopadj 31990  unopadj2 32009
[AkhiezerGlazman] p. 73Theoremelunop2 32084  lnopunii 32083
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32157
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27919
[Alling] p. 184Axiom Bbdayfo 27641
[Alling] p. 184Axiom Oltsso 27640
[Alling] p. 184Axiom SDnodense 27656
[Alling] p. 185Lemma 0nocvxmin 27747
[Alling] p. 185Theoremconway 27771
[Alling] p. 185Axiom FEnoeta 27707
[Alling] p. 186Theorem 4lesrec 27791  lesrecd 27792
[Alling], p. 2Definitionrp-brsslt 43850
[Alling], p. 3Notenla0001 43853  nla0002 43851  nla0003 43852
[Apostol] p. 18Theorem I.1addcan 11330  addcan2d 11350  addcan2i 11340  addcand 11349  addcani 11339
[Apostol] p. 18Theorem I.2negeu 11383
[Apostol] p. 18Theorem I.3negsub 11442  negsubd 11511  negsubi 11472
[Apostol] p. 18Theorem I.4negneg 11444  negnegd 11496  negnegi 11464
[Apostol] p. 18Theorem I.5subdi 11583  subdid 11606  subdii 11599  subdir 11584  subdird 11607  subdiri 11600
[Apostol] p. 18Theorem I.6mul01 11325  mul01d 11345  mul01i 11336  mul02 11324  mul02d 11344  mul02i 11335
[Apostol] p. 18Theorem I.7mulcan 11787  mulcan2d 11784  mulcand 11783  mulcani 11789
[Apostol] p. 18Theorem I.8receu 11795  xreceu 32981
[Apostol] p. 18Theorem I.9divrec 11825  divrecd 11934  divreci 11900  divreczi 11893
[Apostol] p. 18Theorem I.10recrec 11852  recreci 11887
[Apostol] p. 18Theorem I.11mul0or 11790  mul0ord 11798  mul0ori 11797
[Apostol] p. 18Theorem I.12mul2neg 11589  mul2negd 11605  mul2negi 11598  mulneg1 11586  mulneg1d 11603  mulneg1i 11596
[Apostol] p. 18Theorem I.13divadddiv 11870  divadddivd 11975  divadddivi 11917
[Apostol] p. 18Theorem I.14divmuldiv 11855  divmuldivd 11972  divmuldivi 11915  rdivmuldivd 20393
[Apostol] p. 18Theorem I.15divdivdiv 11856  divdivdivd 11978  divdivdivi 11918
[Apostol] p. 20Axiom 7rpaddcl 12966  rpaddcld 13001  rpmulcl 12967  rpmulcld 13002
[Apostol] p. 20Axiom 8rpneg 12976
[Apostol] p. 20Axiom 90nrp 12979
[Apostol] p. 20Theorem I.17lttri 11272
[Apostol] p. 20Theorem I.18ltadd1d 11743  ltadd1dd 11761  ltadd1i 11704
[Apostol] p. 20Theorem I.19ltmul1 12005  ltmul1a 12004  ltmul1i 12074  ltmul1ii 12084  ltmul2 12006  ltmul2d 13028  ltmul2dd 13042  ltmul2i 12077
[Apostol] p. 20Theorem I.20msqgt0 11670  msqgt0d 11717  msqgt0i 11687
[Apostol] p. 20Theorem I.210lt1 11672
[Apostol] p. 20Theorem I.23lt0neg1 11656  lt0neg1d 11719  ltneg 11650  ltnegd 11728  ltnegi 11694
[Apostol] p. 20Theorem I.25lt2add 11635  lt2addd 11773  lt2addi 11712
[Apostol] p. 20Definition of positive numbersdf-rp 12943
[Apostol] p. 21Exercise 4recgt0 12001  recgt0d 12090  recgt0i 12061  recgt0ii 12062
[Apostol] p. 22Definition of integersdf-z 12525
[Apostol] p. 22Definition of positive integersdfnn3 12188
[Apostol] p. 22Definition of rationalsdf-q 12899
[Apostol] p. 24Theorem I.26supeu 9367
[Apostol] p. 26Theorem I.28nnunb 12433
[Apostol] p. 26Theorem I.29arch 12434  archd 45592
[Apostol] p. 28Exercise 2btwnz 12632
[Apostol] p. 28Exercise 3nnrecl 12435
[Apostol] p. 28Exercise 4rebtwnz 12897
[Apostol] p. 28Exercise 5zbtwnre 12896
[Apostol] p. 28Exercise 6qbtwnre 13151
[Apostol] p. 28Exercise 10(a)zeneo 16308  zneo 12612  zneoALTV 48139
[Apostol] p. 29Theorem I.35cxpsqrtth 26694  msqsqrtd 15405  resqrtth 15217  sqrtth 15327  sqrtthi 15333  sqsqrtd 15404
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12177
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12863
[Apostol] p. 361Remarkcrreczi 14190
[Apostol] p. 363Remarkabsgt0i 15362
[Apostol] p. 363Exampleabssubd 15418  abssubi 15366
[ApostolNT] p. 7Remarkfmtno0 47997  fmtno1 47998  fmtno2 48007  fmtno3 48008  fmtno4 48009  fmtno5fac 48039  fmtnofz04prm 48034
[ApostolNT] p. 7Definitiondf-fmtno 47985
[ApostolNT] p. 8Definitiondf-ppi 27063
[ApostolNT] p. 14Definitiondf-dvds 16222
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16238
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16263
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16258
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16251
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16253
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16239
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16240
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16245
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16280
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16282
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16284
[ApostolNT] p. 15Definitiondf-gcd 16464  dfgcd2 16515
[ApostolNT] p. 16Definitionisprm2 16651
[ApostolNT] p. 16Theorem 1.5coprmdvds 16622
[ApostolNT] p. 16Theorem 1.7prminf 16886
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16482
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16516
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16518
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16497
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16489
[ApostolNT] p. 17Theorem 1.8coprm 16681
[ApostolNT] p. 17Theorem 1.9euclemma 16683
[ApostolNT] p. 17Theorem 1.101arith2 16899
[ApostolNT] p. 18Theorem 1.13prmrec 16893
[ApostolNT] p. 19Theorem 1.14divalg 16372
[ApostolNT] p. 20Theorem 1.15eucalg 16556
[ApostolNT] p. 24Definitiondf-mu 27064
[ApostolNT] p. 25Definitiondf-phi 16736
[ApostolNT] p. 25Theorem 2.1musum 27154
[ApostolNT] p. 26Theorem 2.2phisum 16761
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16746
[ApostolNT] p. 28Theorem 2.5(c)phimul 16750
[ApostolNT] p. 32Definitiondf-vma 27061
[ApostolNT] p. 32Theorem 2.9muinv 27156
[ApostolNT] p. 32Theorem 2.10vmasum 27179
[ApostolNT] p. 38Remarkdf-sgm 27065
[ApostolNT] p. 38Definitiondf-sgm 27065
[ApostolNT] p. 75Definitiondf-chp 27062  df-cht 27060
[ApostolNT] p. 104Definitioncongr 16633
[ApostolNT] p. 106Remarkdvdsval3 16225
[ApostolNT] p. 106Definitionmoddvds 16232
[ApostolNT] p. 107Example 2mod2eq0even 16315
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16316
[ApostolNT] p. 107Example 4zmod1congr 13847
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13887
[ApostolNT] p. 107Theorem 5.2(c)modexp 14200
[ApostolNT] p. 108Theorem 5.3modmulconst 16257
[ApostolNT] p. 109Theorem 5.4cncongr1 16636
[ApostolNT] p. 109Theorem 5.6gcdmodi 17045
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16638
[ApostolNT] p. 113Theorem 5.17eulerth 16753
[ApostolNT] p. 113Theorem 5.18vfermltl 16772
[ApostolNT] p. 114Theorem 5.19fermltl 16754
[ApostolNT] p. 116Theorem 5.24wilthimp 27035
[ApostolNT] p. 179Definitiondf-lgs 27258  lgsprme0 27302
[ApostolNT] p. 180Example 11lgs 27303
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27279
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27294
[ApostolNT] p. 181Theorem 9.4m1lgs 27351
[ApostolNT] p. 181Theorem 9.52lgs 27370  2lgsoddprm 27379
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27337
[ApostolNT] p. 185Theorem 9.8lgsquad 27346
[ApostolNT] p. 188Definitiondf-lgs 27258  lgs1 27304
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27295
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27297
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27305
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27306
[Baer] p. 40Property (b)mapdord 42084
[Baer] p. 40Property (c)mapd11 42085
[Baer] p. 40Property (e)mapdin 42108  mapdlsm 42110
[Baer] p. 40Property (f)mapd0 42111
[Baer] p. 40Definition of projectivitydf-mapd 42071  mapd1o 42094
[Baer] p. 41Property (g)mapdat 42113
[Baer] p. 44Part (1)mapdpg 42152
[Baer] p. 45Part (2)hdmap1eq 42247  mapdheq 42174  mapdheq2 42175  mapdheq2biN 42176
[Baer] p. 45Part (3)baerlem3 42159
[Baer] p. 46Part (4)mapdheq4 42178  mapdheq4lem 42177
[Baer] p. 46Part (5)baerlem5a 42160  baerlem5abmN 42164  baerlem5amN 42162  baerlem5b 42161  baerlem5bmN 42163
[Baer] p. 47Part (6)hdmap1l6 42267  hdmap1l6a 42255  hdmap1l6e 42260  hdmap1l6f 42261  hdmap1l6g 42262  hdmap1l6lem1 42253  hdmap1l6lem2 42254  mapdh6N 42193  mapdh6aN 42181  mapdh6eN 42186  mapdh6fN 42187  mapdh6gN 42188  mapdh6lem1N 42179  mapdh6lem2N 42180
[Baer] p. 48Part 9hdmapval 42274
[Baer] p. 48Part 10hdmap10 42286
[Baer] p. 48Part 11hdmapadd 42289
[Baer] p. 48Part (6)hdmap1l6h 42263  mapdh6hN 42189
[Baer] p. 48Part (7)mapdh75cN 42199  mapdh75d 42200  mapdh75e 42198  mapdh75fN 42201  mapdh7cN 42195  mapdh7dN 42196  mapdh7eN 42194  mapdh7fN 42197
[Baer] p. 48Part (8)mapdh8 42234  mapdh8a 42221  mapdh8aa 42222  mapdh8ab 42223  mapdh8ac 42224  mapdh8ad 42225  mapdh8b 42226  mapdh8c 42227  mapdh8d 42229  mapdh8d0N 42228  mapdh8e 42230  mapdh8g 42231  mapdh8i 42232  mapdh8j 42233
[Baer] p. 48Part (9)mapdh9a 42235
[Baer] p. 48Equation 10mapdhvmap 42215
[Baer] p. 49Part 12hdmap11 42294  hdmapeq0 42290  hdmapf1oN 42311  hdmapneg 42292  hdmaprnN 42310  hdmaprnlem1N 42295  hdmaprnlem3N 42296  hdmaprnlem3uN 42297  hdmaprnlem4N 42299  hdmaprnlem6N 42300  hdmaprnlem7N 42301  hdmaprnlem8N 42302  hdmaprnlem9N 42303  hdmapsub 42293
[Baer] p. 49Part 14hdmap14lem1 42314  hdmap14lem10 42323  hdmap14lem1a 42312  hdmap14lem2N 42315  hdmap14lem2a 42313  hdmap14lem3 42316  hdmap14lem8 42321  hdmap14lem9 42322
[Baer] p. 50Part 14hdmap14lem11 42324  hdmap14lem12 42325  hdmap14lem13 42326  hdmap14lem14 42327  hdmap14lem15 42328  hgmapval 42333
[Baer] p. 50Part 15hgmapadd 42340  hgmapmul 42341  hgmaprnlem2N 42343  hgmapvs 42337
[Baer] p. 50Part 16hgmaprnN 42347
[Baer] p. 110Lemma 1hdmapip0com 42363
[Baer] p. 110Line 27hdmapinvlem1 42364
[Baer] p. 110Line 28hdmapinvlem2 42365
[Baer] p. 110Line 30hdmapinvlem3 42366
[Baer] p. 110Part 1.2hdmapglem5 42368  hgmapvv 42372
[Baer] p. 110Proposition 1hdmapinvlem4 42367
[Baer] p. 111Line 10hgmapvvlem1 42369
[Baer] p. 111Line 15hdmapg 42376  hdmapglem7 42375
[Bauer], p. 483Theorem 1.22irrexpq 26695  2irrexpqALT 26764
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2570
[BellMachover] p. 460Notationdf-mo 2540
[BellMachover] p. 460Definitionmo3 2565
[BellMachover] p. 461Axiom Extax-ext 2709
[BellMachover] p. 462Theorem 1.1axextmo 2713
[BellMachover] p. 463Axiom Repaxrep5 5221
[BellMachover] p. 463Scheme Sepax-sep 5232
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37371  sepex 5236
[BellMachover] p. 466Problemaxpow2 5310
[BellMachover] p. 466Axiom Powaxpow3 5311
[BellMachover] p. 466Axiom Unionaxun2 7691
[BellMachover] p. 468Definitiondf-ord 6327
[BellMachover] p. 469Theorem 2.2(i)ordirr 6342
[BellMachover] p. 469Theorem 2.2(iii)onelon 6349
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6344
[BellMachover] p. 471Definition of Ndf-om 7818
[BellMachover] p. 471Problem 2.5(ii)uniordint 7755
[BellMachover] p. 471Definition of Limdf-lim 6329
[BellMachover] p. 472Axiom Infzfinf2 9563
[BellMachover] p. 473Theorem 2.8limom 7833
[BellMachover] p. 477Equation 3.1df-r1 9688
[BellMachover] p. 478Definitionrankval2 9742  rankval2b 35242
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9706  r1ord3g 9703
[BellMachover] p. 480Axiom Regzfreg 9511
[BellMachover] p. 488Axiom ACac5 10399  dfac4 10044
[BellMachover] p. 490Definition of alephalephval3 10032
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39765
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32424
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32466  chirredi 32465
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32454
[Beran] p. 3Definition of joinsshjval3 31425
[Beran] p. 39Theorem 2.3(i)cmcm2 31687  cmcm2i 31664  cmcm2ii 31669  cmt2N 39696
[Beran] p. 40Theorem 2.3(iii)lecm 31688  lecmi 31673  lecmii 31674
[Beran] p. 45Theorem 3.4cmcmlem 31662
[Beran] p. 49Theorem 4.2cm2j 31691  cm2ji 31696  cm2mi 31697
[Beran] p. 95Definitiondf-sh 31278  issh2 31280
[Beran] p. 95Lemma 3.1(S5)his5 31157
[Beran] p. 95Lemma 3.1(S6)his6 31170
[Beran] p. 95Lemma 3.1(S7)his7 31161
[Beran] p. 95Lemma 3.2(S8)ho01i 31899
[Beran] p. 95Lemma 3.2(S9)hoeq1 31901
[Beran] p. 95Lemma 3.2(S10)ho02i 31900
[Beran] p. 95Lemma 3.2(S11)hoeq2 31902
[Beran] p. 95Postulate (S1)ax-his1 31153  his1i 31171
[Beran] p. 95Postulate (S2)ax-his2 31154
[Beran] p. 95Postulate (S3)ax-his3 31155
[Beran] p. 95Postulate (S4)ax-his4 31156
[Beran] p. 96Definition of normdf-hnorm 31039  dfhnorm2 31193  normval 31195
[Beran] p. 96Definition for Cauchy sequencehcau 31255
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31044
[Beran] p. 96Definition of complete subspaceisch3 31312
[Beran] p. 96Definition of convergedf-hlim 31043  hlimi 31259
[Beran] p. 97Theorem 3.3(i)norm-i-i 31204  norm-i 31200
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31208  norm-ii 31209  normlem0 31180  normlem1 31181  normlem2 31182  normlem3 31183  normlem4 31184  normlem5 31185  normlem6 31186  normlem7 31187  normlem7tALT 31190
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31210  norm-iii 31211
[Beran] p. 98Remark 3.4bcs 31252  bcsiALT 31250  bcsiHIL 31251
[Beran] p. 98Remark 3.4(B)normlem9at 31192  normpar 31226  normpari 31225
[Beran] p. 98Remark 3.4(C)normpyc 31217  normpyth 31216  normpythi 31213
[Beran] p. 99Remarklnfn0 32118  lnfn0i 32113  lnop0 32037  lnop0i 32041
[Beran] p. 99Theorem 3.5(i)nmcexi 32097  nmcfnex 32124  nmcfnexi 32122  nmcopex 32100  nmcopexi 32098
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32125  nmcfnlbi 32123  nmcoplb 32101  nmcoplbi 32099
[Beran] p. 99Theorem 3.5(iii)lnfncon 32127  lnfnconi 32126  lnopcon 32106  lnopconi 32105
[Beran] p. 100Lemma 3.6normpar2i 31227
[Beran] p. 101Lemma 3.6norm3adifi 31224  norm3adifii 31219  norm3dif 31221  norm3difi 31218
[Beran] p. 102Theorem 3.7(i)chocunii 31372  pjhth 31464  pjhtheu 31465  pjpjhth 31496  pjpjhthi 31497  pjth 25406
[Beran] p. 102Theorem 3.7(ii)ococ 31477  ococi 31476
[Beran] p. 103Remark 3.8nlelchi 32132
[Beran] p. 104Theorem 3.9riesz3i 32133  riesz4 32135  riesz4i 32134
[Beran] p. 104Theorem 3.10cnlnadj 32150  cnlnadjeu 32149  cnlnadjeui 32148  cnlnadji 32147  cnlnadjlem1 32138  nmopadjlei 32159
[Beran] p. 106Theorem 3.11(i)adjeq0 32162
[Beran] p. 106Theorem 3.11(v)nmopadji 32161
[Beran] p. 106Theorem 3.11(ii)adjmul 32163
[Beran] p. 106Theorem 3.11(iv)adjadj 32007
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32173  nmopcoadji 32172
[Beran] p. 106Theorem 3.11(iii)adjadd 32164
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32174
[Beran] p. 106Theorem 3.11(viii)adjcoi 32171  pjadj2coi 32275  pjadjcoi 32232
[Beran] p. 107Definitiondf-ch 31292  isch2 31294
[Beran] p. 107Remark 3.12choccl 31377  isch3 31312  occl 31375  ocsh 31354  shoccl 31376  shocsh 31355
[Beran] p. 107Remark 3.12(B)ococin 31479
[Beran] p. 108Theorem 3.13chintcl 31403
[Beran] p. 109Property (i)pjadj2 32258  pjadj3 32259  pjadji 31756  pjadjii 31745
[Beran] p. 109Property (ii)pjidmco 32252  pjidmcoi 32248  pjidmi 31744
[Beran] p. 110Definition of projector orderingpjordi 32244
[Beran] p. 111Remarkho0val 31821  pjch1 31741
[Beran] p. 111Definitiondf-hfmul 31805  df-hfsum 31804  df-hodif 31803  df-homul 31802  df-hosum 31801
[Beran] p. 111Lemma 4.4(i)pjo 31742
[Beran] p. 111Lemma 4.4(ii)pjch 31765  pjchi 31503
[Beran] p. 111Lemma 4.4(iii)pjoc2 31510  pjoc2i 31509
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31751
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32236  pjssmii 31752
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32235
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32234
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32239
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32237  pjssge0ii 31753
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32238  pjdifnormii 31754
[Bobzien] p. 116Statement T3stoic3 1778
[Bobzien] p. 117Statement T2stoic2a 1776
[Bobzien] p. 117Statement T4stoic4a 1779
[Bobzien] p. 117Conclusion the contradictorystoic1a 1774
[Bogachev] p. 16Definition 1.5df-oms 34436
[Bogachev] p. 17Lemma 1.5.4omssubadd 34444
[Bogachev] p. 17Example 1.5.2omsmon 34442
[Bogachev] p. 41Definition 1.11.2df-carsg 34446
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34466
[Bogachev] p. 116Definition 2.3.1df-itgm 34497  df-sitm 34475
[Bogachev] p. 118Chapter 2.4.4df-itgm 34497
[Bogachev] p. 118Definition 2.4.1df-sitg 34474
[Bollobas] p. 1Section I.1df-edg 29117  isuhgrop 29139  isusgrop 29231  isuspgrop 29230
[Bollobas] p. 2Section I.1df-isubgr 48331  df-subgr 29337  uhgrspan1 29372  uhgrspansubgr 29360
[Bollobas] p. 3Definitiondf-gric 48351  gricuspgr 48388  isuspgrim 48366
[Bollobas] p. 3Section I.1cusgrsize 29523  df-clnbgr 48289  df-cusgr 29481  df-nbgr 29402  fusgrmaxsize 29533
[Bollobas] p. 4Definitiondf-upwlks 48604  df-wlks 29668
[Bollobas] p. 4Section I.1finsumvtxdg2size 29619  finsumvtxdgeven 29621  fusgr1th 29620  fusgrvtxdgonume 29623  vtxdgoddnumeven 29622
[Bollobas] p. 5Notationdf-pths 29782
[Bollobas] p. 5Definitiondf-crcts 29854  df-cycls 29855  df-trls 29759  df-wlkson 29669
[Bollobas] p. 7Section I.1df-ushgr 29128
[BourbakiAlg1] p. 1Definition 1df-clintop 48670  df-cllaw 48656  df-mgm 18608  df-mgm2 48689
[BourbakiAlg1] p. 4Definition 5df-assintop 48671  df-asslaw 48658  df-sgrp 18687  df-sgrp2 48691
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48690  df-comlaw 48657
[BourbakiAlg1] p. 12Definition 2df-mnd 18703
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33086  mndlactf1o 33090  mndractf1 33088  mndractf1o 33091
[BourbakiAlg1] p. 92Definition 1df-ring 20216
[BourbakiAlg1] p. 93Section I.8.1df-rng 20134
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33777
[BourbakiAlg2] p. 113Chapter 5.assafld 33781  assarrginv 33780
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33822  fldextrspunfld 33820  fldextrspunlem1 33819  fldextrspunlem2 33821  fldextrspunlsp 33818  fldextrspunlsplem 33817
[BourbakiCAlg2], p. 228Proposition 21arithidom 33597  dfufd2 33610
[BourbakiEns] p. Proposition 8fcof1 7242  fcofo 7243
[BourbakiTop1] p. Remarkxnegmnf 13162  xnegpnf 13161
[BourbakiTop1] p. Remark rexneg 13163
[BourbakiTop1] p. Remark 3ust0 24185  ustfilxp 24178
[BourbakiTop1] p. Axiom GT'tgpsubcn 24055
[BourbakiTop1] p. Criterionishmeo 23724
[BourbakiTop1] p. Example 1cstucnd 24248  iducn 24247  snfil 23829
[BourbakiTop1] p. Example 2neifil 23845
[BourbakiTop1] p. Theorem 1cnextcn 24032
[BourbakiTop1] p. Theorem 2ucnextcn 24268
[BourbakiTop1] p. Theorem 3df-hcmp 34101
[BourbakiTop1] p. Paragraph 3infil 23828
[BourbakiTop1] p. Definition 1df-ucn 24240  df-ust 24166  filintn0 23826  filn0 23827  istgp 24042  ucnprima 24246
[BourbakiTop1] p. Definition 2df-cfilu 24251
[BourbakiTop1] p. Definition 3df-cusp 24262  df-usp 24222  df-utop 24196  trust 24194
[BourbakiTop1] p. Definition 6df-pcmp 34000
[BourbakiTop1] p. Property V_issnei2 23081
[BourbakiTop1] p. Theorem 1(d)iscncl 23234
[BourbakiTop1] p. Condition F_Iustssel 24171
[BourbakiTop1] p. Condition U_Iustdiag 24174
[BourbakiTop1] p. Property V_iiinnei 23090
[BourbakiTop1] p. Property V_ivneiptopreu 23098  neissex 23092
[BourbakiTop1] p. Proposition 1neips 23078  neiss 23074  ucncn 24249  ustund 24187  ustuqtop 24211
[BourbakiTop1] p. Proposition 2cnpco 23232  neiptopreu 23098  utop2nei 24215  utop3cls 24216
[BourbakiTop1] p. Proposition 3fmucnd 24256  uspreg 24238  utopreg 24217
[BourbakiTop1] p. Proposition 4imasncld 23656  imasncls 23657  imasnopn 23655
[BourbakiTop1] p. Proposition 9cnpflf2 23965
[BourbakiTop1] p. Condition F_IIustincl 24173
[BourbakiTop1] p. Condition U_IIustinvel 24175
[BourbakiTop1] p. Property V_iiielnei 23076
[BourbakiTop1] p. Proposition 11cnextucn 24267
[BourbakiTop1] p. Condition F_IIbustbasel 24172
[BourbakiTop1] p. Condition U_IIIustexhalf 24176
[BourbakiTop1] p. Definition C'''df-cmp 23352
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23811
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22859
[BourbakiTop2] p. 195Definition 1df-ldlf 33997
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46490
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46492  stoweid 46491
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46429  stoweidlem10 46438  stoweidlem14 46442  stoweidlem15 46443  stoweidlem35 46463  stoweidlem36 46464  stoweidlem37 46465  stoweidlem38 46466  stoweidlem40 46468  stoweidlem41 46469  stoweidlem43 46471  stoweidlem44 46472  stoweidlem46 46474  stoweidlem5 46433  stoweidlem50 46478  stoweidlem52 46480  stoweidlem53 46481  stoweidlem55 46483  stoweidlem56 46484
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46451  stoweidlem24 46452  stoweidlem27 46455  stoweidlem28 46456  stoweidlem30 46458
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46462  stoweidlem59 46487  stoweidlem60 46488
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46473  stoweidlem49 46477  stoweidlem7 46435
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46459  stoweidlem39 46467  stoweidlem42 46470  stoweidlem48 46476  stoweidlem51 46479  stoweidlem54 46482  stoweidlem57 46485  stoweidlem58 46486
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46453
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46445
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46439  stoweidlem13 46441  stoweidlem26 46454  stoweidlem61 46489
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46446
[Bruck] p. 1Section I.1df-clintop 48670  df-mgm 18608  df-mgm2 48689
[Bruck] p. 23Section II.1df-sgrp 18687  df-sgrp2 48691
[Bruck] p. 28Theorem 3.2dfgrp3 19015
[ChoquetDD] p. 2Definition of mappingdf-mpt 5168
[Church] p. 129Section II.24df-ifp 1064  dfifp2 1065
[Clemente] p. 10Definition ITnatded 30473
[Clemente] p. 10Definition I` `m,nnatded 30473
[Clemente] p. 11Definition E=>m,nnatded 30473
[Clemente] p. 11Definition I=>m,nnatded 30473
[Clemente] p. 11Definition E` `(1)natded 30473
[Clemente] p. 11Definition E` `(2)natded 30473
[Clemente] p. 12Definition E` `m,n,pnatded 30473
[Clemente] p. 12Definition I` `n(1)natded 30473
[Clemente] p. 12Definition I` `n(2)natded 30473
[Clemente] p. 13Definition I` `m,n,pnatded 30473
[Clemente] p. 14Proof 5.11natded 30473
[Clemente] p. 14Definition E` `nnatded 30473
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30475  ex-natded5.2 30474
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30478  ex-natded5.3 30477
[Clemente] p. 18Theorem 5.5ex-natded5.5 30480
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30482  ex-natded5.7 30481
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30484  ex-natded5.8 30483
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30486  ex-natded5.13 30485
[Clemente] p. 32Definition I` `nnatded 30473
[Clemente] p. 32Definition E` `m,n,p,anatded 30473
[Clemente] p. 32Definition E` `n,tnatded 30473
[Clemente] p. 32Definition I` `n,tnatded 30473
[Clemente] p. 43Theorem 9.20ex-natded9.20 30487
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30488
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30490  ex-natded9.26 30489
[Cohen] p. 301Remarkrelogoprlem 26555
[Cohen] p. 301Property 2relogmul 26556  relogmuld 26589
[Cohen] p. 301Property 3relogdiv 26557  relogdivd 26590
[Cohen] p. 301Property 4relogexp 26560
[Cohen] p. 301Property 1alog1 26549
[Cohen] p. 301Property 1bloge 26550
[Cohen4] p. 348Observationrelogbcxpb 26751
[Cohen4] p. 349Propertyrelogbf 26755
[Cohen4] p. 352Definitionelogb 26734
[Cohen4] p. 361Property 2relogbmul 26741
[Cohen4] p. 361Property 3logbrec 26746  relogbdiv 26743
[Cohen4] p. 361Property 4relogbreexp 26739
[Cohen4] p. 361Property 6relogbexp 26744
[Cohen4] p. 361Property 1(a)logbid1 26732
[Cohen4] p. 361Property 1(b)logb1 26733
[Cohen4] p. 367Propertylogbchbase 26735
[Cohen4] p. 377Property 2logblt 26748
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34429  sxbrsigalem4 34431
[Cohn] p. 81Section II.5acsdomd 18523  acsinfd 18522  acsinfdimd 18524  acsmap2d 18521  acsmapd 18520
[Cohn] p. 143Example 5.1.1sxbrsiga 34434
[Connell] p. 57Definitiondf-scmat 22456  df-scmatalt 48869
[Conway] p. 4Definitionlesrec 27791  lesrecd 27792
[Conway] p. 5Definitionaddsval 27954  addsval2 27955  df-adds 27952  df-muls 28099  df-negs 28013
[Conway] p. 7Theorem0lt1s 27804
[Conway] p. 12Theorem 12pw2cut2 28454
[Conway] p. 16Theorem 0(i)sltsright 27853
[Conway] p. 16Theorem 0(ii)sltsleft 27852
[Conway] p. 16Theorem 0(iii)lesid 27731
[Conway] p. 17Theorem 3addsass 27997  addsassd 27998  addscom 27958  addscomd 27959  addsrid 27956  addsridd 27957
[Conway] p. 17Definitiondf-0s 27799
[Conway] p. 17Theorem 4(ii)negnegs 28036
[Conway] p. 17Theorem 4(iii)negsid 28033  negsidd 28034
[Conway] p. 18Theorem 5leadds1 27981  leadds1d 27987
[Conway] p. 18Definitiondf-1s 27800
[Conway] p. 18Theorem 6(ii)negscl 28028  negscld 28029
[Conway] p. 18Theorem 6(iii)addscld 27972
[Conway] p. 19Notemulsunif2 28162
[Conway] p. 19Theorem 7addsdi 28147  addsdid 28148  addsdird 28149  mulnegs1d 28152  mulnegs2d 28153  mulsass 28158  mulsassd 28159  mulscom 28131  mulscomd 28132
[Conway] p. 19Theorem 8(i)mulscl 28126  mulscld 28127
[Conway] p. 19Theorem 8(iii)lemulsd 28130  ltmuls 28128  ltmulsd 28129
[Conway] p. 20Theorem 9mulsgt0 28136  mulsgt0d 28137
[Conway] p. 21Theorem 10(iv)precsex 28210
[Conway] p. 23Theorem 11eqcuts3 27796
[Conway] p. 24Definitiondf-reno 28482
[Conway] p. 24Theorem 13(ii)readdscl 28491  remulscl 28494  renegscl 28490
[Conway] p. 27Definitiondf-ons 28244  elons2 28250
[Conway] p. 27Theorem 14ltonsex 28254
[Conway] p. 28Theorem 15oncutlt 28256  onswe 28264
[Conway] p. 29Remarkmadebday 27892  newbday 27894  oldbday 27893
[Conway] p. 29Definitiondf-made 27819  df-new 27821  df-old 27820
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13820
[Crawley] p. 1Definition of posetdf-poset 18279
[Crawley] p. 107Theorem 13.2hlsupr 39832
[Crawley] p. 110Theorem 13.3arglem1N 40636  dalaw 40332
[Crawley] p. 111Theorem 13.4hlathil 42407
[Crawley] p. 111Definition of set Wdf-watsN 40436
[Crawley] p. 111Definition of dilationdf-dilN 40552  df-ldil 40550  isldil 40556
[Crawley] p. 111Definition of translationdf-ltrn 40551  df-trnN 40553  isltrn 40565  ltrnu 40567
[Crawley] p. 112Lemma Acdlema1N 40237  cdlema2N 40238  exatleN 39850
[Crawley] p. 112Lemma B1cvrat 39922  cdlemb 40240  cdlemb2 40487  cdlemb3 41052  idltrn 40596  l1cvat 39501  lhpat 40489  lhpat2 40491  lshpat 39502  ltrnel 40585  ltrnmw 40597
[Crawley] p. 112Lemma Ccdlemc1 40637  cdlemc2 40638  ltrnnidn 40620  trlat 40615  trljat1 40612  trljat2 40613  trljat3 40614  trlne 40631  trlnidat 40619  trlnle 40632
[Crawley] p. 112Definition of automorphismdf-pautN 40437
[Crawley] p. 113Lemma Ccdlemc 40643  cdlemc3 40639  cdlemc4 40640
[Crawley] p. 113Lemma Dcdlemd 40653  cdlemd1 40644  cdlemd2 40645  cdlemd3 40646  cdlemd4 40647  cdlemd5 40648  cdlemd6 40649  cdlemd7 40650  cdlemd8 40651  cdlemd9 40652  cdleme31sde 40831  cdleme31se 40828  cdleme31se2 40829  cdleme31snd 40832  cdleme32a 40887  cdleme32b 40888  cdleme32c 40889  cdleme32d 40890  cdleme32e 40891  cdleme32f 40892  cdleme32fva 40883  cdleme32fva1 40884  cdleme32fvcl 40886  cdleme32le 40893  cdleme48fv 40945  cdleme4gfv 40953  cdleme50eq 40987  cdleme50f 40988  cdleme50f1 40989  cdleme50f1o 40992  cdleme50laut 40993  cdleme50ldil 40994  cdleme50lebi 40986  cdleme50rn 40991  cdleme50rnlem 40990  cdlemeg49le 40957  cdlemeg49lebilem 40985
[Crawley] p. 113Lemma Ecdleme 41006  cdleme00a 40655  cdleme01N 40667  cdleme02N 40668  cdleme0a 40657  cdleme0aa 40656  cdleme0b 40658  cdleme0c 40659  cdleme0cp 40660  cdleme0cq 40661  cdleme0dN 40662  cdleme0e 40663  cdleme0ex1N 40669  cdleme0ex2N 40670  cdleme0fN 40664  cdleme0gN 40665  cdleme0moN 40671  cdleme1 40673  cdleme10 40700  cdleme10tN 40704  cdleme11 40716  cdleme11a 40706  cdleme11c 40707  cdleme11dN 40708  cdleme11e 40709  cdleme11fN 40710  cdleme11g 40711  cdleme11h 40712  cdleme11j 40713  cdleme11k 40714  cdleme11l 40715  cdleme12 40717  cdleme13 40718  cdleme14 40719  cdleme15 40724  cdleme15a 40720  cdleme15b 40721  cdleme15c 40722  cdleme15d 40723  cdleme16 40731  cdleme16aN 40705  cdleme16b 40725  cdleme16c 40726  cdleme16d 40727  cdleme16e 40728  cdleme16f 40729  cdleme16g 40730  cdleme19a 40749  cdleme19b 40750  cdleme19c 40751  cdleme19d 40752  cdleme19e 40753  cdleme19f 40754  cdleme1b 40672  cdleme2 40674  cdleme20aN 40755  cdleme20bN 40756  cdleme20c 40757  cdleme20d 40758  cdleme20e 40759  cdleme20f 40760  cdleme20g 40761  cdleme20h 40762  cdleme20i 40763  cdleme20j 40764  cdleme20k 40765  cdleme20l 40768  cdleme20l1 40766  cdleme20l2 40767  cdleme20m 40769  cdleme20y 40748  cdleme20zN 40747  cdleme21 40783  cdleme21d 40776  cdleme21e 40777  cdleme22a 40786  cdleme22aa 40785  cdleme22b 40787  cdleme22cN 40788  cdleme22d 40789  cdleme22e 40790  cdleme22eALTN 40791  cdleme22f 40792  cdleme22f2 40793  cdleme22g 40794  cdleme23a 40795  cdleme23b 40796  cdleme23c 40797  cdleme26e 40805  cdleme26eALTN 40807  cdleme26ee 40806  cdleme26f 40809  cdleme26f2 40811  cdleme26f2ALTN 40810  cdleme26fALTN 40808  cdleme27N 40815  cdleme27a 40813  cdleme27cl 40812  cdleme28c 40818  cdleme3 40683  cdleme30a 40824  cdleme31fv 40836  cdleme31fv1 40837  cdleme31fv1s 40838  cdleme31fv2 40839  cdleme31id 40840  cdleme31sc 40830  cdleme31sdnN 40833  cdleme31sn 40826  cdleme31sn1 40827  cdleme31sn1c 40834  cdleme31sn2 40835  cdleme31so 40825  cdleme35a 40894  cdleme35b 40896  cdleme35c 40897  cdleme35d 40898  cdleme35e 40899  cdleme35f 40900  cdleme35fnpq 40895  cdleme35g 40901  cdleme35h 40902  cdleme35h2 40903  cdleme35sn2aw 40904  cdleme35sn3a 40905  cdleme36a 40906  cdleme36m 40907  cdleme37m 40908  cdleme38m 40909  cdleme38n 40910  cdleme39a 40911  cdleme39n 40912  cdleme3b 40675  cdleme3c 40676  cdleme3d 40677  cdleme3e 40678  cdleme3fN 40679  cdleme3fa 40682  cdleme3g 40680  cdleme3h 40681  cdleme4 40684  cdleme40m 40913  cdleme40n 40914  cdleme40v 40915  cdleme40w 40916  cdleme41fva11 40923  cdleme41sn3aw 40920  cdleme41sn4aw 40921  cdleme41snaw 40922  cdleme42a 40917  cdleme42b 40924  cdleme42c 40918  cdleme42d 40919  cdleme42e 40925  cdleme42f 40926  cdleme42g 40927  cdleme42h 40928  cdleme42i 40929  cdleme42k 40930  cdleme42ke 40931  cdleme42keg 40932  cdleme42mN 40933  cdleme42mgN 40934  cdleme43aN 40935  cdleme43bN 40936  cdleme43cN 40937  cdleme43dN 40938  cdleme5 40686  cdleme50ex 41005  cdleme50ltrn 41003  cdleme51finvN 41002  cdleme51finvfvN 41001  cdleme51finvtrN 41004  cdleme6 40687  cdleme7 40695  cdleme7a 40689  cdleme7aa 40688  cdleme7b 40690  cdleme7c 40691  cdleme7d 40692  cdleme7e 40693  cdleme7ga 40694  cdleme8 40696  cdleme8tN 40701  cdleme9 40699  cdleme9a 40697  cdleme9b 40698  cdleme9tN 40703  cdleme9taN 40702  cdlemeda 40744  cdlemedb 40743  cdlemednpq 40745  cdlemednuN 40746  cdlemefr27cl 40849  cdlemefr32fva1 40856  cdlemefr32fvaN 40855  cdlemefrs32fva 40846  cdlemefrs32fva1 40847  cdlemefs27cl 40859  cdlemefs32fva1 40869  cdlemefs32fvaN 40868  cdlemesner 40742  cdlemeulpq 40666
[Crawley] p. 114Lemma E4atex 40522  4atexlem7 40521  cdleme0nex 40736  cdleme17a 40732  cdleme17c 40734  cdleme17d 40944  cdleme17d1 40735  cdleme17d2 40941  cdleme18a 40737  cdleme18b 40738  cdleme18c 40739  cdleme18d 40741  cdleme4a 40685
[Crawley] p. 115Lemma Ecdleme21a 40771  cdleme21at 40774  cdleme21b 40772  cdleme21c 40773  cdleme21ct 40775  cdleme21f 40778  cdleme21g 40779  cdleme21h 40780  cdleme21i 40781  cdleme22gb 40740
[Crawley] p. 116Lemma Fcdlemf 41009  cdlemf1 41007  cdlemf2 41008
[Crawley] p. 116Lemma Gcdlemftr1 41013  cdlemg16 41103  cdlemg28 41150  cdlemg28a 41139  cdlemg28b 41149  cdlemg3a 41043  cdlemg42 41175  cdlemg43 41176  cdlemg44 41179  cdlemg44a 41177  cdlemg46 41181  cdlemg47 41182  cdlemg9 41080  ltrnco 41165  ltrncom 41184  tgrpabl 41197  trlco 41173
[Crawley] p. 116Definition of Gdf-tgrp 41189
[Crawley] p. 117Lemma Gcdlemg17 41123  cdlemg17b 41108
[Crawley] p. 117Definition of Edf-edring-rN 41202  df-edring 41203
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41206
[Crawley] p. 118Remarktendopltp 41226
[Crawley] p. 118Lemma Hcdlemh 41263  cdlemh1 41261  cdlemh2 41262
[Crawley] p. 118Lemma Icdlemi 41266  cdlemi1 41264  cdlemi2 41265
[Crawley] p. 118Lemma Jcdlemj1 41267  cdlemj2 41268  cdlemj3 41269  tendocan 41270
[Crawley] p. 118Lemma Kcdlemk 41420  cdlemk1 41277  cdlemk10 41289  cdlemk11 41295  cdlemk11t 41392  cdlemk11ta 41375  cdlemk11tb 41377  cdlemk11tc 41391  cdlemk11u-2N 41335  cdlemk11u 41317  cdlemk12 41296  cdlemk12u-2N 41336  cdlemk12u 41318  cdlemk13-2N 41322  cdlemk13 41298  cdlemk14-2N 41324  cdlemk14 41300  cdlemk15-2N 41325  cdlemk15 41301  cdlemk16-2N 41326  cdlemk16 41303  cdlemk16a 41302  cdlemk17-2N 41327  cdlemk17 41304  cdlemk18-2N 41332  cdlemk18-3N 41346  cdlemk18 41314  cdlemk19-2N 41333  cdlemk19 41315  cdlemk19u 41416  cdlemk1u 41305  cdlemk2 41278  cdlemk20-2N 41338  cdlemk20 41320  cdlemk21-2N 41337  cdlemk21N 41319  cdlemk22-3 41347  cdlemk22 41339  cdlemk23-3 41348  cdlemk24-3 41349  cdlemk25-3 41350  cdlemk26-3 41352  cdlemk26b-3 41351  cdlemk27-3 41353  cdlemk28-3 41354  cdlemk29-3 41357  cdlemk3 41279  cdlemk30 41340  cdlemk31 41342  cdlemk32 41343  cdlemk33N 41355  cdlemk34 41356  cdlemk35 41358  cdlemk36 41359  cdlemk37 41360  cdlemk38 41361  cdlemk39 41362  cdlemk39u 41414  cdlemk4 41280  cdlemk41 41366  cdlemk42 41387  cdlemk42yN 41390  cdlemk43N 41409  cdlemk45 41393  cdlemk46 41394  cdlemk47 41395  cdlemk48 41396  cdlemk49 41397  cdlemk5 41282  cdlemk50 41398  cdlemk51 41399  cdlemk52 41400  cdlemk53 41403  cdlemk54 41404  cdlemk55 41407  cdlemk55u 41412  cdlemk56 41417  cdlemk5a 41281  cdlemk5auN 41306  cdlemk5u 41307  cdlemk6 41283  cdlemk6u 41308  cdlemk7 41294  cdlemk7u-2N 41334  cdlemk7u 41316  cdlemk8 41284  cdlemk9 41285  cdlemk9bN 41286  cdlemki 41287  cdlemkid 41382  cdlemkj-2N 41328  cdlemkj 41309  cdlemksat 41292  cdlemksel 41291  cdlemksv 41290  cdlemksv2 41293  cdlemkuat 41312  cdlemkuel-2N 41330  cdlemkuel-3 41344  cdlemkuel 41311  cdlemkuv-2N 41329  cdlemkuv2-2 41331  cdlemkuv2-3N 41345  cdlemkuv2 41313  cdlemkuvN 41310  cdlemkvcl 41288  cdlemky 41372  cdlemkyyN 41408  tendoex 41421
[Crawley] p. 120Remarkdva1dim 41431
[Crawley] p. 120Lemma Lcdleml1N 41422  cdleml2N 41423  cdleml3N 41424  cdleml4N 41425  cdleml5N 41426  cdleml6 41427  cdleml7 41428  cdleml8 41429  cdleml9 41430  dia1dim 41507
[Crawley] p. 120Lemma Mdia11N 41494  diaf11N 41495  dialss 41492  diaord 41493  dibf11N 41607  djajN 41583
[Crawley] p. 120Definition of isomorphism mapdiaval 41478
[Crawley] p. 121Lemma Mcdlemm10N 41564  dia2dimlem1 41510  dia2dimlem2 41511  dia2dimlem3 41512  dia2dimlem4 41513  dia2dimlem5 41514  diaf1oN 41576  diarnN 41575  dvheveccl 41558  dvhopN 41562
[Crawley] p. 121Lemma Ncdlemn 41658  cdlemn10 41652  cdlemn11 41657  cdlemn11a 41653  cdlemn11b 41654  cdlemn11c 41655  cdlemn11pre 41656  cdlemn2 41641  cdlemn2a 41642  cdlemn3 41643  cdlemn4 41644  cdlemn4a 41645  cdlemn5 41647  cdlemn5pre 41646  cdlemn6 41648  cdlemn7 41649  cdlemn8 41650  cdlemn9 41651  diclspsn 41640
[Crawley] p. 121Definition of phi(q)df-dic 41619
[Crawley] p. 122Lemma Ndih11 41711  dihf11 41713  dihjust 41663  dihjustlem 41662  dihord 41710  dihord1 41664  dihord10 41669  dihord11b 41668  dihord11c 41670  dihord2 41673  dihord2a 41665  dihord2b 41666  dihord2cN 41667  dihord2pre 41671  dihord2pre2 41672  dihordlem6 41659  dihordlem7 41660  dihordlem7b 41661
[Crawley] p. 122Definition of isomorphism mapdihffval 41676  dihfval 41677  dihval 41678
[Diestel] p. 3Definitiondf-gric 48351  df-grim 48348  isuspgrim 48366
[Diestel] p. 3Section 1.1df-cusgr 29481  df-nbgr 29402
[Diestel] p. 3Definition by df-grisom 48347
[Diestel] p. 4Section 1.1df-isubgr 48331  df-subgr 29337  uhgrspan1 29372  uhgrspansubgr 29360
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29623  vtxdgoddnumeven 29622
[Diestel] p. 27Section 1.10df-ushgr 29128
[EGA] p. 80Notation 1.1.1rspecval 34008
[EGA] p. 80Proposition 1.1.2zartop 34020
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34012  zarcls1 34013
[EGA] p. 81Corollary 1.1.8zart0 34023
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34026
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34029
[Eisenberg] p. 67Definition 5.3df-dif 3893
[Eisenberg] p. 82Definition 6.3dfom3 9568
[Eisenberg] p. 125Definition 8.21df-map 8775
[Eisenberg] p. 216Example 13.2(4)omenps 9576
[Eisenberg] p. 310Theorem 19.8cardprc 9904
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10477
[Enderton] p. 18Axiom of Empty Setaxnul 5241
[Enderton] p. 19Definitiondf-tp 4573
[Enderton] p. 26Exercise 5unissb 4884
[Enderton] p. 26Exercise 10pwel 5324
[Enderton] p. 28Exercise 7(b)pwun 5524
[Enderton] p. 30Theorem "Distributive laws"iinin1 5022  iinin2 5021  iinun2 5016  iunin1 5015  iunin1f 32627  iunin2 5014  uniin1 32621  uniin2 32622
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5020  iundif2 5017
[Enderton] p. 32Exercise 20unineq 4229
[Enderton] p. 33Exercise 23iinuni 5041
[Enderton] p. 33Exercise 25iununi 5042
[Enderton] p. 33Exercise 24(a)iinpw 5049
[Enderton] p. 33Exercise 24(b)iunpw 7725  iunpwss 5050
[Enderton] p. 36Definitionopthwiener 5469
[Enderton] p. 38Exercise 6(a)unipw 5403
[Enderton] p. 38Exercise 6(b)pwuni 4889
[Enderton] p. 41Lemma 3Dopeluu 5424  rnex 7861  rnexg 7853
[Enderton] p. 41Exercise 8dmuni 5870  rnuni 6113
[Enderton] p. 42Definition of a functiondffun7 6526  dffun8 6527
[Enderton] p. 43Definition of function valuefunfv2 6929
[Enderton] p. 43Definition of single-rootedfuncnv 6568
[Enderton] p. 44Definition (d)dfima2 6028  dfima3 6029
[Enderton] p. 47Theorem 3Hfvco2 6938
[Enderton] p. 49Axiom of Choice (first form)ac7 10395  ac7g 10396  df-ac 10038  dfac2 10054  dfac2a 10052  dfac2b 10053  dfac3 10043  dfac7 10055
[Enderton] p. 50Theorem 3K(a)imauni 7201
[Enderton] p. 52Definitiondf-map 8775
[Enderton] p. 53Exercise 21coass 6231
[Enderton] p. 53Exercise 27dmco 6220
[Enderton] p. 53Exercise 14(a)funin 6575
[Enderton] p. 53Exercise 22(a)imass2 6068
[Enderton] p. 54Remarkixpf 8868  ixpssmap 8880
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8846
[Enderton] p. 55Axiom of Choice (second form)ac9 10405  ac9s 10415
[Enderton] p. 56Theorem 3Meqvrelref 39015  erref 8664
[Enderton] p. 57Lemma 3Neqvrelthi 39018  erthi 8700
[Enderton] p. 57Definitiondf-ec 8645
[Enderton] p. 58Definitiondf-qs 8649
[Enderton] p. 61Exercise 35df-ec 8645
[Enderton] p. 65Exercise 56(a)dmun 5866
[Enderton] p. 68Definition of successordf-suc 6330
[Enderton] p. 71Definitiondf-tr 5194  dftr4 5199
[Enderton] p. 72Theorem 4Eunisuc 6405  unisucg 6404
[Enderton] p. 73Exercise 6unisuc 6405  unisucg 6404
[Enderton] p. 73Exercise 5(a)truni 5209
[Enderton] p. 73Exercise 5(b)trint 5211  trintALT 45307
[Enderton] p. 79Theorem 4I(A1)nna0 8540
[Enderton] p. 79Theorem 4I(A2)nnasuc 8542  onasuc 8463
[Enderton] p. 79Definition of operation valuedf-ov 7370
[Enderton] p. 80Theorem 4J(A1)nnm0 8541
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8543  onmsuc 8464
[Enderton] p. 81Theorem 4K(1)nnaass 8558
[Enderton] p. 81Theorem 4K(2)nna0r 8545  nnacom 8553
[Enderton] p. 81Theorem 4K(3)nndi 8559
[Enderton] p. 81Theorem 4K(4)nnmass 8560
[Enderton] p. 81Theorem 4K(5)nnmcom 8562
[Enderton] p. 82Exercise 16nnm0r 8546  nnmsucr 8561
[Enderton] p. 88Exercise 23nnaordex 8574
[Enderton] p. 129Definitiondf-en 8894
[Enderton] p. 132Theorem 6B(b)canth 7321
[Enderton] p. 133Exercise 1xpomen 9937
[Enderton] p. 133Exercise 2qnnen 16180
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9141
[Enderton] p. 135Corollary 6Cphp3 9143
[Enderton] p. 136Corollary 6Enneneq 9140
[Enderton] p. 136Corollary 6D(a)pssinf 9172
[Enderton] p. 136Corollary 6D(b)ominf 9174
[Enderton] p. 137Lemma 6Fpssnn 9103
[Enderton] p. 138Corollary 6Gssfi 9107
[Enderton] p. 139Theorem 6H(c)mapen 9079
[Enderton] p. 142Theorem 6I(3)xpdjuen 10102
[Enderton] p. 142Theorem 6I(4)mapdjuen 10103
[Enderton] p. 143Theorem 6Jdju0en 10098  dju1en 10094
[Enderton] p. 144Exercise 13iunfi 9253  unifi 9254  unifi2 9255
[Enderton] p. 144Corollary 6Kundif2 4418  unfi 9105  unfi2 9220
[Enderton] p. 145Figure 38ffoss 7899
[Enderton] p. 145Definitiondf-dom 8895
[Enderton] p. 146Example 1domen 8908  domeng 8909
[Enderton] p. 146Example 3nndomo 9152  nnsdom 9575  nnsdomg 9209
[Enderton] p. 149Theorem 6L(a)djudom2 10106
[Enderton] p. 149Theorem 6L(c)mapdom1 9080  xpdom1 9014  xpdom1g 9012  xpdom2g 9011
[Enderton] p. 149Theorem 6L(d)mapdom2 9086
[Enderton] p. 151Theorem 6Mzorn 10429  zorng 10426
[Enderton] p. 151Theorem 6M(4)ac8 10414  dfac5 10051
[Enderton] p. 159Theorem 6Qunictb 10498
[Enderton] p. 164Exampleinfdif 10130
[Enderton] p. 168Definitiondf-po 5539
[Enderton] p. 192Theorem 7M(a)oneli 6439
[Enderton] p. 192Theorem 7M(b)ontr1 6371
[Enderton] p. 192Theorem 7M(c)onirri 6438
[Enderton] p. 193Corollary 7N(b)0elon 6379
[Enderton] p. 193Corollary 7N(c)onsuci 7790
[Enderton] p. 193Corollary 7N(d)ssonunii 7735
[Enderton] p. 194Remarkonprc 7732
[Enderton] p. 194Exercise 16suc11 6433
[Enderton] p. 197Definitiondf-card 9863
[Enderton] p. 197Theorem 7Pcarden 10473
[Enderton] p. 200Exercise 25tfis 7806
[Enderton] p. 202Lemma 7Tr1tr 9700
[Enderton] p. 202Definitiondf-r1 9688
[Enderton] p. 202Theorem 7Qr1val1 9710
[Enderton] p. 204Theorem 7V(b)rankval4 9791  rankval4b 35243
[Enderton] p. 206Theorem 7X(b)en2lp 9527
[Enderton] p. 207Exercise 30rankpr 9781  rankprb 9775  rankpw 9767  rankpwi 9747  rankuniss 9790
[Enderton] p. 207Exercise 34opthreg 9539
[Enderton] p. 208Exercise 35suc11reg 9540
[Enderton] p. 212Definition of alephalephval3 10032
[Enderton] p. 213Theorem 8A(a)alephord2 9998
[Enderton] p. 213Theorem 8A(b)cardalephex 10012
[Enderton] p. 218Theorem Schema 8Eonfununi 8281
[Enderton] p. 222Definition of kardkarden 9819  kardex 9818
[Enderton] p. 238Theorem 8Roeoa 8533
[Enderton] p. 238Theorem 8Soeoe 8535
[Enderton] p. 240Exercise 25oarec 8497
[Enderton] p. 257Definition of cofinalitycflm 10172
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17608
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17550
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18519  mrieqv2d 17605  mrieqvd 17604
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17609
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17614  mreexexlem2d 17611
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18525  mreexfidimd 17616
[Frege1879] p. 11Statementdf3or2 44195
[Frege1879] p. 12Statementdf3an2 44196  dfxor4 44193  dfxor5 44194
[Frege1879] p. 26Axiom 1ax-frege1 44217
[Frege1879] p. 26Axiom 2ax-frege2 44218
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44222
[Frege1879] p. 31Proposition 4frege4 44226
[Frege1879] p. 32Proposition 5frege5 44227
[Frege1879] p. 33Proposition 6frege6 44233
[Frege1879] p. 34Proposition 7frege7 44235
[Frege1879] p. 35Axiom 8ax-frege8 44236  axfrege8 44234
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37761
[Frege1879] p. 35Proposition 9frege9 44239
[Frege1879] p. 36Proposition 10frege10 44247
[Frege1879] p. 36Proposition 11frege11 44241
[Frege1879] p. 37Proposition 12frege12 44240
[Frege1879] p. 37Proposition 13frege13 44249
[Frege1879] p. 37Proposition 14frege14 44250
[Frege1879] p. 38Proposition 15frege15 44253
[Frege1879] p. 38Proposition 16frege16 44243
[Frege1879] p. 39Proposition 17frege17 44248
[Frege1879] p. 39Proposition 18frege18 44245
[Frege1879] p. 39Proposition 19frege19 44251
[Frege1879] p. 40Proposition 20frege20 44255
[Frege1879] p. 40Proposition 21frege21 44254
[Frege1879] p. 41Proposition 22frege22 44246
[Frege1879] p. 42Proposition 23frege23 44252
[Frege1879] p. 42Proposition 24frege24 44242
[Frege1879] p. 42Proposition 25frege25 44244  rp-frege25 44232
[Frege1879] p. 42Proposition 26frege26 44237
[Frege1879] p. 43Axiom 28ax-frege28 44257
[Frege1879] p. 43Proposition 27frege27 44238
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 44258
[Frege1879] p. 44Axiom 31ax-frege31 44261  axfrege31 44260
[Frege1879] p. 44Proposition 30frege30 44259
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 44262
[Frege1879] p. 44Proposition 33frege33 44263
[Frege1879] p. 45Proposition 34frege34 44264
[Frege1879] p. 45Proposition 35frege35 44265
[Frege1879] p. 45Proposition 36frege36 44266
[Frege1879] p. 46Proposition 37frege37 44267
[Frege1879] p. 46Proposition 38frege38 44268
[Frege1879] p. 46Proposition 39frege39 44269
[Frege1879] p. 46Proposition 40frege40 44270
[Frege1879] p. 47Axiom 41ax-frege41 44272  axfrege41 44271
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 44273
[Frege1879] p. 47Proposition 43frege43 44274
[Frege1879] p. 47Proposition 44frege44 44275
[Frege1879] p. 47Proposition 45frege45 44276
[Frege1879] p. 48Proposition 46frege46 44277
[Frege1879] p. 48Proposition 47frege47 44278
[Frege1879] p. 49Proposition 48frege48 44279
[Frege1879] p. 49Proposition 49frege49 44280
[Frege1879] p. 49Proposition 50frege50 44281
[Frege1879] p. 50Axiom 52ax-frege52a 44284  ax-frege52c 44315  frege52aid 44285  frege52b 44316
[Frege1879] p. 50Axiom 54ax-frege54a 44289  ax-frege54c 44319  frege54b 44320
[Frege1879] p. 50Proposition 51frege51 44282
[Frege1879] p. 50Proposition 52dfsbcq 3731
[Frege1879] p. 50Proposition 53frege53a 44287  frege53aid 44286  frege53b 44317  frege53c 44341
[Frege1879] p. 50Proposition 54biid 261  eqid 2737
[Frege1879] p. 50Proposition 55frege55a 44295  frege55aid 44292  frege55b 44324  frege55c 44345  frege55cor1a 44296  frege55lem2a 44294  frege55lem2b 44323  frege55lem2c 44344
[Frege1879] p. 50Proposition 56frege56a 44298  frege56aid 44297  frege56b 44325  frege56c 44346
[Frege1879] p. 51Axiom 58ax-frege58a 44302  ax-frege58b 44328  frege58bid 44329  frege58c 44348
[Frege1879] p. 51Proposition 57frege57a 44300  frege57aid 44299  frege57b 44326  frege57c 44347
[Frege1879] p. 51Proposition 58spsbc 3742
[Frege1879] p. 51Proposition 59frege59a 44304  frege59b 44331  frege59c 44349
[Frege1879] p. 52Proposition 60frege60a 44305  frege60b 44332  frege60c 44350
[Frege1879] p. 52Proposition 61frege61a 44306  frege61b 44333  frege61c 44351
[Frege1879] p. 52Proposition 62frege62a 44307  frege62b 44334  frege62c 44352
[Frege1879] p. 52Proposition 63frege63a 44308  frege63b 44335  frege63c 44353
[Frege1879] p. 53Proposition 64frege64a 44309  frege64b 44336  frege64c 44354
[Frege1879] p. 53Proposition 65frege65a 44310  frege65b 44337  frege65c 44355
[Frege1879] p. 54Proposition 66frege66a 44311  frege66b 44338  frege66c 44356
[Frege1879] p. 54Proposition 67frege67a 44312  frege67b 44339  frege67c 44357
[Frege1879] p. 54Proposition 68frege68a 44313  frege68b 44340  frege68c 44358
[Frege1879] p. 55Definition 69dffrege69 44359
[Frege1879] p. 58Proposition 70frege70 44360
[Frege1879] p. 59Proposition 71frege71 44361
[Frege1879] p. 59Proposition 72frege72 44362
[Frege1879] p. 59Proposition 73frege73 44363
[Frege1879] p. 60Definition 76dffrege76 44366
[Frege1879] p. 60Proposition 74frege74 44364
[Frege1879] p. 60Proposition 75frege75 44365
[Frege1879] p. 62Proposition 77frege77 44367  frege77d 44173
[Frege1879] p. 63Proposition 78frege78 44368
[Frege1879] p. 63Proposition 79frege79 44369
[Frege1879] p. 63Proposition 80frege80 44370
[Frege1879] p. 63Proposition 81frege81 44371  frege81d 44174
[Frege1879] p. 64Proposition 82frege82 44372
[Frege1879] p. 65Proposition 83frege83 44373  frege83d 44175
[Frege1879] p. 65Proposition 84frege84 44374
[Frege1879] p. 66Proposition 85frege85 44375
[Frege1879] p. 66Proposition 86frege86 44376
[Frege1879] p. 66Proposition 87frege87 44377  frege87d 44177
[Frege1879] p. 67Proposition 88frege88 44378
[Frege1879] p. 68Proposition 89frege89 44379
[Frege1879] p. 68Proposition 90frege90 44380
[Frege1879] p. 68Proposition 91frege91 44381  frege91d 44178
[Frege1879] p. 69Proposition 92frege92 44382
[Frege1879] p. 70Proposition 93frege93 44383
[Frege1879] p. 70Proposition 94frege94 44384
[Frege1879] p. 70Proposition 95frege95 44385
[Frege1879] p. 71Definition 99dffrege99 44389
[Frege1879] p. 71Proposition 96frege96 44386  frege96d 44176
[Frege1879] p. 71Proposition 97frege97 44387  frege97d 44179
[Frege1879] p. 71Proposition 98frege98 44388  frege98d 44180
[Frege1879] p. 72Proposition 100frege100 44390
[Frege1879] p. 72Proposition 101frege101 44391
[Frege1879] p. 72Proposition 102frege102 44392  frege102d 44181
[Frege1879] p. 73Proposition 103frege103 44393
[Frege1879] p. 73Proposition 104frege104 44394
[Frege1879] p. 73Proposition 105frege105 44395
[Frege1879] p. 73Proposition 106frege106 44396  frege106d 44182
[Frege1879] p. 74Proposition 107frege107 44397
[Frege1879] p. 74Proposition 108frege108 44398  frege108d 44183
[Frege1879] p. 74Proposition 109frege109 44399  frege109d 44184
[Frege1879] p. 75Proposition 110frege110 44400
[Frege1879] p. 75Proposition 111frege111 44401  frege111d 44186
[Frege1879] p. 76Proposition 112frege112 44402
[Frege1879] p. 76Proposition 113frege113 44403
[Frege1879] p. 76Proposition 114frege114 44404  frege114d 44185
[Frege1879] p. 77Definition 115dffrege115 44405
[Frege1879] p. 77Proposition 116frege116 44406
[Frege1879] p. 78Proposition 117frege117 44407
[Frege1879] p. 78Proposition 118frege118 44408
[Frege1879] p. 78Proposition 119frege119 44409
[Frege1879] p. 78Proposition 120frege120 44410
[Frege1879] p. 79Proposition 121frege121 44411
[Frege1879] p. 79Proposition 122frege122 44412  frege122d 44187
[Frege1879] p. 79Proposition 123frege123 44413
[Frege1879] p. 80Proposition 124frege124 44414  frege124d 44188
[Frege1879] p. 81Proposition 125frege125 44415
[Frege1879] p. 81Proposition 126frege126 44416  frege126d 44189
[Frege1879] p. 82Proposition 127frege127 44417
[Frege1879] p. 83Proposition 128frege128 44418
[Frege1879] p. 83Proposition 129frege129 44419  frege129d 44190
[Frege1879] p. 84Proposition 130frege130 44420
[Frege1879] p. 85Proposition 131frege131 44421  frege131d 44191
[Frege1879] p. 86Proposition 132frege132 44422
[Frege1879] p. 86Proposition 133frege133 44423  frege133d 44192
[Fremlin1] p. 13Definition 111G (b)df-salgen 46741
[Fremlin1] p. 13Definition 111G (d)borelmbl 47064
[Fremlin1] p. 13Proposition 111G (b)salgenss 46764
[Fremlin1] p. 14Definition 112Aismea 46879
[Fremlin1] p. 15Remark 112B (d)psmeasure 46899
[Fremlin1] p. 15Property 112C (a)meadjun 46890  meadjunre 46904
[Fremlin1] p. 15Property 112C (b)meassle 46891
[Fremlin1] p. 15Property 112C (c)meaunle 46892
[Fremlin1] p. 16Property 112C (d)iundjiun 46888  meaiunle 46897  meaiunlelem 46896
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46909  meaiuninc2 46910  meaiuninc3 46913  meaiuninc3v 46912  meaiunincf 46911  meaiuninclem 46908
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46915  meaiininc2 46916  meaiininclem 46914
[Fremlin1] p. 19Theorem 113Ccaragen0 46934  caragendifcl 46942  caratheodory 46956  omelesplit 46946
[Fremlin1] p. 19Definition 113Aisome 46922  isomennd 46959  isomenndlem 46958
[Fremlin1] p. 19Remark 113B (c)omeunle 46944
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46963  voncmpl 47049
[Fremlin1] p. 19Definition 113A (ii)omessle 46926
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46951  carageniuncllem1 46949  carageniuncllem2 46950  caragenuncl 46941  caragenuncllem 46940  caragenunicl 46952
[Fremlin1] p. 21Remark 113Dcaragenel2d 46960
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46954  caratheodorylem2 46955
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46963
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47022  hoidmv1lelem1 47019  hoidmv1lelem2 47020  hoidmv1lelem3 47021
[Fremlin1] p. 25Definition 114Eisvonmbl 47066
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47022  hoidmvle 47028  hoidmvlelem1 47023  hoidmvlelem2 47024  hoidmvlelem3 47025  hoidmvlelem4 47026  hoidmvlelem5 47027  hsphoidmvle2 47013  hsphoif 47004  hsphoival 47007
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46976
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46984
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47011  hoidmvn0val 47012  hoidmvval 47005  hoidmvval0 47015  hoidmvval0b 47018
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47016  hsphoidmvle 47014
[Fremlin1] p. 30Definition 115Cdf-ovoln 46965  df-voln 46967
[Fremlin1] p. 30Proposition 115D (a)dmovn 47032  ovn0 46994  ovn0lem 46993  ovnf 46991  ovnome 47001  ovnssle 46989  ovnsslelem 46988  ovnsupge0 46985
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47031  ovnhoilem1 47029  ovnhoilem2 47030  vonhoi 47095
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47048  hoidifhspf 47046  hoidifhspval 47036  hoidifhspval2 47043  hoidifhspval3 47047  hspmbl 47057  hspmbllem1 47054  hspmbllem2 47055  hspmbllem3 47056
[Fremlin1] p. 31Definition 115Evoncmpl 47049  vonmea 47002
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47000  ovnsubadd2 47074  ovnsubadd2lem 47073  ovnsubaddlem1 46998  ovnsubaddlem2 46999
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47059  hoimbl2 47093  hoimbllem 47058  hspdifhsp 47044  opnvonmbl 47062  opnvonmbllem2 47061
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47064
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47107  iccvonmbllem 47106  ioovonmbl 47105
[Fremlin1] p. 32Proposition 115G (d)vonicc 47113  vonicclem2 47112  vonioo 47110  vonioolem2 47109  vonn0icc 47116  vonn0icc2 47120  vonn0ioo 47115  vonn0ioo2 47118
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47117  snvonmbl 47114  vonct 47121  vonsn 47119
[Fremlin1] p. 35Lemma 121Asubsalsal 46787
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46786  subsaliuncllem 46785
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47153  salpreimalegt 47137  salpreimaltle 47154
[Fremlin1] p. 35Proposition 121B (i)issmf 47156  issmff 47162  issmflem 47155
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47173  issmflelem 47172  smfpreimale 47182
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47184  issmfgtlem 47183
[Fremlin1] p. 36Definition 121Cdf-smblfn 47124  issmf 47156  issmff 47162  issmfge 47198  issmfgelem 47197  issmfgt 47184  issmfgtlem 47183  issmfle 47173  issmflelem 47172  issmflem 47155
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47135  salpreimagtlt 47158  salpreimalelt 47157
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47198  issmfgelem 47197
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47181
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47179  cnfsmf 47168
[Fremlin1] p. 36Proposition 121D (c)decsmf 47195  decsmflem 47194  incsmf 47170  incsmflem 47169
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47129  pimconstlt1 47130  smfconst 47177
[Fremlin1] p. 37Proposition 121E (b)smfadd 47193  smfaddlem1 47191  smfaddlem2 47192
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47224
[Fremlin1] p. 37Proposition 121E (d)smfmul 47223  smfmullem1 47219  smfmullem2 47220  smfmullem3 47221  smfmullem4 47222
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47225
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47228  smfpimbor1lem2 47227
[Fremlin1] p. 37Proposition 121E (g)smfco 47230
[Fremlin1] p. 37Proposition 121E (h)smfres 47218
[Fremlin1] p. 38Proposition 121E (e)smfrec 47217
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47226  smfresal 47216
[Fremlin1] p. 38Proposition 121F (a)smflim 47205  smflim2 47234  smflimlem1 47199  smflimlem2 47200  smflimlem3 47201  smflimlem4 47202  smflimlem5 47203  smflimlem6 47204  smflimmpt 47238
[Fremlin1] p. 38Proposition 121F (b)smfsup 47242  smfsuplem1 47239  smfsuplem2 47240  smfsuplem3 47241  smfsupmpt 47243  smfsupxr 47244
[Fremlin1] p. 38Proposition 121F (c)smfinf 47246  smfinflem 47245  smfinfmpt 47247
[Fremlin1] p. 39Remark 121Gsmflim 47205  smflim2 47234  smflimmpt 47238
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47236
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47266  smfdivdmmbl2 47269  smfinfdmmbl 47277  smfinfdmmbllem 47276  smfsupdmmbl 47273  smfsupdmmbllem 47272
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47256  smflimsuplem2 47249  smflimsuplem6 47253  smflimsuplem7 47254  smflimsuplem8 47255  smflimsupmpt 47257
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47259  smfliminflem 47258  smfliminfmpt 47260
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47124
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47270  fsupdm2 47271
[Fremlin1], p. 39Proposition 121Hadddmmbl 47261  adddmmbl2 47262  finfdm 47274  finfdm2 47275  fsupdm 47270  fsupdm2 47271  muldmmbl 47263  muldmmbl2 47264
[Fremlin1], p. 39Proposition 121F (c)finfdm 47274  finfdm2 47275
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25503
[Fremlin5] p. 213Lemma 565Cauniioovol 25546
[Fremlin5] p. 214Lemma 565Cauniioombl 25556
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38019
[Fremlin5] p. 220Theorem 565Maftc1anc 38022
[FreydScedrov] p. 283Axiom of Infinityax-inf 9559  inf1 9543  inf2 9544
[Gleason] p. 117Proposition 9-2.1df-enq 10834  enqer 10844
[Gleason] p. 117Proposition 9-2.2df-1nq 10839  df-nq 10835
[Gleason] p. 117Proposition 9-2.3df-plpq 10831  df-plq 10837
[Gleason] p. 119Proposition 9-2.4caovmo 7604  df-mpq 10832  df-mq 10838
[Gleason] p. 119Proposition 9-2.5df-rq 10840
[Gleason] p. 119Proposition 9-2.6ltexnq 10898
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10899  ltbtwnnq 10901
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10894
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10895
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10902
[Gleason] p. 121Definition 9-3.1df-np 10904
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10916
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10918
[Gleason] p. 122Definitiondf-1p 10905
[Gleason] p. 122Remark (1)prub 10917
[Gleason] p. 122Lemma 9-3.4prlem934 10956
[Gleason] p. 122Proposition 9-3.2df-ltp 10908
[Gleason] p. 122Proposition 9-3.3ltsopr 10955  psslinpr 10954  supexpr 10977  suplem1pr 10975  suplem2pr 10976
[Gleason] p. 123Proposition 9-3.5addclpr 10941  addclprlem1 10939  addclprlem2 10940  df-plp 10906
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10945
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10944
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10957
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10966  ltexprlem1 10959  ltexprlem2 10960  ltexprlem3 10961  ltexprlem4 10962  ltexprlem5 10963  ltexprlem6 10964  ltexprlem7 10965
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10968  ltaprlem 10967
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10969
[Gleason] p. 124Lemma 9-3.6prlem936 10970
[Gleason] p. 124Proposition 9-3.7df-mp 10907  mulclpr 10943  mulclprlem 10942  reclem2pr 10971
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10952
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10947
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10946
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10951
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10974  reclem3pr 10972  reclem4pr 10973
[Gleason] p. 126Proposition 9-4.1df-enr 10978  enrer 10986
[Gleason] p. 126Proposition 9-4.2df-0r 10983  df-1r 10984  df-nr 10979
[Gleason] p. 126Proposition 9-4.3df-mr 10981  df-plr 10980  negexsr 11025  recexsr 11030  recexsrlem 11026
[Gleason] p. 127Proposition 9-4.4df-ltr 10982
[Gleason] p. 130Proposition 10-1.3creui 12154  creur 12153  cru 12151
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11111  axcnre 11087
[Gleason] p. 132Definition 10-3.1crim 15077  crimd 15194  crimi 15155  crre 15076  crred 15193  crrei 15154
[Gleason] p. 132Definition 10-3.2remim 15079  remimd 15160
[Gleason] p. 133Definition 10.36absval2 15246  absval2d 15410  absval2i 15360
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15103  cjaddd 15182  cjaddi 15150
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15104  cjmuld 15183  cjmuli 15151
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15102  cjcjd 15161  cjcji 15133
[Gleason] p. 133Proposition 10-3.4(f)cjre 15101  cjreb 15085  cjrebd 15164  cjrebi 15136  cjred 15188  rere 15084  rereb 15082  rerebd 15163  rerebi 15135  rered 15186
[Gleason] p. 133Proposition 10-3.4(h)addcj 15110  addcjd 15174  addcji 15145
[Gleason] p. 133Proposition 10-3.7(a)absval 15200
[Gleason] p. 133Proposition 10-3.7(b)abscj 15241  abscjd 15415  abscji 15364
[Gleason] p. 133Proposition 10-3.7(c)abs00 15251  abs00d 15411  abs00i 15361  absne0d 15412
[Gleason] p. 133Proposition 10-3.7(d)releabs 15284  releabsd 15416  releabsi 15365
[Gleason] p. 133Proposition 10-3.7(f)absmul 15256  absmuld 15419  absmuli 15367
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15244  sqabsaddi 15368
[Gleason] p. 133Proposition 10-3.7(h)abstri 15293  abstrid 15421  abstrii 15371
[Gleason] p. 134Definition 10-4.1df-exp 14024  exp0 14027  expp1 14030  expp1d 14109
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26643  cxpaddd 26681  expadd 14066  expaddd 14110  expaddz 14068
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26652  cxpmuld 26701  expmul 14069  expmuld 14111  expmulz 14070
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26649  mulcxpd 26692  mulexp 14063  mulexpd 14123  mulexpz 14064
[Gleason] p. 140Exercise 1znnen 16179
[Gleason] p. 141Definition 11-2.1fzval 13463
[Gleason] p. 168Proposition 12-2.1(a)climadd 15594  rlimadd 15605  rlimdiv 15608
[Gleason] p. 168Proposition 12-2.1(b)climsub 15596  rlimsub 15606
[Gleason] p. 168Proposition 12-2.1(c)climmul 15595  rlimmul 15607
[Gleason] p. 171Corollary 12-2.2climmulc2 15599
[Gleason] p. 172Corollary 12-2.5climrecl 15545
[Gleason] p. 172Proposition 12-2.4(c)climabs 15566  climcj 15567  climim 15569  climre 15568  rlimabs 15571  rlimcj 15572  rlimim 15574  rlimre 15573
[Gleason] p. 173Definition 12-3.1df-ltxr 11184  df-xr 11183  ltxr 13066
[Gleason] p. 175Definition 12-4.1df-limsup 15433  limsupval 15436
[Gleason] p. 180Theorem 12-5.1climsup 15632
[Gleason] p. 180Theorem 12-5.3caucvg 15641  caucvgb 15642  caucvgbf 45917  caucvgr 15638  climcau 15633
[Gleason] p. 182Exercise 3cvgcmp 15779
[Gleason] p. 182Exercise 4cvgrat 15848
[Gleason] p. 195Theorem 13-2.12abs1m 15298
[Gleason] p. 217Lemma 13-4.1btwnzge0 13787
[Gleason] p. 223Definition 14-1.1df-met 21346
[Gleason] p. 223Definition 14-1.1(a)met0 24308  xmet0 24307
[Gleason] p. 223Definition 14-1.1(b)metgt0 24324
[Gleason] p. 223Definition 14-1.1(c)metsym 24315
[Gleason] p. 223Definition 14-1.1(d)mettri 24317  mstri 24434  xmettri 24316  xmstri 24433
[Gleason] p. 225Definition 14-1.5xpsmet 24347
[Gleason] p. 230Proposition 14-2.6txlm 23613
[Gleason] p. 240Theorem 14-4.3metcnp4 25277
[Gleason] p. 240Proposition 14-4.2metcnp3 24505
[Gleason] p. 243Proposition 14-4.16addcn 24831  addcn2 15556  mulcn 24833  mulcn2 15558  subcn 24832  subcn2 15557
[Gleason] p. 295Remarkbcval3 14268  bcval4 14269
[Gleason] p. 295Equation 2bcpasc 14283
[Gleason] p. 295Definition of binomial coefficientbcval 14266  df-bc 14265
[Gleason] p. 296Remarkbcn0 14272  bcnn 14274
[Gleason] p. 296Theorem 15-2.8binom 15795
[Gleason] p. 308Equation 2ef0 16056
[Gleason] p. 308Equation 3efcj 16057
[Gleason] p. 309Corollary 15-4.3efne0 16063
[Gleason] p. 309Corollary 15-4.4efexp 16068
[Gleason] p. 310Equation 14sinadd 16131
[Gleason] p. 310Equation 15cosadd 16132
[Gleason] p. 311Equation 17sincossq 16143
[Gleason] p. 311Equation 18cosbnd 16148  sinbnd 16147
[Gleason] p. 311Lemma 15-4.7sqeqor 14178  sqeqori 14176
[Gleason] p. 311Definition of ` `df-pi 16037
[Godowski] p. 730Equation SFgoeqi 32344
[GodowskiGreechie] p. 249Equation IV3oai 31739
[Golan] p. 1Remarksrgisid 20190
[Golan] p. 1Definitiondf-srg 20168
[Golan] p. 149Definitiondf-slmd 33262
[Gonshor] p. 7Definitiondf-cuts 27752
[Gonshor] p. 9Theorem 2.5lesrec 27791  lesrecd 27792
[Gonshor] p. 10Theorem 2.6cofcut1 27912  cofcut1d 27913
[Gonshor] p. 10Theorem 2.7cofcut2 27914  cofcut2d 27915
[Gonshor] p. 12Theorem 2.9cofcutr 27916  cofcutr1d 27917  cofcutr2d 27918
[Gonshor] p. 13Definitiondf-adds 27952
[Gonshor] p. 14Theorem 3.1addsprop 27968
[Gonshor] p. 15Theorem 3.2addsunif 27994
[Gonshor] p. 17Theorem 3.4mulsprop 28122
[Gonshor] p. 18Theorem 3.5mulsunif 28142
[Gonshor] p. 28Lemma 4.2halfcut 28450
[Gonshor] p. 28Theorem 4.2pw2cut 28452
[Gonshor] p. 30Theorem 4.2addhalfcut 28451
[Gonshor] p. 39Theorem 4.4(b)elreno2 28487
[Gonshor] p. 95Theorem 6.1addbday 28010
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36341
[Gratzer] p. 23Section 0.6df-mre 17548
[Gratzer] p. 27Section 0.6df-mri 17550
[Hall] p. 1Section 1.1df-asslaw 48658  df-cllaw 48656  df-comlaw 48657
[Hall] p. 2Section 1.2df-clintop 48670
[Hall] p. 7Section 1.3df-sgrp2 48691
[Halmos] p. 28Partition ` `df-parts 39189  dfmembpart2 39194
[Halmos] p. 31Theorem 17.3riesz1 32136  riesz2 32137
[Halmos] p. 41Definition of Hermitianhmopadj2 32012
[Halmos] p. 42Definition of projector orderingpjordi 32244
[Halmos] p. 43Theorem 26.1elpjhmop 32256  elpjidm 32255  pjnmopi 32219
[Halmos] p. 44Remarkpjinormi 31758  pjinormii 31747
[Halmos] p. 44Theorem 26.2elpjch 32260  pjrn 31778  pjrni 31773  pjvec 31767
[Halmos] p. 44Theorem 26.3pjnorm2 31798
[Halmos] p. 44Theorem 26.4hmopidmpj 32225  hmopidmpji 32223
[Halmos] p. 45Theorem 27.1pjinvari 32262
[Halmos] p. 45Theorem 27.3pjoci 32251  pjocvec 31768
[Halmos] p. 45Theorem 27.4pjorthcoi 32240
[Halmos] p. 48Theorem 29.2pjssposi 32243
[Halmos] p. 48Theorem 29.3pjssdif1i 32246  pjssdif2i 32245
[Halmos] p. 50Definition of spectrumdf-spec 31926
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1797
[Hatcher] p. 25Definitiondf-phtpc 24959  df-phtpy 24938
[Hatcher] p. 26Definitiondf-pco 24972  df-pi1 24975
[Hatcher] p. 26Proposition 1.2phtpcer 24962
[Hatcher] p. 26Proposition 1.3pi1grp 25017
[Hefferon] p. 240Definition 3.12df-dmat 22455  df-dmatalt 48868
[Helfgott] p. 2Theoremtgoldbach 48287
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48272
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48284  bgoldbtbnd 48279  bgoldbtbnd 48279  tgblthelfgott 48285
[Helfgott] p. 5Proposition 1.1circlevma 34786
[Helfgott] p. 69Statement 7.49circlemethhgt 34787
[Helfgott] p. 69Statement 7.50hgt750lema 34801  hgt750lemb 34800  hgt750leme 34802  hgt750lemf 34797  hgt750lemg 34798
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48281  tgoldbachgt 34807  tgoldbachgtALTV 48282  tgoldbachgtd 34806
[Helfgott] p. 70Statement 7.49ax-hgt749 34788
[Herstein] p. 54Exercise 28df-grpo 30564
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18920  grpoideu 30580  mndideu 18713
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18950  grpoinveu 30590
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18981  grpo2inv 30602
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18994  grpoinvop 30604
[Herstein] p. 57Exercise 1dfgrp3e 19016
[Hitchcock] p. 5Rule A3mptnan 1770
[Hitchcock] p. 5Rule A4mptxor 1771
[Hitchcock] p. 5Rule A5mtpxor 1773
[Holland] p. 1519Theorem 2sumdmdi 32491
[Holland] p. 1520Lemma 5cdj1i 32504  cdj3i 32512  cdj3lem1 32505  cdjreui 32503
[Holland] p. 1524Lemma 7mddmdin0i 32502
[Holland95] p. 13Theorem 3.6hlathil 42407
[Holland95] p. 14Line 15hgmapvs 42337
[Holland95] p. 14Line 16hdmaplkr 42359
[Holland95] p. 14Line 17hdmapellkr 42360
[Holland95] p. 14Line 19hdmapglnm2 42357
[Holland95] p. 14Line 20hdmapip0com 42363
[Holland95] p. 14Theorem 3.6hdmapevec2 42282
[Holland95] p. 14Lines 24 and 25hdmapoc 42377
[Holland95] p. 204Definition of involutiondf-srng 20817
[Holland95] p. 212Definition of subspacedf-psubsp 39949
[Holland95] p. 214Lemma 3.3lclkrlem2v 41974
[Holland95] p. 214Definition 3.2df-lpolN 41927
[Holland95] p. 214Definition of nonsingularpnonsingN 40379
[Holland95] p. 215Lemma 3.3(1)dihoml4 41823  poml4N 40399
[Holland95] p. 215Lemma 3.3(2)dochexmid 41914  pexmidALTN 40424  pexmidN 40415
[Holland95] p. 218Theorem 3.6lclkr 41979
[Holland95] p. 218Definition of dual vector spacedf-ldual 39570  ldualset 39571
[Holland95] p. 222Item 1df-lines 39947  df-pointsN 39948
[Holland95] p. 222Item 2df-polarityN 40349
[Holland95] p. 223Remarkispsubcl2N 40393  omllaw4 39692  pol1N 40356  polcon3N 40363
[Holland95] p. 223Definitiondf-psubclN 40381
[Holland95] p. 223Equation for polaritypolval2N 40352
[Holmes] p. 40Definitiondf-xrn 38701
[Hughes] p. 44Equation 1.21bax-his3 31155
[Hughes] p. 47Definition of projection operatordfpjop 32253
[Hughes] p. 49Equation 1.30eighmre 32034  eigre 31906  eigrei 31905
[Hughes] p. 49Equation 1.31eighmorth 32035  eigorth 31909  eigorthi 31908
[Hughes] p. 137Remark (ii)eigposi 31907
[Huneke] p. 1Claim 1frgrncvvdeq 30379
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30375
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30376
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30377
[Huneke] p. 2Claim 2frgrregorufr 30395  frgrregorufr0 30394  frgrregorufrg 30396
[Huneke] p. 2Claim 3frgrhash2wsp 30402  frrusgrord 30411  frrusgrord0 30410
[Huneke] p. 2Statementdf-clwwlknon 30158
[Huneke] p. 2Statement 4frgrwopreglem4 30385
[Huneke] p. 2Statement 5frgrwopreg1 30388  frgrwopreg2 30389  frgrwopregasn 30386  frgrwopregbsn 30387
[Huneke] p. 2Statement 6frgrwopreglem5 30391
[Huneke] p. 2Statement 7fusgreghash2wspv 30405
[Huneke] p. 2Statement 8fusgreghash2wsp 30408
[Huneke] p. 2Statement 9clwlksndivn 30156  numclwlk1 30441  numclwlk1lem1 30439  numclwlk1lem2 30440  numclwwlk1 30431  numclwwlk8 30462
[Huneke] p. 2Definition 3frgrwopreglem1 30382
[Huneke] p. 2Definition 4df-clwlks 29839
[Huneke] p. 2Definition 62clwwlk 30417
[Huneke] p. 2Definition 7numclwwlkovh 30443  numclwwlkovh0 30442
[Huneke] p. 2Statement 10numclwwlk2 30451
[Huneke] p. 2Statement 11rusgrnumwlkg 30048
[Huneke] p. 2Statement 12numclwwlk3 30455
[Huneke] p. 2Statement 13numclwwlk5 30458
[Huneke] p. 2Statement 14numclwwlk7 30461
[Indrzejczak] p. 33Definition ` `Enatded 30473  natded 30473
[Indrzejczak] p. 33Definition ` `Inatded 30473
[Indrzejczak] p. 34Definition ` `Enatded 30473  natded 30473
[Indrzejczak] p. 34Definition ` `Inatded 30473
[Jech] p. 4Definition of classcv 1541  cvjust 2731
[Jech] p. 42Lemma 6.1alephexp1 10502
[Jech] p. 42Equation 6.1alephadd 10500  alephmul 10501
[Jech] p. 43Lemma 6.2infmap 10499  infmap2 10139
[Jech] p. 71Lemma 9.3jech9.3 9738
[Jech] p. 72Equation 9.3scott0 9810  scottex 9809
[Jech] p. 72Exercise 9.1rankval4 9791  rankval4b 35243
[Jech] p. 72Scheme "Collection Principle"cp 9815
[Jech] p. 78Noteopthprc 5695
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43343
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43431
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43432
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43355
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43359
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43360  rmyp1 43361
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43362  rmym1 43363
[JonesMatijasevic] p. 695Equation 2.11rmx0 43353  rmx1 43354  rmxluc 43364
[JonesMatijasevic] p. 695Equation 2.12rmy0 43357  rmy1 43358  rmyluc 43365
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43367
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43368
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43388  jm2.17b 43389  jm2.17c 43390
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43421
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43425
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43416
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43391  jm2.24nn 43387
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43430
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43436  rmygeid 43392
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43448
[Juillerat] p. 11Section *5etransc 46711  etransclem47 46709  etransclem48 46710
[Juillerat] p. 12Equation (7)etransclem44 46706
[Juillerat] p. 12Equation *(7)etransclem46 46708
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46694
[Juillerat] p. 13Proofetransclem35 46697
[Juillerat] p. 13Part of case 2 proven inetransclem38 46700
[Juillerat] p. 13Part of case 2 provenetransclem24 46686
[Juillerat] p. 13Part of case 2: proven inetransclem41 46703
[Juillerat] p. 14Proofetransclem23 46685
[KalishMontague] p. 81Note 1ax-6 1969
[KalishMontague] p. 85Lemma 2equid 2014
[KalishMontague] p. 85Lemma 3equcomi 2019
[KalishMontague] p. 86Lemma 7cbvalivw 2009  cbvaliw 2008  wl-cbvmotv 37838  wl-motae 37840  wl-moteq 37839
[KalishMontague] p. 87Lemma 8spimvw 1988  spimw 1972
[KalishMontague] p. 87Lemma 9spfw 2035  spw 2036
[Kalmbach] p. 14Definition of latticechabs1 31587  chabs1i 31589  chabs2 31588  chabs2i 31590  chjass 31604  chjassi 31557  latabs1 18441  latabs2 18442
[Kalmbach] p. 15Definition of atomdf-at 32409  ela 32410
[Kalmbach] p. 15Definition of coverscvbr2 32354  cvrval2 39720
[Kalmbach] p. 16Definitiondf-ol 39624  df-oml 39625
[Kalmbach] p. 20Definition of commutescmbr 31655  cmbri 31661  cmtvalN 39657  df-cm 31654  df-cmtN 39623
[Kalmbach] p. 22Remarkomllaw5N 39693  pjoml5 31684  pjoml5i 31659
[Kalmbach] p. 22Definitionpjoml2 31682  pjoml2i 31656
[Kalmbach] p. 22Theorem 2(v)cmcm 31685  cmcmi 31663  cmcmii 31668  cmtcomN 39695
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39691  omlsi 31475  pjoml 31507  pjomli 31506
[Kalmbach] p. 22Definition of OML lawomllaw2N 39690
[Kalmbach] p. 23Remarkcmbr2i 31667  cmcm3 31686  cmcm3i 31665  cmcm3ii 31670  cmcm4i 31666  cmt3N 39697  cmt4N 39698  cmtbr2N 39699
[Kalmbach] p. 23Lemma 3cmbr3 31679  cmbr3i 31671  cmtbr3N 39700
[Kalmbach] p. 25Theorem 5fh1 31689  fh1i 31692  fh2 31690  fh2i 31693  omlfh1N 39704
[Kalmbach] p. 65Remarkchjatom 32428  chslej 31569  chsleji 31529  shslej 31451  shsleji 31441
[Kalmbach] p. 65Proposition 1chocin 31566  chocini 31525  chsupcl 31411  chsupval2 31481  h0elch 31326  helch 31314  hsupval2 31480  ocin 31367  ococss 31364  shococss 31365
[Kalmbach] p. 65Definition of subspace sumshsval 31383
[Kalmbach] p. 66Remarkdf-pjh 31466  pjssmi 32236  pjssmii 31752
[Kalmbach] p. 67Lemma 3osum 31716  osumi 31713
[Kalmbach] p. 67Lemma 4pjci 32271
[Kalmbach] p. 103Exercise 6atmd2 32471
[Kalmbach] p. 103Exercise 12mdsl0 32381
[Kalmbach] p. 140Remarkhatomic 32431  hatomici 32430  hatomistici 32433
[Kalmbach] p. 140Proposition 1atlatmstc 39765
[Kalmbach] p. 140Proposition 1(i)atexch 32452  lsatexch 39489
[Kalmbach] p. 140Proposition 1(ii)chcv1 32426  cvlcvr1 39785  cvr1 39856
[Kalmbach] p. 140Proposition 1(iii)cvexch 32445  cvexchi 32440  cvrexch 39866
[Kalmbach] p. 149Remark 2chrelati 32435  hlrelat 39848  hlrelat5N 39847  lrelat 39460
[Kalmbach] p. 153Exercise 5lsmcv 21139  lsmsatcv 39456  spansncv 31724  spansncvi 31723
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39475  spansncv2 32364
[Kalmbach] p. 266Definitiondf-st 32282
[Kalmbach2] p. 8Definition of adjointdf-adjh 31920
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10569  fpwwe2 10566
[KanamoriPincus] p. 416Corollary 1.3canth4 10570
[KanamoriPincus] p. 417Corollary 1.6canthp1 10577
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10572
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10574
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10587
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10591  gchxpidm 10592
[KanamoriPincus] p. 419Theorem 2.1gchacg 10603  gchhar 10602
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10137  unxpwdom 9504
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10593
[Kreyszig] p. 3Property M1metcl 24297  xmetcl 24296
[Kreyszig] p. 4Property M2meteq0 24304
[Kreyszig] p. 8Definition 1.1-8dscmet 24537
[Kreyszig] p. 12Equation 5conjmul 11872  muleqadd 11794
[Kreyszig] p. 18Definition 1.3-2mopnval 24403
[Kreyszig] p. 19Remarkmopntopon 24404
[Kreyszig] p. 19Theorem T1mopn0 24463  mopnm 24409
[Kreyszig] p. 19Theorem T2unimopn 24461
[Kreyszig] p. 19Definition of neighborhoodneibl 24466
[Kreyszig] p. 20Definition 1.3-3metcnp2 24507
[Kreyszig] p. 25Definition 1.4-1lmbr 23223  lmmbr 25225  lmmbr2 25226
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23345
[Kreyszig] p. 28Theorem 1.4-5lmcau 25280
[Kreyszig] p. 28Definition 1.4-3iscau 25243  iscmet2 25261
[Kreyszig] p. 30Theorem 1.4-7cmetss 25283
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23426  metelcls 25272
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25273  metcld2 25274
[Kreyszig] p. 51Equation 2clmvneg1 25066  lmodvneg1 20900  nvinv 30710  vcm 30647
[Kreyszig] p. 51Equation 1aclm0vs 25062  lmod0vs 20890  slmd0vs 33285  vc0 30645
[Kreyszig] p. 51Equation 1blmodvs0 20891  slmdvs0 33286  vcz 30646
[Kreyszig] p. 58Definition 2.2-1imsmet 30762  ngpmet 24568  nrmmetd 24539
[Kreyszig] p. 59Equation 1imsdval 30757  imsdval2 30758  ncvspds 25128  ngpds 24569
[Kreyszig] p. 63Problem 1nmval 24554  nvnd 30759
[Kreyszig] p. 64Problem 2nmeq0 24583  nmge0 24582  nvge0 30744  nvz 30740
[Kreyszig] p. 64Problem 3nmrtri 24589  nvabs 30743
[Kreyszig] p. 91Definition 2.7-1isblo3i 30872
[Kreyszig] p. 92Equation 2df-nmoo 30816
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30878  blocni 30876
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30877
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25171  ipeq0 21618  ipz 30790
[Kreyszig] p. 135Problem 2cphpyth 25183  pythi 30921
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30925
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25205
[Kreyszig] p. 144Equation 4supcvg 15821
[Kreyszig] p. 144Theorem 3.3-1minvec 25403  minveco 30955
[Kreyszig] p. 196Definition 3.9-1df-aj 30821
[Kreyszig] p. 247Theorem 4.7-2bcth 25296
[Kreyszig] p. 249Theorem 4.7-3ubth 30944
[Kreyszig] p. 470Definition of positive operator orderingleop 32194  leopg 32193
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32212
[Kreyszig] p. 525Theorem 10.1-1htth 30989
[Kulpa] p. 547Theorempoimir 37974
[Kulpa] p. 547Equation (1)poimirlem32 37973
[Kulpa] p. 547Equation (2)poimirlem31 37972
[Kulpa] p. 548Theorembroucube 37975
[Kulpa] p. 548Equation (6)poimirlem26 37967
[Kulpa] p. 548Equation (7)poimirlem27 37968
[Kunen] p. 10Axiom 0ax6e 2388  axnul 5241
[Kunen] p. 11Axiom 3axnul 5241
[Kunen] p. 12Axiom 6zfrep6 5225
[Kunen] p. 24Definition 10.24mapval 8785  mapvalg 8783
[Kunen] p. 30Lemma 10.20fodomg 10444
[Kunen] p. 31Definition 10.24mapex 7892
[Kunen] p. 95Definition 2.1df-r1 9688
[Kunen] p. 97Lemma 2.10r1elss 9730  r1elssi 9729
[Kunen] p. 107Exercise 4rankop 9782  rankopb 9776  rankuni 9787  rankxplim 9803  rankxpsuc 9806
[Kunen2] p. 47Lemma I.9.9relpfr 45381
[Kunen2] p. 53Lemma I.9.21trfr 45389
[Kunen2] p. 53Lemma I.9.24(2)wffr 45388
[Kunen2] p. 53Definition I.9.20tcfr 45390
[Kunen2] p. 95Lemma I.16.2ralabso 45395  rexabso 45396
[Kunen2] p. 96Example I.16.3disjabso 45402  n0abso 45403  ssabso 45401
[Kunen2] p. 111Lemma II.2.4(1)traxext 45404
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45414
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45409
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45412
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45413
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45408
[Kunen2] p. 112Corollary II.2.5wfaxext 45420  wfaxpr 45425  wfaxreg 45427  wfaxrep 45421  wfaxsep 45422  wfaxun 45426
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45411
[Kunen2] p. 113Corollary II.2.9wfaxpow 45424
[Kunen2] p. 114Theorem II.2.13wfaxext 45420
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45419  omelaxinf2 45416
[Kunen2] p. 114Corollary II.2.12wfac8prim 45429  wfaxinf2 45428
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45442  permaxext 45432  permaxinf2 45440  permaxnul 45435  permaxpow 45436  permaxpr 45437  permaxrep 45433  permaxsep 45434  permaxun 45438
[Kunen2] p. 148Definition II.9.1brpermmodel 45430
[Kunen2] p. 149Exercise II.9.3permac8prim 45441
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4947
[Lang] , p. 225Corollary 1.3finexttrb 33809
[Lang] p. Definitiondf-rn 5642
[Lang] p. 3Statementlidrideqd 18637  mndbn0 18718
[Lang] p. 3Definitiondf-mnd 18703
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18655
[Lang] p. 4Property of composites. Second formulagsumccat 18809
[Lang] p. 5Equationgsumreidx 19892
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48652
[Lang] p. 6Examplenn0mnd 48649
[Lang] p. 6Equationgsumxp2 19955
[Lang] p. 6Statementcycsubm 19177
[Lang] p. 6Definitionmulgnn0gsum 19056
[Lang] p. 6Observationmndlsmidm 19645
[Lang] p. 7Definitiondfgrp2e 18939
[Lang] p. 30Definitiondf-tocyc 33168
[Lang] p. 32Property (a)cyc3genpm 33213
[Lang] p. 32Property (b)cyc3conja 33218  cycpmconjv 33203
[Lang] p. 53Definitiondf-cat 17634
[Lang] p. 53Axiom CAT 1cat1 18064  cat1lem 18063
[Lang] p. 54Definitiondf-iso 17716
[Lang] p. 57Definitiondf-inito 17951  df-termo 17952
[Lang] p. 58Exampleirinitoringc 21459
[Lang] p. 58Statementinitoeu1 17978  termoeu1 17985
[Lang] p. 62Definitiondf-func 17825
[Lang] p. 65Definitiondf-nat 17913
[Lang] p. 91Notedf-ringc 20623
[Lang] p. 92Statementmxidlprm 33530
[Lang] p. 92Definitionisprmidlc 33507
[Lang] p. 128Remarkdsmmlmod 21725
[Lang] p. 129Prooflincscm 48900  lincscmcl 48902  lincsum 48899  lincsumcl 48901
[Lang] p. 129Statementlincolss 48904
[Lang] p. 129Observationdsmmfi 21718
[Lang] p. 141Theorem 5.3dimkerim 33771  qusdimsum 33772
[Lang] p. 141Corollary 5.4lssdimle 33752
[Lang] p. 147Definitionsnlindsntor 48941
[Lang] p. 504Statementmat1 22412  matring 22408
[Lang] p. 504Definitiondf-mamu 22356
[Lang] p. 505Statementmamuass 22367  mamutpos 22423  matassa 22409  mattposvs 22420  tposmap 22422
[Lang] p. 513Definitionmdet1 22566  mdetf 22560
[Lang] p. 513Theorem 4.4cramer 22656
[Lang] p. 514Proposition 4.6mdetleib 22552
[Lang] p. 514Proposition 4.8mdettpos 22576
[Lang] p. 515Definitiondf-minmar1 22600  smadiadetr 22640
[Lang] p. 515Corollary 4.9mdetero 22575  mdetralt 22573
[Lang] p. 517Proposition 4.15mdetmul 22588
[Lang] p. 518Definitiondf-madu 22599
[Lang] p. 518Proposition 4.16madulid 22610  madurid 22609  matinv 22642
[Lang] p. 561Theorem 3.1cayleyhamilton 22855
[Lang], p. 190Chapter 6vieta 33724
[Lang], p. 224Proposition 1.1extdgfialg 33838  finextalg 33842
[Lang], p. 224Proposition 1.2extdgmul 33807  fedgmul 33775
[Lang], p. 225Proposition 1.4algextdeg 33869
[Lang], p. 561Remarkchpmatply1 22797
[Lang], p. 561Definitiondf-chpmat 22792
[Lang2] p. 3Notationsdf-ind 12160
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44761
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44756
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44762
[LeBlanc] p. 277Rule R2axnul 5241
[Levy] p. 12Axiom 4.3.1df-clab 2716  wl-df.clab 37823
[Levy] p. 59Definitiondf-ttrcl 9629
[Levy] p. 64Theorem 5.6(ii)frinsg 9675
[Levy] p. 338Axiomdf-clel 2812  df-cleq 2729  wl-df.clel 37827  wl-df.cleq 37824
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2812  df-cleq 2729  wl-df.clel 37827  wl-df.cleq 37824
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2716  wl-df.clab 37823
[Levy] p. 358Axiomdf-clab 2716  wl-df.clab 37823
[Levy58] p. 2Definition Iisfin1-3 10308
[Levy58] p. 2Definition IIdf-fin2 10208
[Levy58] p. 2Definition Iadf-fin1a 10207
[Levy58] p. 2Definition IIIdf-fin3 10210
[Levy58] p. 3Definition Vdf-fin5 10211
[Levy58] p. 3Definition IVdf-fin4 10209
[Levy58] p. 4Definition VIdf-fin6 10212
[Levy58] p. 4Definition VIIdf-fin7 10213
[Levy58], p. 3Theorem 1fin1a2 10337
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27650
[Lipparini] p. 3Lemma 2.1.4noresle 27661
[Lipparini] p. 6Proposition 4.2noinfbnd1 27693  nosupbnd1 27678
[Lipparini] p. 6Proposition 4.3noinfbnd2 27695  nosupbnd2 27680
[Lipparini] p. 7Theorem 5.1noetasuplem3 27699  noetasuplem4 27700
[Lipparini] p. 7Corollary 4.4nosupinfsep 27696
[Lopez-Astorga] p. 12Rule 1mptnan 1770
[Lopez-Astorga] p. 12Rule 2mptxor 1771
[Lopez-Astorga] p. 12Rule 3mtpxor 1773
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32479
[Maeda] p. 168Lemma 5mdsym 32483  mdsymi 32482
[Maeda] p. 168Lemma 4(i)mdsymlem4 32477  mdsymlem6 32479  mdsymlem7 32480
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32481
[MaedaMaeda] p. 1Remarkssdmd1 32384  ssdmd2 32385  ssmd1 32382  ssmd2 32383
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32380
[MaedaMaeda] p. 1Definition 1.1df-dmd 32352  df-md 32351  mdbr 32365
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32402  mdslj1i 32390  mdslj2i 32391  mdslle1i 32388  mdslle2i 32389  mdslmd1i 32400  mdslmd2i 32401
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32392  mdsl2bi 32394  mdsl2i 32393
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32406
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32403
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32404
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32381
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32386  mdsl3 32387
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32405
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32500
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39767  hlrelat1 39846
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39485
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32407  cvmdi 32395  cvnbtwn4 32360  cvrnbtwn4 39725
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32408
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39786  cvp 32446  cvrp 39862  lcvp 39486
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32470
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32469
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39779  hlexch4N 39838
[MaedaMaeda] p. 34Exercise 7.1atabsi 32472
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39889
[MaedaMaeda] p. 61Definition 15.10psubN 40195  atpsubN 40199  df-pointsN 39948  pointpsubN 40197
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39950  pmap11 40208  pmaple 40207  pmapsub 40214  pmapval 40203
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40211  pmap1N 40213
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40216  pmapglb2N 40217  pmapglb2xN 40218  pmapglbx 40215
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40298
[MaedaMaeda] p. 67Postulate PS1ps-1 39923
[MaedaMaeda] p. 68Lemma 16.2df-padd 40242  paddclN 40288  paddidm 40287
[MaedaMaeda] p. 68Condition PS2ps-2 39924
[MaedaMaeda] p. 68Equation 16.2.1paddass 40284
[MaedaMaeda] p. 69Lemma 16.4ps-1 39923
[MaedaMaeda] p. 69Theorem 16.4ps-2 39924
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19650  lsmmod2 19651  lssats 39458  shatomici 32429  shatomistici 32432  shmodi 31461  shmodsi 31460
[MaedaMaeda] p. 130Remark 29.6dmdmd 32371  mdsymlem7 32480
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31660
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31564
[MaedaMaeda] p. 139Remarksumdmdii 32486
[Margaris] p. 40Rule Cexlimiv 1932
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1782  df-or 849  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30470
[Margaris] p. 59Section 14notnotrALTVD 45341
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45342
[Margaris] p. 79Rule Cexinst01 45052  exinst11 45053
[Margaris] p. 89Theorem 19.219.2 1978  19.2g 2196  r19.2z 4440
[Margaris] p. 89Theorem 19.319.3 2210  rr19.3v 3610
[Margaris] p. 89Theorem 19.5alcom 2165
[Margaris] p. 89Theorem 19.6alex 1828
[Margaris] p. 89Theorem 19.7alnex 1783
[Margaris] p. 89Theorem 19.819.8a 2189
[Margaris] p. 89Theorem 19.919.9 2213  19.9h 2293  exlimd 2226  exlimdh 2297
[Margaris] p. 89Theorem 19.11excom 2168  excomim 2169
[Margaris] p. 89Theorem 19.1219.12 2333
[Margaris] p. 90Section 19conventions-labels 30471  conventions-labels 30471  conventions-labels 30471  conventions-labels 30471
[Margaris] p. 90Theorem 19.14exnal 1829
[Margaris] p. 90Theorem 19.152albi 44805  albi 1820
[Margaris] p. 90Theorem 19.1619.16 2233
[Margaris] p. 90Theorem 19.1719.17 2234
[Margaris] p. 90Theorem 19.182exbi 44807  exbi 1849
[Margaris] p. 90Theorem 19.1919.19 2237
[Margaris] p. 90Theorem 19.202alim 44804  2alimdv 1920  alimd 2220  alimdh 1819  alimdv 1918  ax-4 1811  ralimdaa 3239  ralimdv 3152  ralimdva 3150  ralimdvva 3185  sbcimdv 3798
[Margaris] p. 90Theorem 19.2119.21 2215  19.21h 2294  19.21t 2214  19.21vv 44803  alrimd 2223  alrimdd 2222  alrimdh 1865  alrimdv 1931  alrimi 2221  alrimih 1826  alrimiv 1929  alrimivv 1930  bj-alrimdh 36889  hbralrimi 3128  r19.21be 3231  r19.21bi 3230  ralrimd 3243  ralrimdv 3136  ralrimdva 3138  ralrimdvv 3182  ralrimdvva 3193  ralrimi 3236  ralrimia 3237  ralrimiv 3129  ralrimiva 3130  ralrimivv 3179  ralrimivva 3181  ralrimivvva 3184  ralrimivw 3134
[Margaris] p. 90Theorem 19.222exim 44806  2eximdv 1921  bj-exim 36904  exim 1836  eximd 2224  eximdh 1866  eximdv 1919  rexim 3079  reximd2a 3248  reximdai 3240  reximdd 45578  reximddv 3154  reximddv2 3197  reximddv3 3155  reximdv 3153  reximdv2 3148  reximdva 3151  reximdvai 3149  reximdvva 3186  reximi2 3071
[Margaris] p. 90Theorem 19.2319.23 2219  19.23bi 2199  19.23h 2295  19.23t 2218  exlimdv 1935  exlimdvv 1936  exlimexi 44951  exlimiv 1932  exlimivv 1934  rexlimd3 45574  rexlimdv 3137  rexlimdv3a 3143  rexlimdva 3139  rexlimdva2 3141  rexlimdvaa 3140  rexlimdvv 3194  rexlimdvva 3195  rexlimdvvva 3196  rexlimdvw 3144  rexlimiv 3132  rexlimiva 3131  rexlimivv 3180
[Margaris] p. 90Theorem 19.2419.24 1993
[Margaris] p. 90Theorem 19.2519.25 1882
[Margaris] p. 90Theorem 19.2619.26 1872
[Margaris] p. 90Theorem 19.2719.27 2235  r19.27z 4451  r19.27zv 4452
[Margaris] p. 90Theorem 19.2819.28 2236  19.28vv 44813  r19.28z 4443  r19.28zf 45589  r19.28zv 4447  rr19.28v 3611
[Margaris] p. 90Theorem 19.2919.29 1875  r19.29d2r 3125  r19.29imd 3103
[Margaris] p. 90Theorem 19.3019.30 1883
[Margaris] p. 90Theorem 19.3119.31 2242  19.31vv 44811
[Margaris] p. 90Theorem 19.3219.32 2241  r19.32 47540
[Margaris] p. 90Theorem 19.3319.33-2 44809  19.33 1886
[Margaris] p. 90Theorem 19.3419.34 1994
[Margaris] p. 90Theorem 19.3519.35 1879
[Margaris] p. 90Theorem 19.3619.36 2238  19.36vv 44810  r19.36zv 4453
[Margaris] p. 90Theorem 19.3719.37 2240  19.37vv 44812  r19.37zv 4448
[Margaris] p. 90Theorem 19.3819.38 1841
[Margaris] p. 90Theorem 19.3919.39 1992
[Margaris] p. 90Theorem 19.4019.40-2 1889  19.40 1888  r19.40 3104
[Margaris] p. 90Theorem 19.4119.41 2243  19.41rg 44977
[Margaris] p. 90Theorem 19.4219.42 2244
[Margaris] p. 90Theorem 19.4319.43 1884
[Margaris] p. 90Theorem 19.4419.44 2245  r19.44zv 4450
[Margaris] p. 90Theorem 19.4519.45 2246  r19.45zv 4449
[Margaris] p. 110Exercise 2(b)eu1 2611
[Mayet] p. 370Remarkjpi 32341  largei 32338  stri 32328
[Mayet3] p. 9Definition of CH-statesdf-hst 32283  ishst 32285
[Mayet3] p. 10Theoremhstrbi 32337  hstri 32336
[Mayet3] p. 1223Theorem 4.1mayete3i 31799
[Mayet3] p. 1240Theorem 7.1mayetes3i 31800
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32349
[MegPav2000] p. 2345Definition 3.4-1chintcl 31403  chsupcl 31411
[MegPav2000] p. 2345Definition 3.4-2hatomic 32431
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32425
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32452
[MegPav2000] p. 2366Figure 7pl42N 40429
[MegPav2002] p. 362Lemma 2.2latj31 18453  latj32 18451  latjass 18449
[Megill] p. 444Axiom C5ax-5 1912  ax5ALT 39353
[Megill] p. 444Section 7conventions 30470
[Megill] p. 445Lemma L12aecom-o 39347  ax-c11n 39334  axc11n 2431
[Megill] p. 446Lemma L17equtrr 2024
[Megill] p. 446Lemma L18ax6fromc10 39342
[Megill] p. 446Lemma L19hbnae-o 39374  hbnae 2437
[Megill] p. 447Remark 9.1dfsb1 2486  sbid 2263  sbidd-misc 50188  sbidd 50187
[Megill] p. 448Remark 9.6axc14 2468
[Megill] p. 448Scheme C4'ax-c4 39330
[Megill] p. 448Scheme C5'ax-c5 39329  sp 2191
[Megill] p. 448Scheme C6'ax-11 2163
[Megill] p. 448Scheme C7'ax-c7 39331
[Megill] p. 448Scheme C8'ax-7 2010
[Megill] p. 448Scheme C9'ax-c9 39336
[Megill] p. 448Scheme C10'ax-6 1969  ax-c10 39332
[Megill] p. 448Scheme C11'ax-c11 39333
[Megill] p. 448Scheme C12'ax-8 2116
[Megill] p. 448Scheme C13'ax-9 2124
[Megill] p. 448Scheme C14'ax-c14 39337
[Megill] p. 448Scheme C15'ax-c15 39335
[Megill] p. 448Scheme C16'ax-c16 39338
[Megill] p. 448Theorem 9.4dral1-o 39350  dral1 2444  dral2-o 39376  dral2 2443  drex1 2446  drex2 2447  drsb1 2500  drsb2 2274
[Megill] p. 449Theorem 9.7sbcom2 2179  sbequ 2089  sbid2v 2514
[Megill] p. 450Example in Appendixhba1-o 39343  hba1 2300
[Mendelson] p. 35Axiom A3hirstL-ax3 47334
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3818  rspsbca 3819  stdpc4 2074
[Mendelson] p. 69Axiom 5ax-c4 39330  ra4 3825  stdpc5 2216
[Mendelson] p. 81Rule Cexlimiv 1932
[Mendelson] p. 95Axiom 6stdpc6 2030
[Mendelson] p. 95Axiom 7stdpc7 2258
[Mendelson] p. 225Axiom system NBGru 3727
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5469
[Mendelson] p. 231Exercise 4.10(k)inv1 4339
[Mendelson] p. 231Exercise 4.10(l)unv 4340
[Mendelson] p. 231Exercise 4.10(n)dfin3 4218
[Mendelson] p. 231Exercise 4.10(o)df-nul 4275
[Mendelson] p. 231Exercise 4.10(q)dfin4 4219
[Mendelson] p. 231Exercise 4.10(s)ddif 4082
[Mendelson] p. 231Definition of uniondfun3 4217
[Mendelson] p. 235Exercise 4.12(c)univ 5404
[Mendelson] p. 235Exercise 4.12(d)pwv 4848
[Mendelson] p. 235Exercise 4.12(j)pwin 5522
[Mendelson] p. 235Exercise 4.12(k)pwunss 4560
[Mendelson] p. 235Exercise 4.12(l)pwssun 5523
[Mendelson] p. 235Exercise 4.12(n)uniin 4875
[Mendelson] p. 235Exercise 4.12(p)reli 5782
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6234
[Mendelson] p. 244Proposition 4.8(g)epweon 7729
[Mendelson] p. 246Definition of successordf-suc 6330
[Mendelson] p. 250Exercise 4.36oelim2 8531
[Mendelson] p. 254Proposition 4.22(b)xpen 9078
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8999  xpsneng 9000
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9006  xpcomeng 9007
[Mendelson] p. 254Proposition 4.22(e)xpassen 9009
[Mendelson] p. 255Definitionbrsdom 8921
[Mendelson] p. 255Exercise 4.39endisj 9002
[Mendelson] p. 255Exercise 4.41mapprc 8777
[Mendelson] p. 255Exercise 4.43mapsnen 8984  mapsnend 8983
[Mendelson] p. 255Exercise 4.45mapunen 9084
[Mendelson] p. 255Exercise 4.47xpmapen 9083
[Mendelson] p. 255Exercise 4.42(a)map0e 8830
[Mendelson] p. 255Exercise 4.42(b)map1 8987
[Mendelson] p. 257Proposition 4.24(a)undom 9003
[Mendelson] p. 258Exercise 4.56(c)djuassen 10101  djucomen 10100
[Mendelson] p. 258Exercise 4.56(f)djudom1 10105
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10099
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8466
[Mendelson] p. 266Proposition 4.34(f)oaordex 8493
[Mendelson] p. 275Proposition 4.42(d)entri3 10481
[Mendelson] p. 281Definitiondf-r1 9688
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9737
[Mendelson] p. 287Axiom system MKru 3727
[MertziosUnger] p. 152Definitiondf-frgr 30329
[MertziosUnger] p. 153Remark 1frgrconngr 30364
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30366  vdgn1frgrv3 30367
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30368
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30361
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30354  2pthfrgrrn 30352  2pthfrgrrn2 30353
[Mittelstaedt] p. 9Definitiondf-oc 31323
[Monk1] p. 22Remarkconventions 30470
[Monk1] p. 22Theorem 3.1conventions 30470
[Monk1] p. 26Theorem 2.8(vii)ssin 4180
[Monk1] p. 33Theorem 3.2(i)ssrel 5739  ssrelf 32688
[Monk1] p. 33Theorem 3.2(ii)eqrel 5740
[Monk1] p. 34Definition 3.3df-opab 5149
[Monk1] p. 36Theorem 3.7(i)coi1 6228  coi2 6229
[Monk1] p. 36Theorem 3.8(v)dm0 5876  rn0 5882
[Monk1] p. 36Theorem 3.7(ii)cnvi 6106
[Monk1] p. 37Theorem 3.13(i)relxp 5649
[Monk1] p. 37Theorem 3.13(x)dmxp 5885  rnxp 6135
[Monk1] p. 37Theorem 3.13(ii)0xp 5730  xp0 5731
[Monk1] p. 38Theorem 3.16(ii)ima0 6043
[Monk1] p. 38Theorem 3.16(viii)imai 6040
[Monk1] p. 39Theorem 3.17imaex 7865  imaexg 7864
[Monk1] p. 39Theorem 3.16(xi)imassrn 6037
[Monk1] p. 41Theorem 4.3(i)fnopfv 7028  funfvop 7003
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6895
[Monk1] p. 42Theorem 4.4(iii)fvelima 6906
[Monk1] p. 43Theorem 4.6funun 6545
[Monk1] p. 43Theorem 4.8(iv)dff13 7209  dff13f 7210
[Monk1] p. 46Theorem 4.15(v)funex 7174  funrnex 7907
[Monk1] p. 50Definition 5.4fniunfv 7202
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6192
[Monk1] p. 52Theorem 5.11(viii)ssint 4907
[Monk1] p. 52Definition 5.13 (i)1stval2 7959  df-1st 7942
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7960  df-2nd 7943
[Monk1] p. 112Theorem 15.17(v)ranksn 9778  ranksnb 9751
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9779
[Monk1] p. 112Theorem 15.17(iii)rankun 9780  rankunb 9774
[Monk1] p. 113Theorem 15.18r1val3 9762
[Monk1] p. 113Definition 15.19df-r1 9688  r1val2 9761
[Monk1] p. 117Lemmazorn2 10428  zorn2g 10425
[Monk1] p. 133Theorem 18.11cardom 9910
[Monk1] p. 133Theorem 18.12canth3 10483
[Monk1] p. 133Theorem 18.14carduni 9905
[Monk2] p. 105Axiom C4ax-4 1811
[Monk2] p. 105Axiom C7ax-7 2010
[Monk2] p. 105Axiom C8ax-12 2185  ax-c15 39335  ax12v2 2187
[Monk2] p. 108Lemma 5ax-c4 39330
[Monk2] p. 109Lemma 12ax-11 2163
[Monk2] p. 109Lemma 15equvini 2460  equvinv 2031  eqvinop 5441
[Monk2] p. 113Axiom C5-1ax-5 1912  ax5ALT 39353
[Monk2] p. 113Axiom C5-2ax-10 2147
[Monk2] p. 113Axiom C5-3ax-11 2163
[Monk2] p. 114Lemma 21sp 2191
[Monk2] p. 114Lemma 22axc4 2327  hba1-o 39343  hba1 2300
[Monk2] p. 114Lemma 23nfia1 2159
[Monk2] p. 114Lemma 24nfa2 2182  nfra2 3339  nfra2w 3274
[Moore] p. 53Part Idf-mre 17548
[Munkres] p. 77Example 2distop 22960  indistop 22967  indistopon 22966
[Munkres] p. 77Example 3fctop 22969  fctop2 22970
[Munkres] p. 77Example 4cctop 22971
[Munkres] p. 78Definition of basisdf-bases 22911  isbasis3g 22914
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17406  tgval2 22921
[Munkres] p. 79Remarktgcl 22934
[Munkres] p. 80Lemma 2.1tgval3 22928
[Munkres] p. 80Lemma 2.2tgss2 22952  tgss3 22951
[Munkres] p. 81Lemma 2.3basgen 22953  basgen2 22954
[Munkres] p. 83Exercise 3topdifinf 37665  topdifinfeq 37666  topdifinffin 37664  topdifinfindis 37662
[Munkres] p. 89Definition of subspace topologyresttop 23125
[Munkres] p. 93Theorem 6.1(1)0cld 23003  topcld 23000
[Munkres] p. 93Theorem 6.1(2)iincld 23004
[Munkres] p. 93Theorem 6.1(3)uncld 23006
[Munkres] p. 94Definition of closureclsval 23002
[Munkres] p. 94Definition of interiorntrval 23001
[Munkres] p. 95Theorem 6.5(a)clsndisj 23040  elcls 23038
[Munkres] p. 95Theorem 6.5(b)elcls3 23048
[Munkres] p. 97Theorem 6.6clslp 23113  neindisj 23082
[Munkres] p. 97Corollary 6.7cldlp 23115
[Munkres] p. 97Definition of limit pointislp2 23110  lpval 23104
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23280
[Munkres] p. 102Definition of continuous functiondf-cn 23192  iscn 23200  iscn2 23203
[Munkres] p. 107Theorem 7.2(g)cncnp 23245  cncnp2 23246  cncnpi 23243  df-cnp 23193  iscnp 23202  iscnp2 23204
[Munkres] p. 127Theorem 10.1metcn 24508
[Munkres] p. 128Theorem 10.3metcn4 25278
[Nathanson] p. 123Remarkreprgt 34765  reprinfz1 34766  reprlt 34763
[Nathanson] p. 123Definitiondf-repr 34753
[Nathanson] p. 123Chapter 5.1circlemethnat 34785
[Nathanson] p. 123Propositionbreprexp 34777  breprexpnat 34778  itgexpif 34750
[NielsenChuang] p. 195Equation 4.73unierri 32175
[OeSilva] p. 2042Section 2ax-bgbltosilva 48280
[Pfenning] p. 17Definition XMnatded 30473
[Pfenning] p. 17Definition NNCnatded 30473  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30473
[Pfenning] p. 18Rule"natded 30473
[Pfenning] p. 18Definition /\Inatded 30473
[Pfenning] p. 18Definition ` `Enatded 30473  natded 30473  natded 30473  natded 30473  natded 30473
[Pfenning] p. 18Definition ` `Inatded 30473  natded 30473  natded 30473  natded 30473  natded 30473
[Pfenning] p. 18Definition ` `ELnatded 30473
[Pfenning] p. 18Definition ` `ERnatded 30473
[Pfenning] p. 18Definition ` `Ea,unatded 30473
[Pfenning] p. 18Definition ` `IRnatded 30473
[Pfenning] p. 18Definition ` `Ianatded 30473
[Pfenning] p. 127Definition =Enatded 30473
[Pfenning] p. 127Definition =Inatded 30473
[Ponnusamy] p. 361Theorem 6.44cphip0l 25169  df-dip 30772  dip0l 30789  ip0l 21616
[Ponnusamy] p. 361Equation 6.45cphipval 25210  ipval 30774
[Ponnusamy] p. 362Equation I1dipcj 30785  ipcj 21614
[Ponnusamy] p. 362Equation I3cphdir 25172  dipdir 30913  ipdir 21619  ipdiri 30901
[Ponnusamy] p. 362Equation I4ipidsq 30781  nmsq 25161
[Ponnusamy] p. 362Equation 6.46ip0i 30896
[Ponnusamy] p. 362Equation 6.47ip1i 30898
[Ponnusamy] p. 362Equation 6.48ip2i 30899
[Ponnusamy] p. 363Equation I2cphass 25178  dipass 30916  ipass 21625  ipassi 30912
[Prugovecki] p. 186Definition of brabraval 32015  df-bra 31921
[Prugovecki] p. 376Equation 8.1df-kb 31922  kbval 32025
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32453
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40334
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32467  atcvat4i 32468  cvrat3 39888  cvrat4 39889  lsatcvat3 39498
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32353  cvrval 39715  df-cv 32350  df-lcv 39465  lspsncv0 21144
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40346
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40347
[Quine] p. 16Definition 2.1df-clab 2716  rabid 3411  rabidd 45585  wl-df.clab 37823
[Quine] p. 17Definition 2.1''dfsb7 2286
[Quine] p. 18Definition 2.7df-cleq 2729  wl-df.cleq 37824
[Quine] p. 19Definition 2.9conventions 30470  df-v 3432
[Quine] p. 34Theorem 5.1eqabb 2876
[Quine] p. 35Theorem 5.2abid1 2873  abid2f 2930
[Quine] p. 40Theorem 6.1sb5 2283
[Quine] p. 40Theorem 6.2sb6 2091  sbalex 2250
[Quine] p. 41Theorem 6.3df-clel 2812  wl-df.clel 37827
[Quine] p. 41Theorem 6.4eqid 2737  eqid1 30537
[Quine] p. 41Theorem 6.5eqcom 2744
[Quine] p. 42Theorem 6.6df-sbc 3730
[Quine] p. 42Theorem 6.7dfsbcq 3731  dfsbcq2 3732
[Quine] p. 43Theorem 6.8vex 3434
[Quine] p. 43Theorem 6.9isset 3444
[Quine] p. 44Theorem 7.3spcgf 3534  spcgv 3539  spcimgf 3496
[Quine] p. 44Theorem 6.11spsbc 3742  spsbcd 3743
[Quine] p. 44Theorem 6.12elex 3451
[Quine] p. 44Theorem 6.13elab 3623  elabg 3620  elabgf 3618
[Quine] p. 44Theorem 6.14noel 4279
[Quine] p. 48Theorem 7.2snprc 4662
[Quine] p. 48Definition 7.1df-pr 4571  df-sn 4569
[Quine] p. 49Theorem 7.4snss 4729  snssg 4728
[Quine] p. 49Theorem 7.5prss 4764  prssg 4763
[Quine] p. 49Theorem 7.6prid1 4707  prid1g 4705  prid2 4708  prid2g 4706  snid 4607  snidg 4605
[Quine] p. 51Theorem 7.12snex 5382
[Quine] p. 51Theorem 7.13prex 5381
[Quine] p. 53Theorem 8.2unisn 4870  unisnALT 45352  unisng 4869
[Quine] p. 53Theorem 8.3uniun 4874
[Quine] p. 54Theorem 8.6elssuni 4882
[Quine] p. 54Theorem 8.7uni0 4879
[Quine] p. 56Theorem 8.17uniabio 6469
[Quine] p. 56Definition 8.18dfaiota2 47528  dfiota2 6456
[Quine] p. 57Theorem 8.19aiotaval 47537  iotaval 6473
[Quine] p. 57Theorem 8.22iotanul 6479
[Quine] p. 58Theorem 8.23iotaex 6475
[Quine] p. 58Definition 9.1df-op 4575
[Quine] p. 61Theorem 9.5opabid 5480  opabidw 5479  opelopab 5497  opelopaba 5491  opelopabaf 5499  opelopabf 5500  opelopabg 5493  opelopabga 5488  opelopabgf 5495  oprabid 7399  oprabidw 7398
[Quine] p. 64Definition 9.11df-xp 5637
[Quine] p. 64Definition 9.12df-cnv 5639
[Quine] p. 64Definition 9.15df-id 5526
[Quine] p. 65Theorem 10.3fun0 6564
[Quine] p. 65Theorem 10.4funi 6531
[Quine] p. 65Theorem 10.5funsn 6552  funsng 6550
[Quine] p. 65Definition 10.1df-fun 6501
[Quine] p. 65Definition 10.2args 6058  dffv4 6838
[Quine] p. 68Definition 10.11conventions 30470  df-fv 6507  fv2 6836
[Quine] p. 124Theorem 17.3nn0opth2 14234  nn0opth2i 14233  nn0opthi 14232  omopthi 8597
[Quine] p. 177Definition 25.2df-rdg 8349
[Quine] p. 232Equation icarddom 10476
[Quine] p. 284Axiom 39(vi)funimaex 6587  funimaexg 6586
[Quine] p. 331Axiom system NFru 3727
[ReedSimon] p. 36Definition (iii)ax-his3 31155
[ReedSimon] p. 63Exercise 4(a)df-dip 30772  polid 31230  polid2i 31228  polidi 31229
[ReedSimon] p. 63Exercise 4(b)df-ph 30884
[ReedSimon] p. 195Remarklnophm 32090  lnophmi 32089
[Retherford] p. 49Exercise 1(i)leopadd 32203
[Retherford] p. 49Exercise 1(ii)leopmul 32205  leopmuli 32204
[Retherford] p. 49Exercise 1(iv)leoptr 32208
[Retherford] p. 49Definition VI.1df-leop 31923  leoppos 32197
[Retherford] p. 49Exercise 1(iii)leoptri 32207
[Retherford] p. 49Definition of operator orderingleop3 32196
[Ribenboim] p. 181Remarknprmdvdsfacm1 48081
[Ribenboim], p. 181Statementppivalnn 48089
[Roman] p. 4Definitiondf-dmat 22455  df-dmatalt 48868
[Roman] p. 18Part Preliminariesdf-rng 20134
[Roman] p. 19Part Preliminariesdf-ring 20216
[Roman] p. 46Theorem 1.6isldepslvec2 48955
[Roman] p. 112Noteisldepslvec2 48955  ldepsnlinc 48978  zlmodzxznm 48967
[Roman] p. 112Examplezlmodzxzequa 48966  zlmodzxzequap 48969  zlmodzxzldep 48974
[Roman] p. 170Theorem 7.8cayleyhamilton 22855
[Rosenlicht] p. 80Theoremheicant 37976
[Rosser] p. 281Definitiondf-op 4575
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34789
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34790
[Rotman] p. 28Remarkpgrpgt2nabl 48836  pmtr3ncom 19450
[Rotman] p. 31Theorem 3.4symggen2 19446
[Rotman] p. 42Theorem 3.15cayley 19389  cayleyth 19390
[Rudin] p. 164Equation 27efcan 16061
[Rudin] p. 164Equation 30efzval 16069
[Rudin] p. 167Equation 48absefi 16163
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1773
[Sanford] p. 39Rule 4mptxor 1771
[Sanford] p. 40Rule 1mptnan 1770
[Schechter] p. 51Definition of antisymmetryintasym 6079
[Schechter] p. 51Definition of irreflexivityintirr 6082
[Schechter] p. 51Definition of symmetrycnvsym 6078
[Schechter] p. 51Definition of transitivitycotr 6076
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17548
[Schechter] p. 79Definition of Moore closuredf-mrc 17549
[Schechter] p. 82Section 4.5df-mrc 17549
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17551
[Schechter] p. 139Definition AC3dfac9 10059
[Schechter] p. 141Definition (MC)dfac11 43490
[Schechter] p. 149Axiom DC1ax-dc 10368  axdc3 10376
[Schechter] p. 187Definition of "ring with unit"isring 20218  isrngo 38218
[Schechter] p. 276Remark 11.6.espan0 31613
[Schechter] p. 276Definition of spandf-span 31380  spanval 31404
[Schechter] p. 428Definition 15.35bastop1 22958
[Schloeder] p. 1Lemma 1.3onelon 6349  onelord 43679  ordelon 6348  ordelord 6346
[Schloeder] p. 1Lemma 1.7onepsuc 43680  sucidg 6407
[Schloeder] p. 1Remark 1.50elon 6379  onsuc 7764  ord0 6378  ordsuci 7762
[Schloeder] p. 1Theorem 1.9epsoon 43681
[Schloeder] p. 1Definition 1.1dftr5 5197
[Schloeder] p. 1Definition 1.2dford3 43456  elon2 6335
[Schloeder] p. 1Definition 1.4df-suc 6330
[Schloeder] p. 1Definition 1.6epel 5534  epelg 5532
[Schloeder] p. 1Theorem 1.9(i)elirr 9514  epirron 43682  ordirr 6342
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43684  oneptr 43683  ontr1 6371
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6367  oneptri 43685  ordtri3or 6356
[Schloeder] p. 2Lemma 1.10ondif1 8436  ord0eln0 6380
[Schloeder] p. 2Lemma 1.13elsuci 6393  onsucss 43694  trsucss 6414
[Schloeder] p. 2Lemma 1.14ordsucss 7769
[Schloeder] p. 2Lemma 1.15onnbtwn 6420  ordnbtwn 6419
[Schloeder] p. 2Lemma 1.16orddif0suc 43696  ordnexbtwnsuc 43695
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10323  onsucf1lem 43697  onsucf1o 43700  onsucf1olem 43698  onsucrn 43699
[Schloeder] p. 2Lemma 1.18dflim7 43701
[Schloeder] p. 2Remark 1.12ordzsl 7796
[Schloeder] p. 2Theorem 1.10ondif1i 43690  ordne0gt0 43689
[Schloeder] p. 2Definition 1.11dflim6 43692  limnsuc 43693  onsucelab 43691
[Schloeder] p. 3Remark 1.21omex 9564
[Schloeder] p. 3Theorem 1.19tfinds 7811
[Schloeder] p. 3Theorem 1.22omelon 9567  ordom 7827
[Schloeder] p. 3Definition 1.20dfom3 9568
[Schloeder] p. 4Lemma 2.21onn 8576
[Schloeder] p. 4Lemma 2.7ssonuni 7734  ssorduni 7733
[Schloeder] p. 4Remark 2.4oa1suc 8466
[Schloeder] p. 4Theorem 1.23dfom5 9571  limom 7833
[Schloeder] p. 4Definition 2.1df-1o 8405  df1o2 8412
[Schloeder] p. 4Definition 2.3oa0 8451  oa0suclim 43703  oalim 8467  oasuc 8459
[Schloeder] p. 4Definition 2.5om0 8452  om0suclim 43704  omlim 8468  omsuc 8461
[Schloeder] p. 4Definition 2.6oe0 8457  oe0m1 8456  oe0suclim 43705  oelim 8469  oesuc 8462
[Schloeder] p. 5Lemma 2.10onsupuni 43657
[Schloeder] p. 5Lemma 2.11onsupsucismax 43707
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43708
[Schloeder] p. 5Lemma 2.13limexissup 43709  limexissupab 43711  limiun 43710  limuni 6386
[Schloeder] p. 5Lemma 2.14oa0r 8473
[Schloeder] p. 5Lemma 2.15om1 8477  om1om1r 43712  om1r 8478
[Schloeder] p. 5Remark 2.8oacl 8470  oaomoecl 43706  oecl 8472  omcl 8471
[Schloeder] p. 5Definition 2.9onsupintrab 43659
[Schloeder] p. 6Lemma 2.16oe1 8479
[Schloeder] p. 6Lemma 2.17oe1m 8480
[Schloeder] p. 6Lemma 2.18oe0rif 43713
[Schloeder] p. 6Theorem 2.19oasubex 43714
[Schloeder] p. 6Theorem 2.20nnacl 8547  nnamecl 43715  nnecl 8549  nnmcl 8548
[Schloeder] p. 7Lemma 3.1onsucwordi 43716
[Schloeder] p. 7Lemma 3.2oaword1 8487
[Schloeder] p. 7Lemma 3.3oaword2 8488
[Schloeder] p. 7Lemma 3.4oalimcl 8495
[Schloeder] p. 7Lemma 3.5oaltublim 43718
[Schloeder] p. 8Lemma 3.6oaordi3 43719
[Schloeder] p. 8Lemma 3.81oaomeqom 43721
[Schloeder] p. 8Lemma 3.10oa00 8494
[Schloeder] p. 8Lemma 3.11omge1 43725  omword1 8508
[Schloeder] p. 8Remark 3.9oaordnr 43724  oaordnrex 43723
[Schloeder] p. 8Theorem 3.7oaord3 43720
[Schloeder] p. 9Lemma 3.12omge2 43726  omword2 8509
[Schloeder] p. 9Lemma 3.13omlim2 43727
[Schloeder] p. 9Lemma 3.14omord2lim 43728
[Schloeder] p. 9Lemma 3.15omord2i 43729  omordi 8501
[Schloeder] p. 9Theorem 3.16omord 8503  omord2com 43730
[Schloeder] p. 10Lemma 3.172omomeqom 43731  df-2o 8406
[Schloeder] p. 10Lemma 3.19oege1 43734  oewordi 8527
[Schloeder] p. 10Lemma 3.20oege2 43735  oeworde 8529
[Schloeder] p. 10Lemma 3.21rp-oelim2 43736
[Schloeder] p. 10Lemma 3.22oeord2lim 43737
[Schloeder] p. 10Remark 3.18omnord1 43733  omnord1ex 43732
[Schloeder] p. 11Lemma 3.23oeord2i 43738
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43740
[Schloeder] p. 11Remark 3.26oenord1 43744  oenord1ex 43743
[Schloeder] p. 11Theorem 4.1oaomoencom 43745
[Schloeder] p. 11Theorem 4.2oaass 8496
[Schloeder] p. 11Theorem 3.24oeord2com 43739
[Schloeder] p. 12Theorem 4.3odi 8514
[Schloeder] p. 13Theorem 4.4omass 8515
[Schloeder] p. 14Remark 4.6oenass 43747
[Schloeder] p. 14Theorem 4.7oeoa 8533
[Schloeder] p. 15Lemma 5.1cantnftermord 43748
[Schloeder] p. 15Lemma 5.2cantnfub 43749  cantnfub2 43750
[Schloeder] p. 16Theorem 5.3cantnf2 43753
[Schwabhauser] p. 10Axiom A1axcgrrflx 28983  axtgcgrrflx 28530
[Schwabhauser] p. 10Axiom A2axcgrtr 28984
[Schwabhauser] p. 10Axiom A3axcgrid 28985  axtgcgrid 28531
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28516
[Schwabhauser] p. 11Axiom A4axsegcon 28996  axtgsegcon 28532  df-trkgcb 28518
[Schwabhauser] p. 11Axiom A5ax5seg 29007  axtg5seg 28533  df-trkgcb 28518
[Schwabhauser] p. 11Axiom A6axbtwnid 29008  axtgbtwnid 28534  df-trkgb 28517
[Schwabhauser] p. 12Axiom A7axpasch 29010  axtgpasch 28535  df-trkgb 28517
[Schwabhauser] p. 12Axiom A8axlowdim2 29029  df-trkg2d 34809
[Schwabhauser] p. 13Axiom A8axtglowdim2 28538
[Schwabhauser] p. 13Axiom A9axtgupdim2 28539  df-trkg2d 34809
[Schwabhauser] p. 13Axiom A10axeuclid 29032  axtgeucl 28540  df-trkge 28519
[Schwabhauser] p. 13Axiom A11axcont 29045  axtgcont 28537  axtgcont1 28536  df-trkgb 28517
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36169
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36171
[Schwabhauser] p. 27Theorem 2.3cgrtr 36174
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36178
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36179  tgcgrcomimp 28545  tgcgrcoml 28547  tgcgrcomr 28546
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36184  tgcgrtriv 28552
[Schwabhauser] p. 28Theorem 2.105segofs 36188  tg5segofs 34817
[Schwabhauser] p. 28Definition 2.10df-afs 34814  df-ofs 36165
[Schwabhauser] p. 29Theorem 2.11cgrextend 36190  tgcgrextend 28553
[Schwabhauser] p. 29Theorem 2.12segconeq 36192  tgsegconeq 28554
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36204  btwntriv2 36194  tgbtwntriv2 28555
[Schwabhauser] p. 30Theorem 3.2btwncomim 36195  tgbtwncom 28556
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36198  tgbtwntriv1 28559
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36199  tgbtwnswapid 28560
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36205  btwnintr 36201  tgbtwnexch2 28564  tgbtwnintr 28561
[Schwabhauser] p. 30Theorem 3.6btwnexch 36207  btwnexch3 36202  tgbtwnexch 28566  tgbtwnexch3 28562
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36206  tgbtwnouttr 28565  tgbtwnouttr2 28563
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29028
[Schwabhauser] p. 32Theorem 3.14btwndiff 36209  tgbtwndiff 28574
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28567  trisegint 36210
[Schwabhauser] p. 34Theorem 4.2ifscgr 36226  tgifscgr 28576
[Schwabhauser] p. 34Theorem 4.11colcom 28626  colrot1 28627  colrot2 28628  lncom 28690  lnrot1 28691  lnrot2 28692
[Schwabhauser] p. 34Definition 4.1df-ifs 36222
[Schwabhauser] p. 35Theorem 4.3cgrsub 36227  tgcgrsub 28577
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36237  tgcgrxfr 28586
[Schwabhauser] p. 35Statement 4.4ercgrg 28585
[Schwabhauser] p. 35Definition 4.4df-cgr3 36223  df-cgrg 28579
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28579
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36238  tgbtwnxfr 28598
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36244  colinearperm2 36246  colinearperm3 36245  colinearperm4 36247  colinearperm5 36248
[Schwabhauser] p. 36Definition 4.8df-ismt 28601
[Schwabhauser] p. 36Definition 4.10df-colinear 36221  tgellng 28621  tglng 28614
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36249
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36257  lnxfr 28634
[Schwabhauser] p. 37Theorem 4.14lineext 36258  lnext 28635
[Schwabhauser] p. 37Theorem 4.16fscgr 36262  tgfscgr 28636
[Schwabhauser] p. 37Theorem 4.17linecgr 36263  lncgr 28637
[Schwabhauser] p. 37Definition 4.15df-fs 36224
[Schwabhauser] p. 38Theorem 4.18lineid 36265  lnid 28638
[Schwabhauser] p. 38Theorem 4.19idinside 36266  tgidinside 28639
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36283  tgbtwnconn1 28643
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36284  tgbtwnconn2 28644
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36285  tgbtwnconn3 28645
[Schwabhauser] p. 41Theorem 5.5brsegle2 36291
[Schwabhauser] p. 41Definition 5.4df-segle 36289  legov 28653
[Schwabhauser] p. 41Definition 5.5legov2 28654
[Schwabhauser] p. 42Remark 5.13legso 28667
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36292
[Schwabhauser] p. 42Theorem 5.7seglerflx 36294
[Schwabhauser] p. 42Theorem 5.8segletr 36296
[Schwabhauser] p. 42Theorem 5.9segleantisym 36297
[Schwabhauser] p. 42Theorem 5.10seglelin 36298
[Schwabhauser] p. 42Theorem 5.11seglemin 36295
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36300
[Schwabhauser] p. 42Proposition 5.7legid 28655
[Schwabhauser] p. 42Proposition 5.8legtrd 28657
[Schwabhauser] p. 42Proposition 5.9legtri3 28658
[Schwabhauser] p. 42Proposition 5.10legtrid 28659
[Schwabhauser] p. 42Proposition 5.11leg0 28660
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36307
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36308
[Schwabhauser] p. 43Theorem 6.4broutsideof 36303  df-outsideof 36302
[Schwabhauser] p. 43Definition 6.1broutsideof2 36304  ishlg 28670
[Schwabhauser] p. 44Theorem 6.4hlln 28675
[Schwabhauser] p. 44Theorem 6.5hlid 28677  outsideofrflx 36309
[Schwabhauser] p. 44Theorem 6.6hlcomb 28671  hlcomd 28672  outsideofcom 36310
[Schwabhauser] p. 44Theorem 6.7hltr 28678  outsideoftr 36311
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28686  outsideofeu 36313
[Schwabhauser] p. 44Definition 6.8df-ray 36320
[Schwabhauser] p. 45Part 2df-lines2 36321
[Schwabhauser] p. 45Theorem 6.13outsidele 36314
[Schwabhauser] p. 45Theorem 6.15lineunray 36329
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36330  tglineelsb2 28700
[Schwabhauser] p. 45Theorem 6.17linecom 36332  linerflx1 36331  linerflx2 36333  tglinecom 28703  tglinerflx1 28701  tglinerflx2 28702
[Schwabhauser] p. 45Theorem 6.18linethru 36335  tglinethru 28704
[Schwabhauser] p. 45Definition 6.14df-line2 36319  tglng 28614
[Schwabhauser] p. 45Proposition 6.13legbtwn 28662
[Schwabhauser] p. 46Theorem 6.19linethrueu 36338  tglinethrueu 28707
[Schwabhauser] p. 46Theorem 6.21lineintmo 36339  tglineineq 28711  tglineinteq 28713  tglineintmo 28710
[Schwabhauser] p. 46Theorem 6.23colline 28717
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28718
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28719
[Schwabhauser] p. 49Theorem 7.3mirinv 28734
[Schwabhauser] p. 49Theorem 7.7mirmir 28730
[Schwabhauser] p. 49Theorem 7.8mirreu3 28722
[Schwabhauser] p. 49Definition 7.5df-mir 28721  ismir 28727  mirbtwn 28726  mircgr 28725  mirfv 28724  mirval 28723
[Schwabhauser] p. 50Theorem 7.8mirreu 28732
[Schwabhauser] p. 50Theorem 7.9mireq 28733
[Schwabhauser] p. 50Theorem 7.10mirinv 28734
[Schwabhauser] p. 50Theorem 7.11mirf1o 28737
[Schwabhauser] p. 50Theorem 7.13miriso 28738
[Schwabhauser] p. 51Theorem 7.14mirmot 28743
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28740  mirbtwni 28739
[Schwabhauser] p. 51Theorem 7.16mircgrs 28741
[Schwabhauser] p. 51Theorem 7.17miduniq 28753
[Schwabhauser] p. 52Lemma 7.21symquadlem 28757
[Schwabhauser] p. 52Theorem 7.18miduniq1 28754
[Schwabhauser] p. 52Theorem 7.19miduniq2 28755
[Schwabhauser] p. 52Theorem 7.20colmid 28756
[Schwabhauser] p. 53Lemma 7.22krippen 28759
[Schwabhauser] p. 55Lemma 7.25midexlem 28760
[Schwabhauser] p. 57Theorem 8.2ragcom 28766
[Schwabhauser] p. 57Definition 8.1df-rag 28762  israg 28765
[Schwabhauser] p. 58Theorem 8.3ragcol 28767
[Schwabhauser] p. 58Theorem 8.4ragmir 28768
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28770
[Schwabhauser] p. 58Theorem 8.6ragflat2 28771
[Schwabhauser] p. 58Theorem 8.7ragflat 28772
[Schwabhauser] p. 58Theorem 8.8ragtriva 28773
[Schwabhauser] p. 58Theorem 8.9ragflat3 28774  ragncol 28777
[Schwabhauser] p. 58Theorem 8.10ragcgr 28775
[Schwabhauser] p. 59Theorem 8.12perpcom 28781
[Schwabhauser] p. 59Theorem 8.13ragperp 28785
[Schwabhauser] p. 59Theorem 8.14perpneq 28782
[Schwabhauser] p. 59Definition 8.11df-perpg 28764  isperp 28780
[Schwabhauser] p. 59Definition 8.13isperp2 28783
[Schwabhauser] p. 60Theorem 8.18foot 28790
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28798  colperpexlem2 28799
[Schwabhauser] p. 63Theorem 8.21colperpex 28801  colperpexlem3 28800
[Schwabhauser] p. 64Theorem 8.22mideu 28806  midex 28805
[Schwabhauser] p. 66Lemma 8.24opphllem 28803
[Schwabhauser] p. 67Theorem 9.2oppcom 28812
[Schwabhauser] p. 67Definition 9.1islnopp 28807
[Schwabhauser] p. 68Lemma 9.3opphllem2 28816
[Schwabhauser] p. 68Lemma 9.4opphllem5 28819  opphllem6 28820
[Schwabhauser] p. 69Theorem 9.5opphl 28822
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28535
[Schwabhauser] p. 70Theorem 9.6outpasch 28823
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28831
[Schwabhauser] p. 71Definition 9.7df-hpg 28826  hpgbr 28828
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28833
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28832
[Schwabhauser] p. 72Theorem 9.11hpgid 28834
[Schwabhauser] p. 72Theorem 9.12hpgcom 28835
[Schwabhauser] p. 72Theorem 9.13hpgtr 28836
[Schwabhauser] p. 73Theorem 9.18colopp 28837
[Schwabhauser] p. 73Theorem 9.19colhp 28838
[Schwabhauser] p. 88Theorem 10.2lmieu 28852
[Schwabhauser] p. 88Definition 10.1df-mid 28842
[Schwabhauser] p. 89Theorem 10.4lmicom 28856
[Schwabhauser] p. 89Theorem 10.5lmilmi 28857
[Schwabhauser] p. 89Theorem 10.6lmireu 28858
[Schwabhauser] p. 89Theorem 10.7lmieq 28859
[Schwabhauser] p. 89Theorem 10.8lmiinv 28860
[Schwabhauser] p. 89Theorem 10.9lmif1o 28863
[Schwabhauser] p. 89Theorem 10.10lmiiso 28865
[Schwabhauser] p. 89Definition 10.3df-lmi 28843
[Schwabhauser] p. 90Theorem 10.11lmimot 28866
[Schwabhauser] p. 91Theorem 10.12hypcgr 28869
[Schwabhauser] p. 92Theorem 10.14lmiopp 28870
[Schwabhauser] p. 92Theorem 10.15lnperpex 28871
[Schwabhauser] p. 92Theorem 10.16trgcopy 28872  trgcopyeu 28874
[Schwabhauser] p. 95Definition 11.2dfcgra2 28898
[Schwabhauser] p. 95Definition 11.3iscgra 28877
[Schwabhauser] p. 95Proposition 11.4cgracgr 28886
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28884  cgrahl2 28885
[Schwabhauser] p. 96Theorem 11.6cgraid 28887
[Schwabhauser] p. 96Theorem 11.9cgraswap 28888
[Schwabhauser] p. 97Theorem 11.7cgracom 28890
[Schwabhauser] p. 97Theorem 11.8cgratr 28891
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28894  cgrahl 28895
[Schwabhauser] p. 98Theorem 11.13sacgr 28899
[Schwabhauser] p. 98Theorem 11.14oacgr 28900
[Schwabhauser] p. 98Theorem 11.15acopy 28901  acopyeu 28902
[Schwabhauser] p. 101Theorem 11.24inagswap 28909
[Schwabhauser] p. 101Theorem 11.25inaghl 28913
[Schwabhauser] p. 101Definition 11.23isinag 28906
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28921
[Schwabhauser] p. 102Definition 11.27df-leag 28914  isleag 28915
[Schwabhauser] p. 107Theorem 11.49tgsas 28923  tgsas1 28922  tgsas2 28924  tgsas3 28925
[Schwabhauser] p. 108Theorem 11.50tgasa 28927  tgasa1 28926
[Schwabhauser] p. 109Theorem 11.51tgsss1 28928  tgsss2 28929  tgsss3 28930
[Shapiro] p. 230Theorem 6.5.1dchrhash 27234  dchrsum 27232  dchrsum2 27231  sumdchr 27235
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27236  sum2dchr 27237
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20043  ablfacrp2 20044
[Shapiro], p. 328Equation 9.2.4vmasum 27179
[Shapiro], p. 329Equation 9.2.7logfac2 27180
[Shapiro], p. 329Equation 9.2.9logfacrlim 27187
[Shapiro], p. 331Equation 9.2.13vmadivsum 27445
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27448
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27502  vmalogdivsum2 27501
[Shapiro], p. 375Theorem 9.4.1dirith 27492  dirith2 27491
[Shapiro], p. 375Equation 9.4.3rplogsum 27490  rpvmasum 27489  rpvmasum2 27475
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27450
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27488
[Shapiro], p. 377Lemma 9.4.1dchrisum 27455  dchrisumlem1 27452  dchrisumlem2 27453  dchrisumlem3 27454  dchrisumlema 27451
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27458
[Shapiro], p. 379Equation 9.4.16dchrmusum 27487  dchrmusumlem 27485  dchrvmasumlem 27486
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27457
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27459
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27483  dchrisum0re 27476  dchrisumn0 27484
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27469
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27473
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27474
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27529  pntrsumbnd2 27530  pntrsumo1 27528
[Shapiro], p. 405Equation 10.2.1mudivsum 27493
[Shapiro], p. 406Equation 10.2.6mulogsum 27495
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27497
[Shapiro], p. 407Equation 10.2.8mulog2sum 27500
[Shapiro], p. 418Equation 10.4.6logsqvma 27505
[Shapiro], p. 418Equation 10.4.8logsqvma2 27506
[Shapiro], p. 419Equation 10.4.10selberg 27511
[Shapiro], p. 420Equation 10.4.12selberg2lem 27513
[Shapiro], p. 420Equation 10.4.14selberg2 27514
[Shapiro], p. 422Equation 10.6.7selberg3 27522
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27523
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27520  selberg3lem2 27521
[Shapiro], p. 422Equation 10.4.23selberg4 27524
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27518
[Shapiro], p. 428Equation 10.6.2selbergr 27531
[Shapiro], p. 429Equation 10.6.8selberg3r 27532
[Shapiro], p. 430Equation 10.6.11selberg4r 27533
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27547
[Shapiro], p. 434Equation 10.6.27pntlema 27559  pntlemb 27560  pntlemc 27558  pntlemd 27557  pntlemg 27561
[Shapiro], p. 435Equation 10.6.29pntlema 27559
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27551
[Shapiro], p. 436Lemma 10.6.2pntibnd 27556
[Shapiro], p. 436Equation 10.6.34pntlema 27559
[Shapiro], p. 436Equation 10.6.35pntlem3 27572  pntleml 27574
[Stewart] p. 91Lemma 7.3constrss 33887
[Stewart] p. 92Definition 7.4.df-constr 33874
[Stewart] p. 96Theorem 7.10constraddcl 33906  constrinvcl 33917  constrmulcl 33915  constrnegcl 33907  constrsqrtcl 33923
[Stewart] p. 97Theorem 7.11constrextdg2 33893
[Stewart] p. 98Theorem 7.12constrext2chn 33903
[Stewart] p. 99Theorem 7.132sqr3nconstr 33925
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33935
[Stoll] p. 13Definition corresponds to dfsymdif3 4247
[Stoll] p. 16Exercise 4.40dif 4346  dif0 4319
[Stoll] p. 16Exercise 4.8difdifdir 4432
[Stoll] p. 17Theorem 5.1(5)unvdif 4416
[Stoll] p. 19Theorem 5.2(13)undm 4238
[Stoll] p. 19Theorem 5.2(13')indm 4239
[Stoll] p. 20Remarkinvdif 4220
[Stoll] p. 25Definition of ordered tripledf-ot 4577
[Stoll] p. 43Definitionuniiun 5002
[Stoll] p. 44Definitionintiin 5003
[Stoll] p. 45Definitiondf-iin 4937
[Stoll] p. 45Definition indexed uniondf-iun 4936
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4247
[Strang] p. 242Section 6.3expgrowth 44762
[Suppes] p. 22Theorem 2eq0 4291  eq0f 4288
[Suppes] p. 22Theorem 4eqss 3938  eqssd 3940  eqssi 3939
[Suppes] p. 23Theorem 5ss0 4343  ss0b 4342
[Suppes] p. 23Theorem 6sstr 3931  sstrALT2 45261
[Suppes] p. 23Theorem 7pssirr 4044
[Suppes] p. 23Theorem 8pssn2lp 4045
[Suppes] p. 23Theorem 9psstr 4048
[Suppes] p. 23Theorem 10pssss 4039
[Suppes] p. 25Theorem 12elin 3906  elun 4094
[Suppes] p. 26Theorem 15inidm 4168
[Suppes] p. 26Theorem 16in0 4336
[Suppes] p. 27Theorem 23unidm 4098
[Suppes] p. 27Theorem 24un0 4335
[Suppes] p. 27Theorem 25ssun1 4119
[Suppes] p. 27Theorem 26ssequn1 4127
[Suppes] p. 27Theorem 27unss 4131
[Suppes] p. 27Theorem 28indir 4227
[Suppes] p. 27Theorem 29undir 4228
[Suppes] p. 28Theorem 32difid 4317
[Suppes] p. 29Theorem 33difin 4213
[Suppes] p. 29Theorem 34indif 4221
[Suppes] p. 29Theorem 35undif1 4417
[Suppes] p. 29Theorem 36difun2 4422
[Suppes] p. 29Theorem 37difin0 4415
[Suppes] p. 29Theorem 38disjdif 4413
[Suppes] p. 29Theorem 39difundi 4231
[Suppes] p. 29Theorem 40difindi 4233
[Suppes] p. 30Theorem 41nalset 5250
[Suppes] p. 39Theorem 61uniss 4859
[Suppes] p. 39Theorem 65uniop 5470
[Suppes] p. 41Theorem 70intsn 4927
[Suppes] p. 42Theorem 71intpr 4925  intprg 4924
[Suppes] p. 42Theorem 73op1stb 5425
[Suppes] p. 42Theorem 78intun 4923
[Suppes] p. 44Definition 15(a)dfiun2 4975  dfiun2g 4973
[Suppes] p. 44Definition 15(b)dfiin2 4976
[Suppes] p. 47Theorem 86elpw 4546  elpw2 5276  elpw2g 5275  elpwg 4545  elpwgdedVD 45343
[Suppes] p. 47Theorem 87pwid 4564
[Suppes] p. 47Theorem 89pw0 4756
[Suppes] p. 48Theorem 90pwpw0 4757
[Suppes] p. 52Theorem 101xpss12 5646
[Suppes] p. 52Theorem 102xpindi 5789  xpindir 5790
[Suppes] p. 52Theorem 103xpundi 5700  xpundir 5701
[Suppes] p. 54Theorem 105elirrv 9512
[Suppes] p. 58Theorem 2relss 5738
[Suppes] p. 59Theorem 4eldm 5856  eldm2 5857  eldm2g 5855  eldmg 5854
[Suppes] p. 59Definition 3df-dm 5641
[Suppes] p. 60Theorem 6dmin 5867
[Suppes] p. 60Theorem 8rnun 6110
[Suppes] p. 60Theorem 9rnin 6111
[Suppes] p. 60Definition 4dfrn2 5844
[Suppes] p. 61Theorem 11brcnv 5838  brcnvg 5835
[Suppes] p. 62Equation 5elcnv 5832  elcnv2 5833
[Suppes] p. 62Theorem 12relcnv 6070
[Suppes] p. 62Theorem 15cnvin 6109
[Suppes] p. 62Theorem 16cnvun 6107
[Suppes] p. 63Definitiondftrrels2 38980
[Suppes] p. 63Theorem 20co02 6226
[Suppes] p. 63Theorem 21dmcoss 5931
[Suppes] p. 63Definition 7df-co 5640
[Suppes] p. 64Theorem 26cnvco 5841
[Suppes] p. 64Theorem 27coass 6231
[Suppes] p. 65Theorem 31resundi 5959
[Suppes] p. 65Theorem 34elima 6031  elima2 6032  elima3 6033  elimag 6030
[Suppes] p. 65Theorem 35imaundi 6114
[Suppes] p. 66Theorem 40dminss 6118
[Suppes] p. 66Theorem 41imainss 6119
[Suppes] p. 67Exercise 11cnvxp 6122
[Suppes] p. 81Definition 34dfec2 8646
[Suppes] p. 82Theorem 72elec 8690  elecALTV 38592  elecg 8688
[Suppes] p. 82Theorem 73eqvrelth 39016  erth 8698  erth2 8699
[Suppes] p. 83Theorem 74eqvreldisj 39019  erdisj 8701
[Suppes] p. 83Definition 35, df-parts 39189  dfmembpart2 39194
[Suppes] p. 89Theorem 96map0b 8831
[Suppes] p. 89Theorem 97map0 8835  map0g 8832
[Suppes] p. 89Theorem 98mapsn 8836  mapsnd 8834
[Suppes] p. 89Theorem 99mapss 8837
[Suppes] p. 91Definition 12(ii)alephsuc 9990
[Suppes] p. 91Definition 12(iii)alephlim 9989
[Suppes] p. 92Theorem 1enref 8932  enrefg 8931
[Suppes] p. 92Theorem 2ensym 8950  ensymb 8949  ensymi 8951
[Suppes] p. 92Theorem 3entr 8953
[Suppes] p. 92Theorem 4unen 8992
[Suppes] p. 94Theorem 15endom 8926
[Suppes] p. 94Theorem 16ssdomg 8947
[Suppes] p. 94Theorem 17domtr 8954
[Suppes] p. 95Theorem 18sbth 9035
[Suppes] p. 97Theorem 23canth2 9068  canth2g 9069
[Suppes] p. 97Definition 3brsdom2 9039  df-sdom 8896  dfsdom2 9038
[Suppes] p. 97Theorem 21(i)sdomirr 9052
[Suppes] p. 97Theorem 22(i)domnsym 9041
[Suppes] p. 97Theorem 21(ii)sdomnsym 9040
[Suppes] p. 97Theorem 22(ii)domsdomtr 9050
[Suppes] p. 97Theorem 22(iv)brdom2 8929
[Suppes] p. 97Theorem 21(iii)sdomtr 9053
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9048
[Suppes] p. 98Exercise 4fundmen 8978  fundmeng 8979
[Suppes] p. 98Exercise 6xpdom3 9013
[Suppes] p. 98Exercise 11sdomentr 9049
[Suppes] p. 104Theorem 37fofi 9223
[Suppes] p. 104Theorem 38pwfi 9229
[Suppes] p. 105Theorem 40pwfi 9229
[Suppes] p. 111Axiom for cardinal numberscarden 10473
[Suppes] p. 130Definition 3df-tr 5194
[Suppes] p. 132Theorem 9ssonuni 7734
[Suppes] p. 134Definition 6df-suc 6330
[Suppes] p. 136Theorem Schema 22findes 7851  finds 7847  finds1 7850  finds2 7849
[Suppes] p. 151Theorem 42isfinite 9573  isfinite2 9208  isfiniteg 9210  unbnn 9206
[Suppes] p. 162Definition 5df-ltnq 10841  df-ltpq 10833
[Suppes] p. 197Theorem Schema 4tfindes 7814  tfinds 7811  tfinds2 7815
[Suppes] p. 209Theorem 18oaord1 8486
[Suppes] p. 209Theorem 21oaword2 8488
[Suppes] p. 211Theorem 25oaass 8496
[Suppes] p. 225Definition 8iscard2 9900
[Suppes] p. 227Theorem 56ondomon 10485
[Suppes] p. 228Theorem 59harcard 9902
[Suppes] p. 228Definition 12(i)aleph0 9988
[Suppes] p. 228Theorem Schema 61onintss 6376
[Suppes] p. 228Theorem Schema 62onminesb 7747  onminsb 7748
[Suppes] p. 229Theorem 64alephval2 10495
[Suppes] p. 229Theorem 65alephcard 9992
[Suppes] p. 229Theorem 66alephord2i 9999
[Suppes] p. 229Theorem 67alephnbtwn 9993
[Suppes] p. 229Definition 12df-aleph 9864
[Suppes] p. 242Theorem 6weth 10417
[Suppes] p. 242Theorem 8entric 10479
[Suppes] p. 242Theorem 9carden 10473
[Szendrei] p. 11Line 6df-cloneop 35878
[Szendrei] p. 11Paragraph 3df-suppos 35882
[TakeutiZaring] p. 8Axiom 1ax-ext 2709
[TakeutiZaring] p. 13Definition 4.5df-cleq 2729  wl-df.cleq 37824
[TakeutiZaring] p. 13Proposition 4.6df-clel 2812  wl-df.clel 37827
[TakeutiZaring] p. 13Proposition 4.9cvjust 2731
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2757
[TakeutiZaring] p. 14Definition 4.16df-oprab 7371
[TakeutiZaring] p. 14Proposition 4.14ru 3727
[TakeutiZaring] p. 15Axiom 2zfpair 5364
[TakeutiZaring] p. 15Exercise 1elpr 4593  elpr2 4595  elpr2g 4594  elprg 4591
[TakeutiZaring] p. 15Exercise 2elsn 4583  elsn2 4610  elsn2g 4609  elsng 4582  velsn 4584
[TakeutiZaring] p. 15Exercise 3elop 5421
[TakeutiZaring] p. 15Exercise 4sneq 4578  sneqr 4784
[TakeutiZaring] p. 15Definition 5.1dfpr2 4589  dfsn2 4581  dfsn2ALT 4590
[TakeutiZaring] p. 16Axiom 3uniex 7695
[TakeutiZaring] p. 16Exercise 6opth 5430
[TakeutiZaring] p. 16Exercise 7opex 5417
[TakeutiZaring] p. 16Exercise 8rext 5401
[TakeutiZaring] p. 16Corollary 5.8unex 7698  unexg 7697
[TakeutiZaring] p. 16Definition 5.3dftp2 4636
[TakeutiZaring] p. 16Definition 5.5df-uni 4852
[TakeutiZaring] p. 16Definition 5.6df-in 3897  df-un 3895
[TakeutiZaring] p. 16Proposition 5.7unipr 4868  uniprg 4867
[TakeutiZaring] p. 17Axiom 4vpwex 5320
[TakeutiZaring] p. 17Exercise 1eltp 4634
[TakeutiZaring] p. 17Exercise 5elsuc 6396  elsucg 6394  sstr2 3929
[TakeutiZaring] p. 17Exercise 6uncom 4099
[TakeutiZaring] p. 17Exercise 7incom 4150
[TakeutiZaring] p. 17Exercise 8unass 4113
[TakeutiZaring] p. 17Exercise 9inass 4169
[TakeutiZaring] p. 17Exercise 10indi 4225
[TakeutiZaring] p. 17Exercise 11undi 4226
[TakeutiZaring] p. 17Definition 5.9df-pss 3910  df-ss 3907
[TakeutiZaring] p. 17Definition 5.10df-pw 4544
[TakeutiZaring] p. 18Exercise 7unss2 4128
[TakeutiZaring] p. 18Exercise 9dfss2 3908  sseqin2 4164
[TakeutiZaring] p. 18Exercise 10ssid 3945
[TakeutiZaring] p. 18Exercise 12inss1 4178  inss2 4179
[TakeutiZaring] p. 18Exercise 13nss 3987
[TakeutiZaring] p. 18Exercise 15unieq 4862
[TakeutiZaring] p. 18Exercise 18sspwb 5402  sspwimp 45344  sspwimpALT 45351  sspwimpALT2 45354  sspwimpcf 45346
[TakeutiZaring] p. 18Exercise 19pweqb 5409
[TakeutiZaring] p. 19Axiom 5ax-rep 5213
[TakeutiZaring] p. 20Definitiondf-rab 3391
[TakeutiZaring] p. 20Corollary 5.160ex 5243
[TakeutiZaring] p. 20Definition 5.12df-dif 3893
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 36835  dfnul2 4277
[TakeutiZaring] p. 20Proposition 5.15difid 4317
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4294  n0f 4290  neq0 4293  neq0f 4289
[TakeutiZaring] p. 21Axiom 6zfreg 9511
[TakeutiZaring] p. 21Axiom 6'zfregs 9653
[TakeutiZaring] p. 21Theorem 5.22setind 9668
[TakeutiZaring] p. 21Definition 5.20df-v 3432
[TakeutiZaring] p. 21Proposition 5.21vprc 5256
[TakeutiZaring] p. 22Exercise 10ss 4341
[TakeutiZaring] p. 22Exercise 3ssex 5263  ssexg 5265
[TakeutiZaring] p. 22Exercise 4inex1 5259
[TakeutiZaring] p. 22Exercise 5ruv 9522
[TakeutiZaring] p. 22Exercise 6elirr 9514
[TakeutiZaring] p. 22Exercise 7ssdif0 4307
[TakeutiZaring] p. 22Exercise 11difdif 4076
[TakeutiZaring] p. 22Exercise 13undif3 4241  undif3VD 45308
[TakeutiZaring] p. 22Exercise 14difss 4077
[TakeutiZaring] p. 22Exercise 15sscon 4084
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3053
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3063
[TakeutiZaring] p. 23Proposition 6.2xpex 7707  xpexg 7704
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5638
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6570
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6746  fun11 6573
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6512  svrelfun 6571
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5843
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5845
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5643
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5644
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5640
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6159  dfrel2 6154
[TakeutiZaring] p. 25Exercise 3xpss 5647
[TakeutiZaring] p. 25Exercise 5relun 5767
[TakeutiZaring] p. 25Exercise 6reluni 5774
[TakeutiZaring] p. 25Exercise 9inxp 5787
[TakeutiZaring] p. 25Exercise 12relres 5971
[TakeutiZaring] p. 25Exercise 13opelres 5951  opelresi 5953
[TakeutiZaring] p. 25Exercise 14dmres 5978
[TakeutiZaring] p. 25Exercise 15resss 5967
[TakeutiZaring] p. 25Exercise 17resabs1 5972
[TakeutiZaring] p. 25Exercise 18funres 6541
[TakeutiZaring] p. 25Exercise 24relco 6074
[TakeutiZaring] p. 25Exercise 29funco 6539
[TakeutiZaring] p. 25Exercise 30f1co 6748
[TakeutiZaring] p. 26Definition 6.10eu2 2610
[TakeutiZaring] p. 26Definition 6.11conventions 30470  df-fv 6507  fv3 6859
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7876  cnvexg 7875
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7860  dmexg 7852
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7861  rnexg 7853
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44880
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7871
[TakeutiZaring] p. 27Corollary 6.13fvex 6854
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47616  tz6.12-1-afv2 47683  tz6.12-1 6864  tz6.12-afv 47615  tz6.12-afv2 47682  tz6.12 6865  tz6.12c-afv2 47684  tz6.12c 6863
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47679  tz6.12-2 6828  tz6.12i-afv2 47685  tz6.12i 6867
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6502
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6503
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6505  wfo 6497
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6504  wf1 6496
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6506  wf1o 6498
[TakeutiZaring] p. 28Exercise 4eqfnfv 6984  eqfnfv2 6985  eqfnfv2f 6988
[TakeutiZaring] p. 28Exercise 5fvco 6939
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7172
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7170
[TakeutiZaring] p. 29Exercise 9funimaex 6587  funimaexg 6586
[TakeutiZaring] p. 29Definition 6.18df-br 5087
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5540
[TakeutiZaring] p. 30Definition 6.21dffr2 5592  dffr3 6065  eliniseg 6060  iniseg 6063
[TakeutiZaring] p. 30Definition 6.22df-eprel 5531
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5608  fr3nr 7726  frirr 5607
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5584
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7728
[TakeutiZaring] p. 31Exercise 1frss 5595
[TakeutiZaring] p. 31Exercise 4wess 5617
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6312  tz6.26i 6313  wefrc 5625  wereu2 5628
[TakeutiZaring] p. 32Theorem 6.27wfi 6314  wfii 6315
[TakeutiZaring] p. 32Definition 6.28df-isom 6508
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7284
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7285
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7291
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7292
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7293
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7297
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7304
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7306
[TakeutiZaring] p. 35Notationwtr 5193
[TakeutiZaring] p. 35Theorem 7.2trelpss 44881  tz7.2 5614
[TakeutiZaring] p. 35Definition 7.1dftr3 5198
[TakeutiZaring] p. 36Proposition 7.4ordwe 6337
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6345
[TakeutiZaring] p. 36Proposition 7.6ordelord 6346  ordelordALT 44964  ordelordALTVD 45293
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6352  ordelssne 6351
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6350
[TakeutiZaring] p. 37Proposition 7.9ordin 6354
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7736
[TakeutiZaring] p. 38Corollary 7.15ordsson 7737
[TakeutiZaring] p. 38Definition 7.11df-on 6328
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6356
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44976  ordon 7731
[TakeutiZaring] p. 38Proposition 7.13onprc 7732
[TakeutiZaring] p. 39Theorem 7.17tfi 7804
[TakeutiZaring] p. 40Exercise 3ontr2 6372
[TakeutiZaring] p. 40Exercise 7dftr2 5195
[TakeutiZaring] p. 40Exercise 9onssmin 7746
[TakeutiZaring] p. 40Exercise 11unon 7782
[TakeutiZaring] p. 40Exercise 12ordun 6430
[TakeutiZaring] p. 40Exercise 14ordequn 6429
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7733
[TakeutiZaring] p. 40Proposition 7.20elssuni 4882
[TakeutiZaring] p. 41Definition 7.22df-suc 6330
[TakeutiZaring] p. 41Proposition 7.23sssucid 6406  sucidg 6407
[TakeutiZaring] p. 41Proposition 7.24onsuc 7764
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6420  ordnbtwn 6419
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7779
[TakeutiZaring] p. 42Exercise 1df-lim 6329
[TakeutiZaring] p. 42Exercise 4omssnlim 7832
[TakeutiZaring] p. 42Exercise 7ssnlim 7837
[TakeutiZaring] p. 42Exercise 8onsucssi 7792  ordelsuc 7771
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7773
[TakeutiZaring] p. 42Definition 7.27nlimon 7802
[TakeutiZaring] p. 42Definition 7.28dfom2 7819
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7840
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7841
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7842
[TakeutiZaring] p. 43Remarkomon 7829
[TakeutiZaring] p. 43Axiom 7inf3 9556  omex 9564
[TakeutiZaring] p. 43Theorem 7.32ordom 7827
[TakeutiZaring] p. 43Corollary 7.31find 7846
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7843
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7844
[TakeutiZaring] p. 44Exercise 1limomss 7822
[TakeutiZaring] p. 44Exercise 2int0 4905
[TakeutiZaring] p. 44Exercise 3trintss 5212
[TakeutiZaring] p. 44Exercise 4intss1 4906
[TakeutiZaring] p. 44Exercise 5intex 5286
[TakeutiZaring] p. 44Exercise 6oninton 7749
[TakeutiZaring] p. 44Exercise 11ordintdif 6375
[TakeutiZaring] p. 44Definition 7.35df-int 4891
[TakeutiZaring] p. 44Proposition 7.34noinfep 9581
[TakeutiZaring] p. 45Exercise 4onint 7744
[TakeutiZaring] p. 47Lemma 1tfrlem1 8315
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8336
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8337
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8338
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8345  tz7.44-2 8346  tz7.44-3 8347
[TakeutiZaring] p. 50Exercise 1smogt 8307
[TakeutiZaring] p. 50Exercise 3smoiso 8302
[TakeutiZaring] p. 50Definition 7.46df-smo 8286
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8384  tz7.49c 8385
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8382
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8381
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8383
[TakeutiZaring] p. 53Proposition 7.532eu5 2657
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9933
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9934
[TakeutiZaring] p. 56Definition 8.1oalim 8467  oasuc 8459
[TakeutiZaring] p. 57Remarktfindsg 7812
[TakeutiZaring] p. 57Proposition 8.2oacl 8470
[TakeutiZaring] p. 57Proposition 8.3oa0 8451  oa0r 8473
[TakeutiZaring] p. 57Proposition 8.16omcl 8471
[TakeutiZaring] p. 58Corollary 8.5oacan 8483
[TakeutiZaring] p. 58Proposition 8.4nnaord 8555  nnaordi 8554  oaord 8482  oaordi 8481
[TakeutiZaring] p. 59Proposition 8.6iunss2 4993  uniss2 4885
[TakeutiZaring] p. 59Proposition 8.7oawordri 8485
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8490  oawordex 8492
[TakeutiZaring] p. 59Proposition 8.9nnacl 8547
[TakeutiZaring] p. 59Proposition 8.10oaabs 8584
[TakeutiZaring] p. 60Remarkoancom 9572
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8495
[TakeutiZaring] p. 62Exercise 1nnarcl 8552
[TakeutiZaring] p. 62Exercise 5oaword1 8487
[TakeutiZaring] p. 62Definition 8.15om0x 8454  omlim 8468  omsuc 8461
[TakeutiZaring] p. 62Definition 8.15(a)om0 8452
[TakeutiZaring] p. 63Proposition 8.17nnecl 8549  nnmcl 8548
[TakeutiZaring] p. 63Proposition 8.19nnmord 8568  nnmordi 8567  omord 8503  omordi 8501
[TakeutiZaring] p. 63Proposition 8.20omcan 8504
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8572  omwordri 8507
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8474
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8477  om1r 8478
[TakeutiZaring] p. 64Proposition 8.22om00 8510
[TakeutiZaring] p. 64Proposition 8.23omordlim 8512
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8513
[TakeutiZaring] p. 64Proposition 8.25odi 8514
[TakeutiZaring] p. 65Theorem 8.26omass 8515
[TakeutiZaring] p. 67Definition 8.30nnesuc 8544  oe0 8457  oelim 8469  oesuc 8462  onesuc 8465
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8455
[TakeutiZaring] p. 67Proposition 8.32oen0 8522
[TakeutiZaring] p. 67Proposition 8.33oeordi 8523
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8456
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8480
[TakeutiZaring] p. 68Corollary 8.34oeord 8524
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8530
[TakeutiZaring] p. 68Proposition 8.35oewordri 8528
[TakeutiZaring] p. 68Proposition 8.37oeworde 8529
[TakeutiZaring] p. 69Proposition 8.41oeoa 8533
[TakeutiZaring] p. 70Proposition 8.42oeoe 8535
[TakeutiZaring] p. 73Theorem 9.1trcl 9649  tz9.1 9650
[TakeutiZaring] p. 76Definition 9.9df-r1 9688  r10 9692  r1lim 9696  r1limg 9695  r1suc 9694  r1sucg 9693
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9704  r1ord2 9705  r1ordg 9702
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9714
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9739  tz9.13 9715  tz9.13g 9716
[TakeutiZaring] p. 79Definition 9.14df-rank 9689  rankval 9740  rankvalb 9721  rankvalg 9741
[TakeutiZaring] p. 79Proposition 9.16rankel 9763  rankelb 9748
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9777  rankval3 9764  rankval3b 9750
[TakeutiZaring] p. 79Proposition 9.18rankonid 9753
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9719
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9758  rankr1c 9745  rankr1g 9756
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9759
[TakeutiZaring] p. 80Exercise 1rankss 9773  rankssb 9772
[TakeutiZaring] p. 80Exercise 2unbndrank 9766
[TakeutiZaring] p. 80Proposition 9.19bndrank 9765
[TakeutiZaring] p. 83Axiom of Choiceac4 10397  dfac3 10043
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9952  numth 10394  numth2 10393
[TakeutiZaring] p. 85Definition 10.4cardval 10468
[TakeutiZaring] p. 85Proposition 10.5cardid 10469  cardid2 9877
[TakeutiZaring] p. 85Proposition 10.9oncard 9884
[TakeutiZaring] p. 85Proposition 10.10carden 10473
[TakeutiZaring] p. 85Proposition 10.11cardidm 9883
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9868
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9889
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9881
[TakeutiZaring] p. 87Proposition 10.15pwen 9088
[TakeutiZaring] p. 88Exercise 1en0 8965
[TakeutiZaring] p. 88Exercise 7infensuc 9093
[TakeutiZaring] p. 89Exercise 10omxpen 9017
[TakeutiZaring] p. 90Corollary 10.23cardnn 9887
[TakeutiZaring] p. 90Definition 10.27alephiso 10020
[TakeutiZaring] p. 90Proposition 10.20nneneq 9140
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9148
[TakeutiZaring] p. 90Proposition 10.26alephprc 10021
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9145
[TakeutiZaring] p. 91Exercise 2alephle 10010
[TakeutiZaring] p. 91Exercise 3aleph0 9988
[TakeutiZaring] p. 91Exercise 4cardlim 9896
[TakeutiZaring] p. 91Exercise 7infpss 10138
[TakeutiZaring] p. 91Exercise 8infcntss 9233
[TakeutiZaring] p. 91Definition 10.29df-fin 8897  isfi 8922
[TakeutiZaring] p. 92Proposition 10.32onfin 9149
[TakeutiZaring] p. 92Proposition 10.34imadomg 10456
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9010
[TakeutiZaring] p. 93Proposition 10.35fodomb 10448
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10108  unxpdom 9169
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9898  cardsdomelir 9897
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9171
[TakeutiZaring] p. 94Proposition 10.39infxpen 9936
[TakeutiZaring] p. 95Definition 10.42df-map 8775
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10484  infxpidm2 9939
[TakeutiZaring] p. 95Proposition 10.41infdju 10129  infxp 10136
[TakeutiZaring] p. 96Proposition 10.44pw2en 9022  pw2f1o 9020
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9081
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10409
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10404  ac6s5 10413
[TakeutiZaring] p. 98Theorem 10.47unidom 10465
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10466  uniimadomf 10467
[TakeutiZaring] p. 100Definition 11.1cfcof 10196
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10191
[TakeutiZaring] p. 102Exercise 1cfle 10176
[TakeutiZaring] p. 102Exercise 2cf0 10173
[TakeutiZaring] p. 102Exercise 3cfsuc 10179
[TakeutiZaring] p. 102Exercise 4cfom 10186
[TakeutiZaring] p. 102Proposition 11.9coftr 10195
[TakeutiZaring] p. 103Theorem 11.15alephreg 10505
[TakeutiZaring] p. 103Proposition 11.11cardcf 10174
[TakeutiZaring] p. 103Proposition 11.13alephsing 10198
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10019
[TakeutiZaring] p. 104Proposition 11.16carduniima 10018
[TakeutiZaring] p. 104Proposition 11.18alephfp 10030  alephfp2 10031
[TakeutiZaring] p. 106Theorem 11.20gchina 10622
[TakeutiZaring] p. 106Theorem 11.21mappwen 10034
[TakeutiZaring] p. 107Theorem 11.26konigth 10492
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10506
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10507
[Tarski] p. 67Axiom B5ax-c5 39329
[Tarski] p. 67Scheme B5sp 2191
[Tarski] p. 68Lemma 6avril1 30533  equid 2014
[Tarski] p. 69Lemma 7equcomi 2019
[Tarski] p. 70Lemma 14spim 2392  spime 2394  spimew 1973
[Tarski] p. 70Lemma 16ax-12 2185  ax-c15 39335  ax12i 1968
[Tarski] p. 70Lemmas 16 and 17sb6 2091
[Tarski] p. 75Axiom B7ax6v 1970
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1912  ax5ALT 39353
[Tarski], p. 75Scheme B8 of system S2ax-7 2010  ax-8 2116  ax-9 2124
[Tarski1999] p. 178Axiom 4axtgsegcon 28532
[Tarski1999] p. 178Axiom 5axtg5seg 28533
[Tarski1999] p. 179Axiom 7axtgpasch 28535
[Tarski1999] p. 180Axiom 7.1axtgpasch 28535
[Tarski1999] p. 185Axiom 11axtgcont1 28536
[Truss] p. 114Theorem 5.18ruc 16210
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37980
[Viaclovsky8] p. 3Proposition 7ismblfin 37982
[Weierstrass] p. 272Definitiondf-mdet 22550  mdetuni 22587
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 904
[WhiteheadRussell] p. 96Axiom *1.3olc 869
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 870
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 920
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 970
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 37761
[WhiteheadRussell] p. 100Theorem *2.05frege5 44227  imim2 58  wl-luk-imim2 37756
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47461  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 897
[WhiteheadRussell] p. 101Theorem *2.06barbara 2664  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 903
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37759
[WhiteheadRussell] p. 101Theorem *2.11exmid 895
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 898
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 45353  wl-luk-notnotr 37760
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44257  axfrege28 44256  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 868
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 925
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37753
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 890
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 942
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30471  pm2.27 42  wl-luk-pm2.27 37751
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 923
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38692
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 924
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 972
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 973
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 971
[WhiteheadRussell] p. 105Definition *2.33df-3or 1088
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 907
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 908
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 945
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 882
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 883
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 884
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 885
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 886
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 852
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 853
[WhiteheadRussell] p. 107Theorem *2.55orel1 889
[WhiteheadRussell] p. 107Theorem *2.56orel2 891
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 900
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 943
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 944
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 892  pm2.67 893
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 899
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 975
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 901
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 976
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 977
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 934
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 932
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 974
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 978
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 933
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 994
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 995
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 996
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 997
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 998
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 471
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 459
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 402
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 803
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 448
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 449
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 482  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 484  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 765
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 766
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 808
[WhiteheadRussell] p. 113Fact)pm3.45 623
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 810
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 963  pm3.44 962
[WhiteheadRussell] p. 113Theorem *3.47anim12 809
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 966
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 807
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 833
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 806  bitr 805
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 905  pm4.25 906
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1010
[WhiteheadRussell] p. 118Theorem *4.31orcom 871
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 922
[WhiteheadRussell] p. 118Theorem *4.36anbi1 634
[WhiteheadRussell] p. 118Theorem *4.37orbi1 918
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 638
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 979
[WhiteheadRussell] p. 118Definition *4.34df-3an 1089
[WhiteheadRussell] p. 119Theorem *4.41ordi 1008
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1054
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1025
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 999
[WhiteheadRussell] p. 119Theorem *4.45orabs 1001  pm4.45 1000  pm4.45im 828
[WhiteheadRussell] p. 120Theorem *4.5anor 985
[WhiteheadRussell] p. 120Theorem *4.6imor 854
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 984
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 987
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 988
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 989
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 990
[WhiteheadRussell] p. 120Theorem *4.56ioran 986  pm4.56 991
[WhiteheadRussell] p. 120Theorem *4.57oran 992  pm4.57 993
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 857
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 850
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 851
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 398
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 557  pm4.71d 561  pm4.71i 559  pm4.71r 558  pm4.71rd 562  pm4.71ri 560
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 952
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 937
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 964  pm4.77 965
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 935
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1006
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1026
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1027
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 387  impexp 450  pm4.87 844
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 824
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 947  pm5.11g 946
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 948
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 950
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 949
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1015
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1016
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1014
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 825
[WhiteheadRussell] p. 124Theorem *5.22xor 1017
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1050
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1051
[WhiteheadRussell] p. 124Theorem *5.25dfor2 902
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 572
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 388
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1004
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 956
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 831
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 836
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 826
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 834
[WhiteheadRussell] p. 125Theorem *5.41imdi 389  pm5.41 390
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 543
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 542
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1007
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1020
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 951
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1003
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1021
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1022
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1030
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1031
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 36886
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44785
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44786
[WhiteheadRussell] p. 147Theorem *10.2219.26 1872
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44787
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44788
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44789
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1895
[WhiteheadRussell] p. 151Theorem *10.301albitr 44790
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44791
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44792
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44793
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44794
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44796
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44797
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44798
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44795
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2096
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44801
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44802
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2076
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2166
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1831
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1832
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44803
[WhiteheadRussell] p. 162Theorem *11.322alim 44804
[WhiteheadRussell] p. 162Theorem *11.332albi 44805
[WhiteheadRussell] p. 162Theorem *11.342exim 44806
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44808
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44807
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1889
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44810
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44811
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44809
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1830
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44812
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44813
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1848
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44814
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2351
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1862
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44819
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44815
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44816
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44817
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44818
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44823
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44820
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44821
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44822
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44824
[WhiteheadRussell] p. 175Definition *14.02df-eu 2570
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44834  pm13.13b 44835
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44836
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3014
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3015
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3609
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44842
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44843
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44837
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44979  pm13.193 44838
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44839
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44840
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44841
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44848
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44847
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44846
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3792
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44849  pm14.122b 44850  pm14.122c 44851
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44852  pm14.123b 44853  pm14.123c 44854
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44856
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44855
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44857
[WhiteheadRussell] p. 190Theorem *14.22iota4 6480
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44858
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6481
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44859
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44861
[WhiteheadRussell] p. 192Theorem *14.26eupick 2634  eupickbi 2637  sbaniota 44862
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44860
[WhiteheadRussell] p. 192Theorem *14.271eubi 2585
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44863
[WhiteheadRussell] p. 235Definition *30.01conventions 30470  df-fv 6507
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9925  pm54.43lem 9924
[Young] p. 141Definition of operator orderingleop2 32195
[Young] p. 142Example 12.2(i)0leop 32201  idleop 32202
[vandenDries] p. 42Lemma 61irrapx1 43256
[vandenDries] p. 43Theorem 62pellex 43263  pellexlem1 43257

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