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 17580
[Adamek] p. 21Condition 3.1(b)df-cat 17580
[Adamek] p. 22Example 3.3(1)df-setc 17989
[Adamek] p. 24Example 3.3(4.c)0cat 17601  0funcg 49191  df-termc 49579
[Adamek] p. 24Example 3.3(4.d)df-prstc 49656  prsthinc 49570
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49684  df-mndtc 49684
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49680
[Adamek] p. 25Definition 3.5df-oppc 17624
[Adamek] p. 25Example 3.6(1)oduoppcciso 49672
[Adamek] p. 25Example 3.6(2)oppgoppcco 49697  oppgoppchom 49696  oppgoppcid 49698
[Adamek] p. 28Remark 3.9oppciso 17694
[Adamek] p. 28Remark 3.12invf1o 17682  invisoinvl 17703
[Adamek] p. 28Example 3.13idinv 17702  idiso 17701
[Adamek] p. 28Corollary 3.11inveq 17687
[Adamek] p. 28Definition 3.8df-inv 17661  df-iso 17662  dfiso2 17685
[Adamek] p. 28Proposition 3.10sectcan 17668
[Adamek] p. 29Remark 3.16cicer 17719  cicerALT 49152
[Adamek] p. 29Definition 3.15cic 17712  df-cic 17709
[Adamek] p. 29Definition 3.17df-func 17771
[Adamek] p. 29Proposition 3.14(1)invinv 17683
[Adamek] p. 29Proposition 3.14(2)invco 17684  isoco 17690
[Adamek] p. 30Remark 3.19df-func 17771
[Adamek] p. 30Example 3.20(1)idfucl 17794
[Adamek] p. 30Example 3.20(2)diag1 49410
[Adamek] p. 32Proposition 3.21funciso 17787
[Adamek] p. 33Example 3.26(1)discsnterm 49680  discthing 49567
[Adamek] p. 33Example 3.26(2)df-thinc 49524  prsthinc 49570  thincciso 49559  thincciso2 49561  thincciso3 49562  thinccisod 49560
[Adamek] p. 33Example 3.26(3)df-mndtc 49684
[Adamek] p. 33Proposition 3.23cofucl 17801  cofucla 49202
[Adamek] p. 34Remark 3.28(1)cofidfth 49268
[Adamek] p. 34Remark 3.28(2)catciso 18024  catcisoi 49506
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18079
[Adamek] p. 34Definition 3.27(2)df-fth 17820
[Adamek] p. 34Definition 3.27(3)df-full 17819
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18079
[Adamek] p. 35Corollary 3.32ffthiso 17844
[Adamek] p. 35Proposition 3.30(c)cofth 17850
[Adamek] p. 35Proposition 3.30(d)cofull 17849
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18064
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18064
[Adamek] p. 39Remark 3.422oppf 49238
[Adamek] p. 39Definition 3.41df-oppf 49229  funcoppc 17788
[Adamek] p. 39Definition 3.44.df-catc 18012  elcatchom 49503
[Adamek] p. 39Proposition 3.43(c)fthoppc 17838  fthoppf 49270
[Adamek] p. 39Proposition 3.43(d)fulloppc 17837  fulloppf 49269
[Adamek] p. 40Remark 3.48catccat 18021
[Adamek] p. 40Definition 3.470funcg 49191  df-catc 18012
[Adamek] p. 45Exercise 3Gincat 49707
[Adamek] p. 48Remark 4.2(2)cnelsubc 49710  nelsubc3 49177
[Adamek] p. 48Remark 4.2(3)imasubc 49257  imasubc2 49258  imasubc3 49262
[Adamek] p. 48Example 4.3(1.a)0subcat 17751
[Adamek] p. 48Example 4.3(1.b)catsubcat 17752
[Adamek] p. 48Definition 4.1(1)nelsubc3 49177
[Adamek] p. 48Definition 4.1(2)fullsubc 17763
[Adamek] p. 48Definition 4.1(a)df-subc 17725
[Adamek] p. 49Remark 4.4idsubc 49266
[Adamek] p. 49Remark 4.4(1)idemb 49265
[Adamek] p. 49Remark 4.4(2)idfullsubc 49267  ressffth 17853
[Adamek] p. 58Exercise 4Asetc1onsubc 49708
[Adamek] p. 83Definition 6.1df-nat 17859
[Adamek] p. 87Remark 6.14(a)fuccocl 17880
[Adamek] p. 87Remark 6.14(b)fucass 17884
[Adamek] p. 87Definition 6.15df-fuc 17860
[Adamek] p. 88Remark 6.16fuccat 17886
[Adamek] p. 101Definition 7.10funcg 49191  df-inito 17897
[Adamek] p. 101Example 7.2(3)0funcg 49191  df-termc 49579  initc 49197
[Adamek] p. 101Example 7.2 (6)irinitoringc 21422
[Adamek] p. 102Definition 7.4df-termo 17898  oppctermo 49342
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17925
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17929
[Adamek] p. 103Remark 7.8oppczeroo 49343
[Adamek] p. 103Definition 7.7df-zeroo 17899
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21423
[Adamek] p. 103Proposition 7.6termoeu1w 17932
[Adamek] p. 106Definition 7.19df-sect 17660
[Adamek] p. 107Example 7.20(7)thincinv 49575
[Adamek] p. 108Example 7.25(4)thincsect2 49574
[Adamek] p. 110Example 7.33(9)thincmon 49539
[Adamek] p. 110Proposition 7.35sectmon 17695
[Adamek] p. 112Proposition 7.42sectepi 17697
[Adamek] p. 185Section 10.67updjud 9833
[Adamek] p. 193Definition 11.1(1)df-lmd 49751
[Adamek] p. 193Definition 11.3(1)df-lmd 49751
[Adamek] p. 194Definition 11.3(2)df-lmd 49751
[Adamek] p. 202Definition 11.27(1)df-cmd 49752
[Adamek] p. 202Definition 11.27(2)df-cmd 49752
[Adamek] p. 478Item Rngdf-ringc 20567
[AhoHopUll] p. 2Section 1.1df-bigo 48654
[AhoHopUll] p. 12Section 1.3df-blen 48676
[AhoHopUll] p. 318Section 9.1df-concat 14484  df-pfx 14585  df-substr 14555  df-word 14427  lencl 14446  wrd0 14452
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24629  df-nmoo 30732
[AkhiezerGlazman] p. 64Theoremhmopidmch 32140  hmopidmchi 32138
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32188  pjcmul2i 32189
[AkhiezerGlazman] p. 72Theoremcnvunop 31905  unoplin 31907
[AkhiezerGlazman] p. 72Equation 2unopadj 31906  unopadj2 31925
[AkhiezerGlazman] p. 73Theoremelunop2 32000  lnopunii 31999
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32073
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27877
[Alling] p. 184Axiom Bbdayfo 27622
[Alling] p. 184Axiom Osltso 27621
[Alling] p. 184Axiom SDnodense 27637
[Alling] p. 185Lemma 0nocvxmin 27724
[Alling] p. 185Theoremconway 27746
[Alling] p. 185Axiom FEnoeta 27688
[Alling] p. 186Theorem 4slerec 27766  slerecd 27767
[Alling], p. 2Definitionrp-brsslt 43521
[Alling], p. 3Notenla0001 43524  nla0002 43522  nla0003 43523
[Apostol] p. 18Theorem I.1addcan 11303  addcan2d 11323  addcan2i 11313  addcand 11322  addcani 11312
[Apostol] p. 18Theorem I.2negeu 11356
[Apostol] p. 18Theorem I.3negsub 11415  negsubd 11484  negsubi 11445
[Apostol] p. 18Theorem I.4negneg 11417  negnegd 11469  negnegi 11437
[Apostol] p. 18Theorem I.5subdi 11556  subdid 11579  subdii 11572  subdir 11557  subdird 11580  subdiri 11573
[Apostol] p. 18Theorem I.6mul01 11298  mul01d 11318  mul01i 11309  mul02 11297  mul02d 11317  mul02i 11308
[Apostol] p. 18Theorem I.7mulcan 11760  mulcan2d 11757  mulcand 11756  mulcani 11762
[Apostol] p. 18Theorem I.8receu 11768  xreceu 32909
[Apostol] p. 18Theorem I.9divrec 11798  divrecd 11906  divreci 11872  divreczi 11865
[Apostol] p. 18Theorem I.10recrec 11824  recreci 11859
[Apostol] p. 18Theorem I.11mul0or 11763  mul0ord 11771  mul0ori 11770
[Apostol] p. 18Theorem I.12mul2neg 11562  mul2negd 11578  mul2negi 11571  mulneg1 11559  mulneg1d 11576  mulneg1i 11569
[Apostol] p. 18Theorem I.13divadddiv 11842  divadddivd 11947  divadddivi 11889
[Apostol] p. 18Theorem I.14divmuldiv 11827  divmuldivd 11944  divmuldivi 11887  rdivmuldivd 20337
[Apostol] p. 18Theorem I.15divdivdiv 11828  divdivdivd 11950  divdivdivi 11890
[Apostol] p. 20Axiom 7rpaddcl 12920  rpaddcld 12955  rpmulcl 12921  rpmulcld 12956
[Apostol] p. 20Axiom 8rpneg 12930
[Apostol] p. 20Axiom 90nrp 12933
[Apostol] p. 20Theorem I.17lttri 11245
[Apostol] p. 20Theorem I.18ltadd1d 11716  ltadd1dd 11734  ltadd1i 11677
[Apostol] p. 20Theorem I.19ltmul1 11977  ltmul1a 11976  ltmul1i 12046  ltmul1ii 12056  ltmul2 11978  ltmul2d 12982  ltmul2dd 12996  ltmul2i 12049
[Apostol] p. 20Theorem I.20msqgt0 11643  msqgt0d 11690  msqgt0i 11660
[Apostol] p. 20Theorem I.210lt1 11645
[Apostol] p. 20Theorem I.23lt0neg1 11629  lt0neg1d 11692  ltneg 11623  ltnegd 11701  ltnegi 11667
[Apostol] p. 20Theorem I.25lt2add 11608  lt2addd 11746  lt2addi 11685
[Apostol] p. 20Definition of positive numbersdf-rp 12897
[Apostol] p. 21Exercise 4recgt0 11973  recgt0d 12062  recgt0i 12033  recgt0ii 12034
[Apostol] p. 22Definition of integersdf-z 12475
[Apostol] p. 22Definition of positive integersdfnn3 12145
[Apostol] p. 22Definition of rationalsdf-q 12853
[Apostol] p. 24Theorem I.26supeu 9344
[Apostol] p. 26Theorem I.28nnunb 12383
[Apostol] p. 26Theorem I.29arch 12384  archd 45264
[Apostol] p. 28Exercise 2btwnz 12582
[Apostol] p. 28Exercise 3nnrecl 12385
[Apostol] p. 28Exercise 4rebtwnz 12851
[Apostol] p. 28Exercise 5zbtwnre 12850
[Apostol] p. 28Exercise 6qbtwnre 13104
[Apostol] p. 28Exercise 10(a)zeneo 16256  zneo 12562  zneoALTV 47774
[Apostol] p. 29Theorem I.35cxpsqrtth 26672  msqsqrtd 15356  resqrtth 15168  sqrtth 15278  sqrtthi 15284  sqsqrtd 15355
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12134
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12817
[Apostol] p. 361Remarkcrreczi 14141
[Apostol] p. 363Remarkabsgt0i 15313
[Apostol] p. 363Exampleabssubd 15369  abssubi 15317
[ApostolNT] p. 7Remarkfmtno0 47645  fmtno1 47646  fmtno2 47655  fmtno3 47656  fmtno4 47657  fmtno5fac 47687  fmtnofz04prm 47682
[ApostolNT] p. 7Definitiondf-fmtno 47633
[ApostolNT] p. 8Definitiondf-ppi 27043
[ApostolNT] p. 14Definitiondf-dvds 16170
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16186
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16211
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16206
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16199
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16201
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16187
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16188
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16193
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16228
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16230
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16232
[ApostolNT] p. 15Definitiondf-gcd 16412  dfgcd2 16463
[ApostolNT] p. 16Definitionisprm2 16599
[ApostolNT] p. 16Theorem 1.5coprmdvds 16570
[ApostolNT] p. 16Theorem 1.7prminf 16833
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16430
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16464
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16466
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16445
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16437
[ApostolNT] p. 17Theorem 1.8coprm 16628
[ApostolNT] p. 17Theorem 1.9euclemma 16630
[ApostolNT] p. 17Theorem 1.101arith2 16846
[ApostolNT] p. 18Theorem 1.13prmrec 16840
[ApostolNT] p. 19Theorem 1.14divalg 16320
[ApostolNT] p. 20Theorem 1.15eucalg 16504
[ApostolNT] p. 24Definitiondf-mu 27044
[ApostolNT] p. 25Definitiondf-phi 16683
[ApostolNT] p. 25Theorem 2.1musum 27134
[ApostolNT] p. 26Theorem 2.2phisum 16708
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16693
[ApostolNT] p. 28Theorem 2.5(c)phimul 16697
[ApostolNT] p. 32Definitiondf-vma 27041
[ApostolNT] p. 32Theorem 2.9muinv 27136
[ApostolNT] p. 32Theorem 2.10vmasum 27160
[ApostolNT] p. 38Remarkdf-sgm 27045
[ApostolNT] p. 38Definitiondf-sgm 27045
[ApostolNT] p. 75Definitiondf-chp 27042  df-cht 27040
[ApostolNT] p. 104Definitioncongr 16581
[ApostolNT] p. 106Remarkdvdsval3 16173
[ApostolNT] p. 106Definitionmoddvds 16180
[ApostolNT] p. 107Example 2mod2eq0even 16263
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16264
[ApostolNT] p. 107Example 4zmod1congr 13798
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13838
[ApostolNT] p. 107Theorem 5.2(c)modexp 14151
[ApostolNT] p. 108Theorem 5.3modmulconst 16205
[ApostolNT] p. 109Theorem 5.4cncongr1 16584
[ApostolNT] p. 109Theorem 5.6gcdmodi 16992
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16586
[ApostolNT] p. 113Theorem 5.17eulerth 16700
[ApostolNT] p. 113Theorem 5.18vfermltl 16719
[ApostolNT] p. 114Theorem 5.19fermltl 16701
[ApostolNT] p. 116Theorem 5.24wilthimp 27015
[ApostolNT] p. 179Definitiondf-lgs 27239  lgsprme0 27283
[ApostolNT] p. 180Example 11lgs 27284
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27260
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27275
[ApostolNT] p. 181Theorem 9.4m1lgs 27332
[ApostolNT] p. 181Theorem 9.52lgs 27351  2lgsoddprm 27360
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27318
[ApostolNT] p. 185Theorem 9.8lgsquad 27327
[ApostolNT] p. 188Definitiondf-lgs 27239  lgs1 27285
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27276
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27278
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27286
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27287
[Baer] p. 40Property (b)mapdord 41743
[Baer] p. 40Property (c)mapd11 41744
[Baer] p. 40Property (e)mapdin 41767  mapdlsm 41769
[Baer] p. 40Property (f)mapd0 41770
[Baer] p. 40Definition of projectivitydf-mapd 41730  mapd1o 41753
[Baer] p. 41Property (g)mapdat 41772
[Baer] p. 44Part (1)mapdpg 41811
[Baer] p. 45Part (2)hdmap1eq 41906  mapdheq 41833  mapdheq2 41834  mapdheq2biN 41835
[Baer] p. 45Part (3)baerlem3 41818
[Baer] p. 46Part (4)mapdheq4 41837  mapdheq4lem 41836
[Baer] p. 46Part (5)baerlem5a 41819  baerlem5abmN 41823  baerlem5amN 41821  baerlem5b 41820  baerlem5bmN 41822
[Baer] p. 47Part (6)hdmap1l6 41926  hdmap1l6a 41914  hdmap1l6e 41919  hdmap1l6f 41920  hdmap1l6g 41921  hdmap1l6lem1 41912  hdmap1l6lem2 41913  mapdh6N 41852  mapdh6aN 41840  mapdh6eN 41845  mapdh6fN 41846  mapdh6gN 41847  mapdh6lem1N 41838  mapdh6lem2N 41839
[Baer] p. 48Part 9hdmapval 41933
[Baer] p. 48Part 10hdmap10 41945
[Baer] p. 48Part 11hdmapadd 41948
[Baer] p. 48Part (6)hdmap1l6h 41922  mapdh6hN 41848
[Baer] p. 48Part (7)mapdh75cN 41858  mapdh75d 41859  mapdh75e 41857  mapdh75fN 41860  mapdh7cN 41854  mapdh7dN 41855  mapdh7eN 41853  mapdh7fN 41856
[Baer] p. 48Part (8)mapdh8 41893  mapdh8a 41880  mapdh8aa 41881  mapdh8ab 41882  mapdh8ac 41883  mapdh8ad 41884  mapdh8b 41885  mapdh8c 41886  mapdh8d 41888  mapdh8d0N 41887  mapdh8e 41889  mapdh8g 41890  mapdh8i 41891  mapdh8j 41892
[Baer] p. 48Part (9)mapdh9a 41894
[Baer] p. 48Equation 10mapdhvmap 41874
[Baer] p. 49Part 12hdmap11 41953  hdmapeq0 41949  hdmapf1oN 41970  hdmapneg 41951  hdmaprnN 41969  hdmaprnlem1N 41954  hdmaprnlem3N 41955  hdmaprnlem3uN 41956  hdmaprnlem4N 41958  hdmaprnlem6N 41959  hdmaprnlem7N 41960  hdmaprnlem8N 41961  hdmaprnlem9N 41962  hdmapsub 41952
[Baer] p. 49Part 14hdmap14lem1 41973  hdmap14lem10 41982  hdmap14lem1a 41971  hdmap14lem2N 41974  hdmap14lem2a 41972  hdmap14lem3 41975  hdmap14lem8 41980  hdmap14lem9 41981
[Baer] p. 50Part 14hdmap14lem11 41983  hdmap14lem12 41984  hdmap14lem13 41985  hdmap14lem14 41986  hdmap14lem15 41987  hgmapval 41992
[Baer] p. 50Part 15hgmapadd 41999  hgmapmul 42000  hgmaprnlem2N 42002  hgmapvs 41996
[Baer] p. 50Part 16hgmaprnN 42006
[Baer] p. 110Lemma 1hdmapip0com 42022
[Baer] p. 110Line 27hdmapinvlem1 42023
[Baer] p. 110Line 28hdmapinvlem2 42024
[Baer] p. 110Line 30hdmapinvlem3 42025
[Baer] p. 110Part 1.2hdmapglem5 42027  hgmapvv 42031
[Baer] p. 110Proposition 1hdmapinvlem4 42026
[Baer] p. 111Line 10hgmapvvlem1 42028
[Baer] p. 111Line 15hdmapg 42035  hdmapglem7 42034
[Bauer], p. 483Theorem 1.22irrexpq 26673  2irrexpqALT 26743
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2564
[BellMachover] p. 460Notationdf-mo 2535
[BellMachover] p. 460Definitionmo3 2559
[BellMachover] p. 461Axiom Extax-ext 2703
[BellMachover] p. 462Theorem 1.1axextmo 2707
[BellMachover] p. 463Axiom Repaxrep5 5227
[BellMachover] p. 463Scheme Sepax-sep 5236
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37115  sepex 5240
[BellMachover] p. 466Problemaxpow2 5307
[BellMachover] p. 466Axiom Powaxpow3 5308
[BellMachover] p. 466Axiom Unionaxun2 7676
[BellMachover] p. 468Definitiondf-ord 6315
[BellMachover] p. 469Theorem 2.2(i)ordirr 6330
[BellMachover] p. 469Theorem 2.2(iii)onelon 6337
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6332
[BellMachover] p. 471Definition of Ndf-om 7803
[BellMachover] p. 471Problem 2.5(ii)uniordint 7740
[BellMachover] p. 471Definition of Limdf-lim 6317
[BellMachover] p. 472Axiom Infzfinf2 9538
[BellMachover] p. 473Theorem 2.8limom 7818
[BellMachover] p. 477Equation 3.1df-r1 9663
[BellMachover] p. 478Definitionrankval2 9717  rankval2b 35117
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9681  r1ord3g 9678
[BellMachover] p. 480Axiom Regzfreg 9488
[BellMachover] p. 488Axiom ACac5 10374  dfac4 10019
[BellMachover] p. 490Definition of alephalephval3 10007
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39424
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32340
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32382  chirredi 32381
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32370
[Beran] p. 3Definition of joinsshjval3 31341
[Beran] p. 39Theorem 2.3(i)cmcm2 31603  cmcm2i 31580  cmcm2ii 31585  cmt2N 39355
[Beran] p. 40Theorem 2.3(iii)lecm 31604  lecmi 31589  lecmii 31590
[Beran] p. 45Theorem 3.4cmcmlem 31578
[Beran] p. 49Theorem 4.2cm2j 31607  cm2ji 31612  cm2mi 31613
[Beran] p. 95Definitiondf-sh 31194  issh2 31196
[Beran] p. 95Lemma 3.1(S5)his5 31073
[Beran] p. 95Lemma 3.1(S6)his6 31086
[Beran] p. 95Lemma 3.1(S7)his7 31077
[Beran] p. 95Lemma 3.2(S8)ho01i 31815
[Beran] p. 95Lemma 3.2(S9)hoeq1 31817
[Beran] p. 95Lemma 3.2(S10)ho02i 31816
[Beran] p. 95Lemma 3.2(S11)hoeq2 31818
[Beran] p. 95Postulate (S1)ax-his1 31069  his1i 31087
[Beran] p. 95Postulate (S2)ax-his2 31070
[Beran] p. 95Postulate (S3)ax-his3 31071
[Beran] p. 95Postulate (S4)ax-his4 31072
[Beran] p. 96Definition of normdf-hnorm 30955  dfhnorm2 31109  normval 31111
[Beran] p. 96Definition for Cauchy sequencehcau 31171
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30960
[Beran] p. 96Definition of complete subspaceisch3 31228
[Beran] p. 96Definition of convergedf-hlim 30959  hlimi 31175
[Beran] p. 97Theorem 3.3(i)norm-i-i 31120  norm-i 31116
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31124  norm-ii 31125  normlem0 31096  normlem1 31097  normlem2 31098  normlem3 31099  normlem4 31100  normlem5 31101  normlem6 31102  normlem7 31103  normlem7tALT 31106
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31126  norm-iii 31127
[Beran] p. 98Remark 3.4bcs 31168  bcsiALT 31166  bcsiHIL 31167
[Beran] p. 98Remark 3.4(B)normlem9at 31108  normpar 31142  normpari 31141
[Beran] p. 98Remark 3.4(C)normpyc 31133  normpyth 31132  normpythi 31129
[Beran] p. 99Remarklnfn0 32034  lnfn0i 32029  lnop0 31953  lnop0i 31957
[Beran] p. 99Theorem 3.5(i)nmcexi 32013  nmcfnex 32040  nmcfnexi 32038  nmcopex 32016  nmcopexi 32014
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32041  nmcfnlbi 32039  nmcoplb 32017  nmcoplbi 32015
[Beran] p. 99Theorem 3.5(iii)lnfncon 32043  lnfnconi 32042  lnopcon 32022  lnopconi 32021
[Beran] p. 100Lemma 3.6normpar2i 31143
[Beran] p. 101Lemma 3.6norm3adifi 31140  norm3adifii 31135  norm3dif 31137  norm3difi 31134
[Beran] p. 102Theorem 3.7(i)chocunii 31288  pjhth 31380  pjhtheu 31381  pjpjhth 31412  pjpjhthi 31413  pjth 25372
[Beran] p. 102Theorem 3.7(ii)ococ 31393  ococi 31392
[Beran] p. 103Remark 3.8nlelchi 32048
[Beran] p. 104Theorem 3.9riesz3i 32049  riesz4 32051  riesz4i 32050
[Beran] p. 104Theorem 3.10cnlnadj 32066  cnlnadjeu 32065  cnlnadjeui 32064  cnlnadji 32063  cnlnadjlem1 32054  nmopadjlei 32075
[Beran] p. 106Theorem 3.11(i)adjeq0 32078
[Beran] p. 106Theorem 3.11(v)nmopadji 32077
[Beran] p. 106Theorem 3.11(ii)adjmul 32079
[Beran] p. 106Theorem 3.11(iv)adjadj 31923
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32089  nmopcoadji 32088
[Beran] p. 106Theorem 3.11(iii)adjadd 32080
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32090
[Beran] p. 106Theorem 3.11(viii)adjcoi 32087  pjadj2coi 32191  pjadjcoi 32148
[Beran] p. 107Definitiondf-ch 31208  isch2 31210
[Beran] p. 107Remark 3.12choccl 31293  isch3 31228  occl 31291  ocsh 31270  shoccl 31292  shocsh 31271
[Beran] p. 107Remark 3.12(B)ococin 31395
[Beran] p. 108Theorem 3.13chintcl 31319
[Beran] p. 109Property (i)pjadj2 32174  pjadj3 32175  pjadji 31672  pjadjii 31661
[Beran] p. 109Property (ii)pjidmco 32168  pjidmcoi 32164  pjidmi 31660
[Beran] p. 110Definition of projector orderingpjordi 32160
[Beran] p. 111Remarkho0val 31737  pjch1 31657
[Beran] p. 111Definitiondf-hfmul 31721  df-hfsum 31720  df-hodif 31719  df-homul 31718  df-hosum 31717
[Beran] p. 111Lemma 4.4(i)pjo 31658
[Beran] p. 111Lemma 4.4(ii)pjch 31681  pjchi 31419
[Beran] p. 111Lemma 4.4(iii)pjoc2 31426  pjoc2i 31425
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31667
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32152  pjssmii 31668
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32151
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32150
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32155
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32153  pjssge0ii 31669
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32154  pjdifnormii 31670
[Bobzien] p. 116Statement T3stoic3 1777
[Bobzien] p. 117Statement T2stoic2a 1775
[Bobzien] p. 117Statement T4stoic4a 1778
[Bobzien] p. 117Conclusion the contradictorystoic1a 1773
[Bogachev] p. 16Definition 1.5df-oms 34312
[Bogachev] p. 17Lemma 1.5.4omssubadd 34320
[Bogachev] p. 17Example 1.5.2omsmon 34318
[Bogachev] p. 41Definition 1.11.2df-carsg 34322
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34342
[Bogachev] p. 116Definition 2.3.1df-itgm 34373  df-sitm 34351
[Bogachev] p. 118Chapter 2.4.4df-itgm 34373
[Bogachev] p. 118Definition 2.4.1df-sitg 34350
[Bollobas] p. 1Section I.1df-edg 29033  isuhgrop 29055  isusgrop 29147  isuspgrop 29146
[Bollobas] p. 2Section I.1df-isubgr 47966  df-subgr 29253  uhgrspan1 29288  uhgrspansubgr 29276
[Bollobas] p. 3Definitiondf-gric 47986  gricuspgr 48023  isuspgrim 48001
[Bollobas] p. 3Section I.1cusgrsize 29440  df-clnbgr 47924  df-cusgr 29397  df-nbgr 29318  fusgrmaxsize 29450
[Bollobas] p. 4Definitiondf-upwlks 48239  df-wlks 29585
[Bollobas] p. 4Section I.1finsumvtxdg2size 29536  finsumvtxdgeven 29538  fusgr1th 29537  fusgrvtxdgonume 29540  vtxdgoddnumeven 29539
[Bollobas] p. 5Notationdf-pths 29699
[Bollobas] p. 5Definitiondf-crcts 29771  df-cycls 29772  df-trls 29676  df-wlkson 29586
[Bollobas] p. 7Section I.1df-ushgr 29044
[BourbakiAlg1] p. 1Definition 1df-clintop 48305  df-cllaw 48291  df-mgm 18554  df-mgm2 48324
[BourbakiAlg1] p. 4Definition 5df-assintop 48306  df-asslaw 48293  df-sgrp 18633  df-sgrp2 48326
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48325  df-comlaw 48292
[BourbakiAlg1] p. 12Definition 2df-mnd 18649
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33014  mndlactf1o 33018  mndractf1 33016  mndractf1o 33019
[BourbakiAlg1] p. 92Definition 1df-ring 20159
[BourbakiAlg1] p. 93Section I.8.1df-rng 20077
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33653
[BourbakiAlg2] p. 113Chapter 5.assafld 33657  assarrginv 33656
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33698  fldextrspunfld 33696  fldextrspunlem1 33695  fldextrspunlem2 33697  fldextrspunlsp 33694  fldextrspunlsplem 33693
[BourbakiCAlg2], p. 228Proposition 21arithidom 33509  dfufd2 33522
[BourbakiEns] p. Proposition 8fcof1 7227  fcofo 7228
[BourbakiTop1] p. Remarkxnegmnf 13115  xnegpnf 13114
[BourbakiTop1] p. Remark rexneg 13116
[BourbakiTop1] p. Remark 3ust0 24141  ustfilxp 24134
[BourbakiTop1] p. Axiom GT'tgpsubcn 24011
[BourbakiTop1] p. Criterionishmeo 23680
[BourbakiTop1] p. Example 1cstucnd 24204  iducn 24203  snfil 23785
[BourbakiTop1] p. Example 2neifil 23801
[BourbakiTop1] p. Theorem 1cnextcn 23988
[BourbakiTop1] p. Theorem 2ucnextcn 24224
[BourbakiTop1] p. Theorem 3df-hcmp 33977
[BourbakiTop1] p. Paragraph 3infil 23784
[BourbakiTop1] p. Definition 1df-ucn 24196  df-ust 24122  filintn0 23782  filn0 23783  istgp 23998  ucnprima 24202
[BourbakiTop1] p. Definition 2df-cfilu 24207
[BourbakiTop1] p. Definition 3df-cusp 24218  df-usp 24178  df-utop 24152  trust 24150
[BourbakiTop1] p. Definition 6df-pcmp 33876
[BourbakiTop1] p. Property V_issnei2 23037
[BourbakiTop1] p. Theorem 1(d)iscncl 23190
[BourbakiTop1] p. Condition F_Iustssel 24127
[BourbakiTop1] p. Condition U_Iustdiag 24130
[BourbakiTop1] p. Property V_iiinnei 23046
[BourbakiTop1] p. Property V_ivneiptopreu 23054  neissex 23048
[BourbakiTop1] p. Proposition 1neips 23034  neiss 23030  ucncn 24205  ustund 24143  ustuqtop 24167
[BourbakiTop1] p. Proposition 2cnpco 23188  neiptopreu 23054  utop2nei 24171  utop3cls 24172
[BourbakiTop1] p. Proposition 3fmucnd 24212  uspreg 24194  utopreg 24173
[BourbakiTop1] p. Proposition 4imasncld 23612  imasncls 23613  imasnopn 23611
[BourbakiTop1] p. Proposition 9cnpflf2 23921
[BourbakiTop1] p. Condition F_IIustincl 24129
[BourbakiTop1] p. Condition U_IIustinvel 24131
[BourbakiTop1] p. Property V_iiielnei 23032
[BourbakiTop1] p. Proposition 11cnextucn 24223
[BourbakiTop1] p. Condition F_IIbustbasel 24128
[BourbakiTop1] p. Condition U_IIIustexhalf 24132
[BourbakiTop1] p. Definition C'''df-cmp 23308
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23767
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22815
[BourbakiTop2] p. 195Definition 1df-ldlf 33873
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46165
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46167  stoweid 46166
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46104  stoweidlem10 46113  stoweidlem14 46117  stoweidlem15 46118  stoweidlem35 46138  stoweidlem36 46139  stoweidlem37 46140  stoweidlem38 46141  stoweidlem40 46143  stoweidlem41 46144  stoweidlem43 46146  stoweidlem44 46147  stoweidlem46 46149  stoweidlem5 46108  stoweidlem50 46153  stoweidlem52 46155  stoweidlem53 46156  stoweidlem55 46158  stoweidlem56 46159
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46126  stoweidlem24 46127  stoweidlem27 46130  stoweidlem28 46131  stoweidlem30 46133
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46137  stoweidlem59 46162  stoweidlem60 46163
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46148  stoweidlem49 46152  stoweidlem7 46110
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46134  stoweidlem39 46142  stoweidlem42 46145  stoweidlem48 46151  stoweidlem51 46154  stoweidlem54 46157  stoweidlem57 46160  stoweidlem58 46161
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46128
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46120
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46114  stoweidlem13 46116  stoweidlem26 46129  stoweidlem61 46164
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46121
[Bruck] p. 1Section I.1df-clintop 48305  df-mgm 18554  df-mgm2 48324
[Bruck] p. 23Section II.1df-sgrp 18633  df-sgrp2 48326
[Bruck] p. 28Theorem 3.2dfgrp3 18958
[ChoquetDD] p. 2Definition of mappingdf-mpt 5175
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30390
[Clemente] p. 10Definition I` `m,nnatded 30390
[Clemente] p. 11Definition E=>m,nnatded 30390
[Clemente] p. 11Definition I=>m,nnatded 30390
[Clemente] p. 11Definition E` `(1)natded 30390
[Clemente] p. 11Definition E` `(2)natded 30390
[Clemente] p. 12Definition E` `m,n,pnatded 30390
[Clemente] p. 12Definition I` `n(1)natded 30390
[Clemente] p. 12Definition I` `n(2)natded 30390
[Clemente] p. 13Definition I` `m,n,pnatded 30390
[Clemente] p. 14Proof 5.11natded 30390
[Clemente] p. 14Definition E` `nnatded 30390
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30392  ex-natded5.2 30391
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30395  ex-natded5.3 30394
[Clemente] p. 18Theorem 5.5ex-natded5.5 30397
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30399  ex-natded5.7 30398
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30401  ex-natded5.8 30400
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30403  ex-natded5.13 30402
[Clemente] p. 32Definition I` `nnatded 30390
[Clemente] p. 32Definition E` `m,n,p,anatded 30390
[Clemente] p. 32Definition E` `n,tnatded 30390
[Clemente] p. 32Definition I` `n,tnatded 30390
[Clemente] p. 43Theorem 9.20ex-natded9.20 30404
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30405
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30407  ex-natded9.26 30406
[Cohen] p. 301Remarkrelogoprlem 26533
[Cohen] p. 301Property 2relogmul 26534  relogmuld 26567
[Cohen] p. 301Property 3relogdiv 26535  relogdivd 26568
[Cohen] p. 301Property 4relogexp 26538
[Cohen] p. 301Property 1alog1 26527
[Cohen] p. 301Property 1bloge 26528
[Cohen4] p. 348Observationrelogbcxpb 26730
[Cohen4] p. 349Propertyrelogbf 26734
[Cohen4] p. 352Definitionelogb 26713
[Cohen4] p. 361Property 2relogbmul 26720
[Cohen4] p. 361Property 3logbrec 26725  relogbdiv 26722
[Cohen4] p. 361Property 4relogbreexp 26718
[Cohen4] p. 361Property 6relogbexp 26723
[Cohen4] p. 361Property 1(a)logbid1 26711
[Cohen4] p. 361Property 1(b)logb1 26712
[Cohen4] p. 367Propertylogbchbase 26714
[Cohen4] p. 377Property 2logblt 26727
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34305  sxbrsigalem4 34307
[Cohn] p. 81Section II.5acsdomd 18469  acsinfd 18468  acsinfdimd 18470  acsmap2d 18467  acsmapd 18466
[Cohn] p. 143Example 5.1.1sxbrsiga 34310
[Connell] p. 57Definitiondf-scmat 22412  df-scmatalt 48505
[Conway] p. 4Definitionslerec 27766  slerecd 27767
[Conway] p. 5Definitionaddsval 27911  addsval2 27912  df-adds 27909  df-muls 28052  df-negs 27969
[Conway] p. 7Theorem0slt1s 27779
[Conway] p. 12Theorem 12pw2cut2 28388
[Conway] p. 16Theorem 0(i)ssltright 27822
[Conway] p. 16Theorem 0(ii)ssltleft 27821
[Conway] p. 16Theorem 0(iii)slerflex 27708
[Conway] p. 17Theorem 3addsass 27954  addsassd 27955  addscom 27915  addscomd 27916  addsrid 27913  addsridd 27914
[Conway] p. 17Definitiondf-0s 27774
[Conway] p. 17Theorem 4(ii)negnegs 27992
[Conway] p. 17Theorem 4(iii)negsid 27989  negsidd 27990
[Conway] p. 18Theorem 5sleadd1 27938  sleadd1d 27944
[Conway] p. 18Definitiondf-1s 27775
[Conway] p. 18Theorem 6(ii)negscl 27984  negscld 27985
[Conway] p. 18Theorem 6(iii)addscld 27929
[Conway] p. 19Notemulsunif2 28115
[Conway] p. 19Theorem 7addsdi 28100  addsdid 28101  addsdird 28102  mulnegs1d 28105  mulnegs2d 28106  mulsass 28111  mulsassd 28112  mulscom 28084  mulscomd 28085
[Conway] p. 19Theorem 8(i)mulscl 28079  mulscld 28080
[Conway] p. 19Theorem 8(iii)slemuld 28083  sltmul 28081  sltmuld 28082
[Conway] p. 20Theorem 9mulsgt0 28089  mulsgt0d 28090
[Conway] p. 21Theorem 10(iv)precsex 28162
[Conway] p. 23Theorem 11eqscut3 27771
[Conway] p. 24Definitiondf-reno 28402
[Conway] p. 24Theorem 13(ii)readdscl 28407  remulscl 28410  renegscl 28406
[Conway] p. 27Definitiondf-ons 28195  elons2 28201
[Conway] p. 27Theorem 14sltonex 28205
[Conway] p. 28Theorem 15onscutlt 28207  onswe 28212
[Conway] p. 29Remarkmadebday 27851  newbday 27853  oldbday 27852
[Conway] p. 29Definitiondf-made 27794  df-new 27796  df-old 27795
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13771
[Crawley] p. 1Definition of posetdf-poset 18225
[Crawley] p. 107Theorem 13.2hlsupr 39491
[Crawley] p. 110Theorem 13.3arglem1N 40295  dalaw 39991
[Crawley] p. 111Theorem 13.4hlathil 42066
[Crawley] p. 111Definition of set Wdf-watsN 40095
[Crawley] p. 111Definition of dilationdf-dilN 40211  df-ldil 40209  isldil 40215
[Crawley] p. 111Definition of translationdf-ltrn 40210  df-trnN 40212  isltrn 40224  ltrnu 40226
[Crawley] p. 112Lemma Acdlema1N 39896  cdlema2N 39897  exatleN 39509
[Crawley] p. 112Lemma B1cvrat 39581  cdlemb 39899  cdlemb2 40146  cdlemb3 40711  idltrn 40255  l1cvat 39160  lhpat 40148  lhpat2 40150  lshpat 39161  ltrnel 40244  ltrnmw 40256
[Crawley] p. 112Lemma Ccdlemc1 40296  cdlemc2 40297  ltrnnidn 40279  trlat 40274  trljat1 40271  trljat2 40272  trljat3 40273  trlne 40290  trlnidat 40278  trlnle 40291
[Crawley] p. 112Definition of automorphismdf-pautN 40096
[Crawley] p. 113Lemma Ccdlemc 40302  cdlemc3 40298  cdlemc4 40299
[Crawley] p. 113Lemma Dcdlemd 40312  cdlemd1 40303  cdlemd2 40304  cdlemd3 40305  cdlemd4 40306  cdlemd5 40307  cdlemd6 40308  cdlemd7 40309  cdlemd8 40310  cdlemd9 40311  cdleme31sde 40490  cdleme31se 40487  cdleme31se2 40488  cdleme31snd 40491  cdleme32a 40546  cdleme32b 40547  cdleme32c 40548  cdleme32d 40549  cdleme32e 40550  cdleme32f 40551  cdleme32fva 40542  cdleme32fva1 40543  cdleme32fvcl 40545  cdleme32le 40552  cdleme48fv 40604  cdleme4gfv 40612  cdleme50eq 40646  cdleme50f 40647  cdleme50f1 40648  cdleme50f1o 40651  cdleme50laut 40652  cdleme50ldil 40653  cdleme50lebi 40645  cdleme50rn 40650  cdleme50rnlem 40649  cdlemeg49le 40616  cdlemeg49lebilem 40644
[Crawley] p. 113Lemma Ecdleme 40665  cdleme00a 40314  cdleme01N 40326  cdleme02N 40327  cdleme0a 40316  cdleme0aa 40315  cdleme0b 40317  cdleme0c 40318  cdleme0cp 40319  cdleme0cq 40320  cdleme0dN 40321  cdleme0e 40322  cdleme0ex1N 40328  cdleme0ex2N 40329  cdleme0fN 40323  cdleme0gN 40324  cdleme0moN 40330  cdleme1 40332  cdleme10 40359  cdleme10tN 40363  cdleme11 40375  cdleme11a 40365  cdleme11c 40366  cdleme11dN 40367  cdleme11e 40368  cdleme11fN 40369  cdleme11g 40370  cdleme11h 40371  cdleme11j 40372  cdleme11k 40373  cdleme11l 40374  cdleme12 40376  cdleme13 40377  cdleme14 40378  cdleme15 40383  cdleme15a 40379  cdleme15b 40380  cdleme15c 40381  cdleme15d 40382  cdleme16 40390  cdleme16aN 40364  cdleme16b 40384  cdleme16c 40385  cdleme16d 40386  cdleme16e 40387  cdleme16f 40388  cdleme16g 40389  cdleme19a 40408  cdleme19b 40409  cdleme19c 40410  cdleme19d 40411  cdleme19e 40412  cdleme19f 40413  cdleme1b 40331  cdleme2 40333  cdleme20aN 40414  cdleme20bN 40415  cdleme20c 40416  cdleme20d 40417  cdleme20e 40418  cdleme20f 40419  cdleme20g 40420  cdleme20h 40421  cdleme20i 40422  cdleme20j 40423  cdleme20k 40424  cdleme20l 40427  cdleme20l1 40425  cdleme20l2 40426  cdleme20m 40428  cdleme20y 40407  cdleme20zN 40406  cdleme21 40442  cdleme21d 40435  cdleme21e 40436  cdleme22a 40445  cdleme22aa 40444  cdleme22b 40446  cdleme22cN 40447  cdleme22d 40448  cdleme22e 40449  cdleme22eALTN 40450  cdleme22f 40451  cdleme22f2 40452  cdleme22g 40453  cdleme23a 40454  cdleme23b 40455  cdleme23c 40456  cdleme26e 40464  cdleme26eALTN 40466  cdleme26ee 40465  cdleme26f 40468  cdleme26f2 40470  cdleme26f2ALTN 40469  cdleme26fALTN 40467  cdleme27N 40474  cdleme27a 40472  cdleme27cl 40471  cdleme28c 40477  cdleme3 40342  cdleme30a 40483  cdleme31fv 40495  cdleme31fv1 40496  cdleme31fv1s 40497  cdleme31fv2 40498  cdleme31id 40499  cdleme31sc 40489  cdleme31sdnN 40492  cdleme31sn 40485  cdleme31sn1 40486  cdleme31sn1c 40493  cdleme31sn2 40494  cdleme31so 40484  cdleme35a 40553  cdleme35b 40555  cdleme35c 40556  cdleme35d 40557  cdleme35e 40558  cdleme35f 40559  cdleme35fnpq 40554  cdleme35g 40560  cdleme35h 40561  cdleme35h2 40562  cdleme35sn2aw 40563  cdleme35sn3a 40564  cdleme36a 40565  cdleme36m 40566  cdleme37m 40567  cdleme38m 40568  cdleme38n 40569  cdleme39a 40570  cdleme39n 40571  cdleme3b 40334  cdleme3c 40335  cdleme3d 40336  cdleme3e 40337  cdleme3fN 40338  cdleme3fa 40341  cdleme3g 40339  cdleme3h 40340  cdleme4 40343  cdleme40m 40572  cdleme40n 40573  cdleme40v 40574  cdleme40w 40575  cdleme41fva11 40582  cdleme41sn3aw 40579  cdleme41sn4aw 40580  cdleme41snaw 40581  cdleme42a 40576  cdleme42b 40583  cdleme42c 40577  cdleme42d 40578  cdleme42e 40584  cdleme42f 40585  cdleme42g 40586  cdleme42h 40587  cdleme42i 40588  cdleme42k 40589  cdleme42ke 40590  cdleme42keg 40591  cdleme42mN 40592  cdleme42mgN 40593  cdleme43aN 40594  cdleme43bN 40595  cdleme43cN 40596  cdleme43dN 40597  cdleme5 40345  cdleme50ex 40664  cdleme50ltrn 40662  cdleme51finvN 40661  cdleme51finvfvN 40660  cdleme51finvtrN 40663  cdleme6 40346  cdleme7 40354  cdleme7a 40348  cdleme7aa 40347  cdleme7b 40349  cdleme7c 40350  cdleme7d 40351  cdleme7e 40352  cdleme7ga 40353  cdleme8 40355  cdleme8tN 40360  cdleme9 40358  cdleme9a 40356  cdleme9b 40357  cdleme9tN 40362  cdleme9taN 40361  cdlemeda 40403  cdlemedb 40402  cdlemednpq 40404  cdlemednuN 40405  cdlemefr27cl 40508  cdlemefr32fva1 40515  cdlemefr32fvaN 40514  cdlemefrs32fva 40505  cdlemefrs32fva1 40506  cdlemefs27cl 40518  cdlemefs32fva1 40528  cdlemefs32fvaN 40527  cdlemesner 40401  cdlemeulpq 40325
[Crawley] p. 114Lemma E4atex 40181  4atexlem7 40180  cdleme0nex 40395  cdleme17a 40391  cdleme17c 40393  cdleme17d 40603  cdleme17d1 40394  cdleme17d2 40600  cdleme18a 40396  cdleme18b 40397  cdleme18c 40398  cdleme18d 40400  cdleme4a 40344
[Crawley] p. 115Lemma Ecdleme21a 40430  cdleme21at 40433  cdleme21b 40431  cdleme21c 40432  cdleme21ct 40434  cdleme21f 40437  cdleme21g 40438  cdleme21h 40439  cdleme21i 40440  cdleme22gb 40399
[Crawley] p. 116Lemma Fcdlemf 40668  cdlemf1 40666  cdlemf2 40667
[Crawley] p. 116Lemma Gcdlemftr1 40672  cdlemg16 40762  cdlemg28 40809  cdlemg28a 40798  cdlemg28b 40808  cdlemg3a 40702  cdlemg42 40834  cdlemg43 40835  cdlemg44 40838  cdlemg44a 40836  cdlemg46 40840  cdlemg47 40841  cdlemg9 40739  ltrnco 40824  ltrncom 40843  tgrpabl 40856  trlco 40832
[Crawley] p. 116Definition of Gdf-tgrp 40848
[Crawley] p. 117Lemma Gcdlemg17 40782  cdlemg17b 40767
[Crawley] p. 117Definition of Edf-edring-rN 40861  df-edring 40862
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40865
[Crawley] p. 118Remarktendopltp 40885
[Crawley] p. 118Lemma Hcdlemh 40922  cdlemh1 40920  cdlemh2 40921
[Crawley] p. 118Lemma Icdlemi 40925  cdlemi1 40923  cdlemi2 40924
[Crawley] p. 118Lemma Jcdlemj1 40926  cdlemj2 40927  cdlemj3 40928  tendocan 40929
[Crawley] p. 118Lemma Kcdlemk 41079  cdlemk1 40936  cdlemk10 40948  cdlemk11 40954  cdlemk11t 41051  cdlemk11ta 41034  cdlemk11tb 41036  cdlemk11tc 41050  cdlemk11u-2N 40994  cdlemk11u 40976  cdlemk12 40955  cdlemk12u-2N 40995  cdlemk12u 40977  cdlemk13-2N 40981  cdlemk13 40957  cdlemk14-2N 40983  cdlemk14 40959  cdlemk15-2N 40984  cdlemk15 40960  cdlemk16-2N 40985  cdlemk16 40962  cdlemk16a 40961  cdlemk17-2N 40986  cdlemk17 40963  cdlemk18-2N 40991  cdlemk18-3N 41005  cdlemk18 40973  cdlemk19-2N 40992  cdlemk19 40974  cdlemk19u 41075  cdlemk1u 40964  cdlemk2 40937  cdlemk20-2N 40997  cdlemk20 40979  cdlemk21-2N 40996  cdlemk21N 40978  cdlemk22-3 41006  cdlemk22 40998  cdlemk23-3 41007  cdlemk24-3 41008  cdlemk25-3 41009  cdlemk26-3 41011  cdlemk26b-3 41010  cdlemk27-3 41012  cdlemk28-3 41013  cdlemk29-3 41016  cdlemk3 40938  cdlemk30 40999  cdlemk31 41001  cdlemk32 41002  cdlemk33N 41014  cdlemk34 41015  cdlemk35 41017  cdlemk36 41018  cdlemk37 41019  cdlemk38 41020  cdlemk39 41021  cdlemk39u 41073  cdlemk4 40939  cdlemk41 41025  cdlemk42 41046  cdlemk42yN 41049  cdlemk43N 41068  cdlemk45 41052  cdlemk46 41053  cdlemk47 41054  cdlemk48 41055  cdlemk49 41056  cdlemk5 40941  cdlemk50 41057  cdlemk51 41058  cdlemk52 41059  cdlemk53 41062  cdlemk54 41063  cdlemk55 41066  cdlemk55u 41071  cdlemk56 41076  cdlemk5a 40940  cdlemk5auN 40965  cdlemk5u 40966  cdlemk6 40942  cdlemk6u 40967  cdlemk7 40953  cdlemk7u-2N 40993  cdlemk7u 40975  cdlemk8 40943  cdlemk9 40944  cdlemk9bN 40945  cdlemki 40946  cdlemkid 41041  cdlemkj-2N 40987  cdlemkj 40968  cdlemksat 40951  cdlemksel 40950  cdlemksv 40949  cdlemksv2 40952  cdlemkuat 40971  cdlemkuel-2N 40989  cdlemkuel-3 41003  cdlemkuel 40970  cdlemkuv-2N 40988  cdlemkuv2-2 40990  cdlemkuv2-3N 41004  cdlemkuv2 40972  cdlemkuvN 40969  cdlemkvcl 40947  cdlemky 41031  cdlemkyyN 41067  tendoex 41080
[Crawley] p. 120Remarkdva1dim 41090
[Crawley] p. 120Lemma Lcdleml1N 41081  cdleml2N 41082  cdleml3N 41083  cdleml4N 41084  cdleml5N 41085  cdleml6 41086  cdleml7 41087  cdleml8 41088  cdleml9 41089  dia1dim 41166
[Crawley] p. 120Lemma Mdia11N 41153  diaf11N 41154  dialss 41151  diaord 41152  dibf11N 41266  djajN 41242
[Crawley] p. 120Definition of isomorphism mapdiaval 41137
[Crawley] p. 121Lemma Mcdlemm10N 41223  dia2dimlem1 41169  dia2dimlem2 41170  dia2dimlem3 41171  dia2dimlem4 41172  dia2dimlem5 41173  diaf1oN 41235  diarnN 41234  dvheveccl 41217  dvhopN 41221
[Crawley] p. 121Lemma Ncdlemn 41317  cdlemn10 41311  cdlemn11 41316  cdlemn11a 41312  cdlemn11b 41313  cdlemn11c 41314  cdlemn11pre 41315  cdlemn2 41300  cdlemn2a 41301  cdlemn3 41302  cdlemn4 41303  cdlemn4a 41304  cdlemn5 41306  cdlemn5pre 41305  cdlemn6 41307  cdlemn7 41308  cdlemn8 41309  cdlemn9 41310  diclspsn 41299
[Crawley] p. 121Definition of phi(q)df-dic 41278
[Crawley] p. 122Lemma Ndih11 41370  dihf11 41372  dihjust 41322  dihjustlem 41321  dihord 41369  dihord1 41323  dihord10 41328  dihord11b 41327  dihord11c 41329  dihord2 41332  dihord2a 41324  dihord2b 41325  dihord2cN 41326  dihord2pre 41330  dihord2pre2 41331  dihordlem6 41318  dihordlem7 41319  dihordlem7b 41320
[Crawley] p. 122Definition of isomorphism mapdihffval 41335  dihfval 41336  dihval 41337
[Diestel] p. 3Definitiondf-gric 47986  df-grim 47983  isuspgrim 48001
[Diestel] p. 3Section 1.1df-cusgr 29397  df-nbgr 29318
[Diestel] p. 3Definition by df-grisom 47982
[Diestel] p. 4Section 1.1df-isubgr 47966  df-subgr 29253  uhgrspan1 29288  uhgrspansubgr 29276
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29540  vtxdgoddnumeven 29539
[Diestel] p. 27Section 1.10df-ushgr 29044
[EGA] p. 80Notation 1.1.1rspecval 33884
[EGA] p. 80Proposition 1.1.2zartop 33896
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33888  zarcls1 33889
[EGA] p. 81Corollary 1.1.8zart0 33899
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33902
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33905
[Eisenberg] p. 67Definition 5.3df-dif 3900
[Eisenberg] p. 82Definition 6.3dfom3 9543
[Eisenberg] p. 125Definition 8.21df-map 8758
[Eisenberg] p. 216Example 13.2(4)omenps 9551
[Eisenberg] p. 310Theorem 19.8cardprc 9879
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10452
[Enderton] p. 18Axiom of Empty Setaxnul 5245
[Enderton] p. 19Definitiondf-tp 4580
[Enderton] p. 26Exercise 5unissb 4891
[Enderton] p. 26Exercise 10pwel 5321
[Enderton] p. 28Exercise 7(b)pwun 5512
[Enderton] p. 30Theorem "Distributive laws"iinin1 5029  iinin2 5028  iinun2 5023  iunin1 5022  iunin1f 32544  iunin2 5021  uniin1 32538  uniin2 32539
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5027  iundif2 5024
[Enderton] p. 32Exercise 20unineq 4237
[Enderton] p. 33Exercise 23iinuni 5048
[Enderton] p. 33Exercise 25iununi 5049
[Enderton] p. 33Exercise 24(a)iinpw 5056
[Enderton] p. 33Exercise 24(b)iunpw 7710  iunpwss 5057
[Enderton] p. 36Definitionopthwiener 5457
[Enderton] p. 38Exercise 6(a)unipw 5393
[Enderton] p. 38Exercise 6(b)pwuni 4896
[Enderton] p. 41Lemma 3Dopeluu 5413  rnex 7846  rnexg 7838
[Enderton] p. 41Exercise 8dmuni 5859  rnuni 6101
[Enderton] p. 42Definition of a functiondffun7 6514  dffun8 6515
[Enderton] p. 43Definition of function valuefunfv2 6916
[Enderton] p. 43Definition of single-rootedfuncnv 6556
[Enderton] p. 44Definition (d)dfima2 6016  dfima3 6017
[Enderton] p. 47Theorem 3Hfvco2 6925
[Enderton] p. 49Axiom of Choice (first form)ac7 10370  ac7g 10371  df-ac 10013  dfac2 10029  dfac2a 10027  dfac2b 10028  dfac3 10018  dfac7 10030
[Enderton] p. 50Theorem 3K(a)imauni 7186
[Enderton] p. 52Definitiondf-map 8758
[Enderton] p. 53Exercise 21coass 6219
[Enderton] p. 53Exercise 27dmco 6208
[Enderton] p. 53Exercise 14(a)funin 6563
[Enderton] p. 53Exercise 22(a)imass2 6056
[Enderton] p. 54Remarkixpf 8850  ixpssmap 8862
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8828
[Enderton] p. 55Axiom of Choice (second form)ac9 10380  ac9s 10390
[Enderton] p. 56Theorem 3Meqvrelref 38712  erref 8648
[Enderton] p. 57Lemma 3Neqvrelthi 38715  erthi 8684
[Enderton] p. 57Definitiondf-ec 8630
[Enderton] p. 58Definitiondf-qs 8634
[Enderton] p. 61Exercise 35df-ec 8630
[Enderton] p. 65Exercise 56(a)dmun 5855
[Enderton] p. 68Definition of successordf-suc 6318
[Enderton] p. 71Definitiondf-tr 5201  dftr4 5206
[Enderton] p. 72Theorem 4Eunisuc 6393  unisucg 6392
[Enderton] p. 73Exercise 6unisuc 6393  unisucg 6392
[Enderton] p. 73Exercise 5(a)truni 5215
[Enderton] p. 73Exercise 5(b)trint 5217  trintALT 44978
[Enderton] p. 79Theorem 4I(A1)nna0 8525
[Enderton] p. 79Theorem 4I(A2)nnasuc 8527  onasuc 8449
[Enderton] p. 79Definition of operation valuedf-ov 7355
[Enderton] p. 80Theorem 4J(A1)nnm0 8526
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8528  onmsuc 8450
[Enderton] p. 81Theorem 4K(1)nnaass 8543
[Enderton] p. 81Theorem 4K(2)nna0r 8530  nnacom 8538
[Enderton] p. 81Theorem 4K(3)nndi 8544
[Enderton] p. 81Theorem 4K(4)nnmass 8545
[Enderton] p. 81Theorem 4K(5)nnmcom 8547
[Enderton] p. 82Exercise 16nnm0r 8531  nnmsucr 8546
[Enderton] p. 88Exercise 23nnaordex 8559
[Enderton] p. 129Definitiondf-en 8876
[Enderton] p. 132Theorem 6B(b)canth 7306
[Enderton] p. 133Exercise 1xpomen 9912
[Enderton] p. 133Exercise 2qnnen 16128
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9122
[Enderton] p. 135Corollary 6Cphp3 9124
[Enderton] p. 136Corollary 6Enneneq 9121
[Enderton] p. 136Corollary 6D(a)pssinf 9152
[Enderton] p. 136Corollary 6D(b)ominf 9154
[Enderton] p. 137Lemma 6Fpssnn 9084
[Enderton] p. 138Corollary 6Gssfi 9088
[Enderton] p. 139Theorem 6H(c)mapen 9060
[Enderton] p. 142Theorem 6I(3)xpdjuen 10077
[Enderton] p. 142Theorem 6I(4)mapdjuen 10078
[Enderton] p. 143Theorem 6Jdju0en 10073  dju1en 10069
[Enderton] p. 144Exercise 13iunfi 9233  unifi 9234  unifi2 9235
[Enderton] p. 144Corollary 6Kundif2 4426  unfi 9086  unfi2 9200
[Enderton] p. 145Figure 38ffoss 7884
[Enderton] p. 145Definitiondf-dom 8877
[Enderton] p. 146Example 1domen 8890  domeng 8891
[Enderton] p. 146Example 3nndomo 9132  nnsdom 9550  nnsdomg 9189
[Enderton] p. 149Theorem 6L(a)djudom2 10081
[Enderton] p. 149Theorem 6L(c)mapdom1 9061  xpdom1 8995  xpdom1g 8993  xpdom2g 8992
[Enderton] p. 149Theorem 6L(d)mapdom2 9067
[Enderton] p. 151Theorem 6Mzorn 10404  zorng 10401
[Enderton] p. 151Theorem 6M(4)ac8 10389  dfac5 10026
[Enderton] p. 159Theorem 6Qunictb 10472
[Enderton] p. 164Exampleinfdif 10105
[Enderton] p. 168Definitiondf-po 5527
[Enderton] p. 192Theorem 7M(a)oneli 6427
[Enderton] p. 192Theorem 7M(b)ontr1 6359
[Enderton] p. 192Theorem 7M(c)onirri 6426
[Enderton] p. 193Corollary 7N(b)0elon 6367
[Enderton] p. 193Corollary 7N(c)onsuci 7775
[Enderton] p. 193Corollary 7N(d)ssonunii 7720
[Enderton] p. 194Remarkonprc 7717
[Enderton] p. 194Exercise 16suc11 6421
[Enderton] p. 197Definitiondf-card 9838
[Enderton] p. 197Theorem 7Pcarden 10448
[Enderton] p. 200Exercise 25tfis 7791
[Enderton] p. 202Lemma 7Tr1tr 9675
[Enderton] p. 202Definitiondf-r1 9663
[Enderton] p. 202Theorem 7Qr1val1 9685
[Enderton] p. 204Theorem 7V(b)rankval4 9766  rankval4b 35118
[Enderton] p. 206Theorem 7X(b)en2lp 9502
[Enderton] p. 207Exercise 30rankpr 9756  rankprb 9750  rankpw 9742  rankpwi 9722  rankuniss 9765
[Enderton] p. 207Exercise 34opthreg 9514
[Enderton] p. 208Exercise 35suc11reg 9515
[Enderton] p. 212Definition of alephalephval3 10007
[Enderton] p. 213Theorem 8A(a)alephord2 9973
[Enderton] p. 213Theorem 8A(b)cardalephex 9987
[Enderton] p. 218Theorem Schema 8Eonfununi 8267
[Enderton] p. 222Definition of kardkarden 9794  kardex 9793
[Enderton] p. 238Theorem 8Roeoa 8518
[Enderton] p. 238Theorem 8Soeoe 8520
[Enderton] p. 240Exercise 25oarec 8483
[Enderton] p. 257Definition of cofinalitycflm 10147
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17554
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17496
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18465  mrieqv2d 17551  mrieqvd 17550
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17555
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17560  mreexexlem2d 17557
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18471  mreexfidimd 17562
[Frege1879] p. 11Statementdf3or2 43866
[Frege1879] p. 12Statementdf3an2 43867  dfxor4 43864  dfxor5 43865
[Frege1879] p. 26Axiom 1ax-frege1 43888
[Frege1879] p. 26Axiom 2ax-frege2 43889
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43893
[Frege1879] p. 31Proposition 4frege4 43897
[Frege1879] p. 32Proposition 5frege5 43898
[Frege1879] p. 33Proposition 6frege6 43904
[Frege1879] p. 34Proposition 7frege7 43906
[Frege1879] p. 35Axiom 8ax-frege8 43907  axfrege8 43905
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37496
[Frege1879] p. 35Proposition 9frege9 43910
[Frege1879] p. 36Proposition 10frege10 43918
[Frege1879] p. 36Proposition 11frege11 43912
[Frege1879] p. 37Proposition 12frege12 43911
[Frege1879] p. 37Proposition 13frege13 43920
[Frege1879] p. 37Proposition 14frege14 43921
[Frege1879] p. 38Proposition 15frege15 43924
[Frege1879] p. 38Proposition 16frege16 43914
[Frege1879] p. 39Proposition 17frege17 43919
[Frege1879] p. 39Proposition 18frege18 43916
[Frege1879] p. 39Proposition 19frege19 43922
[Frege1879] p. 40Proposition 20frege20 43926
[Frege1879] p. 40Proposition 21frege21 43925
[Frege1879] p. 41Proposition 22frege22 43917
[Frege1879] p. 42Proposition 23frege23 43923
[Frege1879] p. 42Proposition 24frege24 43913
[Frege1879] p. 42Proposition 25frege25 43915  rp-frege25 43903
[Frege1879] p. 42Proposition 26frege26 43908
[Frege1879] p. 43Axiom 28ax-frege28 43928
[Frege1879] p. 43Proposition 27frege27 43909
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43929
[Frege1879] p. 44Axiom 31ax-frege31 43932  axfrege31 43931
[Frege1879] p. 44Proposition 30frege30 43930
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43933
[Frege1879] p. 44Proposition 33frege33 43934
[Frege1879] p. 45Proposition 34frege34 43935
[Frege1879] p. 45Proposition 35frege35 43936
[Frege1879] p. 45Proposition 36frege36 43937
[Frege1879] p. 46Proposition 37frege37 43938
[Frege1879] p. 46Proposition 38frege38 43939
[Frege1879] p. 46Proposition 39frege39 43940
[Frege1879] p. 46Proposition 40frege40 43941
[Frege1879] p. 47Axiom 41ax-frege41 43943  axfrege41 43942
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43944
[Frege1879] p. 47Proposition 43frege43 43945
[Frege1879] p. 47Proposition 44frege44 43946
[Frege1879] p. 47Proposition 45frege45 43947
[Frege1879] p. 48Proposition 46frege46 43948
[Frege1879] p. 48Proposition 47frege47 43949
[Frege1879] p. 49Proposition 48frege48 43950
[Frege1879] p. 49Proposition 49frege49 43951
[Frege1879] p. 49Proposition 50frege50 43952
[Frege1879] p. 50Axiom 52ax-frege52a 43955  ax-frege52c 43986  frege52aid 43956  frege52b 43987
[Frege1879] p. 50Axiom 54ax-frege54a 43960  ax-frege54c 43990  frege54b 43991
[Frege1879] p. 50Proposition 51frege51 43953
[Frege1879] p. 50Proposition 52dfsbcq 3738
[Frege1879] p. 50Proposition 53frege53a 43958  frege53aid 43957  frege53b 43988  frege53c 44012
[Frege1879] p. 50Proposition 54biid 261  eqid 2731
[Frege1879] p. 50Proposition 55frege55a 43966  frege55aid 43963  frege55b 43995  frege55c 44016  frege55cor1a 43967  frege55lem2a 43965  frege55lem2b 43994  frege55lem2c 44015
[Frege1879] p. 50Proposition 56frege56a 43969  frege56aid 43968  frege56b 43996  frege56c 44017
[Frege1879] p. 51Axiom 58ax-frege58a 43973  ax-frege58b 43999  frege58bid 44000  frege58c 44019
[Frege1879] p. 51Proposition 57frege57a 43971  frege57aid 43970  frege57b 43997  frege57c 44018
[Frege1879] p. 51Proposition 58spsbc 3749
[Frege1879] p. 51Proposition 59frege59a 43975  frege59b 44002  frege59c 44020
[Frege1879] p. 52Proposition 60frege60a 43976  frege60b 44003  frege60c 44021
[Frege1879] p. 52Proposition 61frege61a 43977  frege61b 44004  frege61c 44022
[Frege1879] p. 52Proposition 62frege62a 43978  frege62b 44005  frege62c 44023
[Frege1879] p. 52Proposition 63frege63a 43979  frege63b 44006  frege63c 44024
[Frege1879] p. 53Proposition 64frege64a 43980  frege64b 44007  frege64c 44025
[Frege1879] p. 53Proposition 65frege65a 43981  frege65b 44008  frege65c 44026
[Frege1879] p. 54Proposition 66frege66a 43982  frege66b 44009  frege66c 44027
[Frege1879] p. 54Proposition 67frege67a 43983  frege67b 44010  frege67c 44028
[Frege1879] p. 54Proposition 68frege68a 43984  frege68b 44011  frege68c 44029
[Frege1879] p. 55Definition 69dffrege69 44030
[Frege1879] p. 58Proposition 70frege70 44031
[Frege1879] p. 59Proposition 71frege71 44032
[Frege1879] p. 59Proposition 72frege72 44033
[Frege1879] p. 59Proposition 73frege73 44034
[Frege1879] p. 60Definition 76dffrege76 44037
[Frege1879] p. 60Proposition 74frege74 44035
[Frege1879] p. 60Proposition 75frege75 44036
[Frege1879] p. 62Proposition 77frege77 44038  frege77d 43844
[Frege1879] p. 63Proposition 78frege78 44039
[Frege1879] p. 63Proposition 79frege79 44040
[Frege1879] p. 63Proposition 80frege80 44041
[Frege1879] p. 63Proposition 81frege81 44042  frege81d 43845
[Frege1879] p. 64Proposition 82frege82 44043
[Frege1879] p. 65Proposition 83frege83 44044  frege83d 43846
[Frege1879] p. 65Proposition 84frege84 44045
[Frege1879] p. 66Proposition 85frege85 44046
[Frege1879] p. 66Proposition 86frege86 44047
[Frege1879] p. 66Proposition 87frege87 44048  frege87d 43848
[Frege1879] p. 67Proposition 88frege88 44049
[Frege1879] p. 68Proposition 89frege89 44050
[Frege1879] p. 68Proposition 90frege90 44051
[Frege1879] p. 68Proposition 91frege91 44052  frege91d 43849
[Frege1879] p. 69Proposition 92frege92 44053
[Frege1879] p. 70Proposition 93frege93 44054
[Frege1879] p. 70Proposition 94frege94 44055
[Frege1879] p. 70Proposition 95frege95 44056
[Frege1879] p. 71Definition 99dffrege99 44060
[Frege1879] p. 71Proposition 96frege96 44057  frege96d 43847
[Frege1879] p. 71Proposition 97frege97 44058  frege97d 43850
[Frege1879] p. 71Proposition 98frege98 44059  frege98d 43851
[Frege1879] p. 72Proposition 100frege100 44061
[Frege1879] p. 72Proposition 101frege101 44062
[Frege1879] p. 72Proposition 102frege102 44063  frege102d 43852
[Frege1879] p. 73Proposition 103frege103 44064
[Frege1879] p. 73Proposition 104frege104 44065
[Frege1879] p. 73Proposition 105frege105 44066
[Frege1879] p. 73Proposition 106frege106 44067  frege106d 43853
[Frege1879] p. 74Proposition 107frege107 44068
[Frege1879] p. 74Proposition 108frege108 44069  frege108d 43854
[Frege1879] p. 74Proposition 109frege109 44070  frege109d 43855
[Frege1879] p. 75Proposition 110frege110 44071
[Frege1879] p. 75Proposition 111frege111 44072  frege111d 43857
[Frege1879] p. 76Proposition 112frege112 44073
[Frege1879] p. 76Proposition 113frege113 44074
[Frege1879] p. 76Proposition 114frege114 44075  frege114d 43856
[Frege1879] p. 77Definition 115dffrege115 44076
[Frege1879] p. 77Proposition 116frege116 44077
[Frege1879] p. 78Proposition 117frege117 44078
[Frege1879] p. 78Proposition 118frege118 44079
[Frege1879] p. 78Proposition 119frege119 44080
[Frege1879] p. 78Proposition 120frege120 44081
[Frege1879] p. 79Proposition 121frege121 44082
[Frege1879] p. 79Proposition 122frege122 44083  frege122d 43858
[Frege1879] p. 79Proposition 123frege123 44084
[Frege1879] p. 80Proposition 124frege124 44085  frege124d 43859
[Frege1879] p. 81Proposition 125frege125 44086
[Frege1879] p. 81Proposition 126frege126 44087  frege126d 43860
[Frege1879] p. 82Proposition 127frege127 44088
[Frege1879] p. 83Proposition 128frege128 44089
[Frege1879] p. 83Proposition 129frege129 44090  frege129d 43861
[Frege1879] p. 84Proposition 130frege130 44091
[Frege1879] p. 85Proposition 131frege131 44092  frege131d 43862
[Frege1879] p. 86Proposition 132frege132 44093
[Frege1879] p. 86Proposition 133frege133 44094  frege133d 43863
[Fremlin1] p. 13Definition 111G (b)df-salgen 46416
[Fremlin1] p. 13Definition 111G (d)borelmbl 46739
[Fremlin1] p. 13Proposition 111G (b)salgenss 46439
[Fremlin1] p. 14Definition 112Aismea 46554
[Fremlin1] p. 15Remark 112B (d)psmeasure 46574
[Fremlin1] p. 15Property 112C (a)meadjun 46565  meadjunre 46579
[Fremlin1] p. 15Property 112C (b)meassle 46566
[Fremlin1] p. 15Property 112C (c)meaunle 46567
[Fremlin1] p. 16Property 112C (d)iundjiun 46563  meaiunle 46572  meaiunlelem 46571
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46584  meaiuninc2 46585  meaiuninc3 46588  meaiuninc3v 46587  meaiunincf 46586  meaiuninclem 46583
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46590  meaiininc2 46591  meaiininclem 46589
[Fremlin1] p. 19Theorem 113Ccaragen0 46609  caragendifcl 46617  caratheodory 46631  omelesplit 46621
[Fremlin1] p. 19Definition 113Aisome 46597  isomennd 46634  isomenndlem 46633
[Fremlin1] p. 19Remark 113B (c)omeunle 46619
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46638  voncmpl 46724
[Fremlin1] p. 19Definition 113A (ii)omessle 46601
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46626  carageniuncllem1 46624  carageniuncllem2 46625  caragenuncl 46616  caragenuncllem 46615  caragenunicl 46627
[Fremlin1] p. 21Remark 113Dcaragenel2d 46635
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46629  caratheodorylem2 46630
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46638
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46697  hoidmv1lelem1 46694  hoidmv1lelem2 46695  hoidmv1lelem3 46696
[Fremlin1] p. 25Definition 114Eisvonmbl 46741
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46697  hoidmvle 46703  hoidmvlelem1 46698  hoidmvlelem2 46699  hoidmvlelem3 46700  hoidmvlelem4 46701  hoidmvlelem5 46702  hsphoidmvle2 46688  hsphoif 46679  hsphoival 46682
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46651
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46659
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46686  hoidmvn0val 46687  hoidmvval 46680  hoidmvval0 46690  hoidmvval0b 46693
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46691  hsphoidmvle 46689
[Fremlin1] p. 30Definition 115Cdf-ovoln 46640  df-voln 46642
[Fremlin1] p. 30Proposition 115D (a)dmovn 46707  ovn0 46669  ovn0lem 46668  ovnf 46666  ovnome 46676  ovnssle 46664  ovnsslelem 46663  ovnsupge0 46660
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46706  ovnhoilem1 46704  ovnhoilem2 46705  vonhoi 46770
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46723  hoidifhspf 46721  hoidifhspval 46711  hoidifhspval2 46718  hoidifhspval3 46722  hspmbl 46732  hspmbllem1 46729  hspmbllem2 46730  hspmbllem3 46731
[Fremlin1] p. 31Definition 115Evoncmpl 46724  vonmea 46677
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46675  ovnsubadd2 46749  ovnsubadd2lem 46748  ovnsubaddlem1 46673  ovnsubaddlem2 46674
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46734  hoimbl2 46768  hoimbllem 46733  hspdifhsp 46719  opnvonmbl 46737  opnvonmbllem2 46736
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46739
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46782  iccvonmbllem 46781  ioovonmbl 46780
[Fremlin1] p. 32Proposition 115G (d)vonicc 46788  vonicclem2 46787  vonioo 46785  vonioolem2 46784  vonn0icc 46791  vonn0icc2 46795  vonn0ioo 46790  vonn0ioo2 46793
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46792  snvonmbl 46789  vonct 46796  vonsn 46794
[Fremlin1] p. 35Lemma 121Asubsalsal 46462
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46461  subsaliuncllem 46460
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46828  salpreimalegt 46812  salpreimaltle 46829
[Fremlin1] p. 35Proposition 121B (i)issmf 46831  issmff 46837  issmflem 46830
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46848  issmflelem 46847  smfpreimale 46857
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46859  issmfgtlem 46858
[Fremlin1] p. 36Definition 121Cdf-smblfn 46799  issmf 46831  issmff 46837  issmfge 46873  issmfgelem 46872  issmfgt 46859  issmfgtlem 46858  issmfle 46848  issmflelem 46847  issmflem 46830
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46810  salpreimagtlt 46833  salpreimalelt 46832
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46873  issmfgelem 46872
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46856
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46854  cnfsmf 46843
[Fremlin1] p. 36Proposition 121D (c)decsmf 46870  decsmflem 46869  incsmf 46845  incsmflem 46844
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46804  pimconstlt1 46805  smfconst 46852
[Fremlin1] p. 37Proposition 121E (b)smfadd 46868  smfaddlem1 46866  smfaddlem2 46867
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46899
[Fremlin1] p. 37Proposition 121E (d)smfmul 46898  smfmullem1 46894  smfmullem2 46895  smfmullem3 46896  smfmullem4 46897
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46900
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46903  smfpimbor1lem2 46902
[Fremlin1] p. 37Proposition 121E (g)smfco 46905
[Fremlin1] p. 37Proposition 121E (h)smfres 46893
[Fremlin1] p. 38Proposition 121E (e)smfrec 46892
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46901  smfresal 46891
[Fremlin1] p. 38Proposition 121F (a)smflim 46880  smflim2 46909  smflimlem1 46874  smflimlem2 46875  smflimlem3 46876  smflimlem4 46877  smflimlem5 46878  smflimlem6 46879  smflimmpt 46913
[Fremlin1] p. 38Proposition 121F (b)smfsup 46917  smfsuplem1 46914  smfsuplem2 46915  smfsuplem3 46916  smfsupmpt 46918  smfsupxr 46919
[Fremlin1] p. 38Proposition 121F (c)smfinf 46921  smfinflem 46920  smfinfmpt 46922
[Fremlin1] p. 39Remark 121Gsmflim 46880  smflim2 46909  smflimmpt 46913
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46911
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46941  smfdivdmmbl2 46944  smfinfdmmbl 46952  smfinfdmmbllem 46951  smfsupdmmbl 46948  smfsupdmmbllem 46947
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46931  smflimsuplem2 46924  smflimsuplem6 46928  smflimsuplem7 46929  smflimsuplem8 46930  smflimsupmpt 46932
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46934  smfliminflem 46933  smfliminfmpt 46935
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46799
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46945  fsupdm2 46946
[Fremlin1], p. 39Proposition 121Hadddmmbl 46936  adddmmbl2 46937  finfdm 46949  finfdm2 46950  fsupdm 46945  fsupdm2 46946  muldmmbl 46938  muldmmbl2 46939
[Fremlin1], p. 39Proposition 121F (c)finfdm 46949  finfdm2 46950
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25470
[Fremlin5] p. 213Lemma 565Cauniioovol 25513
[Fremlin5] p. 214Lemma 565Cauniioombl 25523
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37744
[Fremlin5] p. 220Theorem 565Maftc1anc 37747
[FreydScedrov] p. 283Axiom of Infinityax-inf 9534  inf1 9518  inf2 9519
[Gleason] p. 117Proposition 9-2.1df-enq 10808  enqer 10818
[Gleason] p. 117Proposition 9-2.2df-1nq 10813  df-nq 10809
[Gleason] p. 117Proposition 9-2.3df-plpq 10805  df-plq 10811
[Gleason] p. 119Proposition 9-2.4caovmo 7589  df-mpq 10806  df-mq 10812
[Gleason] p. 119Proposition 9-2.5df-rq 10814
[Gleason] p. 119Proposition 9-2.6ltexnq 10872
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10873  ltbtwnnq 10875
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10868
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10869
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10876
[Gleason] p. 121Definition 9-3.1df-np 10878
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10890
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10892
[Gleason] p. 122Definitiondf-1p 10879
[Gleason] p. 122Remark (1)prub 10891
[Gleason] p. 122Lemma 9-3.4prlem934 10930
[Gleason] p. 122Proposition 9-3.2df-ltp 10882
[Gleason] p. 122Proposition 9-3.3ltsopr 10929  psslinpr 10928  supexpr 10951  suplem1pr 10949  suplem2pr 10950
[Gleason] p. 123Proposition 9-3.5addclpr 10915  addclprlem1 10913  addclprlem2 10914  df-plp 10880
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10919
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10918
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10931
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10940  ltexprlem1 10933  ltexprlem2 10934  ltexprlem3 10935  ltexprlem4 10936  ltexprlem5 10937  ltexprlem6 10938  ltexprlem7 10939
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10942  ltaprlem 10941
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10943
[Gleason] p. 124Lemma 9-3.6prlem936 10944
[Gleason] p. 124Proposition 9-3.7df-mp 10881  mulclpr 10917  mulclprlem 10916  reclem2pr 10945
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10926
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10921
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10920
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10925
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10948  reclem3pr 10946  reclem4pr 10947
[Gleason] p. 126Proposition 9-4.1df-enr 10952  enrer 10960
[Gleason] p. 126Proposition 9-4.2df-0r 10957  df-1r 10958  df-nr 10953
[Gleason] p. 126Proposition 9-4.3df-mr 10955  df-plr 10954  negexsr 10999  recexsr 11004  recexsrlem 11000
[Gleason] p. 127Proposition 9-4.4df-ltr 10956
[Gleason] p. 130Proposition 10-1.3creui 12126  creur 12125  cru 12123
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11085  axcnre 11061
[Gleason] p. 132Definition 10-3.1crim 15028  crimd 15145  crimi 15106  crre 15027  crred 15144  crrei 15105
[Gleason] p. 132Definition 10-3.2remim 15030  remimd 15111
[Gleason] p. 133Definition 10.36absval2 15197  absval2d 15361  absval2i 15311
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15054  cjaddd 15133  cjaddi 15101
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15055  cjmuld 15134  cjmuli 15102
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15053  cjcjd 15112  cjcji 15084
[Gleason] p. 133Proposition 10-3.4(f)cjre 15052  cjreb 15036  cjrebd 15115  cjrebi 15087  cjred 15139  rere 15035  rereb 15033  rerebd 15114  rerebi 15086  rered 15137
[Gleason] p. 133Proposition 10-3.4(h)addcj 15061  addcjd 15125  addcji 15096
[Gleason] p. 133Proposition 10-3.7(a)absval 15151
[Gleason] p. 133Proposition 10-3.7(b)abscj 15192  abscjd 15366  abscji 15315
[Gleason] p. 133Proposition 10-3.7(c)abs00 15202  abs00d 15362  abs00i 15312  absne0d 15363
[Gleason] p. 133Proposition 10-3.7(d)releabs 15235  releabsd 15367  releabsi 15316
[Gleason] p. 133Proposition 10-3.7(f)absmul 15207  absmuld 15370  absmuli 15318
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15195  sqabsaddi 15319
[Gleason] p. 133Proposition 10-3.7(h)abstri 15244  abstrid 15372  abstrii 15322
[Gleason] p. 134Definition 10-4.1df-exp 13975  exp0 13978  expp1 13981  expp1d 14060
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26621  cxpaddd 26659  expadd 14017  expaddd 14061  expaddz 14019
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26630  cxpmuld 26679  expmul 14020  expmuld 14062  expmulz 14021
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26627  mulcxpd 26670  mulexp 14014  mulexpd 14074  mulexpz 14015
[Gleason] p. 140Exercise 1znnen 16127
[Gleason] p. 141Definition 11-2.1fzval 13415
[Gleason] p. 168Proposition 12-2.1(a)climadd 15545  rlimadd 15556  rlimdiv 15559
[Gleason] p. 168Proposition 12-2.1(b)climsub 15547  rlimsub 15557
[Gleason] p. 168Proposition 12-2.1(c)climmul 15546  rlimmul 15558
[Gleason] p. 171Corollary 12-2.2climmulc2 15550
[Gleason] p. 172Corollary 12-2.5climrecl 15496
[Gleason] p. 172Proposition 12-2.4(c)climabs 15517  climcj 15518  climim 15520  climre 15519  rlimabs 15522  rlimcj 15523  rlimim 15525  rlimre 15524
[Gleason] p. 173Definition 12-3.1df-ltxr 11157  df-xr 11156  ltxr 13020
[Gleason] p. 175Definition 12-4.1df-limsup 15384  limsupval 15387
[Gleason] p. 180Theorem 12-5.1climsup 15583
[Gleason] p. 180Theorem 12-5.3caucvg 15592  caucvgb 15593  caucvgbf 45592  caucvgr 15589  climcau 15584
[Gleason] p. 182Exercise 3cvgcmp 15729
[Gleason] p. 182Exercise 4cvgrat 15796
[Gleason] p. 195Theorem 13-2.12abs1m 15249
[Gleason] p. 217Lemma 13-4.1btwnzge0 13738
[Gleason] p. 223Definition 14-1.1df-met 21291
[Gleason] p. 223Definition 14-1.1(a)met0 24264  xmet0 24263
[Gleason] p. 223Definition 14-1.1(b)metgt0 24280
[Gleason] p. 223Definition 14-1.1(c)metsym 24271
[Gleason] p. 223Definition 14-1.1(d)mettri 24273  mstri 24390  xmettri 24272  xmstri 24389
[Gleason] p. 225Definition 14-1.5xpsmet 24303
[Gleason] p. 230Proposition 14-2.6txlm 23569
[Gleason] p. 240Theorem 14-4.3metcnp4 25243
[Gleason] p. 240Proposition 14-4.2metcnp3 24461
[Gleason] p. 243Proposition 14-4.16addcn 24787  addcn2 15507  mulcn 24789  mulcn2 15509  subcn 24788  subcn2 15508
[Gleason] p. 295Remarkbcval3 14219  bcval4 14220
[Gleason] p. 295Equation 2bcpasc 14234
[Gleason] p. 295Definition of binomial coefficientbcval 14217  df-bc 14216
[Gleason] p. 296Remarkbcn0 14223  bcnn 14225
[Gleason] p. 296Theorem 15-2.8binom 15743
[Gleason] p. 308Equation 2ef0 16004
[Gleason] p. 308Equation 3efcj 16005
[Gleason] p. 309Corollary 15-4.3efne0 16011
[Gleason] p. 309Corollary 15-4.4efexp 16016
[Gleason] p. 310Equation 14sinadd 16079
[Gleason] p. 310Equation 15cosadd 16080
[Gleason] p. 311Equation 17sincossq 16091
[Gleason] p. 311Equation 18cosbnd 16096  sinbnd 16095
[Gleason] p. 311Lemma 15-4.7sqeqor 14129  sqeqori 14127
[Gleason] p. 311Definition of ` `df-pi 15985
[Godowski] p. 730Equation SFgoeqi 32260
[GodowskiGreechie] p. 249Equation IV3oai 31655
[Golan] p. 1Remarksrgisid 20133
[Golan] p. 1Definitiondf-srg 20111
[Golan] p. 149Definitiondf-slmd 33177
[Gonshor] p. 7Definitiondf-scut 27729
[Gonshor] p. 9Theorem 2.5slerec 27766  slerecd 27767
[Gonshor] p. 10Theorem 2.6cofcut1 27870  cofcut1d 27871
[Gonshor] p. 10Theorem 2.7cofcut2 27872  cofcut2d 27873
[Gonshor] p. 12Theorem 2.9cofcutr 27874  cofcutr1d 27875  cofcutr2d 27876
[Gonshor] p. 13Definitiondf-adds 27909
[Gonshor] p. 14Theorem 3.1addsprop 27925
[Gonshor] p. 15Theorem 3.2addsunif 27951
[Gonshor] p. 17Theorem 3.4mulsprop 28075
[Gonshor] p. 18Theorem 3.5mulsunif 28095
[Gonshor] p. 28Lemma 4.2halfcut 28384
[Gonshor] p. 28Theorem 4.2pw2cut 28386
[Gonshor] p. 30Theorem 4.2addhalfcut 28385
[Gonshor] p. 95Theorem 6.1addsbday 27966
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36210
[Gratzer] p. 23Section 0.6df-mre 17494
[Gratzer] p. 27Section 0.6df-mri 17496
[Hall] p. 1Section 1.1df-asslaw 48293  df-cllaw 48291  df-comlaw 48292
[Hall] p. 2Section 1.2df-clintop 48305
[Hall] p. 7Section 1.3df-sgrp2 48326
[Halmos] p. 28Partition ` `df-parts 38869  dfmembpart2 38874
[Halmos] p. 31Theorem 17.3riesz1 32052  riesz2 32053
[Halmos] p. 41Definition of Hermitianhmopadj2 31928
[Halmos] p. 42Definition of projector orderingpjordi 32160
[Halmos] p. 43Theorem 26.1elpjhmop 32172  elpjidm 32171  pjnmopi 32135
[Halmos] p. 44Remarkpjinormi 31674  pjinormii 31663
[Halmos] p. 44Theorem 26.2elpjch 32176  pjrn 31694  pjrni 31689  pjvec 31683
[Halmos] p. 44Theorem 26.3pjnorm2 31714
[Halmos] p. 44Theorem 26.4hmopidmpj 32141  hmopidmpji 32139
[Halmos] p. 45Theorem 27.1pjinvari 32178
[Halmos] p. 45Theorem 27.3pjoci 32167  pjocvec 31684
[Halmos] p. 45Theorem 27.4pjorthcoi 32156
[Halmos] p. 48Theorem 29.2pjssposi 32159
[Halmos] p. 48Theorem 29.3pjssdif1i 32162  pjssdif2i 32161
[Halmos] p. 50Definition of spectrumdf-spec 31842
[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 1796
[Hatcher] p. 25Definitiondf-phtpc 24924  df-phtpy 24903
[Hatcher] p. 26Definitiondf-pco 24938  df-pi1 24941
[Hatcher] p. 26Proposition 1.2phtpcer 24927
[Hatcher] p. 26Proposition 1.3pi1grp 24983
[Hefferon] p. 240Definition 3.12df-dmat 22411  df-dmatalt 48504
[Helfgott] p. 2Theoremtgoldbach 47922
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47907
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47919  bgoldbtbnd 47914  bgoldbtbnd 47914  tgblthelfgott 47920
[Helfgott] p. 5Proposition 1.1circlevma 34662
[Helfgott] p. 69Statement 7.49circlemethhgt 34663
[Helfgott] p. 69Statement 7.50hgt750lema 34677  hgt750lemb 34676  hgt750leme 34678  hgt750lemf 34673  hgt750lemg 34674
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47916  tgoldbachgt 34683  tgoldbachgtALTV 47917  tgoldbachgtd 34682
[Helfgott] p. 70Statement 7.49ax-hgt749 34664
[Herstein] p. 54Exercise 28df-grpo 30480
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18863  grpoideu 30496  mndideu 18659
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18893  grpoinveu 30506
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18924  grpo2inv 30518
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18937  grpoinvop 30520
[Herstein] p. 57Exercise 1dfgrp3e 18959
[Hitchcock] p. 5Rule A3mptnan 1769
[Hitchcock] p. 5Rule A4mptxor 1770
[Hitchcock] p. 5Rule A5mtpxor 1772
[Holland] p. 1519Theorem 2sumdmdi 32407
[Holland] p. 1520Lemma 5cdj1i 32420  cdj3i 32428  cdj3lem1 32421  cdjreui 32419
[Holland] p. 1524Lemma 7mddmdin0i 32418
[Holland95] p. 13Theorem 3.6hlathil 42066
[Holland95] p. 14Line 15hgmapvs 41996
[Holland95] p. 14Line 16hdmaplkr 42018
[Holland95] p. 14Line 17hdmapellkr 42019
[Holland95] p. 14Line 19hdmapglnm2 42016
[Holland95] p. 14Line 20hdmapip0com 42022
[Holland95] p. 14Theorem 3.6hdmapevec2 41941
[Holland95] p. 14Lines 24 and 25hdmapoc 42036
[Holland95] p. 204Definition of involutiondf-srng 20761
[Holland95] p. 212Definition of subspacedf-psubsp 39608
[Holland95] p. 214Lemma 3.3lclkrlem2v 41633
[Holland95] p. 214Definition 3.2df-lpolN 41586
[Holland95] p. 214Definition of nonsingularpnonsingN 40038
[Holland95] p. 215Lemma 3.3(1)dihoml4 41482  poml4N 40058
[Holland95] p. 215Lemma 3.3(2)dochexmid 41573  pexmidALTN 40083  pexmidN 40074
[Holland95] p. 218Theorem 3.6lclkr 41638
[Holland95] p. 218Definition of dual vector spacedf-ldual 39229  ldualset 39230
[Holland95] p. 222Item 1df-lines 39606  df-pointsN 39607
[Holland95] p. 222Item 2df-polarityN 40008
[Holland95] p. 223Remarkispsubcl2N 40052  omllaw4 39351  pol1N 40015  polcon3N 40022
[Holland95] p. 223Definitiondf-psubclN 40040
[Holland95] p. 223Equation for polaritypolval2N 40011
[Holmes] p. 40Definitiondf-xrn 38410
[Hughes] p. 44Equation 1.21bax-his3 31071
[Hughes] p. 47Definition of projection operatordfpjop 32169
[Hughes] p. 49Equation 1.30eighmre 31950  eigre 31822  eigrei 31821
[Hughes] p. 49Equation 1.31eighmorth 31951  eigorth 31825  eigorthi 31824
[Hughes] p. 137Remark (ii)eigposi 31823
[Huneke] p. 1Claim 1frgrncvvdeq 30296
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30292
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30293
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30294
[Huneke] p. 2Claim 2frgrregorufr 30312  frgrregorufr0 30311  frgrregorufrg 30313
[Huneke] p. 2Claim 3frgrhash2wsp 30319  frrusgrord 30328  frrusgrord0 30327
[Huneke] p. 2Statementdf-clwwlknon 30075
[Huneke] p. 2Statement 4frgrwopreglem4 30302
[Huneke] p. 2Statement 5frgrwopreg1 30305  frgrwopreg2 30306  frgrwopregasn 30303  frgrwopregbsn 30304
[Huneke] p. 2Statement 6frgrwopreglem5 30308
[Huneke] p. 2Statement 7fusgreghash2wspv 30322
[Huneke] p. 2Statement 8fusgreghash2wsp 30325
[Huneke] p. 2Statement 9clwlksndivn 30073  numclwlk1 30358  numclwlk1lem1 30356  numclwlk1lem2 30357  numclwwlk1 30348  numclwwlk8 30379
[Huneke] p. 2Definition 3frgrwopreglem1 30299
[Huneke] p. 2Definition 4df-clwlks 29756
[Huneke] p. 2Definition 62clwwlk 30334
[Huneke] p. 2Definition 7numclwwlkovh 30360  numclwwlkovh0 30359
[Huneke] p. 2Statement 10numclwwlk2 30368
[Huneke] p. 2Statement 11rusgrnumwlkg 29965
[Huneke] p. 2Statement 12numclwwlk3 30372
[Huneke] p. 2Statement 13numclwwlk5 30375
[Huneke] p. 2Statement 14numclwwlk7 30378
[Indrzejczak] p. 33Definition ` `Enatded 30390  natded 30390
[Indrzejczak] p. 33Definition ` `Inatded 30390
[Indrzejczak] p. 34Definition ` `Enatded 30390  natded 30390
[Indrzejczak] p. 34Definition ` `Inatded 30390
[Jech] p. 4Definition of classcv 1540  cvjust 2725
[Jech] p. 42Lemma 6.1alephexp1 10476
[Jech] p. 42Equation 6.1alephadd 10474  alephmul 10475
[Jech] p. 43Lemma 6.2infmap 10473  infmap2 10114
[Jech] p. 71Lemma 9.3jech9.3 9713
[Jech] p. 72Equation 9.3scott0 9785  scottex 9784
[Jech] p. 72Exercise 9.1rankval4 9766  rankval4b 35118
[Jech] p. 72Scheme "Collection Principle"cp 9790
[Jech] p. 78Noteopthprc 5683
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43013
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43101
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43102
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43025
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43029
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43030  rmyp1 43031
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43032  rmym1 43033
[JonesMatijasevic] p. 695Equation 2.11rmx0 43023  rmx1 43024  rmxluc 43034
[JonesMatijasevic] p. 695Equation 2.12rmy0 43027  rmy1 43028  rmyluc 43035
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43037
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43038
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43058  jm2.17b 43059  jm2.17c 43060
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43091
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43095
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43086
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43061  jm2.24nn 43057
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43100
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43106  rmygeid 43062
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43118
[Juillerat] p. 11Section *5etransc 46386  etransclem47 46384  etransclem48 46385
[Juillerat] p. 12Equation (7)etransclem44 46381
[Juillerat] p. 12Equation *(7)etransclem46 46383
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46369
[Juillerat] p. 13Proofetransclem35 46372
[Juillerat] p. 13Part of case 2 proven inetransclem38 46375
[Juillerat] p. 13Part of case 2 provenetransclem24 46361
[Juillerat] p. 13Part of case 2: proven inetransclem41 46378
[Juillerat] p. 14Proofetransclem23 46360
[KalishMontague] p. 81Note 1ax-6 1968
[KalishMontague] p. 85Lemma 2equid 2013
[KalishMontague] p. 85Lemma 3equcomi 2018
[KalishMontague] p. 86Lemma 7cbvalivw 2008  cbvaliw 2007  wl-cbvmotv 37564  wl-motae 37566  wl-moteq 37565
[KalishMontague] p. 87Lemma 8spimvw 1987  spimw 1971
[KalishMontague] p. 87Lemma 9spfw 2034  spw 2035
[Kalmbach] p. 14Definition of latticechabs1 31503  chabs1i 31505  chabs2 31504  chabs2i 31506  chjass 31520  chjassi 31473  latabs1 18387  latabs2 18388
[Kalmbach] p. 15Definition of atomdf-at 32325  ela 32326
[Kalmbach] p. 15Definition of coverscvbr2 32270  cvrval2 39379
[Kalmbach] p. 16Definitiondf-ol 39283  df-oml 39284
[Kalmbach] p. 20Definition of commutescmbr 31571  cmbri 31577  cmtvalN 39316  df-cm 31570  df-cmtN 39282
[Kalmbach] p. 22Remarkomllaw5N 39352  pjoml5 31600  pjoml5i 31575
[Kalmbach] p. 22Definitionpjoml2 31598  pjoml2i 31572
[Kalmbach] p. 22Theorem 2(v)cmcm 31601  cmcmi 31579  cmcmii 31584  cmtcomN 39354
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39350  omlsi 31391  pjoml 31423  pjomli 31422
[Kalmbach] p. 22Definition of OML lawomllaw2N 39349
[Kalmbach] p. 23Remarkcmbr2i 31583  cmcm3 31602  cmcm3i 31581  cmcm3ii 31586  cmcm4i 31582  cmt3N 39356  cmt4N 39357  cmtbr2N 39358
[Kalmbach] p. 23Lemma 3cmbr3 31595  cmbr3i 31587  cmtbr3N 39359
[Kalmbach] p. 25Theorem 5fh1 31605  fh1i 31608  fh2 31606  fh2i 31609  omlfh1N 39363
[Kalmbach] p. 65Remarkchjatom 32344  chslej 31485  chsleji 31445  shslej 31367  shsleji 31357
[Kalmbach] p. 65Proposition 1chocin 31482  chocini 31441  chsupcl 31327  chsupval2 31397  h0elch 31242  helch 31230  hsupval2 31396  ocin 31283  ococss 31280  shococss 31281
[Kalmbach] p. 65Definition of subspace sumshsval 31299
[Kalmbach] p. 66Remarkdf-pjh 31382  pjssmi 32152  pjssmii 31668
[Kalmbach] p. 67Lemma 3osum 31632  osumi 31629
[Kalmbach] p. 67Lemma 4pjci 32187
[Kalmbach] p. 103Exercise 6atmd2 32387
[Kalmbach] p. 103Exercise 12mdsl0 32297
[Kalmbach] p. 140Remarkhatomic 32347  hatomici 32346  hatomistici 32349
[Kalmbach] p. 140Proposition 1atlatmstc 39424
[Kalmbach] p. 140Proposition 1(i)atexch 32368  lsatexch 39148
[Kalmbach] p. 140Proposition 1(ii)chcv1 32342  cvlcvr1 39444  cvr1 39515
[Kalmbach] p. 140Proposition 1(iii)cvexch 32361  cvexchi 32356  cvrexch 39525
[Kalmbach] p. 149Remark 2chrelati 32351  hlrelat 39507  hlrelat5N 39506  lrelat 39119
[Kalmbach] p. 153Exercise 5lsmcv 21084  lsmsatcv 39115  spansncv 31640  spansncvi 31639
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39134  spansncv2 32280
[Kalmbach] p. 266Definitiondf-st 32198
[Kalmbach2] p. 8Definition of adjointdf-adjh 31836
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10543  fpwwe2 10540
[KanamoriPincus] p. 416Corollary 1.3canth4 10544
[KanamoriPincus] p. 417Corollary 1.6canthp1 10551
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10546
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10548
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10561
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10565  gchxpidm 10566
[KanamoriPincus] p. 419Theorem 2.1gchacg 10577  gchhar 10576
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10112  unxpwdom 9481
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10567
[Kreyszig] p. 3Property M1metcl 24253  xmetcl 24252
[Kreyszig] p. 4Property M2meteq0 24260
[Kreyszig] p. 8Definition 1.1-8dscmet 24493
[Kreyszig] p. 12Equation 5conjmul 11844  muleqadd 11767
[Kreyszig] p. 18Definition 1.3-2mopnval 24359
[Kreyszig] p. 19Remarkmopntopon 24360
[Kreyszig] p. 19Theorem T1mopn0 24419  mopnm 24365
[Kreyszig] p. 19Theorem T2unimopn 24417
[Kreyszig] p. 19Definition of neighborhoodneibl 24422
[Kreyszig] p. 20Definition 1.3-3metcnp2 24463
[Kreyszig] p. 25Definition 1.4-1lmbr 23179  lmmbr 25191  lmmbr2 25192
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23301
[Kreyszig] p. 28Theorem 1.4-5lmcau 25246
[Kreyszig] p. 28Definition 1.4-3iscau 25209  iscmet2 25227
[Kreyszig] p. 30Theorem 1.4-7cmetss 25249
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23382  metelcls 25238
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25239  metcld2 25240
[Kreyszig] p. 51Equation 2clmvneg1 25032  lmodvneg1 20844  nvinv 30626  vcm 30563
[Kreyszig] p. 51Equation 1aclm0vs 25028  lmod0vs 20834  slmd0vs 33200  vc0 30561
[Kreyszig] p. 51Equation 1blmodvs0 20835  slmdvs0 33201  vcz 30562
[Kreyszig] p. 58Definition 2.2-1imsmet 30678  ngpmet 24524  nrmmetd 24495
[Kreyszig] p. 59Equation 1imsdval 30673  imsdval2 30674  ncvspds 25094  ngpds 24525
[Kreyszig] p. 63Problem 1nmval 24510  nvnd 30675
[Kreyszig] p. 64Problem 2nmeq0 24539  nmge0 24538  nvge0 30660  nvz 30656
[Kreyszig] p. 64Problem 3nmrtri 24545  nvabs 30659
[Kreyszig] p. 91Definition 2.7-1isblo3i 30788
[Kreyszig] p. 92Equation 2df-nmoo 30732
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30794  blocni 30792
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30793
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25137  ipeq0 21581  ipz 30706
[Kreyszig] p. 135Problem 2cphpyth 25149  pythi 30837
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30841
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25171
[Kreyszig] p. 144Equation 4supcvg 15769
[Kreyszig] p. 144Theorem 3.3-1minvec 25369  minveco 30871
[Kreyszig] p. 196Definition 3.9-1df-aj 30737
[Kreyszig] p. 247Theorem 4.7-2bcth 25262
[Kreyszig] p. 249Theorem 4.7-3ubth 30860
[Kreyszig] p. 470Definition of positive operator orderingleop 32110  leopg 32109
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32128
[Kreyszig] p. 525Theorem 10.1-1htth 30905
[Kulpa] p. 547Theorempoimir 37699
[Kulpa] p. 547Equation (1)poimirlem32 37698
[Kulpa] p. 547Equation (2)poimirlem31 37697
[Kulpa] p. 548Theorembroucube 37700
[Kulpa] p. 548Equation (6)poimirlem26 37692
[Kulpa] p. 548Equation (7)poimirlem27 37693
[Kunen] p. 10Axiom 0ax6e 2383  axnul 5245
[Kunen] p. 11Axiom 3axnul 5245
[Kunen] p. 12Axiom 6zfrep6 7893
[Kunen] p. 24Definition 10.24mapval 8768  mapvalg 8766
[Kunen] p. 30Lemma 10.20fodomg 10419
[Kunen] p. 31Definition 10.24mapex 7877
[Kunen] p. 95Definition 2.1df-r1 9663
[Kunen] p. 97Lemma 2.10r1elss 9705  r1elssi 9704
[Kunen] p. 107Exercise 4rankop 9757  rankopb 9751  rankuni 9762  rankxplim 9778  rankxpsuc 9781
[Kunen2] p. 47Lemma I.9.9relpfr 45052
[Kunen2] p. 53Lemma I.9.21trfr 45060
[Kunen2] p. 53Lemma I.9.24(2)wffr 45059
[Kunen2] p. 53Definition I.9.20tcfr 45061
[Kunen2] p. 95Lemma I.16.2ralabso 45066  rexabso 45067
[Kunen2] p. 96Example I.16.3disjabso 45073  n0abso 45074  ssabso 45072
[Kunen2] p. 111Lemma II.2.4(1)traxext 45075
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45085
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45080
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45083
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45084
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45079
[Kunen2] p. 112Corollary II.2.5wfaxext 45091  wfaxpr 45096  wfaxreg 45098  wfaxrep 45092  wfaxsep 45093  wfaxun 45097
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45082
[Kunen2] p. 113Corollary II.2.9wfaxpow 45095
[Kunen2] p. 114Theorem II.2.13wfaxext 45091
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45090  omelaxinf2 45087
[Kunen2] p. 114Corollary II.2.12wfac8prim 45100  wfaxinf2 45099
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45113  permaxext 45103  permaxinf2 45111  permaxnul 45106  permaxpow 45107  permaxpr 45108  permaxrep 45104  permaxsep 45105  permaxun 45109
[Kunen2] p. 148Definition II.9.1brpermmodel 45101
[Kunen2] p. 149Exercise II.9.3permac8prim 45112
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4954
[Lang] , p. 225Corollary 1.3finexttrb 33685
[Lang] p. Definitiondf-rn 5630
[Lang] p. 3Statementlidrideqd 18583  mndbn0 18664
[Lang] p. 3Definitiondf-mnd 18649
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18601
[Lang] p. 4Property of composites. Second formulagsumccat 18755
[Lang] p. 5Equationgsumreidx 19835
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48287
[Lang] p. 6Examplenn0mnd 48284
[Lang] p. 6Equationgsumxp2 19898
[Lang] p. 6Statementcycsubm 19120
[Lang] p. 6Definitionmulgnn0gsum 18999
[Lang] p. 6Observationmndlsmidm 19588
[Lang] p. 7Definitiondfgrp2e 18882
[Lang] p. 30Definitiondf-tocyc 33083
[Lang] p. 32Property (a)cyc3genpm 33128
[Lang] p. 32Property (b)cyc3conja 33133  cycpmconjv 33118
[Lang] p. 53Definitiondf-cat 17580
[Lang] p. 53Axiom CAT 1cat1 18010  cat1lem 18009
[Lang] p. 54Definitiondf-iso 17662
[Lang] p. 57Definitiondf-inito 17897  df-termo 17898
[Lang] p. 58Exampleirinitoringc 21422
[Lang] p. 58Statementinitoeu1 17924  termoeu1 17931
[Lang] p. 62Definitiondf-func 17771
[Lang] p. 65Definitiondf-nat 17859
[Lang] p. 91Notedf-ringc 20567
[Lang] p. 92Statementmxidlprm 33442
[Lang] p. 92Definitionisprmidlc 33419
[Lang] p. 128Remarkdsmmlmod 21688
[Lang] p. 129Prooflincscm 48536  lincscmcl 48538  lincsum 48535  lincsumcl 48537
[Lang] p. 129Statementlincolss 48540
[Lang] p. 129Observationdsmmfi 21681
[Lang] p. 141Theorem 5.3dimkerim 33647  qusdimsum 33648
[Lang] p. 141Corollary 5.4lssdimle 33627
[Lang] p. 147Definitionsnlindsntor 48577
[Lang] p. 504Statementmat1 22368  matring 22364
[Lang] p. 504Definitiondf-mamu 22312
[Lang] p. 505Statementmamuass 22323  mamutpos 22379  matassa 22365  mattposvs 22376  tposmap 22378
[Lang] p. 513Definitionmdet1 22522  mdetf 22516
[Lang] p. 513Theorem 4.4cramer 22612
[Lang] p. 514Proposition 4.6mdetleib 22508
[Lang] p. 514Proposition 4.8mdettpos 22532
[Lang] p. 515Definitiondf-minmar1 22556  smadiadetr 22596
[Lang] p. 515Corollary 4.9mdetero 22531  mdetralt 22529
[Lang] p. 517Proposition 4.15mdetmul 22544
[Lang] p. 518Definitiondf-madu 22555
[Lang] p. 518Proposition 4.16madulid 22566  madurid 22565  matinv 22598
[Lang] p. 561Theorem 3.1cayleyhamilton 22811
[Lang], p. 224Proposition 1.1extdgfialg 33714  finextalg 33718
[Lang], p. 224Proposition 1.2extdgmul 33683  fedgmul 33651
[Lang], p. 225Proposition 1.4algextdeg 33745
[Lang], p. 561Remarkchpmatply1 22753
[Lang], p. 561Definitiondf-chpmat 22748
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44432
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44427
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44433
[LeBlanc] p. 277Rule R2axnul 5245
[Levy] p. 12Axiom 4.3.1df-clab 2710
[Levy] p. 59Definitiondf-ttrcl 9604
[Levy] p. 64Theorem 5.6(ii)frinsg 9650
[Levy] p. 338Axiomdf-clel 2806  df-cleq 2723
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2806  df-cleq 2723
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2710
[Levy] p. 358Axiomdf-clab 2710
[Levy58] p. 2Definition Iisfin1-3 10283
[Levy58] p. 2Definition IIdf-fin2 10183
[Levy58] p. 2Definition Iadf-fin1a 10182
[Levy58] p. 2Definition IIIdf-fin3 10185
[Levy58] p. 3Definition Vdf-fin5 10186
[Levy58] p. 3Definition IVdf-fin4 10184
[Levy58] p. 4Definition VIdf-fin6 10187
[Levy58] p. 4Definition VIIdf-fin7 10188
[Levy58], p. 3Theorem 1fin1a2 10312
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27631
[Lipparini] p. 3Lemma 2.1.4noresle 27642
[Lipparini] p. 6Proposition 4.2noinfbnd1 27674  nosupbnd1 27659
[Lipparini] p. 6Proposition 4.3noinfbnd2 27676  nosupbnd2 27661
[Lipparini] p. 7Theorem 5.1noetasuplem3 27680  noetasuplem4 27681
[Lipparini] p. 7Corollary 4.4nosupinfsep 27677
[Lopez-Astorga] p. 12Rule 1mptnan 1769
[Lopez-Astorga] p. 12Rule 2mptxor 1770
[Lopez-Astorga] p. 12Rule 3mtpxor 1772
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32395
[Maeda] p. 168Lemma 5mdsym 32399  mdsymi 32398
[Maeda] p. 168Lemma 4(i)mdsymlem4 32393  mdsymlem6 32395  mdsymlem7 32396
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32397
[MaedaMaeda] p. 1Remarkssdmd1 32300  ssdmd2 32301  ssmd1 32298  ssmd2 32299
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32296
[MaedaMaeda] p. 1Definition 1.1df-dmd 32268  df-md 32267  mdbr 32281
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32318  mdslj1i 32306  mdslj2i 32307  mdslle1i 32304  mdslle2i 32305  mdslmd1i 32316  mdslmd2i 32317
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32308  mdsl2bi 32310  mdsl2i 32309
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32322
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32319
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32320
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32297
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32302  mdsl3 32303
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32321
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32416
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39426  hlrelat1 39505
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39144
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32323  cvmdi 32311  cvnbtwn4 32276  cvrnbtwn4 39384
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32324
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39445  cvp 32362  cvrp 39521  lcvp 39145
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32386
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32385
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39438  hlexch4N 39497
[MaedaMaeda] p. 34Exercise 7.1atabsi 32388
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39548
[MaedaMaeda] p. 61Definition 15.10psubN 39854  atpsubN 39858  df-pointsN 39607  pointpsubN 39856
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39609  pmap11 39867  pmaple 39866  pmapsub 39873  pmapval 39862
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39870  pmap1N 39872
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39875  pmapglb2N 39876  pmapglb2xN 39877  pmapglbx 39874
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39957
[MaedaMaeda] p. 67Postulate PS1ps-1 39582
[MaedaMaeda] p. 68Lemma 16.2df-padd 39901  paddclN 39947  paddidm 39946
[MaedaMaeda] p. 68Condition PS2ps-2 39583
[MaedaMaeda] p. 68Equation 16.2.1paddass 39943
[MaedaMaeda] p. 69Lemma 16.4ps-1 39582
[MaedaMaeda] p. 69Theorem 16.4ps-2 39583
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19593  lsmmod2 19594  lssats 39117  shatomici 32345  shatomistici 32348  shmodi 31377  shmodsi 31376
[MaedaMaeda] p. 130Remark 29.6dmdmd 32287  mdsymlem7 32396
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31576
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31480
[MaedaMaeda] p. 139Remarksumdmdii 32402
[Margaris] p. 40Rule Cexlimiv 1931
[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 1781  df-or 848  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30387
[Margaris] p. 59Section 14notnotrALTVD 45012
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45013
[Margaris] p. 79Rule Cexinst01 44723  exinst11 44724
[Margaris] p. 89Theorem 19.219.2 1977  19.2g 2191  r19.2z 4444
[Margaris] p. 89Theorem 19.319.3 2205  rr19.3v 3617
[Margaris] p. 89Theorem 19.5alcom 2162
[Margaris] p. 89Theorem 19.6alex 1827
[Margaris] p. 89Theorem 19.7alnex 1782
[Margaris] p. 89Theorem 19.819.8a 2184
[Margaris] p. 89Theorem 19.919.9 2208  19.9h 2288  exlimd 2221  exlimdh 2292
[Margaris] p. 89Theorem 19.11excom 2165  excomim 2166
[Margaris] p. 89Theorem 19.1219.12 2328
[Margaris] p. 90Section 19conventions-labels 30388  conventions-labels 30388  conventions-labels 30388  conventions-labels 30388
[Margaris] p. 90Theorem 19.14exnal 1828
[Margaris] p. 90Theorem 19.152albi 44476  albi 1819
[Margaris] p. 90Theorem 19.1619.16 2228
[Margaris] p. 90Theorem 19.1719.17 2229
[Margaris] p. 90Theorem 19.182exbi 44478  exbi 1848
[Margaris] p. 90Theorem 19.1919.19 2232
[Margaris] p. 90Theorem 19.202alim 44475  2alimdv 1919  alimd 2215  alimdh 1818  alimdv 1917  ax-4 1810  ralimdaa 3233  ralimdv 3146  ralimdva 3144  ralimdvva 3179  sbcimdv 3805
[Margaris] p. 90Theorem 19.2119.21 2210  19.21h 2289  19.21t 2209  19.21vv 44474  alrimd 2218  alrimdd 2217  alrimdh 1864  alrimdv 1930  alrimi 2216  alrimih 1825  alrimiv 1928  alrimivv 1929  hbralrimi 3122  r19.21be 3225  r19.21bi 3224  ralrimd 3237  ralrimdv 3130  ralrimdva 3132  ralrimdvv 3176  ralrimdvva 3187  ralrimi 3230  ralrimia 3231  ralrimiv 3123  ralrimiva 3124  ralrimivv 3173  ralrimivva 3175  ralrimivvva 3178  ralrimivw 3128
[Margaris] p. 90Theorem 19.222exim 44477  2eximdv 1920  exim 1835  eximd 2219  eximdh 1865  eximdv 1918  rexim 3073  reximd2a 3242  reximdai 3234  reximdd 45250  reximddv 3148  reximddv2 3191  reximddv3 3149  reximdv 3147  reximdv2 3142  reximdva 3145  reximdvai 3143  reximdvva 3180  reximi2 3065
[Margaris] p. 90Theorem 19.2319.23 2214  19.23bi 2194  19.23h 2290  19.23t 2213  exlimdv 1934  exlimdvv 1935  exlimexi 44622  exlimiv 1931  exlimivv 1933  rexlimd3 45246  rexlimdv 3131  rexlimdv3a 3137  rexlimdva 3133  rexlimdva2 3135  rexlimdvaa 3134  rexlimdvv 3188  rexlimdvva 3189  rexlimdvvva 3190  rexlimdvw 3138  rexlimiv 3126  rexlimiva 3125  rexlimivv 3174
[Margaris] p. 90Theorem 19.2419.24 1992
[Margaris] p. 90Theorem 19.2519.25 1881
[Margaris] p. 90Theorem 19.2619.26 1871
[Margaris] p. 90Theorem 19.2719.27 2230  r19.27z 4454  r19.27zv 4455
[Margaris] p. 90Theorem 19.2819.28 2231  19.28vv 44484  r19.28z 4447  r19.28zf 45261  r19.28zv 4450  rr19.28v 3618
[Margaris] p. 90Theorem 19.2919.29 1874  r19.29d2r 3119  r19.29imd 3097
[Margaris] p. 90Theorem 19.3019.30 1882
[Margaris] p. 90Theorem 19.3119.31 2237  19.31vv 44482
[Margaris] p. 90Theorem 19.3219.32 2236  r19.32 47203
[Margaris] p. 90Theorem 19.3319.33-2 44480  19.33 1885
[Margaris] p. 90Theorem 19.3419.34 1993
[Margaris] p. 90Theorem 19.3519.35 1878
[Margaris] p. 90Theorem 19.3619.36 2233  19.36vv 44481  r19.36zv 4456
[Margaris] p. 90Theorem 19.3719.37 2235  19.37vv 44483  r19.37zv 4451
[Margaris] p. 90Theorem 19.3819.38 1840
[Margaris] p. 90Theorem 19.3919.39 1991
[Margaris] p. 90Theorem 19.4019.40-2 1888  19.40 1887  r19.40 3098
[Margaris] p. 90Theorem 19.4119.41 2238  19.41rg 44648
[Margaris] p. 90Theorem 19.4219.42 2239
[Margaris] p. 90Theorem 19.4319.43 1883
[Margaris] p. 90Theorem 19.4419.44 2240  r19.44zv 4453
[Margaris] p. 90Theorem 19.4519.45 2241  r19.45zv 4452
[Margaris] p. 110Exercise 2(b)eu1 2605
[Mayet] p. 370Remarkjpi 32257  largei 32254  stri 32244
[Mayet3] p. 9Definition of CH-statesdf-hst 32199  ishst 32201
[Mayet3] p. 10Theoremhstrbi 32253  hstri 32252
[Mayet3] p. 1223Theorem 4.1mayete3i 31715
[Mayet3] p. 1240Theorem 7.1mayetes3i 31716
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32265
[MegPav2000] p. 2345Definition 3.4-1chintcl 31319  chsupcl 31327
[MegPav2000] p. 2345Definition 3.4-2hatomic 32347
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32341
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32368
[MegPav2000] p. 2366Figure 7pl42N 40088
[MegPav2002] p. 362Lemma 2.2latj31 18399  latj32 18397  latjass 18395
[Megill] p. 444Axiom C5ax-5 1911  ax5ALT 39012
[Megill] p. 444Section 7conventions 30387
[Megill] p. 445Lemma L12aecom-o 39006  ax-c11n 38993  axc11n 2426
[Megill] p. 446Lemma L17equtrr 2023
[Megill] p. 446Lemma L18ax6fromc10 39001
[Megill] p. 446Lemma L19hbnae-o 39033  hbnae 2432
[Megill] p. 447Remark 9.1dfsb1 2481  sbid 2258  sbidd-misc 49825  sbidd 49824
[Megill] p. 448Remark 9.6axc14 2463
[Megill] p. 448Scheme C4'ax-c4 38989
[Megill] p. 448Scheme C5'ax-c5 38988  sp 2186
[Megill] p. 448Scheme C6'ax-11 2160
[Megill] p. 448Scheme C7'ax-c7 38990
[Megill] p. 448Scheme C8'ax-7 2009
[Megill] p. 448Scheme C9'ax-c9 38995
[Megill] p. 448Scheme C10'ax-6 1968  ax-c10 38991
[Megill] p. 448Scheme C11'ax-c11 38992
[Megill] p. 448Scheme C12'ax-8 2113
[Megill] p. 448Scheme C13'ax-9 2121
[Megill] p. 448Scheme C14'ax-c14 38996
[Megill] p. 448Scheme C15'ax-c15 38994
[Megill] p. 448Scheme C16'ax-c16 38997
[Megill] p. 448Theorem 9.4dral1-o 39009  dral1 2439  dral2-o 39035  dral2 2438  drex1 2441  drex2 2442  drsb1 2495  drsb2 2269
[Megill] p. 449Theorem 9.7sbcom2 2176  sbequ 2086  sbid2v 2509
[Megill] p. 450Example in Appendixhba1-o 39002  hba1 2295
[Mendelson] p. 35Axiom A3hirstL-ax3 46997
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3825  rspsbca 3826  stdpc4 2071
[Mendelson] p. 69Axiom 5ax-c4 38989  ra4 3832  stdpc5 2211
[Mendelson] p. 81Rule Cexlimiv 1931
[Mendelson] p. 95Axiom 6stdpc6 2029
[Mendelson] p. 95Axiom 7stdpc7 2253
[Mendelson] p. 225Axiom system NBGru 3734
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5457
[Mendelson] p. 231Exercise 4.10(k)inv1 4347
[Mendelson] p. 231Exercise 4.10(l)unv 4348
[Mendelson] p. 231Exercise 4.10(n)dfin3 4226
[Mendelson] p. 231Exercise 4.10(o)df-nul 4283
[Mendelson] p. 231Exercise 4.10(q)dfin4 4227
[Mendelson] p. 231Exercise 4.10(s)ddif 4090
[Mendelson] p. 231Definition of uniondfun3 4225
[Mendelson] p. 235Exercise 4.12(c)univ 5394
[Mendelson] p. 235Exercise 4.12(d)pwv 4855
[Mendelson] p. 235Exercise 4.12(j)pwin 5510
[Mendelson] p. 235Exercise 4.12(k)pwunss 4567
[Mendelson] p. 235Exercise 4.12(l)pwssun 5511
[Mendelson] p. 235Exercise 4.12(n)uniin 4882
[Mendelson] p. 235Exercise 4.12(p)reli 5771
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6222
[Mendelson] p. 244Proposition 4.8(g)epweon 7714
[Mendelson] p. 246Definition of successordf-suc 6318
[Mendelson] p. 250Exercise 4.36oelim2 8516
[Mendelson] p. 254Proposition 4.22(b)xpen 9059
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8980  xpsneng 8981
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8987  xpcomeng 8988
[Mendelson] p. 254Proposition 4.22(e)xpassen 8990
[Mendelson] p. 255Definitionbrsdom 8903
[Mendelson] p. 255Exercise 4.39endisj 8983
[Mendelson] p. 255Exercise 4.41mapprc 8760
[Mendelson] p. 255Exercise 4.43mapsnen 8965  mapsnend 8964
[Mendelson] p. 255Exercise 4.45mapunen 9065
[Mendelson] p. 255Exercise 4.47xpmapen 9064
[Mendelson] p. 255Exercise 4.42(a)map0e 8812
[Mendelson] p. 255Exercise 4.42(b)map1 8968
[Mendelson] p. 257Proposition 4.24(a)undom 8984
[Mendelson] p. 258Exercise 4.56(c)djuassen 10076  djucomen 10075
[Mendelson] p. 258Exercise 4.56(f)djudom1 10080
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10074
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8452
[Mendelson] p. 266Proposition 4.34(f)oaordex 8479
[Mendelson] p. 275Proposition 4.42(d)entri3 10456
[Mendelson] p. 281Definitiondf-r1 9663
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9712
[Mendelson] p. 287Axiom system MKru 3734
[MertziosUnger] p. 152Definitiondf-frgr 30246
[MertziosUnger] p. 153Remark 1frgrconngr 30281
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30283  vdgn1frgrv3 30284
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30285
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30278
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30271  2pthfrgrrn 30269  2pthfrgrrn2 30270
[Mittelstaedt] p. 9Definitiondf-oc 31239
[Monk1] p. 22Remarkconventions 30387
[Monk1] p. 22Theorem 3.1conventions 30387
[Monk1] p. 26Theorem 2.8(vii)ssin 4188
[Monk1] p. 33Theorem 3.2(i)ssrel 5727  ssrelf 32605
[Monk1] p. 33Theorem 3.2(ii)eqrel 5728
[Monk1] p. 34Definition 3.3df-opab 5156
[Monk1] p. 36Theorem 3.7(i)coi1 6216  coi2 6217
[Monk1] p. 36Theorem 3.8(v)dm0 5865  rn0 5871
[Monk1] p. 36Theorem 3.7(ii)cnvi 6094
[Monk1] p. 37Theorem 3.13(i)relxp 5637
[Monk1] p. 37Theorem 3.13(x)dmxp 5874  rnxp 6123
[Monk1] p. 37Theorem 3.13(ii)0xp 5718  xp0 5719
[Monk1] p. 38Theorem 3.16(ii)ima0 6031
[Monk1] p. 38Theorem 3.16(viii)imai 6028
[Monk1] p. 39Theorem 3.17imaex 7850  imaexg 7849
[Monk1] p. 39Theorem 3.16(xi)imassrn 6025
[Monk1] p. 41Theorem 4.3(i)fnopfv 7014  funfvop 6989
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6882
[Monk1] p. 42Theorem 4.4(iii)fvelima 6893
[Monk1] p. 43Theorem 4.6funun 6533
[Monk1] p. 43Theorem 4.8(iv)dff13 7194  dff13f 7195
[Monk1] p. 46Theorem 4.15(v)funex 7159  funrnex 7892
[Monk1] p. 50Definition 5.4fniunfv 7187
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6180
[Monk1] p. 52Theorem 5.11(viii)ssint 4914
[Monk1] p. 52Definition 5.13 (i)1stval2 7944  df-1st 7927
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7945  df-2nd 7928
[Monk1] p. 112Theorem 15.17(v)ranksn 9753  ranksnb 9726
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9754
[Monk1] p. 112Theorem 15.17(iii)rankun 9755  rankunb 9749
[Monk1] p. 113Theorem 15.18r1val3 9737
[Monk1] p. 113Definition 15.19df-r1 9663  r1val2 9736
[Monk1] p. 117Lemmazorn2 10403  zorn2g 10400
[Monk1] p. 133Theorem 18.11cardom 9885
[Monk1] p. 133Theorem 18.12canth3 10458
[Monk1] p. 133Theorem 18.14carduni 9880
[Monk2] p. 105Axiom C4ax-4 1810
[Monk2] p. 105Axiom C7ax-7 2009
[Monk2] p. 105Axiom C8ax-12 2180  ax-c15 38994  ax12v2 2182
[Monk2] p. 108Lemma 5ax-c4 38989
[Monk2] p. 109Lemma 12ax-11 2160
[Monk2] p. 109Lemma 15equvini 2455  equvinv 2030  eqvinop 5430
[Monk2] p. 113Axiom C5-1ax-5 1911  ax5ALT 39012
[Monk2] p. 113Axiom C5-2ax-10 2144
[Monk2] p. 113Axiom C5-3ax-11 2160
[Monk2] p. 114Lemma 21sp 2186
[Monk2] p. 114Lemma 22axc4 2322  hba1-o 39002  hba1 2295
[Monk2] p. 114Lemma 23nfia1 2156
[Monk2] p. 114Lemma 24nfa2 2179  nfra2 3342  nfra2w 3268
[Moore] p. 53Part Idf-mre 17494
[Munkres] p. 77Example 2distop 22916  indistop 22923  indistopon 22922
[Munkres] p. 77Example 3fctop 22925  fctop2 22926
[Munkres] p. 77Example 4cctop 22927
[Munkres] p. 78Definition of basisdf-bases 22867  isbasis3g 22870
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17353  tgval2 22877
[Munkres] p. 79Remarktgcl 22890
[Munkres] p. 80Lemma 2.1tgval3 22884
[Munkres] p. 80Lemma 2.2tgss2 22908  tgss3 22907
[Munkres] p. 81Lemma 2.3basgen 22909  basgen2 22910
[Munkres] p. 83Exercise 3topdifinf 37400  topdifinfeq 37401  topdifinffin 37399  topdifinfindis 37397
[Munkres] p. 89Definition of subspace topologyresttop 23081
[Munkres] p. 93Theorem 6.1(1)0cld 22959  topcld 22956
[Munkres] p. 93Theorem 6.1(2)iincld 22960
[Munkres] p. 93Theorem 6.1(3)uncld 22962
[Munkres] p. 94Definition of closureclsval 22958
[Munkres] p. 94Definition of interiorntrval 22957
[Munkres] p. 95Theorem 6.5(a)clsndisj 22996  elcls 22994
[Munkres] p. 95Theorem 6.5(b)elcls3 23004
[Munkres] p. 97Theorem 6.6clslp 23069  neindisj 23038
[Munkres] p. 97Corollary 6.7cldlp 23071
[Munkres] p. 97Definition of limit pointislp2 23066  lpval 23060
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23236
[Munkres] p. 102Definition of continuous functiondf-cn 23148  iscn 23156  iscn2 23159
[Munkres] p. 107Theorem 7.2(g)cncnp 23201  cncnp2 23202  cncnpi 23199  df-cnp 23149  iscnp 23158  iscnp2 23160
[Munkres] p. 127Theorem 10.1metcn 24464
[Munkres] p. 128Theorem 10.3metcn4 25244
[Nathanson] p. 123Remarkreprgt 34641  reprinfz1 34642  reprlt 34639
[Nathanson] p. 123Definitiondf-repr 34629
[Nathanson] p. 123Chapter 5.1circlemethnat 34661
[Nathanson] p. 123Propositionbreprexp 34653  breprexpnat 34654  itgexpif 34626
[NielsenChuang] p. 195Equation 4.73unierri 32091
[OeSilva] p. 2042Section 2ax-bgbltosilva 47915
[Pfenning] p. 17Definition XMnatded 30390
[Pfenning] p. 17Definition NNCnatded 30390  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30390
[Pfenning] p. 18Rule"natded 30390
[Pfenning] p. 18Definition /\Inatded 30390
[Pfenning] p. 18Definition ` `Enatded 30390  natded 30390  natded 30390  natded 30390  natded 30390
[Pfenning] p. 18Definition ` `Inatded 30390  natded 30390  natded 30390  natded 30390  natded 30390
[Pfenning] p. 18Definition ` `ELnatded 30390
[Pfenning] p. 18Definition ` `ERnatded 30390
[Pfenning] p. 18Definition ` `Ea,unatded 30390
[Pfenning] p. 18Definition ` `IRnatded 30390
[Pfenning] p. 18Definition ` `Ianatded 30390
[Pfenning] p. 127Definition =Enatded 30390
[Pfenning] p. 127Definition =Inatded 30390
[Ponnusamy] p. 361Theorem 6.44cphip0l 25135  df-dip 30688  dip0l 30705  ip0l 21579
[Ponnusamy] p. 361Equation 6.45cphipval 25176  ipval 30690
[Ponnusamy] p. 362Equation I1dipcj 30701  ipcj 21577
[Ponnusamy] p. 362Equation I3cphdir 25138  dipdir 30829  ipdir 21582  ipdiri 30817
[Ponnusamy] p. 362Equation I4ipidsq 30697  nmsq 25127
[Ponnusamy] p. 362Equation 6.46ip0i 30812
[Ponnusamy] p. 362Equation 6.47ip1i 30814
[Ponnusamy] p. 362Equation 6.48ip2i 30815
[Ponnusamy] p. 363Equation I2cphass 25144  dipass 30832  ipass 21588  ipassi 30828
[Prugovecki] p. 186Definition of brabraval 31931  df-bra 31837
[Prugovecki] p. 376Equation 8.1df-kb 31838  kbval 31941
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32369
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39993
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32383  atcvat4i 32384  cvrat3 39547  cvrat4 39548  lsatcvat3 39157
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32269  cvrval 39374  df-cv 32266  df-lcv 39124  lspsncv0 21089
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40005
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40006
[Quine] p. 16Definition 2.1df-clab 2710  rabid 3416  rabidd 45257
[Quine] p. 17Definition 2.1''dfsb7 2281
[Quine] p. 18Definition 2.7df-cleq 2723
[Quine] p. 19Definition 2.9conventions 30387  df-v 3438
[Quine] p. 34Theorem 5.1eqabb 2870
[Quine] p. 35Theorem 5.2abid1 2867  abid2f 2925
[Quine] p. 40Theorem 6.1sb5 2278
[Quine] p. 40Theorem 6.2sb6 2088  sbalex 2245
[Quine] p. 41Theorem 6.3df-clel 2806
[Quine] p. 41Theorem 6.4eqid 2731  eqid1 30454
[Quine] p. 41Theorem 6.5eqcom 2738
[Quine] p. 42Theorem 6.6df-sbc 3737
[Quine] p. 42Theorem 6.7dfsbcq 3738  dfsbcq2 3739
[Quine] p. 43Theorem 6.8vex 3440
[Quine] p. 43Theorem 6.9isset 3450
[Quine] p. 44Theorem 7.3spcgf 3541  spcgv 3546  spcimgf 3503
[Quine] p. 44Theorem 6.11spsbc 3749  spsbcd 3750
[Quine] p. 44Theorem 6.12elex 3457
[Quine] p. 44Theorem 6.13elab 3630  elabg 3627  elabgf 3625
[Quine] p. 44Theorem 6.14noel 4287
[Quine] p. 48Theorem 7.2snprc 4669
[Quine] p. 48Definition 7.1df-pr 4578  df-sn 4576
[Quine] p. 49Theorem 7.4snss 4736  snssg 4735
[Quine] p. 49Theorem 7.5prss 4771  prssg 4770
[Quine] p. 49Theorem 7.6prid1 4714  prid1g 4712  prid2 4715  prid2g 4713  snid 4614  snidg 4612
[Quine] p. 51Theorem 7.12snex 5376
[Quine] p. 51Theorem 7.13prex 5377
[Quine] p. 53Theorem 8.2unisn 4877  unisnALT 45023  unisng 4876
[Quine] p. 53Theorem 8.3uniun 4881
[Quine] p. 54Theorem 8.6elssuni 4889
[Quine] p. 54Theorem 8.7uni0 4886
[Quine] p. 56Theorem 8.17uniabio 6457
[Quine] p. 56Definition 8.18dfaiota2 47191  dfiota2 6444
[Quine] p. 57Theorem 8.19aiotaval 47200  iotaval 6461
[Quine] p. 57Theorem 8.22iotanul 6467
[Quine] p. 58Theorem 8.23iotaex 6463
[Quine] p. 58Definition 9.1df-op 4582
[Quine] p. 61Theorem 9.5opabid 5468  opabidw 5467  opelopab 5485  opelopaba 5479  opelopabaf 5487  opelopabf 5488  opelopabg 5481  opelopabga 5476  opelopabgf 5483  oprabid 7384  oprabidw 7383
[Quine] p. 64Definition 9.11df-xp 5625
[Quine] p. 64Definition 9.12df-cnv 5627
[Quine] p. 64Definition 9.15df-id 5514
[Quine] p. 65Theorem 10.3fun0 6552
[Quine] p. 65Theorem 10.4funi 6519
[Quine] p. 65Theorem 10.5funsn 6540  funsng 6538
[Quine] p. 65Definition 10.1df-fun 6489
[Quine] p. 65Definition 10.2args 6046  dffv4 6825
[Quine] p. 68Definition 10.11conventions 30387  df-fv 6495  fv2 6823
[Quine] p. 124Theorem 17.3nn0opth2 14185  nn0opth2i 14184  nn0opthi 14183  omopthi 8582
[Quine] p. 177Definition 25.2df-rdg 8335
[Quine] p. 232Equation icarddom 10451
[Quine] p. 284Axiom 39(vi)funimaex 6575  funimaexg 6574
[Quine] p. 331Axiom system NFru 3734
[ReedSimon] p. 36Definition (iii)ax-his3 31071
[ReedSimon] p. 63Exercise 4(a)df-dip 30688  polid 31146  polid2i 31144  polidi 31145
[ReedSimon] p. 63Exercise 4(b)df-ph 30800
[ReedSimon] p. 195Remarklnophm 32006  lnophmi 32005
[Retherford] p. 49Exercise 1(i)leopadd 32119
[Retherford] p. 49Exercise 1(ii)leopmul 32121  leopmuli 32120
[Retherford] p. 49Exercise 1(iv)leoptr 32124
[Retherford] p. 49Definition VI.1df-leop 31839  leoppos 32113
[Retherford] p. 49Exercise 1(iii)leoptri 32123
[Retherford] p. 49Definition of operator orderingleop3 32112
[Roman] p. 4Definitiondf-dmat 22411  df-dmatalt 48504
[Roman] p. 18Part Preliminariesdf-rng 20077
[Roman] p. 19Part Preliminariesdf-ring 20159
[Roman] p. 46Theorem 1.6isldepslvec2 48591
[Roman] p. 112Noteisldepslvec2 48591  ldepsnlinc 48614  zlmodzxznm 48603
[Roman] p. 112Examplezlmodzxzequa 48602  zlmodzxzequap 48605  zlmodzxzldep 48610
[Roman] p. 170Theorem 7.8cayleyhamilton 22811
[Rosenlicht] p. 80Theoremheicant 37701
[Rosser] p. 281Definitiondf-op 4582
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34665
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34666
[Rotman] p. 28Remarkpgrpgt2nabl 48471  pmtr3ncom 19393
[Rotman] p. 31Theorem 3.4symggen2 19389
[Rotman] p. 42Theorem 3.15cayley 19332  cayleyth 19333
[Rudin] p. 164Equation 27efcan 16009
[Rudin] p. 164Equation 30efzval 16017
[Rudin] p. 167Equation 48absefi 16111
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1772
[Sanford] p. 39Rule 4mptxor 1770
[Sanford] p. 40Rule 1mptnan 1769
[Schechter] p. 51Definition of antisymmetryintasym 6067
[Schechter] p. 51Definition of irreflexivityintirr 6070
[Schechter] p. 51Definition of symmetrycnvsym 6066
[Schechter] p. 51Definition of transitivitycotr 6064
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17494
[Schechter] p. 79Definition of Moore closuredf-mrc 17495
[Schechter] p. 82Section 4.5df-mrc 17495
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17497
[Schechter] p. 139Definition AC3dfac9 10034
[Schechter] p. 141Definition (MC)dfac11 43160
[Schechter] p. 149Axiom DC1ax-dc 10343  axdc3 10351
[Schechter] p. 187Definition of "ring with unit"isring 20161  isrngo 37943
[Schechter] p. 276Remark 11.6.espan0 31529
[Schechter] p. 276Definition of spandf-span 31296  spanval 31320
[Schechter] p. 428Definition 15.35bastop1 22914
[Schloeder] p. 1Lemma 1.3onelon 6337  onelord 43349  ordelon 6336  ordelord 6334
[Schloeder] p. 1Lemma 1.7onepsuc 43350  sucidg 6395
[Schloeder] p. 1Remark 1.50elon 6367  onsuc 7749  ord0 6366  ordsuci 7747
[Schloeder] p. 1Theorem 1.9epsoon 43351
[Schloeder] p. 1Definition 1.1dftr5 5204
[Schloeder] p. 1Definition 1.2dford3 43126  elon2 6323
[Schloeder] p. 1Definition 1.4df-suc 6318
[Schloeder] p. 1Definition 1.6epel 5522  epelg 5520
[Schloeder] p. 1Theorem 1.9(i)elirr 9491  epirron 43352  ordirr 6330
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43354  oneptr 43353  ontr1 6359
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6355  oneptri 43355  ordtri3or 6344
[Schloeder] p. 2Lemma 1.10ondif1 8422  ord0eln0 6368
[Schloeder] p. 2Lemma 1.13elsuci 6381  onsucss 43364  trsucss 6402
[Schloeder] p. 2Lemma 1.14ordsucss 7754
[Schloeder] p. 2Lemma 1.15onnbtwn 6408  ordnbtwn 6407
[Schloeder] p. 2Lemma 1.16orddif0suc 43366  ordnexbtwnsuc 43365
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10298  onsucf1lem 43367  onsucf1o 43370  onsucf1olem 43368  onsucrn 43369
[Schloeder] p. 2Lemma 1.18dflim7 43371
[Schloeder] p. 2Remark 1.12ordzsl 7781
[Schloeder] p. 2Theorem 1.10ondif1i 43360  ordne0gt0 43359
[Schloeder] p. 2Definition 1.11dflim6 43362  limnsuc 43363  onsucelab 43361
[Schloeder] p. 3Remark 1.21omex 9539
[Schloeder] p. 3Theorem 1.19tfinds 7796
[Schloeder] p. 3Theorem 1.22omelon 9542  ordom 7812
[Schloeder] p. 3Definition 1.20dfom3 9543
[Schloeder] p. 4Lemma 2.21onn 8561
[Schloeder] p. 4Lemma 2.7ssonuni 7719  ssorduni 7718
[Schloeder] p. 4Remark 2.4oa1suc 8452
[Schloeder] p. 4Theorem 1.23dfom5 9546  limom 7818
[Schloeder] p. 4Definition 2.1df-1o 8391  df1o2 8398
[Schloeder] p. 4Definition 2.3oa0 8437  oa0suclim 43373  oalim 8453  oasuc 8445
[Schloeder] p. 4Definition 2.5om0 8438  om0suclim 43374  omlim 8454  omsuc 8447
[Schloeder] p. 4Definition 2.6oe0 8443  oe0m1 8442  oe0suclim 43375  oelim 8455  oesuc 8448
[Schloeder] p. 5Lemma 2.10onsupuni 43327
[Schloeder] p. 5Lemma 2.11onsupsucismax 43377
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43378
[Schloeder] p. 5Lemma 2.13limexissup 43379  limexissupab 43381  limiun 43380  limuni 6374
[Schloeder] p. 5Lemma 2.14oa0r 8459
[Schloeder] p. 5Lemma 2.15om1 8463  om1om1r 43382  om1r 8464
[Schloeder] p. 5Remark 2.8oacl 8456  oaomoecl 43376  oecl 8458  omcl 8457
[Schloeder] p. 5Definition 2.9onsupintrab 43329
[Schloeder] p. 6Lemma 2.16oe1 8465
[Schloeder] p. 6Lemma 2.17oe1m 8466
[Schloeder] p. 6Lemma 2.18oe0rif 43383
[Schloeder] p. 6Theorem 2.19oasubex 43384
[Schloeder] p. 6Theorem 2.20nnacl 8532  nnamecl 43385  nnecl 8534  nnmcl 8533
[Schloeder] p. 7Lemma 3.1onsucwordi 43386
[Schloeder] p. 7Lemma 3.2oaword1 8473
[Schloeder] p. 7Lemma 3.3oaword2 8474
[Schloeder] p. 7Lemma 3.4oalimcl 8481
[Schloeder] p. 7Lemma 3.5oaltublim 43388
[Schloeder] p. 8Lemma 3.6oaordi3 43389
[Schloeder] p. 8Lemma 3.81oaomeqom 43391
[Schloeder] p. 8Lemma 3.10oa00 8480
[Schloeder] p. 8Lemma 3.11omge1 43395  omword1 8494
[Schloeder] p. 8Remark 3.9oaordnr 43394  oaordnrex 43393
[Schloeder] p. 8Theorem 3.7oaord3 43390
[Schloeder] p. 9Lemma 3.12omge2 43396  omword2 8495
[Schloeder] p. 9Lemma 3.13omlim2 43397
[Schloeder] p. 9Lemma 3.14omord2lim 43398
[Schloeder] p. 9Lemma 3.15omord2i 43399  omordi 8487
[Schloeder] p. 9Theorem 3.16omord 8489  omord2com 43400
[Schloeder] p. 10Lemma 3.172omomeqom 43401  df-2o 8392
[Schloeder] p. 10Lemma 3.19oege1 43404  oewordi 8512
[Schloeder] p. 10Lemma 3.20oege2 43405  oeworde 8514
[Schloeder] p. 10Lemma 3.21rp-oelim2 43406
[Schloeder] p. 10Lemma 3.22oeord2lim 43407
[Schloeder] p. 10Remark 3.18omnord1 43403  omnord1ex 43402
[Schloeder] p. 11Lemma 3.23oeord2i 43408
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43410
[Schloeder] p. 11Remark 3.26oenord1 43414  oenord1ex 43413
[Schloeder] p. 11Theorem 4.1oaomoencom 43415
[Schloeder] p. 11Theorem 4.2oaass 8482
[Schloeder] p. 11Theorem 3.24oeord2com 43409
[Schloeder] p. 12Theorem 4.3odi 8500
[Schloeder] p. 13Theorem 4.4omass 8501
[Schloeder] p. 14Remark 4.6oenass 43417
[Schloeder] p. 14Theorem 4.7oeoa 8518
[Schloeder] p. 15Lemma 5.1cantnftermord 43418
[Schloeder] p. 15Lemma 5.2cantnfub 43419  cantnfub2 43420
[Schloeder] p. 16Theorem 5.3cantnf2 43423
[Schwabhauser] p. 10Axiom A1axcgrrflx 28899  axtgcgrrflx 28446
[Schwabhauser] p. 10Axiom A2axcgrtr 28900
[Schwabhauser] p. 10Axiom A3axcgrid 28901  axtgcgrid 28447
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28432
[Schwabhauser] p. 11Axiom A4axsegcon 28912  axtgsegcon 28448  df-trkgcb 28434
[Schwabhauser] p. 11Axiom A5ax5seg 28923  axtg5seg 28449  df-trkgcb 28434
[Schwabhauser] p. 11Axiom A6axbtwnid 28924  axtgbtwnid 28450  df-trkgb 28433
[Schwabhauser] p. 12Axiom A7axpasch 28926  axtgpasch 28451  df-trkgb 28433
[Schwabhauser] p. 12Axiom A8axlowdim2 28945  df-trkg2d 34685
[Schwabhauser] p. 13Axiom A8axtglowdim2 28454
[Schwabhauser] p. 13Axiom A9axtgupdim2 28455  df-trkg2d 34685
[Schwabhauser] p. 13Axiom A10axeuclid 28948  axtgeucl 28456  df-trkge 28435
[Schwabhauser] p. 13Axiom A11axcont 28961  axtgcont 28453  axtgcont1 28452  df-trkgb 28433
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36038
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36040
[Schwabhauser] p. 27Theorem 2.3cgrtr 36043
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36047
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36048  tgcgrcomimp 28461  tgcgrcoml 28463  tgcgrcomr 28462
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36053  tgcgrtriv 28468
[Schwabhauser] p. 28Theorem 2.105segofs 36057  tg5segofs 34693
[Schwabhauser] p. 28Definition 2.10df-afs 34690  df-ofs 36034
[Schwabhauser] p. 29Theorem 2.11cgrextend 36059  tgcgrextend 28469
[Schwabhauser] p. 29Theorem 2.12segconeq 36061  tgsegconeq 28470
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36073  btwntriv2 36063  tgbtwntriv2 28471
[Schwabhauser] p. 30Theorem 3.2btwncomim 36064  tgbtwncom 28472
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36067  tgbtwntriv1 28475
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36068  tgbtwnswapid 28476
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36074  btwnintr 36070  tgbtwnexch2 28480  tgbtwnintr 28477
[Schwabhauser] p. 30Theorem 3.6btwnexch 36076  btwnexch3 36071  tgbtwnexch 28482  tgbtwnexch3 28478
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36075  tgbtwnouttr 28481  tgbtwnouttr2 28479
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28944
[Schwabhauser] p. 32Theorem 3.14btwndiff 36078  tgbtwndiff 28490
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28483  trisegint 36079
[Schwabhauser] p. 34Theorem 4.2ifscgr 36095  tgifscgr 28492
[Schwabhauser] p. 34Theorem 4.11colcom 28542  colrot1 28543  colrot2 28544  lncom 28606  lnrot1 28607  lnrot2 28608
[Schwabhauser] p. 34Definition 4.1df-ifs 36091
[Schwabhauser] p. 35Theorem 4.3cgrsub 36096  tgcgrsub 28493
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36106  tgcgrxfr 28502
[Schwabhauser] p. 35Statement 4.4ercgrg 28501
[Schwabhauser] p. 35Definition 4.4df-cgr3 36092  df-cgrg 28495
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28495
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36107  tgbtwnxfr 28514
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36113  colinearperm2 36115  colinearperm3 36114  colinearperm4 36116  colinearperm5 36117
[Schwabhauser] p. 36Definition 4.8df-ismt 28517
[Schwabhauser] p. 36Definition 4.10df-colinear 36090  tgellng 28537  tglng 28530
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36118
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36126  lnxfr 28550
[Schwabhauser] p. 37Theorem 4.14lineext 36127  lnext 28551
[Schwabhauser] p. 37Theorem 4.16fscgr 36131  tgfscgr 28552
[Schwabhauser] p. 37Theorem 4.17linecgr 36132  lncgr 28553
[Schwabhauser] p. 37Definition 4.15df-fs 36093
[Schwabhauser] p. 38Theorem 4.18lineid 36134  lnid 28554
[Schwabhauser] p. 38Theorem 4.19idinside 36135  tgidinside 28555
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36152  tgbtwnconn1 28559
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36153  tgbtwnconn2 28560
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36154  tgbtwnconn3 28561
[Schwabhauser] p. 41Theorem 5.5brsegle2 36160
[Schwabhauser] p. 41Definition 5.4df-segle 36158  legov 28569
[Schwabhauser] p. 41Definition 5.5legov2 28570
[Schwabhauser] p. 42Remark 5.13legso 28583
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36161
[Schwabhauser] p. 42Theorem 5.7seglerflx 36163
[Schwabhauser] p. 42Theorem 5.8segletr 36165
[Schwabhauser] p. 42Theorem 5.9segleantisym 36166
[Schwabhauser] p. 42Theorem 5.10seglelin 36167
[Schwabhauser] p. 42Theorem 5.11seglemin 36164
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36169
[Schwabhauser] p. 42Proposition 5.7legid 28571
[Schwabhauser] p. 42Proposition 5.8legtrd 28573
[Schwabhauser] p. 42Proposition 5.9legtri3 28574
[Schwabhauser] p. 42Proposition 5.10legtrid 28575
[Schwabhauser] p. 42Proposition 5.11leg0 28576
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36176
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36177
[Schwabhauser] p. 43Theorem 6.4broutsideof 36172  df-outsideof 36171
[Schwabhauser] p. 43Definition 6.1broutsideof2 36173  ishlg 28586
[Schwabhauser] p. 44Theorem 6.4hlln 28591
[Schwabhauser] p. 44Theorem 6.5hlid 28593  outsideofrflx 36178
[Schwabhauser] p. 44Theorem 6.6hlcomb 28587  hlcomd 28588  outsideofcom 36179
[Schwabhauser] p. 44Theorem 6.7hltr 28594  outsideoftr 36180
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28602  outsideofeu 36182
[Schwabhauser] p. 44Definition 6.8df-ray 36189
[Schwabhauser] p. 45Part 2df-lines2 36190
[Schwabhauser] p. 45Theorem 6.13outsidele 36183
[Schwabhauser] p. 45Theorem 6.15lineunray 36198
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36199  tglineelsb2 28616
[Schwabhauser] p. 45Theorem 6.17linecom 36201  linerflx1 36200  linerflx2 36202  tglinecom 28619  tglinerflx1 28617  tglinerflx2 28618
[Schwabhauser] p. 45Theorem 6.18linethru 36204  tglinethru 28620
[Schwabhauser] p. 45Definition 6.14df-line2 36188  tglng 28530
[Schwabhauser] p. 45Proposition 6.13legbtwn 28578
[Schwabhauser] p. 46Theorem 6.19linethrueu 36207  tglinethrueu 28623
[Schwabhauser] p. 46Theorem 6.21lineintmo 36208  tglineineq 28627  tglineinteq 28629  tglineintmo 28626
[Schwabhauser] p. 46Theorem 6.23colline 28633
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28634
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28635
[Schwabhauser] p. 49Theorem 7.3mirinv 28650
[Schwabhauser] p. 49Theorem 7.7mirmir 28646
[Schwabhauser] p. 49Theorem 7.8mirreu3 28638
[Schwabhauser] p. 49Definition 7.5df-mir 28637  ismir 28643  mirbtwn 28642  mircgr 28641  mirfv 28640  mirval 28639
[Schwabhauser] p. 50Theorem 7.8mirreu 28648
[Schwabhauser] p. 50Theorem 7.9mireq 28649
[Schwabhauser] p. 50Theorem 7.10mirinv 28650
[Schwabhauser] p. 50Theorem 7.11mirf1o 28653
[Schwabhauser] p. 50Theorem 7.13miriso 28654
[Schwabhauser] p. 51Theorem 7.14mirmot 28659
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28656  mirbtwni 28655
[Schwabhauser] p. 51Theorem 7.16mircgrs 28657
[Schwabhauser] p. 51Theorem 7.17miduniq 28669
[Schwabhauser] p. 52Lemma 7.21symquadlem 28673
[Schwabhauser] p. 52Theorem 7.18miduniq1 28670
[Schwabhauser] p. 52Theorem 7.19miduniq2 28671
[Schwabhauser] p. 52Theorem 7.20colmid 28672
[Schwabhauser] p. 53Lemma 7.22krippen 28675
[Schwabhauser] p. 55Lemma 7.25midexlem 28676
[Schwabhauser] p. 57Theorem 8.2ragcom 28682
[Schwabhauser] p. 57Definition 8.1df-rag 28678  israg 28681
[Schwabhauser] p. 58Theorem 8.3ragcol 28683
[Schwabhauser] p. 58Theorem 8.4ragmir 28684
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28686
[Schwabhauser] p. 58Theorem 8.6ragflat2 28687
[Schwabhauser] p. 58Theorem 8.7ragflat 28688
[Schwabhauser] p. 58Theorem 8.8ragtriva 28689
[Schwabhauser] p. 58Theorem 8.9ragflat3 28690  ragncol 28693
[Schwabhauser] p. 58Theorem 8.10ragcgr 28691
[Schwabhauser] p. 59Theorem 8.12perpcom 28697
[Schwabhauser] p. 59Theorem 8.13ragperp 28701
[Schwabhauser] p. 59Theorem 8.14perpneq 28698
[Schwabhauser] p. 59Definition 8.11df-perpg 28680  isperp 28696
[Schwabhauser] p. 59Definition 8.13isperp2 28699
[Schwabhauser] p. 60Theorem 8.18foot 28706
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28714  colperpexlem2 28715
[Schwabhauser] p. 63Theorem 8.21colperpex 28717  colperpexlem3 28716
[Schwabhauser] p. 64Theorem 8.22mideu 28722  midex 28721
[Schwabhauser] p. 66Lemma 8.24opphllem 28719
[Schwabhauser] p. 67Theorem 9.2oppcom 28728
[Schwabhauser] p. 67Definition 9.1islnopp 28723
[Schwabhauser] p. 68Lemma 9.3opphllem2 28732
[Schwabhauser] p. 68Lemma 9.4opphllem5 28735  opphllem6 28736
[Schwabhauser] p. 69Theorem 9.5opphl 28738
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28451
[Schwabhauser] p. 70Theorem 9.6outpasch 28739
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28747
[Schwabhauser] p. 71Definition 9.7df-hpg 28742  hpgbr 28744
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28749
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28748
[Schwabhauser] p. 72Theorem 9.11hpgid 28750
[Schwabhauser] p. 72Theorem 9.12hpgcom 28751
[Schwabhauser] p. 72Theorem 9.13hpgtr 28752
[Schwabhauser] p. 73Theorem 9.18colopp 28753
[Schwabhauser] p. 73Theorem 9.19colhp 28754
[Schwabhauser] p. 88Theorem 10.2lmieu 28768
[Schwabhauser] p. 88Definition 10.1df-mid 28758
[Schwabhauser] p. 89Theorem 10.4lmicom 28772
[Schwabhauser] p. 89Theorem 10.5lmilmi 28773
[Schwabhauser] p. 89Theorem 10.6lmireu 28774
[Schwabhauser] p. 89Theorem 10.7lmieq 28775
[Schwabhauser] p. 89Theorem 10.8lmiinv 28776
[Schwabhauser] p. 89Theorem 10.9lmif1o 28779
[Schwabhauser] p. 89Theorem 10.10lmiiso 28781
[Schwabhauser] p. 89Definition 10.3df-lmi 28759
[Schwabhauser] p. 90Theorem 10.11lmimot 28782
[Schwabhauser] p. 91Theorem 10.12hypcgr 28785
[Schwabhauser] p. 92Theorem 10.14lmiopp 28786
[Schwabhauser] p. 92Theorem 10.15lnperpex 28787
[Schwabhauser] p. 92Theorem 10.16trgcopy 28788  trgcopyeu 28790
[Schwabhauser] p. 95Definition 11.2dfcgra2 28814
[Schwabhauser] p. 95Definition 11.3iscgra 28793
[Schwabhauser] p. 95Proposition 11.4cgracgr 28802
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28800  cgrahl2 28801
[Schwabhauser] p. 96Theorem 11.6cgraid 28803
[Schwabhauser] p. 96Theorem 11.9cgraswap 28804
[Schwabhauser] p. 97Theorem 11.7cgracom 28806
[Schwabhauser] p. 97Theorem 11.8cgratr 28807
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28810  cgrahl 28811
[Schwabhauser] p. 98Theorem 11.13sacgr 28815
[Schwabhauser] p. 98Theorem 11.14oacgr 28816
[Schwabhauser] p. 98Theorem 11.15acopy 28817  acopyeu 28818
[Schwabhauser] p. 101Theorem 11.24inagswap 28825
[Schwabhauser] p. 101Theorem 11.25inaghl 28829
[Schwabhauser] p. 101Definition 11.23isinag 28822
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28837
[Schwabhauser] p. 102Definition 11.27df-leag 28830  isleag 28831
[Schwabhauser] p. 107Theorem 11.49tgsas 28839  tgsas1 28838  tgsas2 28840  tgsas3 28841
[Schwabhauser] p. 108Theorem 11.50tgasa 28843  tgasa1 28842
[Schwabhauser] p. 109Theorem 11.51tgsss1 28844  tgsss2 28845  tgsss3 28846
[Shapiro] p. 230Theorem 6.5.1dchrhash 27215  dchrsum 27213  dchrsum2 27212  sumdchr 27216
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27217  sum2dchr 27218
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19986  ablfacrp2 19987
[Shapiro], p. 328Equation 9.2.4vmasum 27160
[Shapiro], p. 329Equation 9.2.7logfac2 27161
[Shapiro], p. 329Equation 9.2.9logfacrlim 27168
[Shapiro], p. 331Equation 9.2.13vmadivsum 27426
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27429
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27483  vmalogdivsum2 27482
[Shapiro], p. 375Theorem 9.4.1dirith 27473  dirith2 27472
[Shapiro], p. 375Equation 9.4.3rplogsum 27471  rpvmasum 27470  rpvmasum2 27456
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27431
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27469
[Shapiro], p. 377Lemma 9.4.1dchrisum 27436  dchrisumlem1 27433  dchrisumlem2 27434  dchrisumlem3 27435  dchrisumlema 27432
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27439
[Shapiro], p. 379Equation 9.4.16dchrmusum 27468  dchrmusumlem 27466  dchrvmasumlem 27467
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27438
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27440
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27464  dchrisum0re 27457  dchrisumn0 27465
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27450
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27454
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27455
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27510  pntrsumbnd2 27511  pntrsumo1 27509
[Shapiro], p. 405Equation 10.2.1mudivsum 27474
[Shapiro], p. 406Equation 10.2.6mulogsum 27476
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27478
[Shapiro], p. 407Equation 10.2.8mulog2sum 27481
[Shapiro], p. 418Equation 10.4.6logsqvma 27486
[Shapiro], p. 418Equation 10.4.8logsqvma2 27487
[Shapiro], p. 419Equation 10.4.10selberg 27492
[Shapiro], p. 420Equation 10.4.12selberg2lem 27494
[Shapiro], p. 420Equation 10.4.14selberg2 27495
[Shapiro], p. 422Equation 10.6.7selberg3 27503
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27504
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27501  selberg3lem2 27502
[Shapiro], p. 422Equation 10.4.23selberg4 27505
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27499
[Shapiro], p. 428Equation 10.6.2selbergr 27512
[Shapiro], p. 429Equation 10.6.8selberg3r 27513
[Shapiro], p. 430Equation 10.6.11selberg4r 27514
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27528
[Shapiro], p. 434Equation 10.6.27pntlema 27540  pntlemb 27541  pntlemc 27539  pntlemd 27538  pntlemg 27542
[Shapiro], p. 435Equation 10.6.29pntlema 27540
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27532
[Shapiro], p. 436Lemma 10.6.2pntibnd 27537
[Shapiro], p. 436Equation 10.6.34pntlema 27540
[Shapiro], p. 436Equation 10.6.35pntlem3 27553  pntleml 27555
[Stewart] p. 91Lemma 7.3constrss 33763
[Stewart] p. 92Definition 7.4.df-constr 33750
[Stewart] p. 96Theorem 7.10constraddcl 33782  constrinvcl 33793  constrmulcl 33791  constrnegcl 33783  constrsqrtcl 33799
[Stewart] p. 97Theorem 7.11constrextdg2 33769
[Stewart] p. 98Theorem 7.12constrext2chn 33779
[Stewart] p. 99Theorem 7.132sqr3nconstr 33801
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33811
[Stoll] p. 13Definition corresponds to dfsymdif3 4255
[Stoll] p. 16Exercise 4.40dif 4354  dif0 4327
[Stoll] p. 16Exercise 4.8difdifdir 4441
[Stoll] p. 17Theorem 5.1(5)unvdif 4424
[Stoll] p. 19Theorem 5.2(13)undm 4246
[Stoll] p. 19Theorem 5.2(13')indm 4247
[Stoll] p. 20Remarkinvdif 4228
[Stoll] p. 25Definition of ordered tripledf-ot 4584
[Stoll] p. 43Definitionuniiun 5009
[Stoll] p. 44Definitionintiin 5010
[Stoll] p. 45Definitiondf-iin 4944
[Stoll] p. 45Definition indexed uniondf-iun 4943
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4255
[Strang] p. 242Section 6.3expgrowth 44433
[Suppes] p. 22Theorem 2eq0 4299  eq0f 4296
[Suppes] p. 22Theorem 4eqss 3945  eqssd 3947  eqssi 3946
[Suppes] p. 23Theorem 5ss0 4351  ss0b 4350
[Suppes] p. 23Theorem 6sstr 3938  sstrALT2 44932
[Suppes] p. 23Theorem 7pssirr 4052
[Suppes] p. 23Theorem 8pssn2lp 4053
[Suppes] p. 23Theorem 9psstr 4056
[Suppes] p. 23Theorem 10pssss 4047
[Suppes] p. 25Theorem 12elin 3913  elun 4102
[Suppes] p. 26Theorem 15inidm 4176
[Suppes] p. 26Theorem 16in0 4344
[Suppes] p. 27Theorem 23unidm 4106
[Suppes] p. 27Theorem 24un0 4343
[Suppes] p. 27Theorem 25ssun1 4127
[Suppes] p. 27Theorem 26ssequn1 4135
[Suppes] p. 27Theorem 27unss 4139
[Suppes] p. 27Theorem 28indir 4235
[Suppes] p. 27Theorem 29undir 4236
[Suppes] p. 28Theorem 32difid 4325
[Suppes] p. 29Theorem 33difin 4221
[Suppes] p. 29Theorem 34indif 4229
[Suppes] p. 29Theorem 35undif1 4425
[Suppes] p. 29Theorem 36difun2 4430
[Suppes] p. 29Theorem 37difin0 4423
[Suppes] p. 29Theorem 38disjdif 4421
[Suppes] p. 29Theorem 39difundi 4239
[Suppes] p. 29Theorem 40difindi 4241
[Suppes] p. 30Theorem 41nalset 5253
[Suppes] p. 39Theorem 61uniss 4866
[Suppes] p. 39Theorem 65uniop 5458
[Suppes] p. 41Theorem 70intsn 4934
[Suppes] p. 42Theorem 71intpr 4932  intprg 4931
[Suppes] p. 42Theorem 73op1stb 5414
[Suppes] p. 42Theorem 78intun 4930
[Suppes] p. 44Definition 15(a)dfiun2 4982  dfiun2g 4980
[Suppes] p. 44Definition 15(b)dfiin2 4983
[Suppes] p. 47Theorem 86elpw 4553  elpw2 5274  elpw2g 5273  elpwg 4552  elpwgdedVD 45014
[Suppes] p. 47Theorem 87pwid 4571
[Suppes] p. 47Theorem 89pw0 4763
[Suppes] p. 48Theorem 90pwpw0 4764
[Suppes] p. 52Theorem 101xpss12 5634
[Suppes] p. 52Theorem 102xpindi 5778  xpindir 5779
[Suppes] p. 52Theorem 103xpundi 5688  xpundir 5689
[Suppes] p. 54Theorem 105elirrv 9489
[Suppes] p. 58Theorem 2relss 5726
[Suppes] p. 59Theorem 4eldm 5845  eldm2 5846  eldm2g 5844  eldmg 5843
[Suppes] p. 59Definition 3df-dm 5629
[Suppes] p. 60Theorem 6dmin 5856
[Suppes] p. 60Theorem 8rnun 6098
[Suppes] p. 60Theorem 9rnin 6099
[Suppes] p. 60Definition 4dfrn2 5833
[Suppes] p. 61Theorem 11brcnv 5827  brcnvg 5824
[Suppes] p. 62Equation 5elcnv 5821  elcnv2 5822
[Suppes] p. 62Theorem 12relcnv 6058
[Suppes] p. 62Theorem 15cnvin 6097
[Suppes] p. 62Theorem 16cnvun 6095
[Suppes] p. 63Definitiondftrrels2 38677
[Suppes] p. 63Theorem 20co02 6214
[Suppes] p. 63Theorem 21dmcoss 5919
[Suppes] p. 63Definition 7df-co 5628
[Suppes] p. 64Theorem 26cnvco 5830
[Suppes] p. 64Theorem 27coass 6219
[Suppes] p. 65Theorem 31resundi 5947
[Suppes] p. 65Theorem 34elima 6019  elima2 6020  elima3 6021  elimag 6018
[Suppes] p. 65Theorem 35imaundi 6102
[Suppes] p. 66Theorem 40dminss 6106
[Suppes] p. 66Theorem 41imainss 6107
[Suppes] p. 67Exercise 11cnvxp 6110
[Suppes] p. 81Definition 34dfec2 8631
[Suppes] p. 82Theorem 72elec 8674  elecALTV 38309  elecg 8672
[Suppes] p. 82Theorem 73eqvrelth 38713  erth 8682  erth2 8683
[Suppes] p. 83Theorem 74eqvreldisj 38716  erdisj 8685
[Suppes] p. 83Definition 35, df-parts 38869  dfmembpart2 38874
[Suppes] p. 89Theorem 96map0b 8813
[Suppes] p. 89Theorem 97map0 8817  map0g 8814
[Suppes] p. 89Theorem 98mapsn 8818  mapsnd 8816
[Suppes] p. 89Theorem 99mapss 8819
[Suppes] p. 91Definition 12(ii)alephsuc 9965
[Suppes] p. 91Definition 12(iii)alephlim 9964
[Suppes] p. 92Theorem 1enref 8913  enrefg 8912
[Suppes] p. 92Theorem 2ensym 8931  ensymb 8930  ensymi 8932
[Suppes] p. 92Theorem 3entr 8934
[Suppes] p. 92Theorem 4unen 8973
[Suppes] p. 94Theorem 15endom 8907
[Suppes] p. 94Theorem 16ssdomg 8928
[Suppes] p. 94Theorem 17domtr 8935
[Suppes] p. 95Theorem 18sbth 9016
[Suppes] p. 97Theorem 23canth2 9049  canth2g 9050
[Suppes] p. 97Definition 3brsdom2 9020  df-sdom 8878  dfsdom2 9019
[Suppes] p. 97Theorem 21(i)sdomirr 9033
[Suppes] p. 97Theorem 22(i)domnsym 9022
[Suppes] p. 97Theorem 21(ii)sdomnsym 9021
[Suppes] p. 97Theorem 22(ii)domsdomtr 9031
[Suppes] p. 97Theorem 22(iv)brdom2 8910
[Suppes] p. 97Theorem 21(iii)sdomtr 9034
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9029
[Suppes] p. 98Exercise 4fundmen 8959  fundmeng 8960
[Suppes] p. 98Exercise 6xpdom3 8994
[Suppes] p. 98Exercise 11sdomentr 9030
[Suppes] p. 104Theorem 37fofi 9203
[Suppes] p. 104Theorem 38pwfi 9209
[Suppes] p. 105Theorem 40pwfi 9209
[Suppes] p. 111Axiom for cardinal numberscarden 10448
[Suppes] p. 130Definition 3df-tr 5201
[Suppes] p. 132Theorem 9ssonuni 7719
[Suppes] p. 134Definition 6df-suc 6318
[Suppes] p. 136Theorem Schema 22findes 7836  finds 7832  finds1 7835  finds2 7834
[Suppes] p. 151Theorem 42isfinite 9548  isfinite2 9188  isfiniteg 9190  unbnn 9186
[Suppes] p. 162Definition 5df-ltnq 10815  df-ltpq 10807
[Suppes] p. 197Theorem Schema 4tfindes 7799  tfinds 7796  tfinds2 7800
[Suppes] p. 209Theorem 18oaord1 8472
[Suppes] p. 209Theorem 21oaword2 8474
[Suppes] p. 211Theorem 25oaass 8482
[Suppes] p. 225Definition 8iscard2 9875
[Suppes] p. 227Theorem 56ondomon 10460
[Suppes] p. 228Theorem 59harcard 9877
[Suppes] p. 228Definition 12(i)aleph0 9963
[Suppes] p. 228Theorem Schema 61onintss 6364
[Suppes] p. 228Theorem Schema 62onminesb 7732  onminsb 7733
[Suppes] p. 229Theorem 64alephval2 10469
[Suppes] p. 229Theorem 65alephcard 9967
[Suppes] p. 229Theorem 66alephord2i 9974
[Suppes] p. 229Theorem 67alephnbtwn 9968
[Suppes] p. 229Definition 12df-aleph 9839
[Suppes] p. 242Theorem 6weth 10392
[Suppes] p. 242Theorem 8entric 10454
[Suppes] p. 242Theorem 9carden 10448
[Szendrei] p. 11Line 6df-cloneop 35747
[Szendrei] p. 11Paragraph 3df-suppos 35751
[TakeutiZaring] p. 8Axiom 1ax-ext 2703
[TakeutiZaring] p. 13Definition 4.5df-cleq 2723
[TakeutiZaring] p. 13Proposition 4.6df-clel 2806
[TakeutiZaring] p. 13Proposition 4.9cvjust 2725
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2751
[TakeutiZaring] p. 14Definition 4.16df-oprab 7356
[TakeutiZaring] p. 14Proposition 4.14ru 3734
[TakeutiZaring] p. 15Axiom 2zfpair 5361
[TakeutiZaring] p. 15Exercise 1elpr 4600  elpr2 4602  elpr2g 4601  elprg 4598
[TakeutiZaring] p. 15Exercise 2elsn 4590  elsn2 4617  elsn2g 4616  elsng 4589  velsn 4591
[TakeutiZaring] p. 15Exercise 3elop 5410
[TakeutiZaring] p. 15Exercise 4sneq 4585  sneqr 4791
[TakeutiZaring] p. 15Definition 5.1dfpr2 4596  dfsn2 4588  dfsn2ALT 4597
[TakeutiZaring] p. 16Axiom 3uniex 7680
[TakeutiZaring] p. 16Exercise 6opth 5419
[TakeutiZaring] p. 16Exercise 7opex 5407
[TakeutiZaring] p. 16Exercise 8rext 5391
[TakeutiZaring] p. 16Corollary 5.8unex 7683  unexg 7682
[TakeutiZaring] p. 16Definition 5.3dftp2 4643
[TakeutiZaring] p. 16Definition 5.5df-uni 4859
[TakeutiZaring] p. 16Definition 5.6df-in 3904  df-un 3902
[TakeutiZaring] p. 16Proposition 5.7unipr 4875  uniprg 4874
[TakeutiZaring] p. 17Axiom 4vpwex 5317
[TakeutiZaring] p. 17Exercise 1eltp 4641
[TakeutiZaring] p. 17Exercise 5elsuc 6384  elsucg 6382  sstr2 3936
[TakeutiZaring] p. 17Exercise 6uncom 4107
[TakeutiZaring] p. 17Exercise 7incom 4158
[TakeutiZaring] p. 17Exercise 8unass 4121
[TakeutiZaring] p. 17Exercise 9inass 4177
[TakeutiZaring] p. 17Exercise 10indi 4233
[TakeutiZaring] p. 17Exercise 11undi 4234
[TakeutiZaring] p. 17Definition 5.9df-pss 3917  df-ss 3914
[TakeutiZaring] p. 17Definition 5.10df-pw 4551
[TakeutiZaring] p. 18Exercise 7unss2 4136
[TakeutiZaring] p. 18Exercise 9dfss2 3915  sseqin2 4172
[TakeutiZaring] p. 18Exercise 10ssid 3952
[TakeutiZaring] p. 18Exercise 12inss1 4186  inss2 4187
[TakeutiZaring] p. 18Exercise 13nss 3994
[TakeutiZaring] p. 18Exercise 15unieq 4869
[TakeutiZaring] p. 18Exercise 18sspwb 5392  sspwimp 45015  sspwimpALT 45022  sspwimpALT2 45025  sspwimpcf 45017
[TakeutiZaring] p. 18Exercise 19pweqb 5399
[TakeutiZaring] p. 19Axiom 5ax-rep 5219
[TakeutiZaring] p. 20Definitiondf-rab 3396
[TakeutiZaring] p. 20Corollary 5.160ex 5247
[TakeutiZaring] p. 20Definition 5.12df-dif 3900
[TakeutiZaring] p. 20Definition 5.14dfnul2 4285
[TakeutiZaring] p. 20Proposition 5.15difid 4325
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4302  n0f 4298  neq0 4301  neq0f 4297
[TakeutiZaring] p. 21Axiom 6zfreg 9488
[TakeutiZaring] p. 21Axiom 6'zfregs 9628
[TakeutiZaring] p. 21Theorem 5.22setind 9643
[TakeutiZaring] p. 21Definition 5.20df-v 3438
[TakeutiZaring] p. 21Proposition 5.21vprc 5255
[TakeutiZaring] p. 22Exercise 10ss 4349
[TakeutiZaring] p. 22Exercise 3ssex 5261  ssexg 5263
[TakeutiZaring] p. 22Exercise 4inex1 5257
[TakeutiZaring] p. 22Exercise 5ruv 9497
[TakeutiZaring] p. 22Exercise 6elirr 9491
[TakeutiZaring] p. 22Exercise 7ssdif0 4315
[TakeutiZaring] p. 22Exercise 11difdif 4084
[TakeutiZaring] p. 22Exercise 13undif3 4249  undif3VD 44979
[TakeutiZaring] p. 22Exercise 14difss 4085
[TakeutiZaring] p. 22Exercise 15sscon 4092
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3048
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3057
[TakeutiZaring] p. 23Proposition 6.2xpex 7692  xpexg 7689
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5626
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6558
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6734  fun11 6561
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6500  svrelfun 6559
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5832
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5834
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5631
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5632
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5628
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6147  dfrel2 6142
[TakeutiZaring] p. 25Exercise 3xpss 5635
[TakeutiZaring] p. 25Exercise 5relun 5755
[TakeutiZaring] p. 25Exercise 6reluni 5763
[TakeutiZaring] p. 25Exercise 9inxp 5776
[TakeutiZaring] p. 25Exercise 12relres 5959
[TakeutiZaring] p. 25Exercise 13opelres 5939  opelresi 5941
[TakeutiZaring] p. 25Exercise 14dmres 5966
[TakeutiZaring] p. 25Exercise 15resss 5955
[TakeutiZaring] p. 25Exercise 17resabs1 5960
[TakeutiZaring] p. 25Exercise 18funres 6529
[TakeutiZaring] p. 25Exercise 24relco 6062
[TakeutiZaring] p. 25Exercise 29funco 6527
[TakeutiZaring] p. 25Exercise 30f1co 6736
[TakeutiZaring] p. 26Definition 6.10eu2 2604
[TakeutiZaring] p. 26Definition 6.11conventions 30387  df-fv 6495  fv3 6846
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7861  cnvexg 7860
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7845  dmexg 7837
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7846  rnexg 7838
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44551
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7856
[TakeutiZaring] p. 27Corollary 6.13fvex 6841
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47279  tz6.12-1-afv2 47346  tz6.12-1 6851  tz6.12-afv 47278  tz6.12-afv2 47345  tz6.12 6852  tz6.12c-afv2 47347  tz6.12c 6850
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47342  tz6.12-2 6815  tz6.12i-afv2 47348  tz6.12i 6854
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6490
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6491
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6493  wfo 6485
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6492  wf1 6484
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6494  wf1o 6486
[TakeutiZaring] p. 28Exercise 4eqfnfv 6970  eqfnfv2 6971  eqfnfv2f 6974
[TakeutiZaring] p. 28Exercise 5fvco 6926
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7157
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7155
[TakeutiZaring] p. 29Exercise 9funimaex 6575  funimaexg 6574
[TakeutiZaring] p. 29Definition 6.18df-br 5094
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5528
[TakeutiZaring] p. 30Definition 6.21dffr2 5580  dffr3 6053  eliniseg 6048  iniseg 6051
[TakeutiZaring] p. 30Definition 6.22df-eprel 5519
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5596  fr3nr 7711  frirr 5595
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5572
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7713
[TakeutiZaring] p. 31Exercise 1frss 5583
[TakeutiZaring] p. 31Exercise 4wess 5605
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6300  tz6.26i 6301  wefrc 5613  wereu2 5616
[TakeutiZaring] p. 32Theorem 6.27wfi 6302  wfii 6303
[TakeutiZaring] p. 32Definition 6.28df-isom 6496
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7269
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7270
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7276
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7277
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7278
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7282
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7289
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7291
[TakeutiZaring] p. 35Notationwtr 5200
[TakeutiZaring] p. 35Theorem 7.2trelpss 44552  tz7.2 5602
[TakeutiZaring] p. 35Definition 7.1dftr3 5205
[TakeutiZaring] p. 36Proposition 7.4ordwe 6325
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6333
[TakeutiZaring] p. 36Proposition 7.6ordelord 6334  ordelordALT 44635  ordelordALTVD 44964
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6340  ordelssne 6339
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6338
[TakeutiZaring] p. 37Proposition 7.9ordin 6342
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7721
[TakeutiZaring] p. 38Corollary 7.15ordsson 7722
[TakeutiZaring] p. 38Definition 7.11df-on 6316
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6344
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44647  ordon 7716
[TakeutiZaring] p. 38Proposition 7.13onprc 7717
[TakeutiZaring] p. 39Theorem 7.17tfi 7789
[TakeutiZaring] p. 40Exercise 3ontr2 6360
[TakeutiZaring] p. 40Exercise 7dftr2 5202
[TakeutiZaring] p. 40Exercise 9onssmin 7731
[TakeutiZaring] p. 40Exercise 11unon 7767
[TakeutiZaring] p. 40Exercise 12ordun 6418
[TakeutiZaring] p. 40Exercise 14ordequn 6417
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7718
[TakeutiZaring] p. 40Proposition 7.20elssuni 4889
[TakeutiZaring] p. 41Definition 7.22df-suc 6318
[TakeutiZaring] p. 41Proposition 7.23sssucid 6394  sucidg 6395
[TakeutiZaring] p. 41Proposition 7.24onsuc 7749
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6408  ordnbtwn 6407
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7764
[TakeutiZaring] p. 42Exercise 1df-lim 6317
[TakeutiZaring] p. 42Exercise 4omssnlim 7817
[TakeutiZaring] p. 42Exercise 7ssnlim 7822
[TakeutiZaring] p. 42Exercise 8onsucssi 7777  ordelsuc 7756
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7758
[TakeutiZaring] p. 42Definition 7.27nlimon 7787
[TakeutiZaring] p. 42Definition 7.28dfom2 7804
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7825
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7826
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7827
[TakeutiZaring] p. 43Remarkomon 7814
[TakeutiZaring] p. 43Axiom 7inf3 9531  omex 9539
[TakeutiZaring] p. 43Theorem 7.32ordom 7812
[TakeutiZaring] p. 43Corollary 7.31find 7831
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7828
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7829
[TakeutiZaring] p. 44Exercise 1limomss 7807
[TakeutiZaring] p. 44Exercise 2int0 4912
[TakeutiZaring] p. 44Exercise 3trintss 5218
[TakeutiZaring] p. 44Exercise 4intss1 4913
[TakeutiZaring] p. 44Exercise 5intex 5284
[TakeutiZaring] p. 44Exercise 6oninton 7734
[TakeutiZaring] p. 44Exercise 11ordintdif 6363
[TakeutiZaring] p. 44Definition 7.35df-int 4898
[TakeutiZaring] p. 44Proposition 7.34noinfep 9556
[TakeutiZaring] p. 45Exercise 4onint 7729
[TakeutiZaring] p. 47Lemma 1tfrlem1 8301
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8322
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8323
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8324
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8331  tz7.44-2 8332  tz7.44-3 8333
[TakeutiZaring] p. 50Exercise 1smogt 8293
[TakeutiZaring] p. 50Exercise 3smoiso 8288
[TakeutiZaring] p. 50Definition 7.46df-smo 8272
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8370  tz7.49c 8371
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8368
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8367
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8369
[TakeutiZaring] p. 53Proposition 7.532eu5 2651
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9908
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9909
[TakeutiZaring] p. 56Definition 8.1oalim 8453  oasuc 8445
[TakeutiZaring] p. 57Remarktfindsg 7797
[TakeutiZaring] p. 57Proposition 8.2oacl 8456
[TakeutiZaring] p. 57Proposition 8.3oa0 8437  oa0r 8459
[TakeutiZaring] p. 57Proposition 8.16omcl 8457
[TakeutiZaring] p. 58Corollary 8.5oacan 8469
[TakeutiZaring] p. 58Proposition 8.4nnaord 8540  nnaordi 8539  oaord 8468  oaordi 8467
[TakeutiZaring] p. 59Proposition 8.6iunss2 5000  uniss2 4892
[TakeutiZaring] p. 59Proposition 8.7oawordri 8471
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8476  oawordex 8478
[TakeutiZaring] p. 59Proposition 8.9nnacl 8532
[TakeutiZaring] p. 59Proposition 8.10oaabs 8569
[TakeutiZaring] p. 60Remarkoancom 9547
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8481
[TakeutiZaring] p. 62Exercise 1nnarcl 8537
[TakeutiZaring] p. 62Exercise 5oaword1 8473
[TakeutiZaring] p. 62Definition 8.15om0x 8440  omlim 8454  omsuc 8447
[TakeutiZaring] p. 62Definition 8.15(a)om0 8438
[TakeutiZaring] p. 63Proposition 8.17nnecl 8534  nnmcl 8533
[TakeutiZaring] p. 63Proposition 8.19nnmord 8553  nnmordi 8552  omord 8489  omordi 8487
[TakeutiZaring] p. 63Proposition 8.20omcan 8490
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8557  omwordri 8493
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8460
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8463  om1r 8464
[TakeutiZaring] p. 64Proposition 8.22om00 8496
[TakeutiZaring] p. 64Proposition 8.23omordlim 8498
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8499
[TakeutiZaring] p. 64Proposition 8.25odi 8500
[TakeutiZaring] p. 65Theorem 8.26omass 8501
[TakeutiZaring] p. 67Definition 8.30nnesuc 8529  oe0 8443  oelim 8455  oesuc 8448  onesuc 8451
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8441
[TakeutiZaring] p. 67Proposition 8.32oen0 8507
[TakeutiZaring] p. 67Proposition 8.33oeordi 8508
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8442
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8466
[TakeutiZaring] p. 68Corollary 8.34oeord 8509
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8515
[TakeutiZaring] p. 68Proposition 8.35oewordri 8513
[TakeutiZaring] p. 68Proposition 8.37oeworde 8514
[TakeutiZaring] p. 69Proposition 8.41oeoa 8518
[TakeutiZaring] p. 70Proposition 8.42oeoe 8520
[TakeutiZaring] p. 73Theorem 9.1trcl 9624  tz9.1 9625
[TakeutiZaring] p. 76Definition 9.9df-r1 9663  r10 9667  r1lim 9671  r1limg 9670  r1suc 9669  r1sucg 9668
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9679  r1ord2 9680  r1ordg 9677
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9689
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9714  tz9.13 9690  tz9.13g 9691
[TakeutiZaring] p. 79Definition 9.14df-rank 9664  rankval 9715  rankvalb 9696  rankvalg 9716
[TakeutiZaring] p. 79Proposition 9.16rankel 9738  rankelb 9723
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9752  rankval3 9739  rankval3b 9725
[TakeutiZaring] p. 79Proposition 9.18rankonid 9728
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9694
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9733  rankr1c 9720  rankr1g 9731
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9734
[TakeutiZaring] p. 80Exercise 1rankss 9748  rankssb 9747
[TakeutiZaring] p. 80Exercise 2unbndrank 9741
[TakeutiZaring] p. 80Proposition 9.19bndrank 9740
[TakeutiZaring] p. 83Axiom of Choiceac4 10372  dfac3 10018
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9927  numth 10369  numth2 10368
[TakeutiZaring] p. 85Definition 10.4cardval 10443
[TakeutiZaring] p. 85Proposition 10.5cardid 10444  cardid2 9852
[TakeutiZaring] p. 85Proposition 10.9oncard 9859
[TakeutiZaring] p. 85Proposition 10.10carden 10448
[TakeutiZaring] p. 85Proposition 10.11cardidm 9858
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9843
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9864
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9856
[TakeutiZaring] p. 87Proposition 10.15pwen 9069
[TakeutiZaring] p. 88Exercise 1en0 8946
[TakeutiZaring] p. 88Exercise 7infensuc 9074
[TakeutiZaring] p. 89Exercise 10omxpen 8998
[TakeutiZaring] p. 90Corollary 10.23cardnn 9862
[TakeutiZaring] p. 90Definition 10.27alephiso 9995
[TakeutiZaring] p. 90Proposition 10.20nneneq 9121
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9129
[TakeutiZaring] p. 90Proposition 10.26alephprc 9996
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9126
[TakeutiZaring] p. 91Exercise 2alephle 9985
[TakeutiZaring] p. 91Exercise 3aleph0 9963
[TakeutiZaring] p. 91Exercise 4cardlim 9871
[TakeutiZaring] p. 91Exercise 7infpss 10113
[TakeutiZaring] p. 91Exercise 8infcntss 9213
[TakeutiZaring] p. 91Definition 10.29df-fin 8879  isfi 8904
[TakeutiZaring] p. 92Proposition 10.32onfin 9130
[TakeutiZaring] p. 92Proposition 10.34imadomg 10431
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8991
[TakeutiZaring] p. 93Proposition 10.35fodomb 10423
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10083  unxpdom 9149
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9873  cardsdomelir 9872
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9151
[TakeutiZaring] p. 94Proposition 10.39infxpen 9911
[TakeutiZaring] p. 95Definition 10.42df-map 8758
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10459  infxpidm2 9914
[TakeutiZaring] p. 95Proposition 10.41infdju 10104  infxp 10111
[TakeutiZaring] p. 96Proposition 10.44pw2en 9003  pw2f1o 9001
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9062
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10384
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10379  ac6s5 10388
[TakeutiZaring] p. 98Theorem 10.47unidom 10440
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10441  uniimadomf 10442
[TakeutiZaring] p. 100Definition 11.1cfcof 10171
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10166
[TakeutiZaring] p. 102Exercise 1cfle 10151
[TakeutiZaring] p. 102Exercise 2cf0 10148
[TakeutiZaring] p. 102Exercise 3cfsuc 10154
[TakeutiZaring] p. 102Exercise 4cfom 10161
[TakeutiZaring] p. 102Proposition 11.9coftr 10170
[TakeutiZaring] p. 103Theorem 11.15alephreg 10479
[TakeutiZaring] p. 103Proposition 11.11cardcf 10149
[TakeutiZaring] p. 103Proposition 11.13alephsing 10173
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9994
[TakeutiZaring] p. 104Proposition 11.16carduniima 9993
[TakeutiZaring] p. 104Proposition 11.18alephfp 10005  alephfp2 10006
[TakeutiZaring] p. 106Theorem 11.20gchina 10596
[TakeutiZaring] p. 106Theorem 11.21mappwen 10009
[TakeutiZaring] p. 107Theorem 11.26konigth 10466
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10480
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10481
[Tarski] p. 67Axiom B5ax-c5 38988
[Tarski] p. 67Scheme B5sp 2186
[Tarski] p. 68Lemma 6avril1 30450  equid 2013
[Tarski] p. 69Lemma 7equcomi 2018
[Tarski] p. 70Lemma 14spim 2387  spime 2389  spimew 1972
[Tarski] p. 70Lemma 16ax-12 2180  ax-c15 38994  ax12i 1967
[Tarski] p. 70Lemmas 16 and 17sb6 2088
[Tarski] p. 75Axiom B7ax6v 1969
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1911  ax5ALT 39012
[Tarski], p. 75Scheme B8 of system S2ax-7 2009  ax-8 2113  ax-9 2121
[Tarski1999] p. 178Axiom 4axtgsegcon 28448
[Tarski1999] p. 178Axiom 5axtg5seg 28449
[Tarski1999] p. 179Axiom 7axtgpasch 28451
[Tarski1999] p. 180Axiom 7.1axtgpasch 28451
[Tarski1999] p. 185Axiom 11axtgcont1 28452
[Truss] p. 114Theorem 5.18ruc 16158
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37705
[Viaclovsky8] p. 3Proposition 7ismblfin 37707
[Weierstrass] p. 272Definitiondf-mdet 22506  mdetuni 22543
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 868
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 869
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 969
[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 37496
[WhiteheadRussell] p. 100Theorem *2.05frege5 43898  imim2 58  wl-luk-imim2 37491
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47124  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2658  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37494
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 45024  wl-luk-notnotr 37495
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43928  axfrege28 43927  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 867
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37488
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 941
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30388  pm2.27 42  wl-luk-pm2.27 37486
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38401
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 971
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 972
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 970
[WhiteheadRussell] p. 105Definition *2.33df-3or 1087
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 944
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 851
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 852
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 942
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 943
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 974
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 975
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 976
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 973
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 977
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 993
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 994
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 995
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 996
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 997
[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 802
[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 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Fact)pm3.45 622
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 809
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 962  pm3.44 961
[WhiteheadRussell] p. 113Theorem *3.47anim12 808
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 965
[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 806
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1009
[WhiteheadRussell] p. 118Theorem *4.31orcom 870
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 978
[WhiteheadRussell] p. 118Definition *4.34df-3an 1088
[WhiteheadRussell] p. 119Theorem *4.41ordi 1007
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1024
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 998
[WhiteheadRussell] p. 119Theorem *4.45orabs 1000  pm4.45 999  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 984
[WhiteheadRussell] p. 120Theorem *4.6imor 853
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 983
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 986
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 987
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 988
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 989
[WhiteheadRussell] p. 120Theorem *4.56ioran 985  pm4.56 990
[WhiteheadRussell] p. 120Theorem *4.57oran 991  pm4.57 992
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 856
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 849
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 850
[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 951
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 963  pm4.77 964
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1005
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1025
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1026
[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 843
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 946  pm5.11g 945
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 947
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 949
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 948
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1014
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1015
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1013
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1016
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[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 1003
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 955
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[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 1006
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1019
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 950
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1002
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1020
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1021
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1029
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1030
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44456
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44457
[WhiteheadRussell] p. 147Theorem *10.2219.26 1871
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44458
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44459
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44460
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1894
[WhiteheadRussell] p. 151Theorem *10.301albitr 44461
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44462
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44463
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44464
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44465
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44467
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44468
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44469
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44466
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2093
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44472
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44473
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2073
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2163
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1830
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1831
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44474
[WhiteheadRussell] p. 162Theorem *11.322alim 44475
[WhiteheadRussell] p. 162Theorem *11.332albi 44476
[WhiteheadRussell] p. 162Theorem *11.342exim 44477
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44479
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44478
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1888
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44481
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44482
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44480
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1829
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44483
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44484
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1847
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44485
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2346
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1861
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44490
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44486
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44487
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44488
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44489
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44494
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44491
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44492
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44493
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44495
[WhiteheadRussell] p. 175Definition *14.02df-eu 2564
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44505  pm13.13b 44506
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44507
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3009
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3010
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3616
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44513
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44514
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44508
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44650  pm13.193 44509
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44510
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44511
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44512
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44519
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44518
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44517
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3799
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44520  pm14.122b 44521  pm14.122c 44522
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44523  pm14.123b 44524  pm14.123c 44525
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44527
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44526
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44528
[WhiteheadRussell] p. 190Theorem *14.22iota4 6468
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44529
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6469
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44530
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44532
[WhiteheadRussell] p. 192Theorem *14.26eupick 2628  eupickbi 2631  sbaniota 44533
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44531
[WhiteheadRussell] p. 192Theorem *14.271eubi 2579
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44534
[WhiteheadRussell] p. 235Definition *30.01conventions 30387  df-fv 6495
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9900  pm54.43lem 9899
[Young] p. 141Definition of operator orderingleop2 32111
[Young] p. 142Example 12.2(i)0leop 32117  idleop 32118
[vandenDries] p. 42Lemma 61irrapx1 42926
[vandenDries] p. 43Theorem 62pellex 42933  pellexlem1 42927

This page was last updated on 12-Feb-2026.
Copyright terms: Public domain