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 17609
[Adamek] p. 21Condition 3.1(b)df-cat 17609
[Adamek] p. 22Example 3.3(1)df-setc 18018
[Adamek] p. 24Example 3.3(4.c)0cat 17630  0funcg 49067  df-termc 49455
[Adamek] p. 24Example 3.3(4.d)df-prstc 49532  prsthinc 49446
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49560  df-mndtc 49560
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49556
[Adamek] p. 25Definition 3.5df-oppc 17653
[Adamek] p. 25Example 3.6(1)oduoppcciso 49548
[Adamek] p. 25Example 3.6(2)oppgoppcco 49573  oppgoppchom 49572  oppgoppcid 49574
[Adamek] p. 28Remark 3.9oppciso 17723
[Adamek] p. 28Remark 3.12invf1o 17711  invisoinvl 17732
[Adamek] p. 28Example 3.13idinv 17731  idiso 17730
[Adamek] p. 28Corollary 3.11inveq 17716
[Adamek] p. 28Definition 3.8df-inv 17690  df-iso 17691  dfiso2 17714
[Adamek] p. 28Proposition 3.10sectcan 17697
[Adamek] p. 29Remark 3.16cicer 17748  cicerALT 49028
[Adamek] p. 29Definition 3.15cic 17741  df-cic 17738
[Adamek] p. 29Definition 3.17df-func 17800
[Adamek] p. 29Proposition 3.14(1)invinv 17712
[Adamek] p. 29Proposition 3.14(2)invco 17713  isoco 17719
[Adamek] p. 30Remark 3.19df-func 17800
[Adamek] p. 30Example 3.20(1)idfucl 17823
[Adamek] p. 30Example 3.20(2)diag1 49286
[Adamek] p. 32Proposition 3.21funciso 17816
[Adamek] p. 33Example 3.26(1)discsnterm 49556  discthing 49443
[Adamek] p. 33Example 3.26(2)df-thinc 49400  prsthinc 49446  thincciso 49435  thincciso2 49437  thincciso3 49438  thinccisod 49436
[Adamek] p. 33Example 3.26(3)df-mndtc 49560
[Adamek] p. 33Proposition 3.23cofucl 17830  cofucla 49078
[Adamek] p. 34Remark 3.28(1)cofidfth 49144
[Adamek] p. 34Remark 3.28(2)catciso 18053  catcisoi 49382
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18108
[Adamek] p. 34Definition 3.27(2)df-fth 17849
[Adamek] p. 34Definition 3.27(3)df-full 17848
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18108
[Adamek] p. 35Corollary 3.32ffthiso 17873
[Adamek] p. 35Proposition 3.30(c)cofth 17879
[Adamek] p. 35Proposition 3.30(d)cofull 17878
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18093
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18093
[Adamek] p. 39Remark 3.422oppf 49114
[Adamek] p. 39Definition 3.41df-oppf 49105  funcoppc 17817
[Adamek] p. 39Definition 3.44.df-catc 18041  elcatchom 49379
[Adamek] p. 39Proposition 3.43(c)fthoppc 17867  fthoppf 49146
[Adamek] p. 39Proposition 3.43(d)fulloppc 17866  fulloppf 49145
[Adamek] p. 40Remark 3.48catccat 18050
[Adamek] p. 40Definition 3.470funcg 49067  df-catc 18041
[Adamek] p. 45Exercise 3Gincat 49583
[Adamek] p. 48Remark 4.2(2)cnelsubc 49586  nelsubc3 49053
[Adamek] p. 48Remark 4.2(3)imasubc 49133  imasubc2 49134  imasubc3 49138
[Adamek] p. 48Example 4.3(1.a)0subcat 17780
[Adamek] p. 48Example 4.3(1.b)catsubcat 17781
[Adamek] p. 48Definition 4.1(1)nelsubc3 49053
[Adamek] p. 48Definition 4.1(2)fullsubc 17792
[Adamek] p. 48Definition 4.1(a)df-subc 17754
[Adamek] p. 49Remark 4.4idsubc 49142
[Adamek] p. 49Remark 4.4(1)idemb 49141
[Adamek] p. 49Remark 4.4(2)idfullsubc 49143  ressffth 17882
[Adamek] p. 58Exercise 4Asetc1onsubc 49584
[Adamek] p. 83Definition 6.1df-nat 17888
[Adamek] p. 87Remark 6.14(a)fuccocl 17909
[Adamek] p. 87Remark 6.14(b)fucass 17913
[Adamek] p. 87Definition 6.15df-fuc 17889
[Adamek] p. 88Remark 6.16fuccat 17915
[Adamek] p. 101Definition 7.10funcg 49067  df-inito 17926
[Adamek] p. 101Example 7.2(3)0funcg 49067  df-termc 49455  initc 49073
[Adamek] p. 101Example 7.2 (6)irinitoringc 21421
[Adamek] p. 102Definition 7.4df-termo 17927  oppctermo 49218
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17954
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17958
[Adamek] p. 103Remark 7.8oppczeroo 49219
[Adamek] p. 103Definition 7.7df-zeroo 17928
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21422
[Adamek] p. 103Proposition 7.6termoeu1w 17961
[Adamek] p. 106Definition 7.19df-sect 17689
[Adamek] p. 107Example 7.20(7)thincinv 49451
[Adamek] p. 108Example 7.25(4)thincsect2 49450
[Adamek] p. 110Example 7.33(9)thincmon 49415
[Adamek] p. 110Proposition 7.35sectmon 17724
[Adamek] p. 112Proposition 7.42sectepi 17726
[Adamek] p. 185Section 10.67updjud 9863
[Adamek] p. 193Definition 11.1(1)df-lmd 49627
[Adamek] p. 193Definition 11.3(1)df-lmd 49627
[Adamek] p. 194Definition 11.3(2)df-lmd 49627
[Adamek] p. 202Definition 11.27(1)df-cmd 49628
[Adamek] p. 202Definition 11.27(2)df-cmd 49628
[Adamek] p. 478Item Rngdf-ringc 20566
[AhoHopUll] p. 2Section 1.1df-bigo 48530
[AhoHopUll] p. 12Section 1.3df-blen 48552
[AhoHopUll] p. 318Section 9.1df-concat 14512  df-pfx 14612  df-substr 14582  df-word 14455  lencl 14474  wrd0 14480
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24629  df-nmoo 30724
[AkhiezerGlazman] p. 64Theoremhmopidmch 32132  hmopidmchi 32130
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32180  pjcmul2i 32181
[AkhiezerGlazman] p. 72Theoremcnvunop 31897  unoplin 31899
[AkhiezerGlazman] p. 72Equation 2unopadj 31898  unopadj2 31917
[AkhiezerGlazman] p. 73Theoremelunop2 31992  lnopunii 31991
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32065
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27875
[Alling] p. 184Axiom Bbdayfo 27622
[Alling] p. 184Axiom Osltso 27621
[Alling] p. 184Axiom SDnodense 27637
[Alling] p. 185Lemma 0nocvxmin 27724
[Alling] p. 185Theoremconway 27745
[Alling] p. 185Axiom FEnoeta 27688
[Alling] p. 186Theorem 4slerec 27765  slerecd 27766
[Alling], p. 2Definitionrp-brsslt 43405
[Alling], p. 3Notenla0001 43408  nla0002 43406  nla0003 43407
[Apostol] p. 18Theorem I.1addcan 11334  addcan2d 11354  addcan2i 11344  addcand 11353  addcani 11343
[Apostol] p. 18Theorem I.2negeu 11387
[Apostol] p. 18Theorem I.3negsub 11446  negsubd 11515  negsubi 11476
[Apostol] p. 18Theorem I.4negneg 11448  negnegd 11500  negnegi 11468
[Apostol] p. 18Theorem I.5subdi 11587  subdid 11610  subdii 11603  subdir 11588  subdird 11611  subdiri 11604
[Apostol] p. 18Theorem I.6mul01 11329  mul01d 11349  mul01i 11340  mul02 11328  mul02d 11348  mul02i 11339
[Apostol] p. 18Theorem I.7mulcan 11791  mulcan2d 11788  mulcand 11787  mulcani 11793
[Apostol] p. 18Theorem I.8receu 11799  xreceu 32892
[Apostol] p. 18Theorem I.9divrec 11829  divrecd 11937  divreci 11903  divreczi 11896
[Apostol] p. 18Theorem I.10recrec 11855  recreci 11890
[Apostol] p. 18Theorem I.11mul0or 11794  mul0ord 11802  mul0ori 11801
[Apostol] p. 18Theorem I.12mul2neg 11593  mul2negd 11609  mul2negi 11602  mulneg1 11590  mulneg1d 11607  mulneg1i 11600
[Apostol] p. 18Theorem I.13divadddiv 11873  divadddivd 11978  divadddivi 11920
[Apostol] p. 18Theorem I.14divmuldiv 11858  divmuldivd 11975  divmuldivi 11918  rdivmuldivd 20333
[Apostol] p. 18Theorem I.15divdivdiv 11859  divdivdivd 11981  divdivdivi 11921
[Apostol] p. 20Axiom 7rpaddcl 12951  rpaddcld 12986  rpmulcl 12952  rpmulcld 12987
[Apostol] p. 20Axiom 8rpneg 12961
[Apostol] p. 20Axiom 90nrp 12964
[Apostol] p. 20Theorem I.17lttri 11276
[Apostol] p. 20Theorem I.18ltadd1d 11747  ltadd1dd 11765  ltadd1i 11708
[Apostol] p. 20Theorem I.19ltmul1 12008  ltmul1a 12007  ltmul1i 12077  ltmul1ii 12087  ltmul2 12009  ltmul2d 13013  ltmul2dd 13027  ltmul2i 12080
[Apostol] p. 20Theorem I.20msqgt0 11674  msqgt0d 11721  msqgt0i 11691
[Apostol] p. 20Theorem I.210lt1 11676
[Apostol] p. 20Theorem I.23lt0neg1 11660  lt0neg1d 11723  ltneg 11654  ltnegd 11732  ltnegi 11698
[Apostol] p. 20Theorem I.25lt2add 11639  lt2addd 11777  lt2addi 11716
[Apostol] p. 20Definition of positive numbersdf-rp 12928
[Apostol] p. 21Exercise 4recgt0 12004  recgt0d 12093  recgt0i 12064  recgt0ii 12065
[Apostol] p. 22Definition of integersdf-z 12506
[Apostol] p. 22Definition of positive integersdfnn3 12176
[Apostol] p. 22Definition of rationalsdf-q 12884
[Apostol] p. 24Theorem I.26supeu 9381
[Apostol] p. 26Theorem I.28nnunb 12414
[Apostol] p. 26Theorem I.29arch 12415  archd 45149
[Apostol] p. 28Exercise 2btwnz 12613
[Apostol] p. 28Exercise 3nnrecl 12416
[Apostol] p. 28Exercise 4rebtwnz 12882
[Apostol] p. 28Exercise 5zbtwnre 12881
[Apostol] p. 28Exercise 6qbtwnre 13135
[Apostol] p. 28Exercise 10(a)zeneo 16285  zneo 12593  zneoALTV 47663
[Apostol] p. 29Theorem I.35cxpsqrtth 26672  msqsqrtd 15385  resqrtth 15197  sqrtth 15307  sqrtthi 15313  sqsqrtd 15384
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12165
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12848
[Apostol] p. 361Remarkcrreczi 14169
[Apostol] p. 363Remarkabsgt0i 15342
[Apostol] p. 363Exampleabssubd 15398  abssubi 15346
[ApostolNT] p. 7Remarkfmtno0 47534  fmtno1 47535  fmtno2 47544  fmtno3 47545  fmtno4 47546  fmtno5fac 47576  fmtnofz04prm 47571
[ApostolNT] p. 7Definitiondf-fmtno 47522
[ApostolNT] p. 8Definitiondf-ppi 27043
[ApostolNT] p. 14Definitiondf-dvds 16199
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16215
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16240
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16235
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16228
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16230
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16216
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16217
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16222
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16257
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16259
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16261
[ApostolNT] p. 15Definitiondf-gcd 16441  dfgcd2 16492
[ApostolNT] p. 16Definitionisprm2 16628
[ApostolNT] p. 16Theorem 1.5coprmdvds 16599
[ApostolNT] p. 16Theorem 1.7prminf 16862
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16459
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16493
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16495
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16474
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16466
[ApostolNT] p. 17Theorem 1.8coprm 16657
[ApostolNT] p. 17Theorem 1.9euclemma 16659
[ApostolNT] p. 17Theorem 1.101arith2 16875
[ApostolNT] p. 18Theorem 1.13prmrec 16869
[ApostolNT] p. 19Theorem 1.14divalg 16349
[ApostolNT] p. 20Theorem 1.15eucalg 16533
[ApostolNT] p. 24Definitiondf-mu 27044
[ApostolNT] p. 25Definitiondf-phi 16712
[ApostolNT] p. 25Theorem 2.1musum 27134
[ApostolNT] p. 26Theorem 2.2phisum 16737
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16722
[ApostolNT] p. 28Theorem 2.5(c)phimul 16726
[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 16610
[ApostolNT] p. 106Remarkdvdsval3 16202
[ApostolNT] p. 106Definitionmoddvds 16209
[ApostolNT] p. 107Example 2mod2eq0even 16292
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16293
[ApostolNT] p. 107Example 4zmod1congr 13826
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13866
[ApostolNT] p. 107Theorem 5.2(c)modexp 14179
[ApostolNT] p. 108Theorem 5.3modmulconst 16234
[ApostolNT] p. 109Theorem 5.4cncongr1 16613
[ApostolNT] p. 109Theorem 5.6gcdmodi 17021
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16615
[ApostolNT] p. 113Theorem 5.17eulerth 16729
[ApostolNT] p. 113Theorem 5.18vfermltl 16748
[ApostolNT] p. 114Theorem 5.19fermltl 16730
[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 41625
[Baer] p. 40Property (c)mapd11 41626
[Baer] p. 40Property (e)mapdin 41649  mapdlsm 41651
[Baer] p. 40Property (f)mapd0 41652
[Baer] p. 40Definition of projectivitydf-mapd 41612  mapd1o 41635
[Baer] p. 41Property (g)mapdat 41654
[Baer] p. 44Part (1)mapdpg 41693
[Baer] p. 45Part (2)hdmap1eq 41788  mapdheq 41715  mapdheq2 41716  mapdheq2biN 41717
[Baer] p. 45Part (3)baerlem3 41700
[Baer] p. 46Part (4)mapdheq4 41719  mapdheq4lem 41718
[Baer] p. 46Part (5)baerlem5a 41701  baerlem5abmN 41705  baerlem5amN 41703  baerlem5b 41702  baerlem5bmN 41704
[Baer] p. 47Part (6)hdmap1l6 41808  hdmap1l6a 41796  hdmap1l6e 41801  hdmap1l6f 41802  hdmap1l6g 41803  hdmap1l6lem1 41794  hdmap1l6lem2 41795  mapdh6N 41734  mapdh6aN 41722  mapdh6eN 41727  mapdh6fN 41728  mapdh6gN 41729  mapdh6lem1N 41720  mapdh6lem2N 41721
[Baer] p. 48Part 9hdmapval 41815
[Baer] p. 48Part 10hdmap10 41827
[Baer] p. 48Part 11hdmapadd 41830
[Baer] p. 48Part (6)hdmap1l6h 41804  mapdh6hN 41730
[Baer] p. 48Part (7)mapdh75cN 41740  mapdh75d 41741  mapdh75e 41739  mapdh75fN 41742  mapdh7cN 41736  mapdh7dN 41737  mapdh7eN 41735  mapdh7fN 41738
[Baer] p. 48Part (8)mapdh8 41775  mapdh8a 41762  mapdh8aa 41763  mapdh8ab 41764  mapdh8ac 41765  mapdh8ad 41766  mapdh8b 41767  mapdh8c 41768  mapdh8d 41770  mapdh8d0N 41769  mapdh8e 41771  mapdh8g 41772  mapdh8i 41773  mapdh8j 41774
[Baer] p. 48Part (9)mapdh9a 41776
[Baer] p. 48Equation 10mapdhvmap 41756
[Baer] p. 49Part 12hdmap11 41835  hdmapeq0 41831  hdmapf1oN 41852  hdmapneg 41833  hdmaprnN 41851  hdmaprnlem1N 41836  hdmaprnlem3N 41837  hdmaprnlem3uN 41838  hdmaprnlem4N 41840  hdmaprnlem6N 41841  hdmaprnlem7N 41842  hdmaprnlem8N 41843  hdmaprnlem9N 41844  hdmapsub 41834
[Baer] p. 49Part 14hdmap14lem1 41855  hdmap14lem10 41864  hdmap14lem1a 41853  hdmap14lem2N 41856  hdmap14lem2a 41854  hdmap14lem3 41857  hdmap14lem8 41862  hdmap14lem9 41863
[Baer] p. 50Part 14hdmap14lem11 41865  hdmap14lem12 41866  hdmap14lem13 41867  hdmap14lem14 41868  hdmap14lem15 41869  hgmapval 41874
[Baer] p. 50Part 15hgmapadd 41881  hgmapmul 41882  hgmaprnlem2N 41884  hgmapvs 41878
[Baer] p. 50Part 16hgmaprnN 41888
[Baer] p. 110Lemma 1hdmapip0com 41904
[Baer] p. 110Line 27hdmapinvlem1 41905
[Baer] p. 110Line 28hdmapinvlem2 41906
[Baer] p. 110Line 30hdmapinvlem3 41907
[Baer] p. 110Part 1.2hdmapglem5 41909  hgmapvv 41913
[Baer] p. 110Proposition 1hdmapinvlem4 41908
[Baer] p. 111Line 10hgmapvvlem1 41910
[Baer] p. 111Line 15hdmapg 41917  hdmapglem7 41916
[Bauer], p. 483Theorem 1.22irrexpq 26673  2irrexpqALT 26743
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2562
[BellMachover] p. 460Notationdf-mo 2533
[BellMachover] p. 460Definitionmo3 2557
[BellMachover] p. 461Axiom Extax-ext 2701
[BellMachover] p. 462Theorem 1.1axextmo 2705
[BellMachover] p. 463Axiom Repaxrep5 5237
[BellMachover] p. 463Scheme Sepax-sep 5246
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37045  sepex 5250
[BellMachover] p. 466Problemaxpow2 5317
[BellMachover] p. 466Axiom Powaxpow3 5318
[BellMachover] p. 466Axiom Unionaxun2 7693
[BellMachover] p. 468Definitiondf-ord 6323
[BellMachover] p. 469Theorem 2.2(i)ordirr 6338
[BellMachover] p. 469Theorem 2.2(iii)onelon 6345
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6340
[BellMachover] p. 471Definition of Ndf-om 7823
[BellMachover] p. 471Problem 2.5(ii)uniordint 7757
[BellMachover] p. 471Definition of Limdf-lim 6325
[BellMachover] p. 472Axiom Infzfinf2 9571
[BellMachover] p. 473Theorem 2.8limom 7838
[BellMachover] p. 477Equation 3.1df-r1 9693
[BellMachover] p. 478Definitionrankval2 9747
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9711  r1ord3g 9708
[BellMachover] p. 480Axiom Regzfreg 9524
[BellMachover] p. 488Axiom ACac5 10406  dfac4 10051
[BellMachover] p. 490Definition of alephalephval3 10039
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39305
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32332
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32374  chirredi 32373
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32362
[Beran] p. 3Definition of joinsshjval3 31333
[Beran] p. 39Theorem 2.3(i)cmcm2 31595  cmcm2i 31572  cmcm2ii 31577  cmt2N 39236
[Beran] p. 40Theorem 2.3(iii)lecm 31596  lecmi 31581  lecmii 31582
[Beran] p. 45Theorem 3.4cmcmlem 31570
[Beran] p. 49Theorem 4.2cm2j 31599  cm2ji 31604  cm2mi 31605
[Beran] p. 95Definitiondf-sh 31186  issh2 31188
[Beran] p. 95Lemma 3.1(S5)his5 31065
[Beran] p. 95Lemma 3.1(S6)his6 31078
[Beran] p. 95Lemma 3.1(S7)his7 31069
[Beran] p. 95Lemma 3.2(S8)ho01i 31807
[Beran] p. 95Lemma 3.2(S9)hoeq1 31809
[Beran] p. 95Lemma 3.2(S10)ho02i 31808
[Beran] p. 95Lemma 3.2(S11)hoeq2 31810
[Beran] p. 95Postulate (S1)ax-his1 31061  his1i 31079
[Beran] p. 95Postulate (S2)ax-his2 31062
[Beran] p. 95Postulate (S3)ax-his3 31063
[Beran] p. 95Postulate (S4)ax-his4 31064
[Beran] p. 96Definition of normdf-hnorm 30947  dfhnorm2 31101  normval 31103
[Beran] p. 96Definition for Cauchy sequencehcau 31163
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30952
[Beran] p. 96Definition of complete subspaceisch3 31220
[Beran] p. 96Definition of convergedf-hlim 30951  hlimi 31167
[Beran] p. 97Theorem 3.3(i)norm-i-i 31112  norm-i 31108
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31116  norm-ii 31117  normlem0 31088  normlem1 31089  normlem2 31090  normlem3 31091  normlem4 31092  normlem5 31093  normlem6 31094  normlem7 31095  normlem7tALT 31098
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31118  norm-iii 31119
[Beran] p. 98Remark 3.4bcs 31160  bcsiALT 31158  bcsiHIL 31159
[Beran] p. 98Remark 3.4(B)normlem9at 31100  normpar 31134  normpari 31133
[Beran] p. 98Remark 3.4(C)normpyc 31125  normpyth 31124  normpythi 31121
[Beran] p. 99Remarklnfn0 32026  lnfn0i 32021  lnop0 31945  lnop0i 31949
[Beran] p. 99Theorem 3.5(i)nmcexi 32005  nmcfnex 32032  nmcfnexi 32030  nmcopex 32008  nmcopexi 32006
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32033  nmcfnlbi 32031  nmcoplb 32009  nmcoplbi 32007
[Beran] p. 99Theorem 3.5(iii)lnfncon 32035  lnfnconi 32034  lnopcon 32014  lnopconi 32013
[Beran] p. 100Lemma 3.6normpar2i 31135
[Beran] p. 101Lemma 3.6norm3adifi 31132  norm3adifii 31127  norm3dif 31129  norm3difi 31126
[Beran] p. 102Theorem 3.7(i)chocunii 31280  pjhth 31372  pjhtheu 31373  pjpjhth 31404  pjpjhthi 31405  pjth 25372
[Beran] p. 102Theorem 3.7(ii)ococ 31385  ococi 31384
[Beran] p. 103Remark 3.8nlelchi 32040
[Beran] p. 104Theorem 3.9riesz3i 32041  riesz4 32043  riesz4i 32042
[Beran] p. 104Theorem 3.10cnlnadj 32058  cnlnadjeu 32057  cnlnadjeui 32056  cnlnadji 32055  cnlnadjlem1 32046  nmopadjlei 32067
[Beran] p. 106Theorem 3.11(i)adjeq0 32070
[Beran] p. 106Theorem 3.11(v)nmopadji 32069
[Beran] p. 106Theorem 3.11(ii)adjmul 32071
[Beran] p. 106Theorem 3.11(iv)adjadj 31915
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32081  nmopcoadji 32080
[Beran] p. 106Theorem 3.11(iii)adjadd 32072
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32082
[Beran] p. 106Theorem 3.11(viii)adjcoi 32079  pjadj2coi 32183  pjadjcoi 32140
[Beran] p. 107Definitiondf-ch 31200  isch2 31202
[Beran] p. 107Remark 3.12choccl 31285  isch3 31220  occl 31283  ocsh 31262  shoccl 31284  shocsh 31263
[Beran] p. 107Remark 3.12(B)ococin 31387
[Beran] p. 108Theorem 3.13chintcl 31311
[Beran] p. 109Property (i)pjadj2 32166  pjadj3 32167  pjadji 31664  pjadjii 31653
[Beran] p. 109Property (ii)pjidmco 32160  pjidmcoi 32156  pjidmi 31652
[Beran] p. 110Definition of projector orderingpjordi 32152
[Beran] p. 111Remarkho0val 31729  pjch1 31649
[Beran] p. 111Definitiondf-hfmul 31713  df-hfsum 31712  df-hodif 31711  df-homul 31710  df-hosum 31709
[Beran] p. 111Lemma 4.4(i)pjo 31650
[Beran] p. 111Lemma 4.4(ii)pjch 31673  pjchi 31411
[Beran] p. 111Lemma 4.4(iii)pjoc2 31418  pjoc2i 31417
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31659
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32144  pjssmii 31660
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32143
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32142
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32147
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32145  pjssge0ii 31661
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32146  pjdifnormii 31662
[Bobzien] p. 116Statement T3stoic3 1776
[Bobzien] p. 117Statement T2stoic2a 1774
[Bobzien] p. 117Statement T4stoic4a 1777
[Bobzien] p. 117Conclusion the contradictorystoic1a 1772
[Bogachev] p. 16Definition 1.5df-oms 34276
[Bogachev] p. 17Lemma 1.5.4omssubadd 34284
[Bogachev] p. 17Example 1.5.2omsmon 34282
[Bogachev] p. 41Definition 1.11.2df-carsg 34286
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34306
[Bogachev] p. 116Definition 2.3.1df-itgm 34337  df-sitm 34315
[Bogachev] p. 118Chapter 2.4.4df-itgm 34337
[Bogachev] p. 118Definition 2.4.1df-sitg 34314
[Bollobas] p. 1Section I.1df-edg 29028  isuhgrop 29050  isusgrop 29142  isuspgrop 29141
[Bollobas] p. 2Section I.1df-isubgr 47854  df-subgr 29248  uhgrspan1 29283  uhgrspansubgr 29271
[Bollobas] p. 3Definitiondf-gric 47874  gricuspgr 47911  isuspgrim 47889
[Bollobas] p. 3Section I.1cusgrsize 29435  df-clnbgr 47813  df-cusgr 29392  df-nbgr 29313  fusgrmaxsize 29445
[Bollobas] p. 4Definitiondf-upwlks 48115  df-wlks 29580
[Bollobas] p. 4Section I.1finsumvtxdg2size 29531  finsumvtxdgeven 29533  fusgr1th 29532  fusgrvtxdgonume 29535  vtxdgoddnumeven 29534
[Bollobas] p. 5Notationdf-pths 29694
[Bollobas] p. 5Definitiondf-crcts 29766  df-cycls 29767  df-trls 29671  df-wlkson 29581
[Bollobas] p. 7Section I.1df-ushgr 29039
[BourbakiAlg1] p. 1Definition 1df-clintop 48181  df-cllaw 48167  df-mgm 18549  df-mgm2 48200
[BourbakiAlg1] p. 4Definition 5df-assintop 48182  df-asslaw 48169  df-sgrp 18628  df-sgrp2 48202
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48201  df-comlaw 48168
[BourbakiAlg1] p. 12Definition 2df-mnd 18644
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33010  mndlactf1o 33014  mndractf1 33012  mndractf1o 33015
[BourbakiAlg1] p. 92Definition 1df-ring 20155
[BourbakiAlg1] p. 93Section I.8.1df-rng 20073
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33622
[BourbakiAlg2] p. 113Chapter 5.assafld 33626  assarrginv 33625
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33666  fldextrspunfld 33664  fldextrspunlem1 33663  fldextrspunlem2 33665  fldextrspunlsp 33662  fldextrspunlsplem 33661
[BourbakiCAlg2], p. 228Proposition 21arithidom 33501  dfufd2 33514
[BourbakiEns] p. Proposition 8fcof1 7244  fcofo 7245
[BourbakiTop1] p. Remarkxnegmnf 13146  xnegpnf 13145
[BourbakiTop1] p. Remark rexneg 13147
[BourbakiTop1] p. Remark 3ust0 24140  ustfilxp 24133
[BourbakiTop1] p. Axiom GT'tgpsubcn 24010
[BourbakiTop1] p. Criterionishmeo 23679
[BourbakiTop1] p. Example 1cstucnd 24204  iducn 24203  snfil 23784
[BourbakiTop1] p. Example 2neifil 23800
[BourbakiTop1] p. Theorem 1cnextcn 23987
[BourbakiTop1] p. Theorem 2ucnextcn 24224
[BourbakiTop1] p. Theorem 3df-hcmp 33940
[BourbakiTop1] p. Paragraph 3infil 23783
[BourbakiTop1] p. Definition 1df-ucn 24196  df-ust 24121  filintn0 23781  filn0 23782  istgp 23997  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 33839
[BourbakiTop1] p. Property V_issnei2 23036
[BourbakiTop1] p. Theorem 1(d)iscncl 23189
[BourbakiTop1] p. Condition F_Iustssel 24126
[BourbakiTop1] p. Condition U_Iustdiag 24129
[BourbakiTop1] p. Property V_iiinnei 23045
[BourbakiTop1] p. Property V_ivneiptopreu 23053  neissex 23047
[BourbakiTop1] p. Proposition 1neips 23033  neiss 23029  ucncn 24205  ustund 24142  ustuqtop 24167
[BourbakiTop1] p. Proposition 2cnpco 23187  neiptopreu 23053  utop2nei 24171  utop3cls 24172
[BourbakiTop1] p. Proposition 3fmucnd 24212  uspreg 24194  utopreg 24173
[BourbakiTop1] p. Proposition 4imasncld 23611  imasncls 23612  imasnopn 23610
[BourbakiTop1] p. Proposition 9cnpflf2 23920
[BourbakiTop1] p. Condition F_IIustincl 24128
[BourbakiTop1] p. Condition U_IIustinvel 24130
[BourbakiTop1] p. Property V_iiielnei 23031
[BourbakiTop1] p. Proposition 11cnextucn 24223
[BourbakiTop1] p. Condition F_IIbustbasel 24127
[BourbakiTop1] p. Condition U_IIIustexhalf 24131
[BourbakiTop1] p. Definition C'''df-cmp 23307
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23766
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22814
[BourbakiTop2] p. 195Definition 1df-ldlf 33836
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46053
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46055  stoweid 46054
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 45992  stoweidlem10 46001  stoweidlem14 46005  stoweidlem15 46006  stoweidlem35 46026  stoweidlem36 46027  stoweidlem37 46028  stoweidlem38 46029  stoweidlem40 46031  stoweidlem41 46032  stoweidlem43 46034  stoweidlem44 46035  stoweidlem46 46037  stoweidlem5 45996  stoweidlem50 46041  stoweidlem52 46043  stoweidlem53 46044  stoweidlem55 46046  stoweidlem56 46047
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46014  stoweidlem24 46015  stoweidlem27 46018  stoweidlem28 46019  stoweidlem30 46021
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46025  stoweidlem59 46050  stoweidlem60 46051
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46036  stoweidlem49 46040  stoweidlem7 45998
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46022  stoweidlem39 46030  stoweidlem42 46033  stoweidlem48 46039  stoweidlem51 46042  stoweidlem54 46045  stoweidlem57 46048  stoweidlem58 46049
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46016
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46008
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46002  stoweidlem13 46004  stoweidlem26 46017  stoweidlem61 46052
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46009
[Bruck] p. 1Section I.1df-clintop 48181  df-mgm 18549  df-mgm2 48200
[Bruck] p. 23Section II.1df-sgrp 18628  df-sgrp2 48202
[Bruck] p. 28Theorem 3.2dfgrp3 18953
[ChoquetDD] p. 2Definition of mappingdf-mpt 5184
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30382
[Clemente] p. 10Definition I` `m,nnatded 30382
[Clemente] p. 11Definition E=>m,nnatded 30382
[Clemente] p. 11Definition I=>m,nnatded 30382
[Clemente] p. 11Definition E` `(1)natded 30382
[Clemente] p. 11Definition E` `(2)natded 30382
[Clemente] p. 12Definition E` `m,n,pnatded 30382
[Clemente] p. 12Definition I` `n(1)natded 30382
[Clemente] p. 12Definition I` `n(2)natded 30382
[Clemente] p. 13Definition I` `m,n,pnatded 30382
[Clemente] p. 14Proof 5.11natded 30382
[Clemente] p. 14Definition E` `nnatded 30382
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30384  ex-natded5.2 30383
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30387  ex-natded5.3 30386
[Clemente] p. 18Theorem 5.5ex-natded5.5 30389
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30391  ex-natded5.7 30390
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30393  ex-natded5.8 30392
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30395  ex-natded5.13 30394
[Clemente] p. 32Definition I` `nnatded 30382
[Clemente] p. 32Definition E` `m,n,p,anatded 30382
[Clemente] p. 32Definition E` `n,tnatded 30382
[Clemente] p. 32Definition I` `n,tnatded 30382
[Clemente] p. 43Theorem 9.20ex-natded9.20 30396
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30397
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30399  ex-natded9.26 30398
[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 34269  sxbrsigalem4 34271
[Cohn] p. 81Section II.5acsdomd 18498  acsinfd 18497  acsinfdimd 18499  acsmap2d 18496  acsmapd 18495
[Cohn] p. 143Example 5.1.1sxbrsiga 34274
[Connell] p. 57Definitiondf-scmat 22411  df-scmatalt 48381
[Conway] p. 4Definitionslerec 27765  slerecd 27766
[Conway] p. 5Definitionaddsval 27909  addsval2 27910  df-adds 27907  df-muls 28050  df-negs 27967
[Conway] p. 7Theorem0slt1s 27778
[Conway] p. 16Theorem 0(i)ssltright 27820
[Conway] p. 16Theorem 0(ii)ssltleft 27819
[Conway] p. 16Theorem 0(iii)slerflex 27708
[Conway] p. 17Theorem 3addsass 27952  addsassd 27953  addscom 27913  addscomd 27914  addsrid 27911  addsridd 27912
[Conway] p. 17Definitiondf-0s 27773
[Conway] p. 17Theorem 4(ii)negnegs 27990
[Conway] p. 17Theorem 4(iii)negsid 27987  negsidd 27988
[Conway] p. 18Theorem 5sleadd1 27936  sleadd1d 27942
[Conway] p. 18Definitiondf-1s 27774
[Conway] p. 18Theorem 6(ii)negscl 27982  negscld 27983
[Conway] p. 18Theorem 6(iii)addscld 27927
[Conway] p. 19Notemulsunif2 28113
[Conway] p. 19Theorem 7addsdi 28098  addsdid 28099  addsdird 28100  mulnegs1d 28103  mulnegs2d 28104  mulsass 28109  mulsassd 28110  mulscom 28082  mulscomd 28083
[Conway] p. 19Theorem 8(i)mulscl 28077  mulscld 28078
[Conway] p. 19Theorem 8(iii)slemuld 28081  sltmul 28079  sltmuld 28080
[Conway] p. 20Theorem 9mulsgt0 28087  mulsgt0d 28088
[Conway] p. 21Theorem 10(iv)precsex 28160
[Conway] p. 23Theorem 11eqscut3 27770
[Conway] p. 24Definitiondf-reno 28398
[Conway] p. 24Theorem 13(ii)readdscl 28403  remulscl 28406  renegscl 28402
[Conway] p. 27Definitiondf-ons 28193  elons2 28199
[Conway] p. 27Theorem 14sltonex 28203
[Conway] p. 28Theorem 15onscutlt 28205  onswe 28210
[Conway] p. 29Remarkmadebday 27849  newbday 27851  oldbday 27850
[Conway] p. 29Definitiondf-made 27792  df-new 27794  df-old 27793
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13799
[Crawley] p. 1Definition of posetdf-poset 18254
[Crawley] p. 107Theorem 13.2hlsupr 39373
[Crawley] p. 110Theorem 13.3arglem1N 40177  dalaw 39873
[Crawley] p. 111Theorem 13.4hlathil 41948
[Crawley] p. 111Definition of set Wdf-watsN 39977
[Crawley] p. 111Definition of dilationdf-dilN 40093  df-ldil 40091  isldil 40097
[Crawley] p. 111Definition of translationdf-ltrn 40092  df-trnN 40094  isltrn 40106  ltrnu 40108
[Crawley] p. 112Lemma Acdlema1N 39778  cdlema2N 39779  exatleN 39391
[Crawley] p. 112Lemma B1cvrat 39463  cdlemb 39781  cdlemb2 40028  cdlemb3 40593  idltrn 40137  l1cvat 39041  lhpat 40030  lhpat2 40032  lshpat 39042  ltrnel 40126  ltrnmw 40138
[Crawley] p. 112Lemma Ccdlemc1 40178  cdlemc2 40179  ltrnnidn 40161  trlat 40156  trljat1 40153  trljat2 40154  trljat3 40155  trlne 40172  trlnidat 40160  trlnle 40173
[Crawley] p. 112Definition of automorphismdf-pautN 39978
[Crawley] p. 113Lemma Ccdlemc 40184  cdlemc3 40180  cdlemc4 40181
[Crawley] p. 113Lemma Dcdlemd 40194  cdlemd1 40185  cdlemd2 40186  cdlemd3 40187  cdlemd4 40188  cdlemd5 40189  cdlemd6 40190  cdlemd7 40191  cdlemd8 40192  cdlemd9 40193  cdleme31sde 40372  cdleme31se 40369  cdleme31se2 40370  cdleme31snd 40373  cdleme32a 40428  cdleme32b 40429  cdleme32c 40430  cdleme32d 40431  cdleme32e 40432  cdleme32f 40433  cdleme32fva 40424  cdleme32fva1 40425  cdleme32fvcl 40427  cdleme32le 40434  cdleme48fv 40486  cdleme4gfv 40494  cdleme50eq 40528  cdleme50f 40529  cdleme50f1 40530  cdleme50f1o 40533  cdleme50laut 40534  cdleme50ldil 40535  cdleme50lebi 40527  cdleme50rn 40532  cdleme50rnlem 40531  cdlemeg49le 40498  cdlemeg49lebilem 40526
[Crawley] p. 113Lemma Ecdleme 40547  cdleme00a 40196  cdleme01N 40208  cdleme02N 40209  cdleme0a 40198  cdleme0aa 40197  cdleme0b 40199  cdleme0c 40200  cdleme0cp 40201  cdleme0cq 40202  cdleme0dN 40203  cdleme0e 40204  cdleme0ex1N 40210  cdleme0ex2N 40211  cdleme0fN 40205  cdleme0gN 40206  cdleme0moN 40212  cdleme1 40214  cdleme10 40241  cdleme10tN 40245  cdleme11 40257  cdleme11a 40247  cdleme11c 40248  cdleme11dN 40249  cdleme11e 40250  cdleme11fN 40251  cdleme11g 40252  cdleme11h 40253  cdleme11j 40254  cdleme11k 40255  cdleme11l 40256  cdleme12 40258  cdleme13 40259  cdleme14 40260  cdleme15 40265  cdleme15a 40261  cdleme15b 40262  cdleme15c 40263  cdleme15d 40264  cdleme16 40272  cdleme16aN 40246  cdleme16b 40266  cdleme16c 40267  cdleme16d 40268  cdleme16e 40269  cdleme16f 40270  cdleme16g 40271  cdleme19a 40290  cdleme19b 40291  cdleme19c 40292  cdleme19d 40293  cdleme19e 40294  cdleme19f 40295  cdleme1b 40213  cdleme2 40215  cdleme20aN 40296  cdleme20bN 40297  cdleme20c 40298  cdleme20d 40299  cdleme20e 40300  cdleme20f 40301  cdleme20g 40302  cdleme20h 40303  cdleme20i 40304  cdleme20j 40305  cdleme20k 40306  cdleme20l 40309  cdleme20l1 40307  cdleme20l2 40308  cdleme20m 40310  cdleme20y 40289  cdleme20zN 40288  cdleme21 40324  cdleme21d 40317  cdleme21e 40318  cdleme22a 40327  cdleme22aa 40326  cdleme22b 40328  cdleme22cN 40329  cdleme22d 40330  cdleme22e 40331  cdleme22eALTN 40332  cdleme22f 40333  cdleme22f2 40334  cdleme22g 40335  cdleme23a 40336  cdleme23b 40337  cdleme23c 40338  cdleme26e 40346  cdleme26eALTN 40348  cdleme26ee 40347  cdleme26f 40350  cdleme26f2 40352  cdleme26f2ALTN 40351  cdleme26fALTN 40349  cdleme27N 40356  cdleme27a 40354  cdleme27cl 40353  cdleme28c 40359  cdleme3 40224  cdleme30a 40365  cdleme31fv 40377  cdleme31fv1 40378  cdleme31fv1s 40379  cdleme31fv2 40380  cdleme31id 40381  cdleme31sc 40371  cdleme31sdnN 40374  cdleme31sn 40367  cdleme31sn1 40368  cdleme31sn1c 40375  cdleme31sn2 40376  cdleme31so 40366  cdleme35a 40435  cdleme35b 40437  cdleme35c 40438  cdleme35d 40439  cdleme35e 40440  cdleme35f 40441  cdleme35fnpq 40436  cdleme35g 40442  cdleme35h 40443  cdleme35h2 40444  cdleme35sn2aw 40445  cdleme35sn3a 40446  cdleme36a 40447  cdleme36m 40448  cdleme37m 40449  cdleme38m 40450  cdleme38n 40451  cdleme39a 40452  cdleme39n 40453  cdleme3b 40216  cdleme3c 40217  cdleme3d 40218  cdleme3e 40219  cdleme3fN 40220  cdleme3fa 40223  cdleme3g 40221  cdleme3h 40222  cdleme4 40225  cdleme40m 40454  cdleme40n 40455  cdleme40v 40456  cdleme40w 40457  cdleme41fva11 40464  cdleme41sn3aw 40461  cdleme41sn4aw 40462  cdleme41snaw 40463  cdleme42a 40458  cdleme42b 40465  cdleme42c 40459  cdleme42d 40460  cdleme42e 40466  cdleme42f 40467  cdleme42g 40468  cdleme42h 40469  cdleme42i 40470  cdleme42k 40471  cdleme42ke 40472  cdleme42keg 40473  cdleme42mN 40474  cdleme42mgN 40475  cdleme43aN 40476  cdleme43bN 40477  cdleme43cN 40478  cdleme43dN 40479  cdleme5 40227  cdleme50ex 40546  cdleme50ltrn 40544  cdleme51finvN 40543  cdleme51finvfvN 40542  cdleme51finvtrN 40545  cdleme6 40228  cdleme7 40236  cdleme7a 40230  cdleme7aa 40229  cdleme7b 40231  cdleme7c 40232  cdleme7d 40233  cdleme7e 40234  cdleme7ga 40235  cdleme8 40237  cdleme8tN 40242  cdleme9 40240  cdleme9a 40238  cdleme9b 40239  cdleme9tN 40244  cdleme9taN 40243  cdlemeda 40285  cdlemedb 40284  cdlemednpq 40286  cdlemednuN 40287  cdlemefr27cl 40390  cdlemefr32fva1 40397  cdlemefr32fvaN 40396  cdlemefrs32fva 40387  cdlemefrs32fva1 40388  cdlemefs27cl 40400  cdlemefs32fva1 40410  cdlemefs32fvaN 40409  cdlemesner 40283  cdlemeulpq 40207
[Crawley] p. 114Lemma E4atex 40063  4atexlem7 40062  cdleme0nex 40277  cdleme17a 40273  cdleme17c 40275  cdleme17d 40485  cdleme17d1 40276  cdleme17d2 40482  cdleme18a 40278  cdleme18b 40279  cdleme18c 40280  cdleme18d 40282  cdleme4a 40226
[Crawley] p. 115Lemma Ecdleme21a 40312  cdleme21at 40315  cdleme21b 40313  cdleme21c 40314  cdleme21ct 40316  cdleme21f 40319  cdleme21g 40320  cdleme21h 40321  cdleme21i 40322  cdleme22gb 40281
[Crawley] p. 116Lemma Fcdlemf 40550  cdlemf1 40548  cdlemf2 40549
[Crawley] p. 116Lemma Gcdlemftr1 40554  cdlemg16 40644  cdlemg28 40691  cdlemg28a 40680  cdlemg28b 40690  cdlemg3a 40584  cdlemg42 40716  cdlemg43 40717  cdlemg44 40720  cdlemg44a 40718  cdlemg46 40722  cdlemg47 40723  cdlemg9 40621  ltrnco 40706  ltrncom 40725  tgrpabl 40738  trlco 40714
[Crawley] p. 116Definition of Gdf-tgrp 40730
[Crawley] p. 117Lemma Gcdlemg17 40664  cdlemg17b 40649
[Crawley] p. 117Definition of Edf-edring-rN 40743  df-edring 40744
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40747
[Crawley] p. 118Remarktendopltp 40767
[Crawley] p. 118Lemma Hcdlemh 40804  cdlemh1 40802  cdlemh2 40803
[Crawley] p. 118Lemma Icdlemi 40807  cdlemi1 40805  cdlemi2 40806
[Crawley] p. 118Lemma Jcdlemj1 40808  cdlemj2 40809  cdlemj3 40810  tendocan 40811
[Crawley] p. 118Lemma Kcdlemk 40961  cdlemk1 40818  cdlemk10 40830  cdlemk11 40836  cdlemk11t 40933  cdlemk11ta 40916  cdlemk11tb 40918  cdlemk11tc 40932  cdlemk11u-2N 40876  cdlemk11u 40858  cdlemk12 40837  cdlemk12u-2N 40877  cdlemk12u 40859  cdlemk13-2N 40863  cdlemk13 40839  cdlemk14-2N 40865  cdlemk14 40841  cdlemk15-2N 40866  cdlemk15 40842  cdlemk16-2N 40867  cdlemk16 40844  cdlemk16a 40843  cdlemk17-2N 40868  cdlemk17 40845  cdlemk18-2N 40873  cdlemk18-3N 40887  cdlemk18 40855  cdlemk19-2N 40874  cdlemk19 40856  cdlemk19u 40957  cdlemk1u 40846  cdlemk2 40819  cdlemk20-2N 40879  cdlemk20 40861  cdlemk21-2N 40878  cdlemk21N 40860  cdlemk22-3 40888  cdlemk22 40880  cdlemk23-3 40889  cdlemk24-3 40890  cdlemk25-3 40891  cdlemk26-3 40893  cdlemk26b-3 40892  cdlemk27-3 40894  cdlemk28-3 40895  cdlemk29-3 40898  cdlemk3 40820  cdlemk30 40881  cdlemk31 40883  cdlemk32 40884  cdlemk33N 40896  cdlemk34 40897  cdlemk35 40899  cdlemk36 40900  cdlemk37 40901  cdlemk38 40902  cdlemk39 40903  cdlemk39u 40955  cdlemk4 40821  cdlemk41 40907  cdlemk42 40928  cdlemk42yN 40931  cdlemk43N 40950  cdlemk45 40934  cdlemk46 40935  cdlemk47 40936  cdlemk48 40937  cdlemk49 40938  cdlemk5 40823  cdlemk50 40939  cdlemk51 40940  cdlemk52 40941  cdlemk53 40944  cdlemk54 40945  cdlemk55 40948  cdlemk55u 40953  cdlemk56 40958  cdlemk5a 40822  cdlemk5auN 40847  cdlemk5u 40848  cdlemk6 40824  cdlemk6u 40849  cdlemk7 40835  cdlemk7u-2N 40875  cdlemk7u 40857  cdlemk8 40825  cdlemk9 40826  cdlemk9bN 40827  cdlemki 40828  cdlemkid 40923  cdlemkj-2N 40869  cdlemkj 40850  cdlemksat 40833  cdlemksel 40832  cdlemksv 40831  cdlemksv2 40834  cdlemkuat 40853  cdlemkuel-2N 40871  cdlemkuel-3 40885  cdlemkuel 40852  cdlemkuv-2N 40870  cdlemkuv2-2 40872  cdlemkuv2-3N 40886  cdlemkuv2 40854  cdlemkuvN 40851  cdlemkvcl 40829  cdlemky 40913  cdlemkyyN 40949  tendoex 40962
[Crawley] p. 120Remarkdva1dim 40972
[Crawley] p. 120Lemma Lcdleml1N 40963  cdleml2N 40964  cdleml3N 40965  cdleml4N 40966  cdleml5N 40967  cdleml6 40968  cdleml7 40969  cdleml8 40970  cdleml9 40971  dia1dim 41048
[Crawley] p. 120Lemma Mdia11N 41035  diaf11N 41036  dialss 41033  diaord 41034  dibf11N 41148  djajN 41124
[Crawley] p. 120Definition of isomorphism mapdiaval 41019
[Crawley] p. 121Lemma Mcdlemm10N 41105  dia2dimlem1 41051  dia2dimlem2 41052  dia2dimlem3 41053  dia2dimlem4 41054  dia2dimlem5 41055  diaf1oN 41117  diarnN 41116  dvheveccl 41099  dvhopN 41103
[Crawley] p. 121Lemma Ncdlemn 41199  cdlemn10 41193  cdlemn11 41198  cdlemn11a 41194  cdlemn11b 41195  cdlemn11c 41196  cdlemn11pre 41197  cdlemn2 41182  cdlemn2a 41183  cdlemn3 41184  cdlemn4 41185  cdlemn4a 41186  cdlemn5 41188  cdlemn5pre 41187  cdlemn6 41189  cdlemn7 41190  cdlemn8 41191  cdlemn9 41192  diclspsn 41181
[Crawley] p. 121Definition of phi(q)df-dic 41160
[Crawley] p. 122Lemma Ndih11 41252  dihf11 41254  dihjust 41204  dihjustlem 41203  dihord 41251  dihord1 41205  dihord10 41210  dihord11b 41209  dihord11c 41211  dihord2 41214  dihord2a 41206  dihord2b 41207  dihord2cN 41208  dihord2pre 41212  dihord2pre2 41213  dihordlem6 41200  dihordlem7 41201  dihordlem7b 41202
[Crawley] p. 122Definition of isomorphism mapdihffval 41217  dihfval 41218  dihval 41219
[Diestel] p. 3Definitiondf-gric 47874  df-grim 47871  isuspgrim 47889
[Diestel] p. 3Section 1.1df-cusgr 29392  df-nbgr 29313
[Diestel] p. 3Definition by df-grisom 47870
[Diestel] p. 4Section 1.1df-isubgr 47854  df-subgr 29248  uhgrspan1 29283  uhgrspansubgr 29271
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29535  vtxdgoddnumeven 29534
[Diestel] p. 27Section 1.10df-ushgr 29039
[EGA] p. 80Notation 1.1.1rspecval 33847
[EGA] p. 80Proposition 1.1.2zartop 33859
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33851  zarcls1 33852
[EGA] p. 81Corollary 1.1.8zart0 33862
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33865
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33868
[Eisenberg] p. 67Definition 5.3df-dif 3914
[Eisenberg] p. 82Definition 6.3dfom3 9576
[Eisenberg] p. 125Definition 8.21df-map 8778
[Eisenberg] p. 216Example 13.2(4)omenps 9584
[Eisenberg] p. 310Theorem 19.8cardprc 9909
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10484
[Enderton] p. 18Axiom of Empty Setaxnul 5255
[Enderton] p. 19Definitiondf-tp 4590
[Enderton] p. 26Exercise 5unissb 4899
[Enderton] p. 26Exercise 10pwel 5331
[Enderton] p. 28Exercise 7(b)pwun 5524
[Enderton] p. 30Theorem "Distributive laws"iinin1 5038  iinin2 5037  iinun2 5032  iunin1 5031  iunin1f 32536  iunin2 5030  uniin1 32530  uniin2 32531
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5036  iundif2 5033
[Enderton] p. 32Exercise 20unineq 4247
[Enderton] p. 33Exercise 23iinuni 5057
[Enderton] p. 33Exercise 25iununi 5058
[Enderton] p. 33Exercise 24(a)iinpw 5065
[Enderton] p. 33Exercise 24(b)iunpw 7727  iunpwss 5066
[Enderton] p. 36Definitionopthwiener 5469
[Enderton] p. 38Exercise 6(a)unipw 5405
[Enderton] p. 38Exercise 6(b)pwuni 4905
[Enderton] p. 41Lemma 3Dopeluu 5425  rnex 7866  rnexg 7858
[Enderton] p. 41Exercise 8dmuni 5868  rnuni 6109
[Enderton] p. 42Definition of a functiondffun7 6527  dffun8 6528
[Enderton] p. 43Definition of function valuefunfv2 6931
[Enderton] p. 43Definition of single-rootedfuncnv 6569
[Enderton] p. 44Definition (d)dfima2 6022  dfima3 6023
[Enderton] p. 47Theorem 3Hfvco2 6940
[Enderton] p. 49Axiom of Choice (first form)ac7 10402  ac7g 10403  df-ac 10045  dfac2 10061  dfac2a 10059  dfac2b 10060  dfac3 10050  dfac7 10062
[Enderton] p. 50Theorem 3K(a)imauni 7202
[Enderton] p. 52Definitiondf-map 8778
[Enderton] p. 53Exercise 21coass 6226
[Enderton] p. 53Exercise 27dmco 6215
[Enderton] p. 53Exercise 14(a)funin 6576
[Enderton] p. 53Exercise 22(a)imass2 6062
[Enderton] p. 54Remarkixpf 8870  ixpssmap 8882
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8848
[Enderton] p. 55Axiom of Choice (second form)ac9 10412  ac9s 10422
[Enderton] p. 56Theorem 3Meqvrelref 38594  erref 8668
[Enderton] p. 57Lemma 3Neqvrelthi 38597  erthi 8704
[Enderton] p. 57Definitiondf-ec 8650
[Enderton] p. 58Definitiondf-qs 8654
[Enderton] p. 61Exercise 35df-ec 8650
[Enderton] p. 65Exercise 56(a)dmun 5864
[Enderton] p. 68Definition of successordf-suc 6326
[Enderton] p. 71Definitiondf-tr 5210  dftr4 5216
[Enderton] p. 72Theorem 4Eunisuc 6401  unisucg 6400
[Enderton] p. 73Exercise 6unisuc 6401  unisucg 6400
[Enderton] p. 73Exercise 5(a)truni 5225
[Enderton] p. 73Exercise 5(b)trint 5227  trintALT 44863
[Enderton] p. 79Theorem 4I(A1)nna0 8545
[Enderton] p. 79Theorem 4I(A2)nnasuc 8547  onasuc 8469
[Enderton] p. 79Definition of operation valuedf-ov 7372
[Enderton] p. 80Theorem 4J(A1)nnm0 8546
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8548  onmsuc 8470
[Enderton] p. 81Theorem 4K(1)nnaass 8563
[Enderton] p. 81Theorem 4K(2)nna0r 8550  nnacom 8558
[Enderton] p. 81Theorem 4K(3)nndi 8564
[Enderton] p. 81Theorem 4K(4)nnmass 8565
[Enderton] p. 81Theorem 4K(5)nnmcom 8567
[Enderton] p. 82Exercise 16nnm0r 8551  nnmsucr 8566
[Enderton] p. 88Exercise 23nnaordex 8579
[Enderton] p. 129Definitiondf-en 8896
[Enderton] p. 132Theorem 6B(b)canth 7323
[Enderton] p. 133Exercise 1xpomen 9944
[Enderton] p. 133Exercise 2qnnen 16157
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9148
[Enderton] p. 135Corollary 6Cphp3 9150
[Enderton] p. 136Corollary 6Enneneq 9147
[Enderton] p. 136Corollary 6D(a)pssinf 9179
[Enderton] p. 136Corollary 6D(b)ominf 9181
[Enderton] p. 137Lemma 6Fpssnn 9109
[Enderton] p. 138Corollary 6Gssfi 9114
[Enderton] p. 139Theorem 6H(c)mapen 9082
[Enderton] p. 142Theorem 6I(3)xpdjuen 10109
[Enderton] p. 142Theorem 6I(4)mapdjuen 10110
[Enderton] p. 143Theorem 6Jdju0en 10105  dju1en 10101
[Enderton] p. 144Exercise 13iunfi 9270  unifi 9271  unifi2 9272
[Enderton] p. 144Corollary 6Kundif2 4436  unfi 9112  unfi2 9235
[Enderton] p. 145Figure 38ffoss 7904
[Enderton] p. 145Definitiondf-dom 8897
[Enderton] p. 146Example 1domen 8910  domeng 8911
[Enderton] p. 146Example 3nndomo 9158  nnsdom 9583  nnsdomg 9222
[Enderton] p. 149Theorem 6L(a)djudom2 10113
[Enderton] p. 149Theorem 6L(c)mapdom1 9083  xpdom1 9017  xpdom1g 9015  xpdom2g 9014
[Enderton] p. 149Theorem 6L(d)mapdom2 9089
[Enderton] p. 151Theorem 6Mzorn 10436  zorng 10433
[Enderton] p. 151Theorem 6M(4)ac8 10421  dfac5 10058
[Enderton] p. 159Theorem 6Qunictb 10504
[Enderton] p. 164Exampleinfdif 10137
[Enderton] p. 168Definitiondf-po 5539
[Enderton] p. 192Theorem 7M(a)oneli 6436
[Enderton] p. 192Theorem 7M(b)ontr1 6367
[Enderton] p. 192Theorem 7M(c)onirri 6435
[Enderton] p. 193Corollary 7N(b)0elon 6375
[Enderton] p. 193Corollary 7N(c)onsuci 7794
[Enderton] p. 193Corollary 7N(d)ssonunii 7737
[Enderton] p. 194Remarkonprc 7734
[Enderton] p. 194Exercise 16suc11 6429
[Enderton] p. 197Definitiondf-card 9868
[Enderton] p. 197Theorem 7Pcarden 10480
[Enderton] p. 200Exercise 25tfis 7811
[Enderton] p. 202Lemma 7Tr1tr 9705
[Enderton] p. 202Definitiondf-r1 9693
[Enderton] p. 202Theorem 7Qr1val1 9715
[Enderton] p. 204Theorem 7V(b)rankval4 9796
[Enderton] p. 206Theorem 7X(b)en2lp 9535
[Enderton] p. 207Exercise 30rankpr 9786  rankprb 9780  rankpw 9772  rankpwi 9752  rankuniss 9795
[Enderton] p. 207Exercise 34opthreg 9547
[Enderton] p. 208Exercise 35suc11reg 9548
[Enderton] p. 212Definition of alephalephval3 10039
[Enderton] p. 213Theorem 8A(a)alephord2 10005
[Enderton] p. 213Theorem 8A(b)cardalephex 10019
[Enderton] p. 218Theorem Schema 8Eonfununi 8287
[Enderton] p. 222Definition of kardkarden 9824  kardex 9823
[Enderton] p. 238Theorem 8Roeoa 8538
[Enderton] p. 238Theorem 8Soeoe 8540
[Enderton] p. 240Exercise 25oarec 8503
[Enderton] p. 257Definition of cofinalitycflm 10179
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17583
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17525
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18494  mrieqv2d 17580  mrieqvd 17579
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17584
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17589  mreexexlem2d 17586
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18500  mreexfidimd 17591
[Frege1879] p. 11Statementdf3or2 43750
[Frege1879] p. 12Statementdf3an2 43751  dfxor4 43748  dfxor5 43749
[Frege1879] p. 26Axiom 1ax-frege1 43772
[Frege1879] p. 26Axiom 2ax-frege2 43773
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43777
[Frege1879] p. 31Proposition 4frege4 43781
[Frege1879] p. 32Proposition 5frege5 43782
[Frege1879] p. 33Proposition 6frege6 43788
[Frege1879] p. 34Proposition 7frege7 43790
[Frege1879] p. 35Axiom 8ax-frege8 43791  axfrege8 43789
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37426
[Frege1879] p. 35Proposition 9frege9 43794
[Frege1879] p. 36Proposition 10frege10 43802
[Frege1879] p. 36Proposition 11frege11 43796
[Frege1879] p. 37Proposition 12frege12 43795
[Frege1879] p. 37Proposition 13frege13 43804
[Frege1879] p. 37Proposition 14frege14 43805
[Frege1879] p. 38Proposition 15frege15 43808
[Frege1879] p. 38Proposition 16frege16 43798
[Frege1879] p. 39Proposition 17frege17 43803
[Frege1879] p. 39Proposition 18frege18 43800
[Frege1879] p. 39Proposition 19frege19 43806
[Frege1879] p. 40Proposition 20frege20 43810
[Frege1879] p. 40Proposition 21frege21 43809
[Frege1879] p. 41Proposition 22frege22 43801
[Frege1879] p. 42Proposition 23frege23 43807
[Frege1879] p. 42Proposition 24frege24 43797
[Frege1879] p. 42Proposition 25frege25 43799  rp-frege25 43787
[Frege1879] p. 42Proposition 26frege26 43792
[Frege1879] p. 43Axiom 28ax-frege28 43812
[Frege1879] p. 43Proposition 27frege27 43793
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43813
[Frege1879] p. 44Axiom 31ax-frege31 43816  axfrege31 43815
[Frege1879] p. 44Proposition 30frege30 43814
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43817
[Frege1879] p. 44Proposition 33frege33 43818
[Frege1879] p. 45Proposition 34frege34 43819
[Frege1879] p. 45Proposition 35frege35 43820
[Frege1879] p. 45Proposition 36frege36 43821
[Frege1879] p. 46Proposition 37frege37 43822
[Frege1879] p. 46Proposition 38frege38 43823
[Frege1879] p. 46Proposition 39frege39 43824
[Frege1879] p. 46Proposition 40frege40 43825
[Frege1879] p. 47Axiom 41ax-frege41 43827  axfrege41 43826
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43828
[Frege1879] p. 47Proposition 43frege43 43829
[Frege1879] p. 47Proposition 44frege44 43830
[Frege1879] p. 47Proposition 45frege45 43831
[Frege1879] p. 48Proposition 46frege46 43832
[Frege1879] p. 48Proposition 47frege47 43833
[Frege1879] p. 49Proposition 48frege48 43834
[Frege1879] p. 49Proposition 49frege49 43835
[Frege1879] p. 49Proposition 50frege50 43836
[Frege1879] p. 50Axiom 52ax-frege52a 43839  ax-frege52c 43870  frege52aid 43840  frege52b 43871
[Frege1879] p. 50Axiom 54ax-frege54a 43844  ax-frege54c 43874  frege54b 43875
[Frege1879] p. 50Proposition 51frege51 43837
[Frege1879] p. 50Proposition 52dfsbcq 3752
[Frege1879] p. 50Proposition 53frege53a 43842  frege53aid 43841  frege53b 43872  frege53c 43896
[Frege1879] p. 50Proposition 54biid 261  eqid 2729
[Frege1879] p. 50Proposition 55frege55a 43850  frege55aid 43847  frege55b 43879  frege55c 43900  frege55cor1a 43851  frege55lem2a 43849  frege55lem2b 43878  frege55lem2c 43899
[Frege1879] p. 50Proposition 56frege56a 43853  frege56aid 43852  frege56b 43880  frege56c 43901
[Frege1879] p. 51Axiom 58ax-frege58a 43857  ax-frege58b 43883  frege58bid 43884  frege58c 43903
[Frege1879] p. 51Proposition 57frege57a 43855  frege57aid 43854  frege57b 43881  frege57c 43902
[Frege1879] p. 51Proposition 58spsbc 3763
[Frege1879] p. 51Proposition 59frege59a 43859  frege59b 43886  frege59c 43904
[Frege1879] p. 52Proposition 60frege60a 43860  frege60b 43887  frege60c 43905
[Frege1879] p. 52Proposition 61frege61a 43861  frege61b 43888  frege61c 43906
[Frege1879] p. 52Proposition 62frege62a 43862  frege62b 43889  frege62c 43907
[Frege1879] p. 52Proposition 63frege63a 43863  frege63b 43890  frege63c 43908
[Frege1879] p. 53Proposition 64frege64a 43864  frege64b 43891  frege64c 43909
[Frege1879] p. 53Proposition 65frege65a 43865  frege65b 43892  frege65c 43910
[Frege1879] p. 54Proposition 66frege66a 43866  frege66b 43893  frege66c 43911
[Frege1879] p. 54Proposition 67frege67a 43867  frege67b 43894  frege67c 43912
[Frege1879] p. 54Proposition 68frege68a 43868  frege68b 43895  frege68c 43913
[Frege1879] p. 55Definition 69dffrege69 43914
[Frege1879] p. 58Proposition 70frege70 43915
[Frege1879] p. 59Proposition 71frege71 43916
[Frege1879] p. 59Proposition 72frege72 43917
[Frege1879] p. 59Proposition 73frege73 43918
[Frege1879] p. 60Definition 76dffrege76 43921
[Frege1879] p. 60Proposition 74frege74 43919
[Frege1879] p. 60Proposition 75frege75 43920
[Frege1879] p. 62Proposition 77frege77 43922  frege77d 43728
[Frege1879] p. 63Proposition 78frege78 43923
[Frege1879] p. 63Proposition 79frege79 43924
[Frege1879] p. 63Proposition 80frege80 43925
[Frege1879] p. 63Proposition 81frege81 43926  frege81d 43729
[Frege1879] p. 64Proposition 82frege82 43927
[Frege1879] p. 65Proposition 83frege83 43928  frege83d 43730
[Frege1879] p. 65Proposition 84frege84 43929
[Frege1879] p. 66Proposition 85frege85 43930
[Frege1879] p. 66Proposition 86frege86 43931
[Frege1879] p. 66Proposition 87frege87 43932  frege87d 43732
[Frege1879] p. 67Proposition 88frege88 43933
[Frege1879] p. 68Proposition 89frege89 43934
[Frege1879] p. 68Proposition 90frege90 43935
[Frege1879] p. 68Proposition 91frege91 43936  frege91d 43733
[Frege1879] p. 69Proposition 92frege92 43937
[Frege1879] p. 70Proposition 93frege93 43938
[Frege1879] p. 70Proposition 94frege94 43939
[Frege1879] p. 70Proposition 95frege95 43940
[Frege1879] p. 71Definition 99dffrege99 43944
[Frege1879] p. 71Proposition 96frege96 43941  frege96d 43731
[Frege1879] p. 71Proposition 97frege97 43942  frege97d 43734
[Frege1879] p. 71Proposition 98frege98 43943  frege98d 43735
[Frege1879] p. 72Proposition 100frege100 43945
[Frege1879] p. 72Proposition 101frege101 43946
[Frege1879] p. 72Proposition 102frege102 43947  frege102d 43736
[Frege1879] p. 73Proposition 103frege103 43948
[Frege1879] p. 73Proposition 104frege104 43949
[Frege1879] p. 73Proposition 105frege105 43950
[Frege1879] p. 73Proposition 106frege106 43951  frege106d 43737
[Frege1879] p. 74Proposition 107frege107 43952
[Frege1879] p. 74Proposition 108frege108 43953  frege108d 43738
[Frege1879] p. 74Proposition 109frege109 43954  frege109d 43739
[Frege1879] p. 75Proposition 110frege110 43955
[Frege1879] p. 75Proposition 111frege111 43956  frege111d 43741
[Frege1879] p. 76Proposition 112frege112 43957
[Frege1879] p. 76Proposition 113frege113 43958
[Frege1879] p. 76Proposition 114frege114 43959  frege114d 43740
[Frege1879] p. 77Definition 115dffrege115 43960
[Frege1879] p. 77Proposition 116frege116 43961
[Frege1879] p. 78Proposition 117frege117 43962
[Frege1879] p. 78Proposition 118frege118 43963
[Frege1879] p. 78Proposition 119frege119 43964
[Frege1879] p. 78Proposition 120frege120 43965
[Frege1879] p. 79Proposition 121frege121 43966
[Frege1879] p. 79Proposition 122frege122 43967  frege122d 43742
[Frege1879] p. 79Proposition 123frege123 43968
[Frege1879] p. 80Proposition 124frege124 43969  frege124d 43743
[Frege1879] p. 81Proposition 125frege125 43970
[Frege1879] p. 81Proposition 126frege126 43971  frege126d 43744
[Frege1879] p. 82Proposition 127frege127 43972
[Frege1879] p. 83Proposition 128frege128 43973
[Frege1879] p. 83Proposition 129frege129 43974  frege129d 43745
[Frege1879] p. 84Proposition 130frege130 43975
[Frege1879] p. 85Proposition 131frege131 43976  frege131d 43746
[Frege1879] p. 86Proposition 132frege132 43977
[Frege1879] p. 86Proposition 133frege133 43978  frege133d 43747
[Fremlin1] p. 13Definition 111G (b)df-salgen 46304
[Fremlin1] p. 13Definition 111G (d)borelmbl 46627
[Fremlin1] p. 13Proposition 111G (b)salgenss 46327
[Fremlin1] p. 14Definition 112Aismea 46442
[Fremlin1] p. 15Remark 112B (d)psmeasure 46462
[Fremlin1] p. 15Property 112C (a)meadjun 46453  meadjunre 46467
[Fremlin1] p. 15Property 112C (b)meassle 46454
[Fremlin1] p. 15Property 112C (c)meaunle 46455
[Fremlin1] p. 16Property 112C (d)iundjiun 46451  meaiunle 46460  meaiunlelem 46459
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46472  meaiuninc2 46473  meaiuninc3 46476  meaiuninc3v 46475  meaiunincf 46474  meaiuninclem 46471
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46478  meaiininc2 46479  meaiininclem 46477
[Fremlin1] p. 19Theorem 113Ccaragen0 46497  caragendifcl 46505  caratheodory 46519  omelesplit 46509
[Fremlin1] p. 19Definition 113Aisome 46485  isomennd 46522  isomenndlem 46521
[Fremlin1] p. 19Remark 113B (c)omeunle 46507
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46526  voncmpl 46612
[Fremlin1] p. 19Definition 113A (ii)omessle 46489
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46514  carageniuncllem1 46512  carageniuncllem2 46513  caragenuncl 46504  caragenuncllem 46503  caragenunicl 46515
[Fremlin1] p. 21Remark 113Dcaragenel2d 46523
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46517  caratheodorylem2 46518
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46526
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46585  hoidmv1lelem1 46582  hoidmv1lelem2 46583  hoidmv1lelem3 46584
[Fremlin1] p. 25Definition 114Eisvonmbl 46629
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46585  hoidmvle 46591  hoidmvlelem1 46586  hoidmvlelem2 46587  hoidmvlelem3 46588  hoidmvlelem4 46589  hoidmvlelem5 46590  hsphoidmvle2 46576  hsphoif 46567  hsphoival 46570
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46539
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46547
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46574  hoidmvn0val 46575  hoidmvval 46568  hoidmvval0 46578  hoidmvval0b 46581
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46579  hsphoidmvle 46577
[Fremlin1] p. 30Definition 115Cdf-ovoln 46528  df-voln 46530
[Fremlin1] p. 30Proposition 115D (a)dmovn 46595  ovn0 46557  ovn0lem 46556  ovnf 46554  ovnome 46564  ovnssle 46552  ovnsslelem 46551  ovnsupge0 46548
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46594  ovnhoilem1 46592  ovnhoilem2 46593  vonhoi 46658
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46611  hoidifhspf 46609  hoidifhspval 46599  hoidifhspval2 46606  hoidifhspval3 46610  hspmbl 46620  hspmbllem1 46617  hspmbllem2 46618  hspmbllem3 46619
[Fremlin1] p. 31Definition 115Evoncmpl 46612  vonmea 46565
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46563  ovnsubadd2 46637  ovnsubadd2lem 46636  ovnsubaddlem1 46561  ovnsubaddlem2 46562
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46622  hoimbl2 46656  hoimbllem 46621  hspdifhsp 46607  opnvonmbl 46625  opnvonmbllem2 46624
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46627
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46670  iccvonmbllem 46669  ioovonmbl 46668
[Fremlin1] p. 32Proposition 115G (d)vonicc 46676  vonicclem2 46675  vonioo 46673  vonioolem2 46672  vonn0icc 46679  vonn0icc2 46683  vonn0ioo 46678  vonn0ioo2 46681
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46680  snvonmbl 46677  vonct 46684  vonsn 46682
[Fremlin1] p. 35Lemma 121Asubsalsal 46350
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46349  subsaliuncllem 46348
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46716  salpreimalegt 46700  salpreimaltle 46717
[Fremlin1] p. 35Proposition 121B (i)issmf 46719  issmff 46725  issmflem 46718
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46736  issmflelem 46735  smfpreimale 46745
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46747  issmfgtlem 46746
[Fremlin1] p. 36Definition 121Cdf-smblfn 46687  issmf 46719  issmff 46725  issmfge 46761  issmfgelem 46760  issmfgt 46747  issmfgtlem 46746  issmfle 46736  issmflelem 46735  issmflem 46718
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46698  salpreimagtlt 46721  salpreimalelt 46720
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46761  issmfgelem 46760
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46744
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46742  cnfsmf 46731
[Fremlin1] p. 36Proposition 121D (c)decsmf 46758  decsmflem 46757  incsmf 46733  incsmflem 46732
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46692  pimconstlt1 46693  smfconst 46740
[Fremlin1] p. 37Proposition 121E (b)smfadd 46756  smfaddlem1 46754  smfaddlem2 46755
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46787
[Fremlin1] p. 37Proposition 121E (d)smfmul 46786  smfmullem1 46782  smfmullem2 46783  smfmullem3 46784  smfmullem4 46785
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46788
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46791  smfpimbor1lem2 46790
[Fremlin1] p. 37Proposition 121E (g)smfco 46793
[Fremlin1] p. 37Proposition 121E (h)smfres 46781
[Fremlin1] p. 38Proposition 121E (e)smfrec 46780
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46789  smfresal 46779
[Fremlin1] p. 38Proposition 121F (a)smflim 46768  smflim2 46797  smflimlem1 46762  smflimlem2 46763  smflimlem3 46764  smflimlem4 46765  smflimlem5 46766  smflimlem6 46767  smflimmpt 46801
[Fremlin1] p. 38Proposition 121F (b)smfsup 46805  smfsuplem1 46802  smfsuplem2 46803  smfsuplem3 46804  smfsupmpt 46806  smfsupxr 46807
[Fremlin1] p. 38Proposition 121F (c)smfinf 46809  smfinflem 46808  smfinfmpt 46810
[Fremlin1] p. 39Remark 121Gsmflim 46768  smflim2 46797  smflimmpt 46801
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46799
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46829  smfdivdmmbl2 46832  smfinfdmmbl 46840  smfinfdmmbllem 46839  smfsupdmmbl 46836  smfsupdmmbllem 46835
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46819  smflimsuplem2 46812  smflimsuplem6 46816  smflimsuplem7 46817  smflimsuplem8 46818  smflimsupmpt 46820
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46822  smfliminflem 46821  smfliminfmpt 46823
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46687
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46833  fsupdm2 46834
[Fremlin1], p. 39Proposition 121Hadddmmbl 46824  adddmmbl2 46825  finfdm 46837  finfdm2 46838  fsupdm 46833  fsupdm2 46834  muldmmbl 46826  muldmmbl2 46827
[Fremlin1], p. 39Proposition 121F (c)finfdm 46837  finfdm2 46838
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25470
[Fremlin5] p. 213Lemma 565Cauniioovol 25513
[Fremlin5] p. 214Lemma 565Cauniioombl 25523
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37685
[Fremlin5] p. 220Theorem 565Maftc1anc 37688
[FreydScedrov] p. 283Axiom of Infinityax-inf 9567  inf1 9551  inf2 9552
[Gleason] p. 117Proposition 9-2.1df-enq 10840  enqer 10850
[Gleason] p. 117Proposition 9-2.2df-1nq 10845  df-nq 10841
[Gleason] p. 117Proposition 9-2.3df-plpq 10837  df-plq 10843
[Gleason] p. 119Proposition 9-2.4caovmo 7606  df-mpq 10838  df-mq 10844
[Gleason] p. 119Proposition 9-2.5df-rq 10846
[Gleason] p. 119Proposition 9-2.6ltexnq 10904
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10905  ltbtwnnq 10907
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10900
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10901
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10908
[Gleason] p. 121Definition 9-3.1df-np 10910
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10922
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10924
[Gleason] p. 122Definitiondf-1p 10911
[Gleason] p. 122Remark (1)prub 10923
[Gleason] p. 122Lemma 9-3.4prlem934 10962
[Gleason] p. 122Proposition 9-3.2df-ltp 10914
[Gleason] p. 122Proposition 9-3.3ltsopr 10961  psslinpr 10960  supexpr 10983  suplem1pr 10981  suplem2pr 10982
[Gleason] p. 123Proposition 9-3.5addclpr 10947  addclprlem1 10945  addclprlem2 10946  df-plp 10912
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10951
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10950
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10963
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10972  ltexprlem1 10965  ltexprlem2 10966  ltexprlem3 10967  ltexprlem4 10968  ltexprlem5 10969  ltexprlem6 10970  ltexprlem7 10971
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10974  ltaprlem 10973
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10975
[Gleason] p. 124Lemma 9-3.6prlem936 10976
[Gleason] p. 124Proposition 9-3.7df-mp 10913  mulclpr 10949  mulclprlem 10948  reclem2pr 10977
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10958
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10953
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10952
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10957
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10980  reclem3pr 10978  reclem4pr 10979
[Gleason] p. 126Proposition 9-4.1df-enr 10984  enrer 10992
[Gleason] p. 126Proposition 9-4.2df-0r 10989  df-1r 10990  df-nr 10985
[Gleason] p. 126Proposition 9-4.3df-mr 10987  df-plr 10986  negexsr 11031  recexsr 11036  recexsrlem 11032
[Gleason] p. 127Proposition 9-4.4df-ltr 10988
[Gleason] p. 130Proposition 10-1.3creui 12157  creur 12156  cru 12154
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11117  axcnre 11093
[Gleason] p. 132Definition 10-3.1crim 15057  crimd 15174  crimi 15135  crre 15056  crred 15173  crrei 15134
[Gleason] p. 132Definition 10-3.2remim 15059  remimd 15140
[Gleason] p. 133Definition 10.36absval2 15226  absval2d 15390  absval2i 15340
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15083  cjaddd 15162  cjaddi 15130
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15084  cjmuld 15163  cjmuli 15131
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15082  cjcjd 15141  cjcji 15113
[Gleason] p. 133Proposition 10-3.4(f)cjre 15081  cjreb 15065  cjrebd 15144  cjrebi 15116  cjred 15168  rere 15064  rereb 15062  rerebd 15143  rerebi 15115  rered 15166
[Gleason] p. 133Proposition 10-3.4(h)addcj 15090  addcjd 15154  addcji 15125
[Gleason] p. 133Proposition 10-3.7(a)absval 15180
[Gleason] p. 133Proposition 10-3.7(b)abscj 15221  abscjd 15395  abscji 15344
[Gleason] p. 133Proposition 10-3.7(c)abs00 15231  abs00d 15391  abs00i 15341  absne0d 15392
[Gleason] p. 133Proposition 10-3.7(d)releabs 15264  releabsd 15396  releabsi 15345
[Gleason] p. 133Proposition 10-3.7(f)absmul 15236  absmuld 15399  absmuli 15347
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15224  sqabsaddi 15348
[Gleason] p. 133Proposition 10-3.7(h)abstri 15273  abstrid 15401  abstrii 15351
[Gleason] p. 134Definition 10-4.1df-exp 14003  exp0 14006  expp1 14009  expp1d 14088
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26621  cxpaddd 26659  expadd 14045  expaddd 14089  expaddz 14047
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26630  cxpmuld 26679  expmul 14048  expmuld 14090  expmulz 14049
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26627  mulcxpd 26670  mulexp 14042  mulexpd 14102  mulexpz 14043
[Gleason] p. 140Exercise 1znnen 16156
[Gleason] p. 141Definition 11-2.1fzval 13446
[Gleason] p. 168Proposition 12-2.1(a)climadd 15574  rlimadd 15585  rlimdiv 15588
[Gleason] p. 168Proposition 12-2.1(b)climsub 15576  rlimsub 15586
[Gleason] p. 168Proposition 12-2.1(c)climmul 15575  rlimmul 15587
[Gleason] p. 171Corollary 12-2.2climmulc2 15579
[Gleason] p. 172Corollary 12-2.5climrecl 15525
[Gleason] p. 172Proposition 12-2.4(c)climabs 15546  climcj 15547  climim 15549  climre 15548  rlimabs 15551  rlimcj 15552  rlimim 15554  rlimre 15553
[Gleason] p. 173Definition 12-3.1df-ltxr 11189  df-xr 11188  ltxr 13051
[Gleason] p. 175Definition 12-4.1df-limsup 15413  limsupval 15416
[Gleason] p. 180Theorem 12-5.1climsup 15612
[Gleason] p. 180Theorem 12-5.3caucvg 15621  caucvgb 15622  caucvgbf 45478  caucvgr 15618  climcau 15613
[Gleason] p. 182Exercise 3cvgcmp 15758
[Gleason] p. 182Exercise 4cvgrat 15825
[Gleason] p. 195Theorem 13-2.12abs1m 15278
[Gleason] p. 217Lemma 13-4.1btwnzge0 13766
[Gleason] p. 223Definition 14-1.1df-met 21290
[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 23568
[Gleason] p. 240Theorem 14-4.3metcnp4 25243
[Gleason] p. 240Proposition 14-4.2metcnp3 24461
[Gleason] p. 243Proposition 14-4.16addcn 24787  addcn2 15536  mulcn 24789  mulcn2 15538  subcn 24788  subcn2 15537
[Gleason] p. 295Remarkbcval3 14247  bcval4 14248
[Gleason] p. 295Equation 2bcpasc 14262
[Gleason] p. 295Definition of binomial coefficientbcval 14245  df-bc 14244
[Gleason] p. 296Remarkbcn0 14251  bcnn 14253
[Gleason] p. 296Theorem 15-2.8binom 15772
[Gleason] p. 308Equation 2ef0 16033
[Gleason] p. 308Equation 3efcj 16034
[Gleason] p. 309Corollary 15-4.3efne0 16040
[Gleason] p. 309Corollary 15-4.4efexp 16045
[Gleason] p. 310Equation 14sinadd 16108
[Gleason] p. 310Equation 15cosadd 16109
[Gleason] p. 311Equation 17sincossq 16120
[Gleason] p. 311Equation 18cosbnd 16125  sinbnd 16124
[Gleason] p. 311Lemma 15-4.7sqeqor 14157  sqeqori 14155
[Gleason] p. 311Definition of ` `df-pi 16014
[Godowski] p. 730Equation SFgoeqi 32252
[GodowskiGreechie] p. 249Equation IV3oai 31647
[Golan] p. 1Remarksrgisid 20129
[Golan] p. 1Definitiondf-srg 20107
[Golan] p. 149Definitiondf-slmd 33170
[Gonshor] p. 7Definitiondf-scut 27729
[Gonshor] p. 9Theorem 2.5slerec 27765  slerecd 27766
[Gonshor] p. 10Theorem 2.6cofcut1 27868  cofcut1d 27869
[Gonshor] p. 10Theorem 2.7cofcut2 27870  cofcut2d 27871
[Gonshor] p. 12Theorem 2.9cofcutr 27872  cofcutr1d 27873  cofcutr2d 27874
[Gonshor] p. 13Definitiondf-adds 27907
[Gonshor] p. 14Theorem 3.1addsprop 27923
[Gonshor] p. 15Theorem 3.2addsunif 27949
[Gonshor] p. 17Theorem 3.4mulsprop 28073
[Gonshor] p. 18Theorem 3.5mulsunif 28093
[Gonshor] p. 28Lemma 4.2halfcut 28381
[Gonshor] p. 28Theorem 4.2pw2cut 28383
[Gonshor] p. 30Theorem 4.2addhalfcut 28382
[Gonshor] p. 95Theorem 6.1addsbday 27964
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36140
[Gratzer] p. 23Section 0.6df-mre 17523
[Gratzer] p. 27Section 0.6df-mri 17525
[Hall] p. 1Section 1.1df-asslaw 48169  df-cllaw 48167  df-comlaw 48168
[Hall] p. 2Section 1.2df-clintop 48181
[Hall] p. 7Section 1.3df-sgrp2 48202
[Halmos] p. 28Partition ` `df-parts 38750  dfmembpart2 38755
[Halmos] p. 31Theorem 17.3riesz1 32044  riesz2 32045
[Halmos] p. 41Definition of Hermitianhmopadj2 31920
[Halmos] p. 42Definition of projector orderingpjordi 32152
[Halmos] p. 43Theorem 26.1elpjhmop 32164  elpjidm 32163  pjnmopi 32127
[Halmos] p. 44Remarkpjinormi 31666  pjinormii 31655
[Halmos] p. 44Theorem 26.2elpjch 32168  pjrn 31686  pjrni 31681  pjvec 31675
[Halmos] p. 44Theorem 26.3pjnorm2 31706
[Halmos] p. 44Theorem 26.4hmopidmpj 32133  hmopidmpji 32131
[Halmos] p. 45Theorem 27.1pjinvari 32170
[Halmos] p. 45Theorem 27.3pjoci 32159  pjocvec 31676
[Halmos] p. 45Theorem 27.4pjorthcoi 32148
[Halmos] p. 48Theorem 29.2pjssposi 32151
[Halmos] p. 48Theorem 29.3pjssdif1i 32154  pjssdif2i 32153
[Halmos] p. 50Definition of spectrumdf-spec 31834
[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 1795
[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 22410  df-dmatalt 48380
[Helfgott] p. 2Theoremtgoldbach 47811
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47796
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47808  bgoldbtbnd 47803  bgoldbtbnd 47803  tgblthelfgott 47809
[Helfgott] p. 5Proposition 1.1circlevma 34626
[Helfgott] p. 69Statement 7.49circlemethhgt 34627
[Helfgott] p. 69Statement 7.50hgt750lema 34641  hgt750lemb 34640  hgt750leme 34642  hgt750lemf 34637  hgt750lemg 34638
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47805  tgoldbachgt 34647  tgoldbachgtALTV 47806  tgoldbachgtd 34646
[Helfgott] p. 70Statement 7.49ax-hgt749 34628
[Herstein] p. 54Exercise 28df-grpo 30472
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18858  grpoideu 30488  mndideu 18654
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18888  grpoinveu 30498
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18919  grpo2inv 30510
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18932  grpoinvop 30512
[Herstein] p. 57Exercise 1dfgrp3e 18954
[Hitchcock] p. 5Rule A3mptnan 1768
[Hitchcock] p. 5Rule A4mptxor 1769
[Hitchcock] p. 5Rule A5mtpxor 1771
[Holland] p. 1519Theorem 2sumdmdi 32399
[Holland] p. 1520Lemma 5cdj1i 32412  cdj3i 32420  cdj3lem1 32413  cdjreui 32411
[Holland] p. 1524Lemma 7mddmdin0i 32410
[Holland95] p. 13Theorem 3.6hlathil 41948
[Holland95] p. 14Line 15hgmapvs 41878
[Holland95] p. 14Line 16hdmaplkr 41900
[Holland95] p. 14Line 17hdmapellkr 41901
[Holland95] p. 14Line 19hdmapglnm2 41898
[Holland95] p. 14Line 20hdmapip0com 41904
[Holland95] p. 14Theorem 3.6hdmapevec2 41823
[Holland95] p. 14Lines 24 and 25hdmapoc 41918
[Holland95] p. 204Definition of involutiondf-srng 20760
[Holland95] p. 212Definition of subspacedf-psubsp 39490
[Holland95] p. 214Lemma 3.3lclkrlem2v 41515
[Holland95] p. 214Definition 3.2df-lpolN 41468
[Holland95] p. 214Definition of nonsingularpnonsingN 39920
[Holland95] p. 215Lemma 3.3(1)dihoml4 41364  poml4N 39940
[Holland95] p. 215Lemma 3.3(2)dochexmid 41455  pexmidALTN 39965  pexmidN 39956
[Holland95] p. 218Theorem 3.6lclkr 41520
[Holland95] p. 218Definition of dual vector spacedf-ldual 39110  ldualset 39111
[Holland95] p. 222Item 1df-lines 39488  df-pointsN 39489
[Holland95] p. 222Item 2df-polarityN 39890
[Holland95] p. 223Remarkispsubcl2N 39934  omllaw4 39232  pol1N 39897  polcon3N 39904
[Holland95] p. 223Definitiondf-psubclN 39922
[Holland95] p. 223Equation for polaritypolval2N 39893
[Holmes] p. 40Definitiondf-xrn 38346
[Hughes] p. 44Equation 1.21bax-his3 31063
[Hughes] p. 47Definition of projection operatordfpjop 32161
[Hughes] p. 49Equation 1.30eighmre 31942  eigre 31814  eigrei 31813
[Hughes] p. 49Equation 1.31eighmorth 31943  eigorth 31817  eigorthi 31816
[Hughes] p. 137Remark (ii)eigposi 31815
[Huneke] p. 1Claim 1frgrncvvdeq 30288
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30284
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30285
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30286
[Huneke] p. 2Claim 2frgrregorufr 30304  frgrregorufr0 30303  frgrregorufrg 30305
[Huneke] p. 2Claim 3frgrhash2wsp 30311  frrusgrord 30320  frrusgrord0 30319
[Huneke] p. 2Statementdf-clwwlknon 30067
[Huneke] p. 2Statement 4frgrwopreglem4 30294
[Huneke] p. 2Statement 5frgrwopreg1 30297  frgrwopreg2 30298  frgrwopregasn 30295  frgrwopregbsn 30296
[Huneke] p. 2Statement 6frgrwopreglem5 30300
[Huneke] p. 2Statement 7fusgreghash2wspv 30314
[Huneke] p. 2Statement 8fusgreghash2wsp 30317
[Huneke] p. 2Statement 9clwlksndivn 30065  numclwlk1 30350  numclwlk1lem1 30348  numclwlk1lem2 30349  numclwwlk1 30340  numclwwlk8 30371
[Huneke] p. 2Definition 3frgrwopreglem1 30291
[Huneke] p. 2Definition 4df-clwlks 29751
[Huneke] p. 2Definition 62clwwlk 30326
[Huneke] p. 2Definition 7numclwwlkovh 30352  numclwwlkovh0 30351
[Huneke] p. 2Statement 10numclwwlk2 30360
[Huneke] p. 2Statement 11rusgrnumwlkg 29957
[Huneke] p. 2Statement 12numclwwlk3 30364
[Huneke] p. 2Statement 13numclwwlk5 30367
[Huneke] p. 2Statement 14numclwwlk7 30370
[Indrzejczak] p. 33Definition ` `Enatded 30382  natded 30382
[Indrzejczak] p. 33Definition ` `Inatded 30382
[Indrzejczak] p. 34Definition ` `Enatded 30382  natded 30382
[Indrzejczak] p. 34Definition ` `Inatded 30382
[Jech] p. 4Definition of classcv 1539  cvjust 2723
[Jech] p. 42Lemma 6.1alephexp1 10508
[Jech] p. 42Equation 6.1alephadd 10506  alephmul 10507
[Jech] p. 43Lemma 6.2infmap 10505  infmap2 10146
[Jech] p. 71Lemma 9.3jech9.3 9743
[Jech] p. 72Equation 9.3scott0 9815  scottex 9814
[Jech] p. 72Exercise 9.1rankval4 9796
[Jech] p. 72Scheme "Collection Principle"cp 9820
[Jech] p. 78Noteopthprc 5695
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42897
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 42985
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 42986
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42909
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42913
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42914  rmyp1 42915
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42916  rmym1 42917
[JonesMatijasevic] p. 695Equation 2.11rmx0 42907  rmx1 42908  rmxluc 42918
[JonesMatijasevic] p. 695Equation 2.12rmy0 42911  rmy1 42912  rmyluc 42919
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42921
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42922
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42942  jm2.17b 42943  jm2.17c 42944
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 42975
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 42979
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 42970
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42945  jm2.24nn 42941
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 42984
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 42990  rmygeid 42946
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43002
[Juillerat] p. 11Section *5etransc 46274  etransclem47 46272  etransclem48 46273
[Juillerat] p. 12Equation (7)etransclem44 46269
[Juillerat] p. 12Equation *(7)etransclem46 46271
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46257
[Juillerat] p. 13Proofetransclem35 46260
[Juillerat] p. 13Part of case 2 proven inetransclem38 46263
[Juillerat] p. 13Part of case 2 provenetransclem24 46249
[Juillerat] p. 13Part of case 2: proven inetransclem41 46266
[Juillerat] p. 14Proofetransclem23 46248
[KalishMontague] p. 81Note 1ax-6 1967
[KalishMontague] p. 85Lemma 2equid 2012
[KalishMontague] p. 85Lemma 3equcomi 2017
[KalishMontague] p. 86Lemma 7cbvalivw 2007  cbvaliw 2006  wl-cbvmotv 37494  wl-motae 37496  wl-moteq 37495
[KalishMontague] p. 87Lemma 8spimvw 1986  spimw 1970
[KalishMontague] p. 87Lemma 9spfw 2033  spw 2034
[Kalmbach] p. 14Definition of latticechabs1 31495  chabs1i 31497  chabs2 31496  chabs2i 31498  chjass 31512  chjassi 31465  latabs1 18416  latabs2 18417
[Kalmbach] p. 15Definition of atomdf-at 32317  ela 32318
[Kalmbach] p. 15Definition of coverscvbr2 32262  cvrval2 39260
[Kalmbach] p. 16Definitiondf-ol 39164  df-oml 39165
[Kalmbach] p. 20Definition of commutescmbr 31563  cmbri 31569  cmtvalN 39197  df-cm 31562  df-cmtN 39163
[Kalmbach] p. 22Remarkomllaw5N 39233  pjoml5 31592  pjoml5i 31567
[Kalmbach] p. 22Definitionpjoml2 31590  pjoml2i 31564
[Kalmbach] p. 22Theorem 2(v)cmcm 31593  cmcmi 31571  cmcmii 31576  cmtcomN 39235
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39231  omlsi 31383  pjoml 31415  pjomli 31414
[Kalmbach] p. 22Definition of OML lawomllaw2N 39230
[Kalmbach] p. 23Remarkcmbr2i 31575  cmcm3 31594  cmcm3i 31573  cmcm3ii 31578  cmcm4i 31574  cmt3N 39237  cmt4N 39238  cmtbr2N 39239
[Kalmbach] p. 23Lemma 3cmbr3 31587  cmbr3i 31579  cmtbr3N 39240
[Kalmbach] p. 25Theorem 5fh1 31597  fh1i 31600  fh2 31598  fh2i 31601  omlfh1N 39244
[Kalmbach] p. 65Remarkchjatom 32336  chslej 31477  chsleji 31437  shslej 31359  shsleji 31349
[Kalmbach] p. 65Proposition 1chocin 31474  chocini 31433  chsupcl 31319  chsupval2 31389  h0elch 31234  helch 31222  hsupval2 31388  ocin 31275  ococss 31272  shococss 31273
[Kalmbach] p. 65Definition of subspace sumshsval 31291
[Kalmbach] p. 66Remarkdf-pjh 31374  pjssmi 32144  pjssmii 31660
[Kalmbach] p. 67Lemma 3osum 31624  osumi 31621
[Kalmbach] p. 67Lemma 4pjci 32179
[Kalmbach] p. 103Exercise 6atmd2 32379
[Kalmbach] p. 103Exercise 12mdsl0 32289
[Kalmbach] p. 140Remarkhatomic 32339  hatomici 32338  hatomistici 32341
[Kalmbach] p. 140Proposition 1atlatmstc 39305
[Kalmbach] p. 140Proposition 1(i)atexch 32360  lsatexch 39029
[Kalmbach] p. 140Proposition 1(ii)chcv1 32334  cvlcvr1 39325  cvr1 39397
[Kalmbach] p. 140Proposition 1(iii)cvexch 32353  cvexchi 32348  cvrexch 39407
[Kalmbach] p. 149Remark 2chrelati 32343  hlrelat 39389  hlrelat5N 39388  lrelat 39000
[Kalmbach] p. 153Exercise 5lsmcv 21083  lsmsatcv 38996  spansncv 31632  spansncvi 31631
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39015  spansncv2 32272
[Kalmbach] p. 266Definitiondf-st 32190
[Kalmbach2] p. 8Definition of adjointdf-adjh 31828
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10575  fpwwe2 10572
[KanamoriPincus] p. 416Corollary 1.3canth4 10576
[KanamoriPincus] p. 417Corollary 1.6canthp1 10583
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10578
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10580
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10593
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10597  gchxpidm 10598
[KanamoriPincus] p. 419Theorem 2.1gchacg 10609  gchhar 10608
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10144  unxpwdom 9518
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10599
[Kreyszig] p. 3Property M1metcl 24253  xmetcl 24252
[Kreyszig] p. 4Property M2meteq0 24260
[Kreyszig] p. 8Definition 1.1-8dscmet 24493
[Kreyszig] p. 12Equation 5conjmul 11875  muleqadd 11798
[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 23178  lmmbr 25191  lmmbr2 25192
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23300
[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 23381  metelcls 25238
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25239  metcld2 25240
[Kreyszig] p. 51Equation 2clmvneg1 25032  lmodvneg1 20843  nvinv 30618  vcm 30555
[Kreyszig] p. 51Equation 1aclm0vs 25028  lmod0vs 20833  slmd0vs 33193  vc0 30553
[Kreyszig] p. 51Equation 1blmodvs0 20834  slmdvs0 33194  vcz 30554
[Kreyszig] p. 58Definition 2.2-1imsmet 30670  ngpmet 24524  nrmmetd 24495
[Kreyszig] p. 59Equation 1imsdval 30665  imsdval2 30666  ncvspds 25094  ngpds 24525
[Kreyszig] p. 63Problem 1nmval 24510  nvnd 30667
[Kreyszig] p. 64Problem 2nmeq0 24539  nmge0 24538  nvge0 30652  nvz 30648
[Kreyszig] p. 64Problem 3nmrtri 24545  nvabs 30651
[Kreyszig] p. 91Definition 2.7-1isblo3i 30780
[Kreyszig] p. 92Equation 2df-nmoo 30724
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30786  blocni 30784
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30785
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25137  ipeq0 21580  ipz 30698
[Kreyszig] p. 135Problem 2cphpyth 25149  pythi 30829
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30833
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25171
[Kreyszig] p. 144Equation 4supcvg 15798
[Kreyszig] p. 144Theorem 3.3-1minvec 25369  minveco 30863
[Kreyszig] p. 196Definition 3.9-1df-aj 30729
[Kreyszig] p. 247Theorem 4.7-2bcth 25262
[Kreyszig] p. 249Theorem 4.7-3ubth 30852
[Kreyszig] p. 470Definition of positive operator orderingleop 32102  leopg 32101
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32120
[Kreyszig] p. 525Theorem 10.1-1htth 30897
[Kulpa] p. 547Theorempoimir 37640
[Kulpa] p. 547Equation (1)poimirlem32 37639
[Kulpa] p. 547Equation (2)poimirlem31 37638
[Kulpa] p. 548Theorembroucube 37641
[Kulpa] p. 548Equation (6)poimirlem26 37633
[Kulpa] p. 548Equation (7)poimirlem27 37634
[Kunen] p. 10Axiom 0ax6e 2381  axnul 5255
[Kunen] p. 11Axiom 3axnul 5255
[Kunen] p. 12Axiom 6zfrep6 7913
[Kunen] p. 24Definition 10.24mapval 8788  mapvalg 8786
[Kunen] p. 30Lemma 10.20fodomg 10451
[Kunen] p. 31Definition 10.24mapex 7897
[Kunen] p. 95Definition 2.1df-r1 9693
[Kunen] p. 97Lemma 2.10r1elss 9735  r1elssi 9734
[Kunen] p. 107Exercise 4rankop 9787  rankopb 9781  rankuni 9792  rankxplim 9808  rankxpsuc 9811
[Kunen2] p. 47Lemma I.9.9relpfr 44937
[Kunen2] p. 53Lemma I.9.21trfr 44945
[Kunen2] p. 53Lemma I.9.24(2)wffr 44944
[Kunen2] p. 53Definition I.9.20tcfr 44946
[Kunen2] p. 95Lemma I.16.2ralabso 44951  rexabso 44952
[Kunen2] p. 96Example I.16.3disjabso 44958  n0abso 44959  ssabso 44957
[Kunen2] p. 111Lemma II.2.4(1)traxext 44960
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 44970
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 44965
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 44968
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 44969
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 44964
[Kunen2] p. 112Corollary II.2.5wfaxext 44976  wfaxpr 44981  wfaxreg 44983  wfaxrep 44977  wfaxsep 44978  wfaxun 44982
[Kunen2] p. 113Lemma II.2.8pwclaxpow 44967
[Kunen2] p. 113Corollary II.2.9wfaxpow 44980
[Kunen2] p. 114Theorem II.2.13wfaxext 44976
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 44975  omelaxinf2 44972
[Kunen2] p. 114Corollary II.2.12wfac8prim 44985  wfaxinf2 44984
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 44998  permaxext 44988  permaxinf2 44996  permaxnul 44991  permaxpow 44992  permaxpr 44993  permaxrep 44989  permaxsep 44990  permaxun 44994
[Kunen2] p. 148Definition II.9.1brpermmodel 44986
[Kunen2] p. 149Exercise II.9.3permac8prim 44997
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4964
[Lang] , p. 225Corollary 1.3finexttrb 33653
[Lang] p. Definitiondf-rn 5642
[Lang] p. 3Statementlidrideqd 18578  mndbn0 18659
[Lang] p. 3Definitiondf-mnd 18644
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18596
[Lang] p. 4Property of composites. Second formulagsumccat 18750
[Lang] p. 5Equationgsumreidx 19831
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48163
[Lang] p. 6Examplenn0mnd 48160
[Lang] p. 6Equationgsumxp2 19894
[Lang] p. 6Statementcycsubm 19116
[Lang] p. 6Definitionmulgnn0gsum 18994
[Lang] p. 6Observationmndlsmidm 19584
[Lang] p. 7Definitiondfgrp2e 18877
[Lang] p. 30Definitiondf-tocyc 33079
[Lang] p. 32Property (a)cyc3genpm 33124
[Lang] p. 32Property (b)cyc3conja 33129  cycpmconjv 33114
[Lang] p. 53Definitiondf-cat 17609
[Lang] p. 53Axiom CAT 1cat1 18039  cat1lem 18038
[Lang] p. 54Definitiondf-iso 17691
[Lang] p. 57Definitiondf-inito 17926  df-termo 17927
[Lang] p. 58Exampleirinitoringc 21421
[Lang] p. 58Statementinitoeu1 17953  termoeu1 17960
[Lang] p. 62Definitiondf-func 17800
[Lang] p. 65Definitiondf-nat 17888
[Lang] p. 91Notedf-ringc 20566
[Lang] p. 92Statementmxidlprm 33434
[Lang] p. 92Definitionisprmidlc 33411
[Lang] p. 128Remarkdsmmlmod 21687
[Lang] p. 129Prooflincscm 48412  lincscmcl 48414  lincsum 48411  lincsumcl 48413
[Lang] p. 129Statementlincolss 48416
[Lang] p. 129Observationdsmmfi 21680
[Lang] p. 141Theorem 5.3dimkerim 33616  qusdimsum 33617
[Lang] p. 141Corollary 5.4lssdimle 33596
[Lang] p. 147Definitionsnlindsntor 48453
[Lang] p. 504Statementmat1 22367  matring 22363
[Lang] p. 504Definitiondf-mamu 22311
[Lang] p. 505Statementmamuass 22322  mamutpos 22378  matassa 22364  mattposvs 22375  tposmap 22377
[Lang] p. 513Definitionmdet1 22521  mdetf 22515
[Lang] p. 513Theorem 4.4cramer 22611
[Lang] p. 514Proposition 4.6mdetleib 22507
[Lang] p. 514Proposition 4.8mdettpos 22531
[Lang] p. 515Definitiondf-minmar1 22555  smadiadetr 22595
[Lang] p. 515Corollary 4.9mdetero 22530  mdetralt 22528
[Lang] p. 517Proposition 4.15mdetmul 22543
[Lang] p. 518Definitiondf-madu 22554
[Lang] p. 518Proposition 4.16madulid 22565  madurid 22564  matinv 22597
[Lang] p. 561Theorem 3.1cayleyhamilton 22810
[Lang], p. 224Proposition 1.2extdgmul 33652  fedgmul 33620
[Lang], p. 561Remarkchpmatply1 22752
[Lang], p. 561Definitiondf-chpmat 22747
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44316
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44311
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44317
[LeBlanc] p. 277Rule R2axnul 5255
[Levy] p. 12Axiom 4.3.1df-clab 2708
[Levy] p. 59Definitiondf-ttrcl 9637
[Levy] p. 64Theorem 5.6(ii)frinsg 9680
[Levy] p. 338Axiomdf-clel 2803  df-cleq 2721
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2803  df-cleq 2721
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2708
[Levy] p. 358Axiomdf-clab 2708
[Levy58] p. 2Definition Iisfin1-3 10315
[Levy58] p. 2Definition IIdf-fin2 10215
[Levy58] p. 2Definition Iadf-fin1a 10214
[Levy58] p. 2Definition IIIdf-fin3 10217
[Levy58] p. 3Definition Vdf-fin5 10218
[Levy58] p. 3Definition IVdf-fin4 10216
[Levy58] p. 4Definition VIdf-fin6 10219
[Levy58] p. 4Definition VIIdf-fin7 10220
[Levy58], p. 3Theorem 1fin1a2 10344
[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 1768
[Lopez-Astorga] p. 12Rule 2mptxor 1769
[Lopez-Astorga] p. 12Rule 3mtpxor 1771
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32387
[Maeda] p. 168Lemma 5mdsym 32391  mdsymi 32390
[Maeda] p. 168Lemma 4(i)mdsymlem4 32385  mdsymlem6 32387  mdsymlem7 32388
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32389
[MaedaMaeda] p. 1Remarkssdmd1 32292  ssdmd2 32293  ssmd1 32290  ssmd2 32291
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32288
[MaedaMaeda] p. 1Definition 1.1df-dmd 32260  df-md 32259  mdbr 32273
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32310  mdslj1i 32298  mdslj2i 32299  mdslle1i 32296  mdslle2i 32297  mdslmd1i 32308  mdslmd2i 32309
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32300  mdsl2bi 32302  mdsl2i 32301
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32314
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32311
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32312
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32289
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32294  mdsl3 32295
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32313
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32408
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39307  hlrelat1 39387
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39025
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32315  cvmdi 32303  cvnbtwn4 32268  cvrnbtwn4 39265
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32316
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39326  cvp 32354  cvrp 39403  lcvp 39026
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32378
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32377
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39319  hlexch4N 39379
[MaedaMaeda] p. 34Exercise 7.1atabsi 32380
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39430
[MaedaMaeda] p. 61Definition 15.10psubN 39736  atpsubN 39740  df-pointsN 39489  pointpsubN 39738
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39491  pmap11 39749  pmaple 39748  pmapsub 39755  pmapval 39744
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39752  pmap1N 39754
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39757  pmapglb2N 39758  pmapglb2xN 39759  pmapglbx 39756
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39839
[MaedaMaeda] p. 67Postulate PS1ps-1 39464
[MaedaMaeda] p. 68Lemma 16.2df-padd 39783  paddclN 39829  paddidm 39828
[MaedaMaeda] p. 68Condition PS2ps-2 39465
[MaedaMaeda] p. 68Equation 16.2.1paddass 39825
[MaedaMaeda] p. 69Lemma 16.4ps-1 39464
[MaedaMaeda] p. 69Theorem 16.4ps-2 39465
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19589  lsmmod2 19590  lssats 38998  shatomici 32337  shatomistici 32340  shmodi 31369  shmodsi 31368
[MaedaMaeda] p. 130Remark 29.6dmdmd 32279  mdsymlem7 32388
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31568
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31472
[MaedaMaeda] p. 139Remarksumdmdii 32394
[Margaris] p. 40Rule Cexlimiv 1930
[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 1780  df-or 848  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30379
[Margaris] p. 59Section 14notnotrALTVD 44897
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44898
[Margaris] p. 79Rule Cexinst01 44608  exinst11 44609
[Margaris] p. 89Theorem 19.219.2 1976  19.2g 2189  r19.2z 4454
[Margaris] p. 89Theorem 19.319.3 2203  rr19.3v 3630
[Margaris] p. 89Theorem 19.5alcom 2160
[Margaris] p. 89Theorem 19.6alex 1826
[Margaris] p. 89Theorem 19.7alnex 1781
[Margaris] p. 89Theorem 19.819.8a 2182
[Margaris] p. 89Theorem 19.919.9 2206  19.9h 2286  exlimd 2219  exlimdh 2290
[Margaris] p. 89Theorem 19.11excom 2163  excomim 2164
[Margaris] p. 89Theorem 19.1219.12 2326
[Margaris] p. 90Section 19conventions-labels 30380  conventions-labels 30380  conventions-labels 30380  conventions-labels 30380
[Margaris] p. 90Theorem 19.14exnal 1827
[Margaris] p. 90Theorem 19.152albi 44360  albi 1818
[Margaris] p. 90Theorem 19.1619.16 2226
[Margaris] p. 90Theorem 19.1719.17 2227
[Margaris] p. 90Theorem 19.182exbi 44362  exbi 1847
[Margaris] p. 90Theorem 19.1919.19 2230
[Margaris] p. 90Theorem 19.202alim 44359  2alimdv 1918  alimd 2213  alimdh 1817  alimdv 1916  ax-4 1809  ralimdaa 3236  ralimdv 3147  ralimdva 3145  ralimdvva 3182  sbcimdv 3819
[Margaris] p. 90Theorem 19.2119.21 2208  19.21h 2287  19.21t 2207  19.21vv 44358  alrimd 2216  alrimdd 2215  alrimdh 1863  alrimdv 1929  alrimi 2214  alrimih 1824  alrimiv 1927  alrimivv 1928  hbralrimi 3123  r19.21be 3228  r19.21bi 3227  ralrimd 3240  ralrimdv 3131  ralrimdva 3133  ralrimdvv 3179  ralrimdvva 3190  ralrimi 3233  ralrimia 3234  ralrimiv 3124  ralrimiva 3125  ralrimivv 3176  ralrimivva 3178  ralrimivvva 3181  ralrimivw 3129
[Margaris] p. 90Theorem 19.222exim 44361  2eximdv 1919  exim 1834  eximd 2217  eximdh 1864  eximdv 1917  rexim 3070  reximd2a 3245  reximdai 3237  reximdd 45135  reximddv 3149  reximddv2 3194  reximddv3 3150  reximdv 3148  reximdv2 3143  reximdva 3146  reximdvai 3144  reximdvva 3183  reximi2 3062
[Margaris] p. 90Theorem 19.2319.23 2212  19.23bi 2192  19.23h 2288  19.23t 2211  exlimdv 1933  exlimdvv 1934  exlimexi 44507  exlimiv 1930  exlimivv 1932  rexlimd3 45131  rexlimdv 3132  rexlimdv3a 3138  rexlimdva 3134  rexlimdva2 3136  rexlimdvaa 3135  rexlimdvv 3191  rexlimdvva 3192  rexlimdvvva 3193  rexlimdvw 3139  rexlimiv 3127  rexlimiva 3126  rexlimivv 3177
[Margaris] p. 90Theorem 19.2419.24 1991
[Margaris] p. 90Theorem 19.2519.25 1880
[Margaris] p. 90Theorem 19.2619.26 1870
[Margaris] p. 90Theorem 19.2719.27 2228  r19.27z 4464  r19.27zv 4465
[Margaris] p. 90Theorem 19.2819.28 2229  19.28vv 44368  r19.28z 4457  r19.28zf 45146  r19.28zv 4460  rr19.28v 3631
[Margaris] p. 90Theorem 19.2919.29 1873  r19.29d2r 3120  r19.29imd 3098
[Margaris] p. 90Theorem 19.3019.30 1881
[Margaris] p. 90Theorem 19.3119.31 2235  19.31vv 44366
[Margaris] p. 90Theorem 19.3219.32 2234  r19.32 47092
[Margaris] p. 90Theorem 19.3319.33-2 44364  19.33 1884
[Margaris] p. 90Theorem 19.3419.34 1992
[Margaris] p. 90Theorem 19.3519.35 1877
[Margaris] p. 90Theorem 19.3619.36 2231  19.36vv 44365  r19.36zv 4466
[Margaris] p. 90Theorem 19.3719.37 2233  19.37vv 44367  r19.37zv 4461
[Margaris] p. 90Theorem 19.3819.38 1839
[Margaris] p. 90Theorem 19.3919.39 1990
[Margaris] p. 90Theorem 19.4019.40-2 1887  19.40 1886  r19.40 3099
[Margaris] p. 90Theorem 19.4119.41 2236  19.41rg 44533
[Margaris] p. 90Theorem 19.4219.42 2237
[Margaris] p. 90Theorem 19.4319.43 1882
[Margaris] p. 90Theorem 19.4419.44 2238  r19.44zv 4463
[Margaris] p. 90Theorem 19.4519.45 2239  r19.45zv 4462
[Margaris] p. 110Exercise 2(b)eu1 2603
[Mayet] p. 370Remarkjpi 32249  largei 32246  stri 32236
[Mayet3] p. 9Definition of CH-statesdf-hst 32191  ishst 32193
[Mayet3] p. 10Theoremhstrbi 32245  hstri 32244
[Mayet3] p. 1223Theorem 4.1mayete3i 31707
[Mayet3] p. 1240Theorem 7.1mayetes3i 31708
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32257
[MegPav2000] p. 2345Definition 3.4-1chintcl 31311  chsupcl 31319
[MegPav2000] p. 2345Definition 3.4-2hatomic 32339
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32333
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32360
[MegPav2000] p. 2366Figure 7pl42N 39970
[MegPav2002] p. 362Lemma 2.2latj31 18428  latj32 18426  latjass 18424
[Megill] p. 444Axiom C5ax-5 1910  ax5ALT 38893
[Megill] p. 444Section 7conventions 30379
[Megill] p. 445Lemma L12aecom-o 38887  ax-c11n 38874  axc11n 2424
[Megill] p. 446Lemma L17equtrr 2022
[Megill] p. 446Lemma L18ax6fromc10 38882
[Megill] p. 446Lemma L19hbnae-o 38914  hbnae 2430
[Megill] p. 447Remark 9.1dfsb1 2479  sbid 2256  sbidd-misc 49701  sbidd 49700
[Megill] p. 448Remark 9.6axc14 2461
[Megill] p. 448Scheme C4'ax-c4 38870
[Megill] p. 448Scheme C5'ax-c5 38869  sp 2184
[Megill] p. 448Scheme C6'ax-11 2158
[Megill] p. 448Scheme C7'ax-c7 38871
[Megill] p. 448Scheme C8'ax-7 2008
[Megill] p. 448Scheme C9'ax-c9 38876
[Megill] p. 448Scheme C10'ax-6 1967  ax-c10 38872
[Megill] p. 448Scheme C11'ax-c11 38873
[Megill] p. 448Scheme C12'ax-8 2111
[Megill] p. 448Scheme C13'ax-9 2119
[Megill] p. 448Scheme C14'ax-c14 38877
[Megill] p. 448Scheme C15'ax-c15 38875
[Megill] p. 448Scheme C16'ax-c16 38878
[Megill] p. 448Theorem 9.4dral1-o 38890  dral1 2437  dral2-o 38916  dral2 2436  drex1 2439  drex2 2440  drsb1 2493  drsb2 2267
[Megill] p. 449Theorem 9.7sbcom2 2174  sbequ 2084  sbid2v 2507
[Megill] p. 450Example in Appendixhba1-o 38883  hba1 2293
[Mendelson] p. 35Axiom A3hirstL-ax3 46886
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3839  rspsbca 3840  stdpc4 2069
[Mendelson] p. 69Axiom 5ax-c4 38870  ra4 3846  stdpc5 2209
[Mendelson] p. 81Rule Cexlimiv 1930
[Mendelson] p. 95Axiom 6stdpc6 2028
[Mendelson] p. 95Axiom 7stdpc7 2251
[Mendelson] p. 225Axiom system NBGru 3748
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5469
[Mendelson] p. 231Exercise 4.10(k)inv1 4357
[Mendelson] p. 231Exercise 4.10(l)unv 4358
[Mendelson] p. 231Exercise 4.10(n)dfin3 4236
[Mendelson] p. 231Exercise 4.10(o)df-nul 4293
[Mendelson] p. 231Exercise 4.10(q)dfin4 4237
[Mendelson] p. 231Exercise 4.10(s)ddif 4100
[Mendelson] p. 231Definition of uniondfun3 4235
[Mendelson] p. 235Exercise 4.12(c)univ 5406
[Mendelson] p. 235Exercise 4.12(d)pwv 4864
[Mendelson] p. 235Exercise 4.12(j)pwin 5522
[Mendelson] p. 235Exercise 4.12(k)pwunss 4577
[Mendelson] p. 235Exercise 4.12(l)pwssun 5523
[Mendelson] p. 235Exercise 4.12(n)uniin 4891
[Mendelson] p. 235Exercise 4.12(p)reli 5780
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6229
[Mendelson] p. 244Proposition 4.8(g)epweon 7731
[Mendelson] p. 246Definition of successordf-suc 6326
[Mendelson] p. 250Exercise 4.36oelim2 8536
[Mendelson] p. 254Proposition 4.22(b)xpen 9081
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9002  xpsneng 9003
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9009  xpcomeng 9010
[Mendelson] p. 254Proposition 4.22(e)xpassen 9012
[Mendelson] p. 255Definitionbrsdom 8923
[Mendelson] p. 255Exercise 4.39endisj 9005
[Mendelson] p. 255Exercise 4.41mapprc 8780
[Mendelson] p. 255Exercise 4.43mapsnen 8985  mapsnend 8984
[Mendelson] p. 255Exercise 4.45mapunen 9087
[Mendelson] p. 255Exercise 4.47xpmapen 9086
[Mendelson] p. 255Exercise 4.42(a)map0e 8832
[Mendelson] p. 255Exercise 4.42(b)map1 8988
[Mendelson] p. 257Proposition 4.24(a)undom 9006
[Mendelson] p. 258Exercise 4.56(c)djuassen 10108  djucomen 10107
[Mendelson] p. 258Exercise 4.56(f)djudom1 10112
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10106
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8472
[Mendelson] p. 266Proposition 4.34(f)oaordex 8499
[Mendelson] p. 275Proposition 4.42(d)entri3 10488
[Mendelson] p. 281Definitiondf-r1 9693
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9742
[Mendelson] p. 287Axiom system MKru 3748
[MertziosUnger] p. 152Definitiondf-frgr 30238
[MertziosUnger] p. 153Remark 1frgrconngr 30273
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30275  vdgn1frgrv3 30276
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30277
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30270
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30263  2pthfrgrrn 30261  2pthfrgrrn2 30262
[Mittelstaedt] p. 9Definitiondf-oc 31231
[Monk1] p. 22Remarkconventions 30379
[Monk1] p. 22Theorem 3.1conventions 30379
[Monk1] p. 26Theorem 2.8(vii)ssin 4198
[Monk1] p. 33Theorem 3.2(i)ssrel 5737  ssrelf 32593
[Monk1] p. 33Theorem 3.2(ii)eqrel 5738
[Monk1] p. 34Definition 3.3df-opab 5165
[Monk1] p. 36Theorem 3.7(i)coi1 6223  coi2 6224
[Monk1] p. 36Theorem 3.8(v)dm0 5874  rn0 5879
[Monk1] p. 36Theorem 3.7(ii)cnvi 6102
[Monk1] p. 37Theorem 3.13(i)relxp 5649
[Monk1] p. 37Theorem 3.13(x)dmxp 5882  rnxp 6131
[Monk1] p. 37Theorem 3.13(ii)0xp 5729  xp0 6119
[Monk1] p. 38Theorem 3.16(ii)ima0 6037
[Monk1] p. 38Theorem 3.16(viii)imai 6034
[Monk1] p. 39Theorem 3.17imaex 7870  imaexg 7869
[Monk1] p. 39Theorem 3.16(xi)imassrn 6031
[Monk1] p. 41Theorem 4.3(i)fnopfv 7029  funfvop 7004
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6897
[Monk1] p. 42Theorem 4.4(iii)fvelima 6908
[Monk1] p. 43Theorem 4.6funun 6546
[Monk1] p. 43Theorem 4.8(iv)dff13 7211  dff13f 7212
[Monk1] p. 46Theorem 4.15(v)funex 7175  funrnex 7912
[Monk1] p. 50Definition 5.4fniunfv 7203
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6188
[Monk1] p. 52Theorem 5.11(viii)ssint 4924
[Monk1] p. 52Definition 5.13 (i)1stval2 7964  df-1st 7947
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7965  df-2nd 7948
[Monk1] p. 112Theorem 15.17(v)ranksn 9783  ranksnb 9756
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9784
[Monk1] p. 112Theorem 15.17(iii)rankun 9785  rankunb 9779
[Monk1] p. 113Theorem 15.18r1val3 9767
[Monk1] p. 113Definition 15.19df-r1 9693  r1val2 9766
[Monk1] p. 117Lemmazorn2 10435  zorn2g 10432
[Monk1] p. 133Theorem 18.11cardom 9915
[Monk1] p. 133Theorem 18.12canth3 10490
[Monk1] p. 133Theorem 18.14carduni 9910
[Monk2] p. 105Axiom C4ax-4 1809
[Monk2] p. 105Axiom C7ax-7 2008
[Monk2] p. 105Axiom C8ax-12 2178  ax-c15 38875  ax12v2 2180
[Monk2] p. 108Lemma 5ax-c4 38870
[Monk2] p. 109Lemma 12ax-11 2158
[Monk2] p. 109Lemma 15equvini 2453  equvinv 2029  eqvinop 5442
[Monk2] p. 113Axiom C5-1ax-5 1910  ax5ALT 38893
[Monk2] p. 113Axiom C5-2ax-10 2142
[Monk2] p. 113Axiom C5-3ax-11 2158
[Monk2] p. 114Lemma 21sp 2184
[Monk2] p. 114Lemma 22axc4 2320  hba1-o 38883  hba1 2293
[Monk2] p. 114Lemma 23nfia1 2154
[Monk2] p. 114Lemma 24nfa2 2177  nfra2 3347  nfra2w 3272
[Moore] p. 53Part Idf-mre 17523
[Munkres] p. 77Example 2distop 22915  indistop 22922  indistopon 22921
[Munkres] p. 77Example 3fctop 22924  fctop2 22925
[Munkres] p. 77Example 4cctop 22926
[Munkres] p. 78Definition of basisdf-bases 22866  isbasis3g 22869
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17382  tgval2 22876
[Munkres] p. 79Remarktgcl 22889
[Munkres] p. 80Lemma 2.1tgval3 22883
[Munkres] p. 80Lemma 2.2tgss2 22907  tgss3 22906
[Munkres] p. 81Lemma 2.3basgen 22908  basgen2 22909
[Munkres] p. 83Exercise 3topdifinf 37330  topdifinfeq 37331  topdifinffin 37329  topdifinfindis 37327
[Munkres] p. 89Definition of subspace topologyresttop 23080
[Munkres] p. 93Theorem 6.1(1)0cld 22958  topcld 22955
[Munkres] p. 93Theorem 6.1(2)iincld 22959
[Munkres] p. 93Theorem 6.1(3)uncld 22961
[Munkres] p. 94Definition of closureclsval 22957
[Munkres] p. 94Definition of interiorntrval 22956
[Munkres] p. 95Theorem 6.5(a)clsndisj 22995  elcls 22993
[Munkres] p. 95Theorem 6.5(b)elcls3 23003
[Munkres] p. 97Theorem 6.6clslp 23068  neindisj 23037
[Munkres] p. 97Corollary 6.7cldlp 23070
[Munkres] p. 97Definition of limit pointislp2 23065  lpval 23059
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23235
[Munkres] p. 102Definition of continuous functiondf-cn 23147  iscn 23155  iscn2 23158
[Munkres] p. 107Theorem 7.2(g)cncnp 23200  cncnp2 23201  cncnpi 23198  df-cnp 23148  iscnp 23157  iscnp2 23159
[Munkres] p. 127Theorem 10.1metcn 24464
[Munkres] p. 128Theorem 10.3metcn4 25244
[Nathanson] p. 123Remarkreprgt 34605  reprinfz1 34606  reprlt 34603
[Nathanson] p. 123Definitiondf-repr 34593
[Nathanson] p. 123Chapter 5.1circlemethnat 34625
[Nathanson] p. 123Propositionbreprexp 34617  breprexpnat 34618  itgexpif 34590
[NielsenChuang] p. 195Equation 4.73unierri 32083
[OeSilva] p. 2042Section 2ax-bgbltosilva 47804
[Pfenning] p. 17Definition XMnatded 30382
[Pfenning] p. 17Definition NNCnatded 30382  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30382
[Pfenning] p. 18Rule"natded 30382
[Pfenning] p. 18Definition /\Inatded 30382
[Pfenning] p. 18Definition ` `Enatded 30382  natded 30382  natded 30382  natded 30382  natded 30382
[Pfenning] p. 18Definition ` `Inatded 30382  natded 30382  natded 30382  natded 30382  natded 30382
[Pfenning] p. 18Definition ` `ELnatded 30382
[Pfenning] p. 18Definition ` `ERnatded 30382
[Pfenning] p. 18Definition ` `Ea,unatded 30382
[Pfenning] p. 18Definition ` `IRnatded 30382
[Pfenning] p. 18Definition ` `Ianatded 30382
[Pfenning] p. 127Definition =Enatded 30382
[Pfenning] p. 127Definition =Inatded 30382
[Ponnusamy] p. 361Theorem 6.44cphip0l 25135  df-dip 30680  dip0l 30697  ip0l 21578
[Ponnusamy] p. 361Equation 6.45cphipval 25176  ipval 30682
[Ponnusamy] p. 362Equation I1dipcj 30693  ipcj 21576
[Ponnusamy] p. 362Equation I3cphdir 25138  dipdir 30821  ipdir 21581  ipdiri 30809
[Ponnusamy] p. 362Equation I4ipidsq 30689  nmsq 25127
[Ponnusamy] p. 362Equation 6.46ip0i 30804
[Ponnusamy] p. 362Equation 6.47ip1i 30806
[Ponnusamy] p. 362Equation 6.48ip2i 30807
[Ponnusamy] p. 363Equation I2cphass 25144  dipass 30824  ipass 21587  ipassi 30820
[Prugovecki] p. 186Definition of brabraval 31923  df-bra 31829
[Prugovecki] p. 376Equation 8.1df-kb 31830  kbval 31933
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32361
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39875
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32375  atcvat4i 32376  cvrat3 39429  cvrat4 39430  lsatcvat3 39038
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32261  cvrval 39255  df-cv 32258  df-lcv 39005  lspsncv0 21088
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39887
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39888
[Quine] p. 16Definition 2.1df-clab 2708  rabid 3424  rabidd 45142
[Quine] p. 17Definition 2.1''dfsb7 2279
[Quine] p. 18Definition 2.7df-cleq 2721
[Quine] p. 19Definition 2.9conventions 30379  df-v 3446
[Quine] p. 34Theorem 5.1eqabb 2867
[Quine] p. 35Theorem 5.2abid1 2864  abid2f 2922
[Quine] p. 40Theorem 6.1sb5 2276
[Quine] p. 40Theorem 6.2sb6 2086  sbalex 2243
[Quine] p. 41Theorem 6.3df-clel 2803
[Quine] p. 41Theorem 6.4eqid 2729  eqid1 30446
[Quine] p. 41Theorem 6.5eqcom 2736
[Quine] p. 42Theorem 6.6df-sbc 3751
[Quine] p. 42Theorem 6.7dfsbcq 3752  dfsbcq2 3753
[Quine] p. 43Theorem 6.8vex 3448
[Quine] p. 43Theorem 6.9isset 3458
[Quine] p. 44Theorem 7.3spcgf 3554  spcgv 3559  spcimgf 3513
[Quine] p. 44Theorem 6.11spsbc 3763  spsbcd 3764
[Quine] p. 44Theorem 6.12elex 3465
[Quine] p. 44Theorem 6.13elab 3643  elabg 3640  elabgf 3638
[Quine] p. 44Theorem 6.14noel 4297
[Quine] p. 48Theorem 7.2snprc 4677
[Quine] p. 48Definition 7.1df-pr 4588  df-sn 4586
[Quine] p. 49Theorem 7.4snss 4745  snssg 4743
[Quine] p. 49Theorem 7.5prss 4780  prssg 4779
[Quine] p. 49Theorem 7.6prid1 4722  prid1g 4720  prid2 4723  prid2g 4721  snid 4622  snidg 4620
[Quine] p. 51Theorem 7.12snex 5386
[Quine] p. 51Theorem 7.13prex 5387
[Quine] p. 53Theorem 8.2unisn 4886  unisnALT 44908  unisng 4885
[Quine] p. 53Theorem 8.3uniun 4890
[Quine] p. 54Theorem 8.6elssuni 4897
[Quine] p. 54Theorem 8.7uni0 4895
[Quine] p. 56Theorem 8.17uniabio 6466
[Quine] p. 56Definition 8.18dfaiota2 47080  dfiota2 6453
[Quine] p. 57Theorem 8.19aiotaval 47089  iotaval 6470
[Quine] p. 57Theorem 8.22iotanul 6477
[Quine] p. 58Theorem 8.23iotaex 6472
[Quine] p. 58Definition 9.1df-op 4592
[Quine] p. 61Theorem 9.5opabid 5480  opabidw 5479  opelopab 5497  opelopaba 5491  opelopabaf 5499  opelopabf 5500  opelopabg 5493  opelopabga 5488  opelopabgf 5495  oprabid 7401  oprabidw 7400
[Quine] p. 64Definition 9.11df-xp 5637
[Quine] p. 64Definition 9.12df-cnv 5639
[Quine] p. 64Definition 9.15df-id 5526
[Quine] p. 65Theorem 10.3fun0 6565
[Quine] p. 65Theorem 10.4funi 6532
[Quine] p. 65Theorem 10.5funsn 6553  funsng 6551
[Quine] p. 65Definition 10.1df-fun 6501
[Quine] p. 65Definition 10.2args 6052  dffv4 6837
[Quine] p. 68Definition 10.11conventions 30379  df-fv 6507  fv2 6835
[Quine] p. 124Theorem 17.3nn0opth2 14213  nn0opth2i 14212  nn0opthi 14211  omopthi 8602
[Quine] p. 177Definition 25.2df-rdg 8355
[Quine] p. 232Equation icarddom 10483
[Quine] p. 284Axiom 39(vi)funimaex 6588  funimaexg 6587
[Quine] p. 331Axiom system NFru 3748
[ReedSimon] p. 36Definition (iii)ax-his3 31063
[ReedSimon] p. 63Exercise 4(a)df-dip 30680  polid 31138  polid2i 31136  polidi 31137
[ReedSimon] p. 63Exercise 4(b)df-ph 30792
[ReedSimon] p. 195Remarklnophm 31998  lnophmi 31997
[Retherford] p. 49Exercise 1(i)leopadd 32111
[Retherford] p. 49Exercise 1(ii)leopmul 32113  leopmuli 32112
[Retherford] p. 49Exercise 1(iv)leoptr 32116
[Retherford] p. 49Definition VI.1df-leop 31831  leoppos 32105
[Retherford] p. 49Exercise 1(iii)leoptri 32115
[Retherford] p. 49Definition of operator orderingleop3 32104
[Roman] p. 4Definitiondf-dmat 22410  df-dmatalt 48380
[Roman] p. 18Part Preliminariesdf-rng 20073
[Roman] p. 19Part Preliminariesdf-ring 20155
[Roman] p. 46Theorem 1.6isldepslvec2 48467
[Roman] p. 112Noteisldepslvec2 48467  ldepsnlinc 48490  zlmodzxznm 48479
[Roman] p. 112Examplezlmodzxzequa 48478  zlmodzxzequap 48481  zlmodzxzldep 48486
[Roman] p. 170Theorem 7.8cayleyhamilton 22810
[Rosenlicht] p. 80Theoremheicant 37642
[Rosser] p. 281Definitiondf-op 4592
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34629
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34630
[Rotman] p. 28Remarkpgrpgt2nabl 48347  pmtr3ncom 19389
[Rotman] p. 31Theorem 3.4symggen2 19385
[Rotman] p. 42Theorem 3.15cayley 19328  cayleyth 19329
[Rudin] p. 164Equation 27efcan 16038
[Rudin] p. 164Equation 30efzval 16046
[Rudin] p. 167Equation 48absefi 16140
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1771
[Sanford] p. 39Rule 4mptxor 1769
[Sanford] p. 40Rule 1mptnan 1768
[Schechter] p. 51Definition of antisymmetryintasym 6076
[Schechter] p. 51Definition of irreflexivityintirr 6079
[Schechter] p. 51Definition of symmetrycnvsym 6073
[Schechter] p. 51Definition of transitivitycotr 6071
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17523
[Schechter] p. 79Definition of Moore closuredf-mrc 17524
[Schechter] p. 82Section 4.5df-mrc 17524
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17526
[Schechter] p. 139Definition AC3dfac9 10066
[Schechter] p. 141Definition (MC)dfac11 43044
[Schechter] p. 149Axiom DC1ax-dc 10375  axdc3 10383
[Schechter] p. 187Definition of "ring with unit"isring 20157  isrngo 37884
[Schechter] p. 276Remark 11.6.espan0 31521
[Schechter] p. 276Definition of spandf-span 31288  spanval 31312
[Schechter] p. 428Definition 15.35bastop1 22913
[Schloeder] p. 1Lemma 1.3onelon 6345  onelord 43233  ordelon 6344  ordelord 6342
[Schloeder] p. 1Lemma 1.7onepsuc 43234  sucidg 6403
[Schloeder] p. 1Remark 1.50elon 6375  onsuc 7767  ord0 6374  ordsuci 7764
[Schloeder] p. 1Theorem 1.9epsoon 43235
[Schloeder] p. 1Definition 1.1dftr5 5213
[Schloeder] p. 1Definition 1.2dford3 43010  elon2 6331
[Schloeder] p. 1Definition 1.4df-suc 6326
[Schloeder] p. 1Definition 1.6epel 5534  epelg 5532
[Schloeder] p. 1Theorem 1.9(i)elirr 9526  epirron 43236  ordirr 6338
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43238  oneptr 43237  ontr1 6367
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6363  oneptri 43239  ordtri3or 6352
[Schloeder] p. 2Lemma 1.10ondif1 8442  ord0eln0 6376
[Schloeder] p. 2Lemma 1.13elsuci 6389  onsucss 43248  trsucss 6410
[Schloeder] p. 2Lemma 1.14ordsucss 7773
[Schloeder] p. 2Lemma 1.15onnbtwn 6416  ordnbtwn 6415
[Schloeder] p. 2Lemma 1.16orddif0suc 43250  ordnexbtwnsuc 43249
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10330  onsucf1lem 43251  onsucf1o 43254  onsucf1olem 43252  onsucrn 43253
[Schloeder] p. 2Lemma 1.18dflim7 43255
[Schloeder] p. 2Remark 1.12ordzsl 7801
[Schloeder] p. 2Theorem 1.10ondif1i 43244  ordne0gt0 43243
[Schloeder] p. 2Definition 1.11dflim6 43246  limnsuc 43247  onsucelab 43245
[Schloeder] p. 3Remark 1.21omex 9572
[Schloeder] p. 3Theorem 1.19tfinds 7816
[Schloeder] p. 3Theorem 1.22omelon 9575  ordom 7832
[Schloeder] p. 3Definition 1.20dfom3 9576
[Schloeder] p. 4Lemma 2.21onn 8581
[Schloeder] p. 4Lemma 2.7ssonuni 7736  ssorduni 7735
[Schloeder] p. 4Remark 2.4oa1suc 8472
[Schloeder] p. 4Theorem 1.23dfom5 9579  limom 7838
[Schloeder] p. 4Definition 2.1df-1o 8411  df1o2 8418
[Schloeder] p. 4Definition 2.3oa0 8457  oa0suclim 43257  oalim 8473  oasuc 8465
[Schloeder] p. 4Definition 2.5om0 8458  om0suclim 43258  omlim 8474  omsuc 8467
[Schloeder] p. 4Definition 2.6oe0 8463  oe0m1 8462  oe0suclim 43259  oelim 8475  oesuc 8468
[Schloeder] p. 5Lemma 2.10onsupuni 43211
[Schloeder] p. 5Lemma 2.11onsupsucismax 43261
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43262
[Schloeder] p. 5Lemma 2.13limexissup 43263  limexissupab 43265  limiun 43264  limuni 6382
[Schloeder] p. 5Lemma 2.14oa0r 8479
[Schloeder] p. 5Lemma 2.15om1 8483  om1om1r 43266  om1r 8484
[Schloeder] p. 5Remark 2.8oacl 8476  oaomoecl 43260  oecl 8478  omcl 8477
[Schloeder] p. 5Definition 2.9onsupintrab 43213
[Schloeder] p. 6Lemma 2.16oe1 8485
[Schloeder] p. 6Lemma 2.17oe1m 8486
[Schloeder] p. 6Lemma 2.18oe0rif 43267
[Schloeder] p. 6Theorem 2.19oasubex 43268
[Schloeder] p. 6Theorem 2.20nnacl 8552  nnamecl 43269  nnecl 8554  nnmcl 8553
[Schloeder] p. 7Lemma 3.1onsucwordi 43270
[Schloeder] p. 7Lemma 3.2oaword1 8493
[Schloeder] p. 7Lemma 3.3oaword2 8494
[Schloeder] p. 7Lemma 3.4oalimcl 8501
[Schloeder] p. 7Lemma 3.5oaltublim 43272
[Schloeder] p. 8Lemma 3.6oaordi3 43273
[Schloeder] p. 8Lemma 3.81oaomeqom 43275
[Schloeder] p. 8Lemma 3.10oa00 8500
[Schloeder] p. 8Lemma 3.11omge1 43279  omword1 8514
[Schloeder] p. 8Remark 3.9oaordnr 43278  oaordnrex 43277
[Schloeder] p. 8Theorem 3.7oaord3 43274
[Schloeder] p. 9Lemma 3.12omge2 43280  omword2 8515
[Schloeder] p. 9Lemma 3.13omlim2 43281
[Schloeder] p. 9Lemma 3.14omord2lim 43282
[Schloeder] p. 9Lemma 3.15omord2i 43283  omordi 8507
[Schloeder] p. 9Theorem 3.16omord 8509  omord2com 43284
[Schloeder] p. 10Lemma 3.172omomeqom 43285  df-2o 8412
[Schloeder] p. 10Lemma 3.19oege1 43288  oewordi 8532
[Schloeder] p. 10Lemma 3.20oege2 43289  oeworde 8534
[Schloeder] p. 10Lemma 3.21rp-oelim2 43290
[Schloeder] p. 10Lemma 3.22oeord2lim 43291
[Schloeder] p. 10Remark 3.18omnord1 43287  omnord1ex 43286
[Schloeder] p. 11Lemma 3.23oeord2i 43292
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43294
[Schloeder] p. 11Remark 3.26oenord1 43298  oenord1ex 43297
[Schloeder] p. 11Theorem 4.1oaomoencom 43299
[Schloeder] p. 11Theorem 4.2oaass 8502
[Schloeder] p. 11Theorem 3.24oeord2com 43293
[Schloeder] p. 12Theorem 4.3odi 8520
[Schloeder] p. 13Theorem 4.4omass 8521
[Schloeder] p. 14Remark 4.6oenass 43301
[Schloeder] p. 14Theorem 4.7oeoa 8538
[Schloeder] p. 15Lemma 5.1cantnftermord 43302
[Schloeder] p. 15Lemma 5.2cantnfub 43303  cantnfub2 43304
[Schloeder] p. 16Theorem 5.3cantnf2 43307
[Schwabhauser] p. 10Axiom A1axcgrrflx 28894  axtgcgrrflx 28442
[Schwabhauser] p. 10Axiom A2axcgrtr 28895
[Schwabhauser] p. 10Axiom A3axcgrid 28896  axtgcgrid 28443
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28428
[Schwabhauser] p. 11Axiom A4axsegcon 28907  axtgsegcon 28444  df-trkgcb 28430
[Schwabhauser] p. 11Axiom A5ax5seg 28918  axtg5seg 28445  df-trkgcb 28430
[Schwabhauser] p. 11Axiom A6axbtwnid 28919  axtgbtwnid 28446  df-trkgb 28429
[Schwabhauser] p. 12Axiom A7axpasch 28921  axtgpasch 28447  df-trkgb 28429
[Schwabhauser] p. 12Axiom A8axlowdim2 28940  df-trkg2d 34649
[Schwabhauser] p. 13Axiom A8axtglowdim2 28450
[Schwabhauser] p. 13Axiom A9axtgupdim2 28451  df-trkg2d 34649
[Schwabhauser] p. 13Axiom A10axeuclid 28943  axtgeucl 28452  df-trkge 28431
[Schwabhauser] p. 13Axiom A11axcont 28956  axtgcont 28449  axtgcont1 28448  df-trkgb 28429
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35968
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35970
[Schwabhauser] p. 27Theorem 2.3cgrtr 35973
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35977
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35978  tgcgrcomimp 28457  tgcgrcoml 28459  tgcgrcomr 28458
[Schwabhauser] p. 28Theorem 2.8cgrtriv 35983  tgcgrtriv 28464
[Schwabhauser] p. 28Theorem 2.105segofs 35987  tg5segofs 34657
[Schwabhauser] p. 28Definition 2.10df-afs 34654  df-ofs 35964
[Schwabhauser] p. 29Theorem 2.11cgrextend 35989  tgcgrextend 28465
[Schwabhauser] p. 29Theorem 2.12segconeq 35991  tgsegconeq 28466
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36003  btwntriv2 35993  tgbtwntriv2 28467
[Schwabhauser] p. 30Theorem 3.2btwncomim 35994  tgbtwncom 28468
[Schwabhauser] p. 30Theorem 3.3btwntriv1 35997  tgbtwntriv1 28471
[Schwabhauser] p. 30Theorem 3.4btwnswapid 35998  tgbtwnswapid 28472
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36004  btwnintr 36000  tgbtwnexch2 28476  tgbtwnintr 28473
[Schwabhauser] p. 30Theorem 3.6btwnexch 36006  btwnexch3 36001  tgbtwnexch 28478  tgbtwnexch3 28474
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36005  tgbtwnouttr 28477  tgbtwnouttr2 28475
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28939
[Schwabhauser] p. 32Theorem 3.14btwndiff 36008  tgbtwndiff 28486
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28479  trisegint 36009
[Schwabhauser] p. 34Theorem 4.2ifscgr 36025  tgifscgr 28488
[Schwabhauser] p. 34Theorem 4.11colcom 28538  colrot1 28539  colrot2 28540  lncom 28602  lnrot1 28603  lnrot2 28604
[Schwabhauser] p. 34Definition 4.1df-ifs 36021
[Schwabhauser] p. 35Theorem 4.3cgrsub 36026  tgcgrsub 28489
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36036  tgcgrxfr 28498
[Schwabhauser] p. 35Statement 4.4ercgrg 28497
[Schwabhauser] p. 35Definition 4.4df-cgr3 36022  df-cgrg 28491
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28491
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36037  tgbtwnxfr 28510
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36043  colinearperm2 36045  colinearperm3 36044  colinearperm4 36046  colinearperm5 36047
[Schwabhauser] p. 36Definition 4.8df-ismt 28513
[Schwabhauser] p. 36Definition 4.10df-colinear 36020  tgellng 28533  tglng 28526
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36048
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36056  lnxfr 28546
[Schwabhauser] p. 37Theorem 4.14lineext 36057  lnext 28547
[Schwabhauser] p. 37Theorem 4.16fscgr 36061  tgfscgr 28548
[Schwabhauser] p. 37Theorem 4.17linecgr 36062  lncgr 28549
[Schwabhauser] p. 37Definition 4.15df-fs 36023
[Schwabhauser] p. 38Theorem 4.18lineid 36064  lnid 28550
[Schwabhauser] p. 38Theorem 4.19idinside 36065  tgidinside 28551
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36082  tgbtwnconn1 28555
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36083  tgbtwnconn2 28556
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36084  tgbtwnconn3 28557
[Schwabhauser] p. 41Theorem 5.5brsegle2 36090
[Schwabhauser] p. 41Definition 5.4df-segle 36088  legov 28565
[Schwabhauser] p. 41Definition 5.5legov2 28566
[Schwabhauser] p. 42Remark 5.13legso 28579
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36091
[Schwabhauser] p. 42Theorem 5.7seglerflx 36093
[Schwabhauser] p. 42Theorem 5.8segletr 36095
[Schwabhauser] p. 42Theorem 5.9segleantisym 36096
[Schwabhauser] p. 42Theorem 5.10seglelin 36097
[Schwabhauser] p. 42Theorem 5.11seglemin 36094
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36099
[Schwabhauser] p. 42Proposition 5.7legid 28567
[Schwabhauser] p. 42Proposition 5.8legtrd 28569
[Schwabhauser] p. 42Proposition 5.9legtri3 28570
[Schwabhauser] p. 42Proposition 5.10legtrid 28571
[Schwabhauser] p. 42Proposition 5.11leg0 28572
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36106
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36107
[Schwabhauser] p. 43Theorem 6.4broutsideof 36102  df-outsideof 36101
[Schwabhauser] p. 43Definition 6.1broutsideof2 36103  ishlg 28582
[Schwabhauser] p. 44Theorem 6.4hlln 28587
[Schwabhauser] p. 44Theorem 6.5hlid 28589  outsideofrflx 36108
[Schwabhauser] p. 44Theorem 6.6hlcomb 28583  hlcomd 28584  outsideofcom 36109
[Schwabhauser] p. 44Theorem 6.7hltr 28590  outsideoftr 36110
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28598  outsideofeu 36112
[Schwabhauser] p. 44Definition 6.8df-ray 36119
[Schwabhauser] p. 45Part 2df-lines2 36120
[Schwabhauser] p. 45Theorem 6.13outsidele 36113
[Schwabhauser] p. 45Theorem 6.15lineunray 36128
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36129  tglineelsb2 28612
[Schwabhauser] p. 45Theorem 6.17linecom 36131  linerflx1 36130  linerflx2 36132  tglinecom 28615  tglinerflx1 28613  tglinerflx2 28614
[Schwabhauser] p. 45Theorem 6.18linethru 36134  tglinethru 28616
[Schwabhauser] p. 45Definition 6.14df-line2 36118  tglng 28526
[Schwabhauser] p. 45Proposition 6.13legbtwn 28574
[Schwabhauser] p. 46Theorem 6.19linethrueu 36137  tglinethrueu 28619
[Schwabhauser] p. 46Theorem 6.21lineintmo 36138  tglineineq 28623  tglineinteq 28625  tglineintmo 28622
[Schwabhauser] p. 46Theorem 6.23colline 28629
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28630
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28631
[Schwabhauser] p. 49Theorem 7.3mirinv 28646
[Schwabhauser] p. 49Theorem 7.7mirmir 28642
[Schwabhauser] p. 49Theorem 7.8mirreu3 28634
[Schwabhauser] p. 49Definition 7.5df-mir 28633  ismir 28639  mirbtwn 28638  mircgr 28637  mirfv 28636  mirval 28635
[Schwabhauser] p. 50Theorem 7.8mirreu 28644
[Schwabhauser] p. 50Theorem 7.9mireq 28645
[Schwabhauser] p. 50Theorem 7.10mirinv 28646
[Schwabhauser] p. 50Theorem 7.11mirf1o 28649
[Schwabhauser] p. 50Theorem 7.13miriso 28650
[Schwabhauser] p. 51Theorem 7.14mirmot 28655
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28652  mirbtwni 28651
[Schwabhauser] p. 51Theorem 7.16mircgrs 28653
[Schwabhauser] p. 51Theorem 7.17miduniq 28665
[Schwabhauser] p. 52Lemma 7.21symquadlem 28669
[Schwabhauser] p. 52Theorem 7.18miduniq1 28666
[Schwabhauser] p. 52Theorem 7.19miduniq2 28667
[Schwabhauser] p. 52Theorem 7.20colmid 28668
[Schwabhauser] p. 53Lemma 7.22krippen 28671
[Schwabhauser] p. 55Lemma 7.25midexlem 28672
[Schwabhauser] p. 57Theorem 8.2ragcom 28678
[Schwabhauser] p. 57Definition 8.1df-rag 28674  israg 28677
[Schwabhauser] p. 58Theorem 8.3ragcol 28679
[Schwabhauser] p. 58Theorem 8.4ragmir 28680
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28682
[Schwabhauser] p. 58Theorem 8.6ragflat2 28683
[Schwabhauser] p. 58Theorem 8.7ragflat 28684
[Schwabhauser] p. 58Theorem 8.8ragtriva 28685
[Schwabhauser] p. 58Theorem 8.9ragflat3 28686  ragncol 28689
[Schwabhauser] p. 58Theorem 8.10ragcgr 28687
[Schwabhauser] p. 59Theorem 8.12perpcom 28693
[Schwabhauser] p. 59Theorem 8.13ragperp 28697
[Schwabhauser] p. 59Theorem 8.14perpneq 28694
[Schwabhauser] p. 59Definition 8.11df-perpg 28676  isperp 28692
[Schwabhauser] p. 59Definition 8.13isperp2 28695
[Schwabhauser] p. 60Theorem 8.18foot 28702
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28710  colperpexlem2 28711
[Schwabhauser] p. 63Theorem 8.21colperpex 28713  colperpexlem3 28712
[Schwabhauser] p. 64Theorem 8.22mideu 28718  midex 28717
[Schwabhauser] p. 66Lemma 8.24opphllem 28715
[Schwabhauser] p. 67Theorem 9.2oppcom 28724
[Schwabhauser] p. 67Definition 9.1islnopp 28719
[Schwabhauser] p. 68Lemma 9.3opphllem2 28728
[Schwabhauser] p. 68Lemma 9.4opphllem5 28731  opphllem6 28732
[Schwabhauser] p. 69Theorem 9.5opphl 28734
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28447
[Schwabhauser] p. 70Theorem 9.6outpasch 28735
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28743
[Schwabhauser] p. 71Definition 9.7df-hpg 28738  hpgbr 28740
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28745
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28744
[Schwabhauser] p. 72Theorem 9.11hpgid 28746
[Schwabhauser] p. 72Theorem 9.12hpgcom 28747
[Schwabhauser] p. 72Theorem 9.13hpgtr 28748
[Schwabhauser] p. 73Theorem 9.18colopp 28749
[Schwabhauser] p. 73Theorem 9.19colhp 28750
[Schwabhauser] p. 88Theorem 10.2lmieu 28764
[Schwabhauser] p. 88Definition 10.1df-mid 28754
[Schwabhauser] p. 89Theorem 10.4lmicom 28768
[Schwabhauser] p. 89Theorem 10.5lmilmi 28769
[Schwabhauser] p. 89Theorem 10.6lmireu 28770
[Schwabhauser] p. 89Theorem 10.7lmieq 28771
[Schwabhauser] p. 89Theorem 10.8lmiinv 28772
[Schwabhauser] p. 89Theorem 10.9lmif1o 28775
[Schwabhauser] p. 89Theorem 10.10lmiiso 28777
[Schwabhauser] p. 89Definition 10.3df-lmi 28755
[Schwabhauser] p. 90Theorem 10.11lmimot 28778
[Schwabhauser] p. 91Theorem 10.12hypcgr 28781
[Schwabhauser] p. 92Theorem 10.14lmiopp 28782
[Schwabhauser] p. 92Theorem 10.15lnperpex 28783
[Schwabhauser] p. 92Theorem 10.16trgcopy 28784  trgcopyeu 28786
[Schwabhauser] p. 95Definition 11.2dfcgra2 28810
[Schwabhauser] p. 95Definition 11.3iscgra 28789
[Schwabhauser] p. 95Proposition 11.4cgracgr 28798
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28796  cgrahl2 28797
[Schwabhauser] p. 96Theorem 11.6cgraid 28799
[Schwabhauser] p. 96Theorem 11.9cgraswap 28800
[Schwabhauser] p. 97Theorem 11.7cgracom 28802
[Schwabhauser] p. 97Theorem 11.8cgratr 28803
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28806  cgrahl 28807
[Schwabhauser] p. 98Theorem 11.13sacgr 28811
[Schwabhauser] p. 98Theorem 11.14oacgr 28812
[Schwabhauser] p. 98Theorem 11.15acopy 28813  acopyeu 28814
[Schwabhauser] p. 101Theorem 11.24inagswap 28821
[Schwabhauser] p. 101Theorem 11.25inaghl 28825
[Schwabhauser] p. 101Definition 11.23isinag 28818
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28833
[Schwabhauser] p. 102Definition 11.27df-leag 28826  isleag 28827
[Schwabhauser] p. 107Theorem 11.49tgsas 28835  tgsas1 28834  tgsas2 28836  tgsas3 28837
[Schwabhauser] p. 108Theorem 11.50tgasa 28839  tgasa1 28838
[Schwabhauser] p. 109Theorem 11.51tgsss1 28840  tgsss2 28841  tgsss3 28842
[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 19982  ablfacrp2 19983
[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 33726
[Stewart] p. 92Definition 7.4.df-constr 33713
[Stewart] p. 96Theorem 7.10constraddcl 33745  constrinvcl 33756  constrmulcl 33754  constrnegcl 33746  constrsqrtcl 33762
[Stewart] p. 97Theorem 7.11constrextdg2 33732
[Stewart] p. 98Theorem 7.12constrext2chn 33742
[Stewart] p. 99Theorem 7.132sqr3nconstr 33764
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33774
[Stoll] p. 13Definition corresponds to dfsymdif3 4265
[Stoll] p. 16Exercise 4.40dif 4364  dif0 4337
[Stoll] p. 16Exercise 4.8difdifdir 4451
[Stoll] p. 17Theorem 5.1(5)unvdif 4434
[Stoll] p. 19Theorem 5.2(13)undm 4256
[Stoll] p. 19Theorem 5.2(13')indm 4257
[Stoll] p. 20Remarkinvdif 4238
[Stoll] p. 25Definition of ordered tripledf-ot 4594
[Stoll] p. 43Definitionuniiun 5017
[Stoll] p. 44Definitionintiin 5018
[Stoll] p. 45Definitiondf-iin 4954
[Stoll] p. 45Definition indexed uniondf-iun 4953
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4265
[Strang] p. 242Section 6.3expgrowth 44317
[Suppes] p. 22Theorem 2eq0 4309  eq0f 4306
[Suppes] p. 22Theorem 4eqss 3959  eqssd 3961  eqssi 3960
[Suppes] p. 23Theorem 5ss0 4361  ss0b 4360
[Suppes] p. 23Theorem 6sstr 3952  sstrALT2 44817
[Suppes] p. 23Theorem 7pssirr 4062
[Suppes] p. 23Theorem 8pssn2lp 4063
[Suppes] p. 23Theorem 9psstr 4066
[Suppes] p. 23Theorem 10pssss 4057
[Suppes] p. 25Theorem 12elin 3927  elun 4112
[Suppes] p. 26Theorem 15inidm 4186
[Suppes] p. 26Theorem 16in0 4354
[Suppes] p. 27Theorem 23unidm 4116
[Suppes] p. 27Theorem 24un0 4353
[Suppes] p. 27Theorem 25ssun1 4137
[Suppes] p. 27Theorem 26ssequn1 4145
[Suppes] p. 27Theorem 27unss 4149
[Suppes] p. 27Theorem 28indir 4245
[Suppes] p. 27Theorem 29undir 4246
[Suppes] p. 28Theorem 32difid 4335
[Suppes] p. 29Theorem 33difin 4231
[Suppes] p. 29Theorem 34indif 4239
[Suppes] p. 29Theorem 35undif1 4435
[Suppes] p. 29Theorem 36difun2 4440
[Suppes] p. 29Theorem 37difin0 4433
[Suppes] p. 29Theorem 38disjdif 4431
[Suppes] p. 29Theorem 39difundi 4249
[Suppes] p. 29Theorem 40difindi 4251
[Suppes] p. 30Theorem 41nalset 5263
[Suppes] p. 39Theorem 61uniss 4875
[Suppes] p. 39Theorem 65uniop 5470
[Suppes] p. 41Theorem 70intsn 4944
[Suppes] p. 42Theorem 71intpr 4942  intprg 4941
[Suppes] p. 42Theorem 73op1stb 5426
[Suppes] p. 42Theorem 78intun 4940
[Suppes] p. 44Definition 15(a)dfiun2 4992  dfiun2g 4990
[Suppes] p. 44Definition 15(b)dfiin2 4993
[Suppes] p. 47Theorem 86elpw 4563  elpw2 5284  elpw2g 5283  elpwg 4562  elpwgdedVD 44899
[Suppes] p. 47Theorem 87pwid 4581
[Suppes] p. 47Theorem 89pw0 4772
[Suppes] p. 48Theorem 90pwpw0 4773
[Suppes] p. 52Theorem 101xpss12 5646
[Suppes] p. 52Theorem 102xpindi 5787  xpindir 5788
[Suppes] p. 52Theorem 103xpundi 5700  xpundir 5701
[Suppes] p. 54Theorem 105elirrv 9525
[Suppes] p. 58Theorem 2relss 5736
[Suppes] p. 59Theorem 4eldm 5854  eldm2 5855  eldm2g 5853  eldmg 5852
[Suppes] p. 59Definition 3df-dm 5641
[Suppes] p. 60Theorem 6dmin 5865
[Suppes] p. 60Theorem 8rnun 6106
[Suppes] p. 60Theorem 9rnin 6107
[Suppes] p. 60Definition 4dfrn2 5842
[Suppes] p. 61Theorem 11brcnv 5836  brcnvg 5833
[Suppes] p. 62Equation 5elcnv 5830  elcnv2 5831
[Suppes] p. 62Theorem 12relcnv 6064
[Suppes] p. 62Theorem 15cnvin 6105
[Suppes] p. 62Theorem 16cnvun 6103
[Suppes] p. 63Definitiondftrrels2 38559
[Suppes] p. 63Theorem 20co02 6221
[Suppes] p. 63Theorem 21dmcoss 5927
[Suppes] p. 63Definition 7df-co 5640
[Suppes] p. 64Theorem 26cnvco 5839
[Suppes] p. 64Theorem 27coass 6226
[Suppes] p. 65Theorem 31resundi 5953
[Suppes] p. 65Theorem 34elima 6025  elima2 6026  elima3 6027  elimag 6024
[Suppes] p. 65Theorem 35imaundi 6110
[Suppes] p. 66Theorem 40dminss 6114
[Suppes] p. 66Theorem 41imainss 6115
[Suppes] p. 67Exercise 11cnvxp 6118
[Suppes] p. 81Definition 34dfec2 8651
[Suppes] p. 82Theorem 72elec 8694  elecALTV 38248  elecg 8692
[Suppes] p. 82Theorem 73eqvrelth 38595  erth 8702  erth2 8703
[Suppes] p. 83Theorem 74eqvreldisj 38598  erdisj 8705
[Suppes] p. 83Definition 35, df-parts 38750  dfmembpart2 38755
[Suppes] p. 89Theorem 96map0b 8833
[Suppes] p. 89Theorem 97map0 8837  map0g 8834
[Suppes] p. 89Theorem 98mapsn 8838  mapsnd 8836
[Suppes] p. 89Theorem 99mapss 8839
[Suppes] p. 91Definition 12(ii)alephsuc 9997
[Suppes] p. 91Definition 12(iii)alephlim 9996
[Suppes] p. 92Theorem 1enref 8933  enrefg 8932
[Suppes] p. 92Theorem 2ensym 8951  ensymb 8950  ensymi 8952
[Suppes] p. 92Theorem 3entr 8954
[Suppes] p. 92Theorem 4unen 8994
[Suppes] p. 94Theorem 15endom 8927
[Suppes] p. 94Theorem 16ssdomg 8948
[Suppes] p. 94Theorem 17domtr 8955
[Suppes] p. 95Theorem 18sbth 9038
[Suppes] p. 97Theorem 23canth2 9071  canth2g 9072
[Suppes] p. 97Definition 3brsdom2 9042  df-sdom 8898  dfsdom2 9041
[Suppes] p. 97Theorem 21(i)sdomirr 9055
[Suppes] p. 97Theorem 22(i)domnsym 9044
[Suppes] p. 97Theorem 21(ii)sdomnsym 9043
[Suppes] p. 97Theorem 22(ii)domsdomtr 9053
[Suppes] p. 97Theorem 22(iv)brdom2 8930
[Suppes] p. 97Theorem 21(iii)sdomtr 9056
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9051
[Suppes] p. 98Exercise 4fundmen 8979  fundmeng 8980
[Suppes] p. 98Exercise 6xpdom3 9016
[Suppes] p. 98Exercise 11sdomentr 9052
[Suppes] p. 104Theorem 37fofi 9238
[Suppes] p. 104Theorem 38pwfi 9244
[Suppes] p. 105Theorem 40pwfi 9244
[Suppes] p. 111Axiom for cardinal numberscarden 10480
[Suppes] p. 130Definition 3df-tr 5210
[Suppes] p. 132Theorem 9ssonuni 7736
[Suppes] p. 134Definition 6df-suc 6326
[Suppes] p. 136Theorem Schema 22findes 7856  finds 7852  finds1 7855  finds2 7854
[Suppes] p. 151Theorem 42isfinite 9581  isfinite2 9221  isfiniteg 9224  unbnn 9219
[Suppes] p. 162Definition 5df-ltnq 10847  df-ltpq 10839
[Suppes] p. 197Theorem Schema 4tfindes 7819  tfinds 7816  tfinds2 7820
[Suppes] p. 209Theorem 18oaord1 8492
[Suppes] p. 209Theorem 21oaword2 8494
[Suppes] p. 211Theorem 25oaass 8502
[Suppes] p. 225Definition 8iscard2 9905
[Suppes] p. 227Theorem 56ondomon 10492
[Suppes] p. 228Theorem 59harcard 9907
[Suppes] p. 228Definition 12(i)aleph0 9995
[Suppes] p. 228Theorem Schema 61onintss 6372
[Suppes] p. 228Theorem Schema 62onminesb 7749  onminsb 7750
[Suppes] p. 229Theorem 64alephval2 10501
[Suppes] p. 229Theorem 65alephcard 9999
[Suppes] p. 229Theorem 66alephord2i 10006
[Suppes] p. 229Theorem 67alephnbtwn 10000
[Suppes] p. 229Definition 12df-aleph 9869
[Suppes] p. 242Theorem 6weth 10424
[Suppes] p. 242Theorem 8entric 10486
[Suppes] p. 242Theorem 9carden 10480
[Szendrei] p. 11Line 6df-cloneop 35676
[Szendrei] p. 11Paragraph 3df-suppos 35680
[TakeutiZaring] p. 8Axiom 1ax-ext 2701
[TakeutiZaring] p. 13Definition 4.5df-cleq 2721
[TakeutiZaring] p. 13Proposition 4.6df-clel 2803
[TakeutiZaring] p. 13Proposition 4.9cvjust 2723
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2749
[TakeutiZaring] p. 14Definition 4.16df-oprab 7373
[TakeutiZaring] p. 14Proposition 4.14ru 3748
[TakeutiZaring] p. 15Axiom 2zfpair 5371
[TakeutiZaring] p. 15Exercise 1elpr 4610  elpr2 4612  elpr2g 4611  elprg 4608
[TakeutiZaring] p. 15Exercise 2elsn 4600  elsn2 4625  elsn2g 4624  elsng 4599  velsn 4601
[TakeutiZaring] p. 15Exercise 3elop 5422
[TakeutiZaring] p. 15Exercise 4sneq 4595  sneqr 4800
[TakeutiZaring] p. 15Definition 5.1dfpr2 4606  dfsn2 4598  dfsn2ALT 4607
[TakeutiZaring] p. 16Axiom 3uniex 7697
[TakeutiZaring] p. 16Exercise 6opth 5431
[TakeutiZaring] p. 16Exercise 7opex 5419
[TakeutiZaring] p. 16Exercise 8rext 5403
[TakeutiZaring] p. 16Corollary 5.8unex 7700  unexg 7699
[TakeutiZaring] p. 16Definition 5.3dftp2 4651
[TakeutiZaring] p. 16Definition 5.5df-uni 4868
[TakeutiZaring] p. 16Definition 5.6df-in 3918  df-un 3916
[TakeutiZaring] p. 16Proposition 5.7unipr 4884  uniprg 4883
[TakeutiZaring] p. 17Axiom 4vpwex 5327
[TakeutiZaring] p. 17Exercise 1eltp 4649
[TakeutiZaring] p. 17Exercise 5elsuc 6392  elsucg 6390  sstr2 3950
[TakeutiZaring] p. 17Exercise 6uncom 4117
[TakeutiZaring] p. 17Exercise 7incom 4168
[TakeutiZaring] p. 17Exercise 8unass 4131
[TakeutiZaring] p. 17Exercise 9inass 4187
[TakeutiZaring] p. 17Exercise 10indi 4243
[TakeutiZaring] p. 17Exercise 11undi 4244
[TakeutiZaring] p. 17Definition 5.9df-pss 3931  df-ss 3928
[TakeutiZaring] p. 17Definition 5.10df-pw 4561
[TakeutiZaring] p. 18Exercise 7unss2 4146
[TakeutiZaring] p. 18Exercise 9dfss2 3929  sseqin2 4182
[TakeutiZaring] p. 18Exercise 10ssid 3966
[TakeutiZaring] p. 18Exercise 12inss1 4196  inss2 4197
[TakeutiZaring] p. 18Exercise 13nss 4008
[TakeutiZaring] p. 18Exercise 15unieq 4878
[TakeutiZaring] p. 18Exercise 18sspwb 5404  sspwimp 44900  sspwimpALT 44907  sspwimpALT2 44910  sspwimpcf 44902
[TakeutiZaring] p. 18Exercise 19pweqb 5411
[TakeutiZaring] p. 19Axiom 5ax-rep 5229
[TakeutiZaring] p. 20Definitiondf-rab 3403
[TakeutiZaring] p. 20Corollary 5.160ex 5257
[TakeutiZaring] p. 20Definition 5.12df-dif 3914
[TakeutiZaring] p. 20Definition 5.14dfnul2 4295
[TakeutiZaring] p. 20Proposition 5.15difid 4335
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4312  n0f 4308  neq0 4311  neq0f 4307
[TakeutiZaring] p. 21Axiom 6zfreg 9524
[TakeutiZaring] p. 21Axiom 6'zfregs 9661
[TakeutiZaring] p. 21Theorem 5.22setind 9663
[TakeutiZaring] p. 21Definition 5.20df-v 3446
[TakeutiZaring] p. 21Proposition 5.21vprc 5265
[TakeutiZaring] p. 22Exercise 10ss 4359
[TakeutiZaring] p. 22Exercise 3ssex 5271  ssexg 5273
[TakeutiZaring] p. 22Exercise 4inex1 5267
[TakeutiZaring] p. 22Exercise 5ruv 9531
[TakeutiZaring] p. 22Exercise 6elirr 9526
[TakeutiZaring] p. 22Exercise 7ssdif0 4325
[TakeutiZaring] p. 22Exercise 11difdif 4094
[TakeutiZaring] p. 22Exercise 13undif3 4259  undif3VD 44864
[TakeutiZaring] p. 22Exercise 14difss 4095
[TakeutiZaring] p. 22Exercise 15sscon 4102
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3045
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3054
[TakeutiZaring] p. 23Proposition 6.2xpex 7709  xpexg 7706
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5638
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6571
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6747  fun11 6574
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6513  svrelfun 6572
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5841
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5843
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5643
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5644
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5640
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6155  dfrel2 6150
[TakeutiZaring] p. 25Exercise 3xpss 5647
[TakeutiZaring] p. 25Exercise 5relun 5765
[TakeutiZaring] p. 25Exercise 6reluni 5772
[TakeutiZaring] p. 25Exercise 9inxp 5785
[TakeutiZaring] p. 25Exercise 12relres 5965
[TakeutiZaring] p. 25Exercise 13opelres 5945  opelresi 5947
[TakeutiZaring] p. 25Exercise 14dmres 5972
[TakeutiZaring] p. 25Exercise 15resss 5961
[TakeutiZaring] p. 25Exercise 17resabs1 5966
[TakeutiZaring] p. 25Exercise 18funres 6542
[TakeutiZaring] p. 25Exercise 24relco 6068
[TakeutiZaring] p. 25Exercise 29funco 6540
[TakeutiZaring] p. 25Exercise 30f1co 6749
[TakeutiZaring] p. 26Definition 6.10eu2 2602
[TakeutiZaring] p. 26Definition 6.11conventions 30379  df-fv 6507  fv3 6858
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7881  cnvexg 7880
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7865  dmexg 7857
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7866  rnexg 7858
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44436
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7876
[TakeutiZaring] p. 27Corollary 6.13fvex 6853
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47168  tz6.12-1-afv2 47235  tz6.12-1 6863  tz6.12-afv 47167  tz6.12-afv2 47234  tz6.12 6865  tz6.12c-afv2 47236  tz6.12c 6862
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47231  tz6.12-2 6828  tz6.12i-afv2 47237  tz6.12i 6868
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6502
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6503
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6505  wfo 6497
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6504  wf1 6496
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6506  wf1o 6498
[TakeutiZaring] p. 28Exercise 4eqfnfv 6985  eqfnfv2 6986  eqfnfv2f 6989
[TakeutiZaring] p. 28Exercise 5fvco 6941
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7173
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7171
[TakeutiZaring] p. 29Exercise 9funimaex 6588  funimaexg 6587
[TakeutiZaring] p. 29Definition 6.18df-br 5103
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5540
[TakeutiZaring] p. 30Definition 6.21dffr2 5592  dffr3 6059  eliniseg 6054  iniseg 6057
[TakeutiZaring] p. 30Definition 6.22df-eprel 5531
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5608  fr3nr 7728  frirr 5607
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5584
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7730
[TakeutiZaring] p. 31Exercise 1frss 5595
[TakeutiZaring] p. 31Exercise 4wess 5617
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6308  tz6.26i 6309  wefrc 5625  wereu2 5628
[TakeutiZaring] p. 32Theorem 6.27wfi 6310  wfii 6311
[TakeutiZaring] p. 32Definition 6.28df-isom 6508
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7286
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7287
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7293
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7294
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7295
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7299
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7306
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7308
[TakeutiZaring] p. 35Notationwtr 5209
[TakeutiZaring] p. 35Theorem 7.2trelpss 44437  tz7.2 5614
[TakeutiZaring] p. 35Definition 7.1dftr3 5215
[TakeutiZaring] p. 36Proposition 7.4ordwe 6333
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6341
[TakeutiZaring] p. 36Proposition 7.6ordelord 6342  ordelordALT 44520  ordelordALTVD 44849
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6348  ordelssne 6347
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6346
[TakeutiZaring] p. 37Proposition 7.9ordin 6350
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7738
[TakeutiZaring] p. 38Corollary 7.15ordsson 7739
[TakeutiZaring] p. 38Definition 7.11df-on 6324
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6352
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44532  ordon 7733
[TakeutiZaring] p. 38Proposition 7.13onprc 7734
[TakeutiZaring] p. 39Theorem 7.17tfi 7809
[TakeutiZaring] p. 40Exercise 3ontr2 6368
[TakeutiZaring] p. 40Exercise 7dftr2 5211
[TakeutiZaring] p. 40Exercise 9onssmin 7748
[TakeutiZaring] p. 40Exercise 11unon 7786
[TakeutiZaring] p. 40Exercise 12ordun 6426
[TakeutiZaring] p. 40Exercise 14ordequn 6425
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7735
[TakeutiZaring] p. 40Proposition 7.20elssuni 4897
[TakeutiZaring] p. 41Definition 7.22df-suc 6326
[TakeutiZaring] p. 41Proposition 7.23sssucid 6402  sucidg 6403
[TakeutiZaring] p. 41Proposition 7.24onsuc 7767
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6416  ordnbtwn 6415
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7783
[TakeutiZaring] p. 42Exercise 1df-lim 6325
[TakeutiZaring] p. 42Exercise 4omssnlim 7837
[TakeutiZaring] p. 42Exercise 7ssnlim 7842
[TakeutiZaring] p. 42Exercise 8onsucssi 7797  ordelsuc 7775
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7777
[TakeutiZaring] p. 42Definition 7.27nlimon 7807
[TakeutiZaring] p. 42Definition 7.28dfom2 7824
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7845
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7846
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7847
[TakeutiZaring] p. 43Remarkomon 7834
[TakeutiZaring] p. 43Axiom 7inf3 9564  omex 9572
[TakeutiZaring] p. 43Theorem 7.32ordom 7832
[TakeutiZaring] p. 43Corollary 7.31find 7851
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7848
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7849
[TakeutiZaring] p. 44Exercise 1limomss 7827
[TakeutiZaring] p. 44Exercise 2int0 4922
[TakeutiZaring] p. 44Exercise 3trintss 5228
[TakeutiZaring] p. 44Exercise 4intss1 4923
[TakeutiZaring] p. 44Exercise 5intex 5294
[TakeutiZaring] p. 44Exercise 6oninton 7751
[TakeutiZaring] p. 44Exercise 11ordintdif 6371
[TakeutiZaring] p. 44Definition 7.35df-int 4907
[TakeutiZaring] p. 44Proposition 7.34noinfep 9589
[TakeutiZaring] p. 45Exercise 4onint 7746
[TakeutiZaring] p. 47Lemma 1tfrlem1 8321
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8342
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8343
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8344
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8351  tz7.44-2 8352  tz7.44-3 8353
[TakeutiZaring] p. 50Exercise 1smogt 8313
[TakeutiZaring] p. 50Exercise 3smoiso 8308
[TakeutiZaring] p. 50Definition 7.46df-smo 8292
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8390  tz7.49c 8391
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8388
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8387
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8389
[TakeutiZaring] p. 53Proposition 7.532eu5 2649
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9940
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9941
[TakeutiZaring] p. 56Definition 8.1oalim 8473  oasuc 8465
[TakeutiZaring] p. 57Remarktfindsg 7817
[TakeutiZaring] p. 57Proposition 8.2oacl 8476
[TakeutiZaring] p. 57Proposition 8.3oa0 8457  oa0r 8479
[TakeutiZaring] p. 57Proposition 8.16omcl 8477
[TakeutiZaring] p. 58Corollary 8.5oacan 8489
[TakeutiZaring] p. 58Proposition 8.4nnaord 8560  nnaordi 8559  oaord 8488  oaordi 8487
[TakeutiZaring] p. 59Proposition 8.6iunss2 5008  uniss2 4901
[TakeutiZaring] p. 59Proposition 8.7oawordri 8491
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8496  oawordex 8498
[TakeutiZaring] p. 59Proposition 8.9nnacl 8552
[TakeutiZaring] p. 59Proposition 8.10oaabs 8589
[TakeutiZaring] p. 60Remarkoancom 9580
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8501
[TakeutiZaring] p. 62Exercise 1nnarcl 8557
[TakeutiZaring] p. 62Exercise 5oaword1 8493
[TakeutiZaring] p. 62Definition 8.15om0x 8460  omlim 8474  omsuc 8467
[TakeutiZaring] p. 62Definition 8.15(a)om0 8458
[TakeutiZaring] p. 63Proposition 8.17nnecl 8554  nnmcl 8553
[TakeutiZaring] p. 63Proposition 8.19nnmord 8573  nnmordi 8572  omord 8509  omordi 8507
[TakeutiZaring] p. 63Proposition 8.20omcan 8510
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8577  omwordri 8513
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8480
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8483  om1r 8484
[TakeutiZaring] p. 64Proposition 8.22om00 8516
[TakeutiZaring] p. 64Proposition 8.23omordlim 8518
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8519
[TakeutiZaring] p. 64Proposition 8.25odi 8520
[TakeutiZaring] p. 65Theorem 8.26omass 8521
[TakeutiZaring] p. 67Definition 8.30nnesuc 8549  oe0 8463  oelim 8475  oesuc 8468  onesuc 8471
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8461
[TakeutiZaring] p. 67Proposition 8.32oen0 8527
[TakeutiZaring] p. 67Proposition 8.33oeordi 8528
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8462
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8486
[TakeutiZaring] p. 68Corollary 8.34oeord 8529
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8535
[TakeutiZaring] p. 68Proposition 8.35oewordri 8533
[TakeutiZaring] p. 68Proposition 8.37oeworde 8534
[TakeutiZaring] p. 69Proposition 8.41oeoa 8538
[TakeutiZaring] p. 70Proposition 8.42oeoe 8540
[TakeutiZaring] p. 73Theorem 9.1trcl 9657  tz9.1 9658
[TakeutiZaring] p. 76Definition 9.9df-r1 9693  r10 9697  r1lim 9701  r1limg 9700  r1suc 9699  r1sucg 9698
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9709  r1ord2 9710  r1ordg 9707
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9719
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9744  tz9.13 9720  tz9.13g 9721
[TakeutiZaring] p. 79Definition 9.14df-rank 9694  rankval 9745  rankvalb 9726  rankvalg 9746
[TakeutiZaring] p. 79Proposition 9.16rankel 9768  rankelb 9753
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9782  rankval3 9769  rankval3b 9755
[TakeutiZaring] p. 79Proposition 9.18rankonid 9758
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9724
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9763  rankr1c 9750  rankr1g 9761
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9764
[TakeutiZaring] p. 80Exercise 1rankss 9778  rankssb 9777
[TakeutiZaring] p. 80Exercise 2unbndrank 9771
[TakeutiZaring] p. 80Proposition 9.19bndrank 9770
[TakeutiZaring] p. 83Axiom of Choiceac4 10404  dfac3 10050
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9959  numth 10401  numth2 10400
[TakeutiZaring] p. 85Definition 10.4cardval 10475
[TakeutiZaring] p. 85Proposition 10.5cardid 10476  cardid2 9882
[TakeutiZaring] p. 85Proposition 10.9oncard 9889
[TakeutiZaring] p. 85Proposition 10.10carden 10480
[TakeutiZaring] p. 85Proposition 10.11cardidm 9888
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9873
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9894
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9886
[TakeutiZaring] p. 87Proposition 10.15pwen 9091
[TakeutiZaring] p. 88Exercise 1en0 8966
[TakeutiZaring] p. 88Exercise 7infensuc 9096
[TakeutiZaring] p. 89Exercise 10omxpen 9020
[TakeutiZaring] p. 90Corollary 10.23cardnn 9892
[TakeutiZaring] p. 90Definition 10.27alephiso 10027
[TakeutiZaring] p. 90Proposition 10.20nneneq 9147
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9155
[TakeutiZaring] p. 90Proposition 10.26alephprc 10028
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9152
[TakeutiZaring] p. 91Exercise 2alephle 10017
[TakeutiZaring] p. 91Exercise 3aleph0 9995
[TakeutiZaring] p. 91Exercise 4cardlim 9901
[TakeutiZaring] p. 91Exercise 7infpss 10145
[TakeutiZaring] p. 91Exercise 8infcntss 9249
[TakeutiZaring] p. 91Definition 10.29df-fin 8899  isfi 8924
[TakeutiZaring] p. 92Proposition 10.32onfin 9156
[TakeutiZaring] p. 92Proposition 10.34imadomg 10463
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9013
[TakeutiZaring] p. 93Proposition 10.35fodomb 10455
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10115  unxpdom 9176
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9903  cardsdomelir 9902
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9178
[TakeutiZaring] p. 94Proposition 10.39infxpen 9943
[TakeutiZaring] p. 95Definition 10.42df-map 8778
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10491  infxpidm2 9946
[TakeutiZaring] p. 95Proposition 10.41infdju 10136  infxp 10143
[TakeutiZaring] p. 96Proposition 10.44pw2en 9025  pw2f1o 9023
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9084
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10416
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10411  ac6s5 10420
[TakeutiZaring] p. 98Theorem 10.47unidom 10472
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10473  uniimadomf 10474
[TakeutiZaring] p. 100Definition 11.1cfcof 10203
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10198
[TakeutiZaring] p. 102Exercise 1cfle 10183
[TakeutiZaring] p. 102Exercise 2cf0 10180
[TakeutiZaring] p. 102Exercise 3cfsuc 10186
[TakeutiZaring] p. 102Exercise 4cfom 10193
[TakeutiZaring] p. 102Proposition 11.9coftr 10202
[TakeutiZaring] p. 103Theorem 11.15alephreg 10511
[TakeutiZaring] p. 103Proposition 11.11cardcf 10181
[TakeutiZaring] p. 103Proposition 11.13alephsing 10205
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10026
[TakeutiZaring] p. 104Proposition 11.16carduniima 10025
[TakeutiZaring] p. 104Proposition 11.18alephfp 10037  alephfp2 10038
[TakeutiZaring] p. 106Theorem 11.20gchina 10628
[TakeutiZaring] p. 106Theorem 11.21mappwen 10041
[TakeutiZaring] p. 107Theorem 11.26konigth 10498
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10512
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10513
[Tarski] p. 67Axiom B5ax-c5 38869
[Tarski] p. 67Scheme B5sp 2184
[Tarski] p. 68Lemma 6avril1 30442  equid 2012
[Tarski] p. 69Lemma 7equcomi 2017
[Tarski] p. 70Lemma 14spim 2385  spime 2387  spimew 1971
[Tarski] p. 70Lemma 16ax-12 2178  ax-c15 38875  ax12i 1966
[Tarski] p. 70Lemmas 16 and 17sb6 2086
[Tarski] p. 75Axiom B7ax6v 1968
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1910  ax5ALT 38893
[Tarski], p. 75Scheme B8 of system S2ax-7 2008  ax-8 2111  ax-9 2119
[Tarski1999] p. 178Axiom 4axtgsegcon 28444
[Tarski1999] p. 178Axiom 5axtg5seg 28445
[Tarski1999] p. 179Axiom 7axtgpasch 28447
[Tarski1999] p. 180Axiom 7.1axtgpasch 28447
[Tarski1999] p. 185Axiom 11axtgcont1 28448
[Truss] p. 114Theorem 5.18ruc 16187
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37646
[Viaclovsky8] p. 3Proposition 7ismblfin 37648
[Weierstrass] p. 272Definitiondf-mdet 22505  mdetuni 22542
[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 37426
[WhiteheadRussell] p. 100Theorem *2.05frege5 43782  imim2 58  wl-luk-imim2 37421
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47013  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2656  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37424
[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 44909  wl-luk-notnotr 37425
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43812  axfrege28 43811  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 37418
[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 30380  pm2.27 42  wl-luk-pm2.27 37416
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38338
[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 44340
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44341
[WhiteheadRussell] p. 147Theorem *10.2219.26 1870
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44342
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44343
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44344
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1893
[WhiteheadRussell] p. 151Theorem *10.301albitr 44345
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44346
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44347
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44348
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44349
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44351
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44352
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44353
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44350
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2091
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44356
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44357
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2071
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2161
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1829
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1830
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44358
[WhiteheadRussell] p. 162Theorem *11.322alim 44359
[WhiteheadRussell] p. 162Theorem *11.332albi 44360
[WhiteheadRussell] p. 162Theorem *11.342exim 44361
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44363
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44362
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1887
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44365
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44366
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44364
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1828
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44367
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44368
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1846
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44369
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2344
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1860
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44374
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44370
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44371
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44372
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44373
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44378
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44375
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44376
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44377
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44379
[WhiteheadRussell] p. 175Definition *14.02df-eu 2562
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44389  pm13.13b 44390
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44391
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3006
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3007
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3629
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44397
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44398
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44392
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44535  pm13.193 44393
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44394
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44395
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44396
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44403
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44402
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44401
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3813
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44404  pm14.122b 44405  pm14.122c 44406
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44407  pm14.123b 44408  pm14.123c 44409
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44411
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44410
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44412
[WhiteheadRussell] p. 190Theorem *14.22iota4 6480
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44413
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6481
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44414
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44416
[WhiteheadRussell] p. 192Theorem *14.26eupick 2626  eupickbi 2629  sbaniota 44417
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44415
[WhiteheadRussell] p. 192Theorem *14.271eubi 2577
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44419
[WhiteheadRussell] p. 235Definition *30.01conventions 30379  df-fv 6507
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9930  pm54.43lem 9929
[Young] p. 141Definition of operator orderingleop2 32103
[Young] p. 142Example 12.2(i)0leop 32109  idleop 32110
[vandenDries] p. 42Lemma 61irrapx1 42809
[vandenDries] p. 43Theorem 62pellex 42816  pellexlem1 42810

This page was last updated on 25-Dec-2025.
Copyright terms: Public domain