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. 28Proposition 3.10sectcan 13674
[Adamek] p. 29Proposition 3.14(1)invinv 13688
[Adamek] p. 29Proposition 3.14(2)invco 13689  isoco 13691
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 26293
[AitkenIBCG] p. 3Definition 2df-angtrg 26289  df-trcng 26292
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 26165  df-ig2 26164
[AitkenIBG] p. 2Definition 4df-li 26180
[AitkenIBG] p. 3Definition 5df-col 26194
[AitkenIBG] p. 3Definition 6df-con2 26199
[AitkenIBG] p. 3Proposition 4isconcl5a 26204  isconcl5ab 26205  isconcl6a 26206  isconcl6ab 26207
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 26212
[AitkenIBG] p. 4Exercise 5tpne 26178
[AitkenIBG] p. 4Definition 8df-seg2 26234
[AitkenIBG] p. 4Definition 10df-sside 26266
[AitkenIBG] p. 4Definition 11df-ray2 26255
[AitkenIBG] p. 10Definition 17df-angle 26261
[AitkenIBG] p. 15Definition 23df-triangle 26263
[AitkenIBG] p. 15Definition 24df-cnvx 26282
[AitkenNG] p. 2Definition 1df-slices 26296
[AitkenNG] p. 2Definition 2df-Cut 26298
[AitkenNG] p. 3Axiom of Dedekinddf-neug 26300
[AitkenNG] p. 4Definition 5df-crcl 26302
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18233  df-nmoo 21339
[AkhiezerGlazman] p. 64Theoremhmopidmch 22749  hmopidmchi 22747
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22797  pjcmul2i 22798
[AkhiezerGlazman] p. 72Theoremcnvunop 22514  unoplin 22516
[AkhiezerGlazman] p. 72Equation 2unopadj 22515  unopadj2 22534
[AkhiezerGlazman] p. 73Theoremelunop2 22609  lnopunii 22608
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22682
[Apostol] p. 18Theorem I.1addcan 9012  addcan2d 9032  addcan2i 9022  addcand 9031  addcani 9021
[Apostol] p. 18Theorem I.2negeu 9058
[Apostol] p. 18Theorem I.3negsub 9111  negsubd 9179  negsubi 9140
[Apostol] p. 18Theorem I.4negneg 9113  negnegd 9164  negnegi 9132
[Apostol] p. 18Theorem I.5subdi 9229  subdid 9251  subdii 9244  subdir 9230  subdird 9252  subdiri 9245
[Apostol] p. 18Theorem I.6mul01 9007  mul01d 9027  mul01i 9018  mul02 9006  mul02d 9026  mul02i 9017
[Apostol] p. 18Theorem I.7mulcan 9421  mulcan2d 9418  mulcand 9417  mulcani 9423
[Apostol] p. 18Theorem I.8receu 9429  xreceu 23121
[Apostol] p. 18Theorem I.9divrec 9456  divrecd 9555  divreci 9521  divreczi 9514
[Apostol] p. 18Theorem I.10recrec 9473  recreci 9508
[Apostol] p. 18Theorem I.11mul0or 9424  mul0ord 9434  mul0ori 9432
[Apostol] p. 18Theorem I.12mul2neg 9235  mul2negd 9250  mul2negi 9243  mulneg1 9232  mulneg1d 9248  mulneg1i 9241
[Apostol] p. 18Theorem I.13divadddiv 9491  divadddivd 9596  divadddivi 9538
[Apostol] p. 18Theorem I.14divmuldiv 9476  divmuldivd 9593  divmuldivi 9536
[Apostol] p. 18Theorem I.15divdivdiv 9477  divdivdivd 9599  divdivdivi 9539
[Apostol] p. 20Axiom 7rpaddcl 10390  rpaddcld 10421  rpmulcl 10391  rpmulcld 10422
[Apostol] p. 20Axiom 8rpneg 10399
[Apostol] p. 20Axiom 90nrp 10400
[Apostol] p. 20Theorem I.17lttri 8961
[Apostol] p. 20Theorem I.18ltadd1d 9381  ltadd1dd 9399  ltadd1i 9343
[Apostol] p. 20Theorem I.19ltmul1 9622  ltmul1a 9621  ltmul1i 9691  ltmul1ii 9701  ltmul2 9623  ltmul2d 10444  ltmul2dd 10458  ltmul2i 9694
[Apostol] p. 20Theorem I.20msqgt0 9310  msqgt0d 9356  msqgt0i 9326
[Apostol] p. 20Theorem I.210lt1 9312
[Apostol] p. 20Theorem I.23lt0neg1 9296  lt0neg1d 9358  ltneg 9290  ltnegd 9366  ltnegi 9333
[Apostol] p. 20Theorem I.25lt2add 9275  lt2addd 9410  lt2addi 9351
[Apostol] p. 20Definition of positive numbersdf-rp 10371
[Apostol] p. 21Exercise 4recgt0 9616  recgt0d 9707  recgt0i 9677  recgt0ii 9678
[Apostol] p. 22Definition of integersdf-z 10041
[Apostol] p. 22Definition of positive integersdfnn3 9776
[Apostol] p. 22Definition of rationalsdf-q 10333
[Apostol] p. 24Theorem I.26supeu 7221
[Apostol] p. 26Theorem I.28nnunb 9977
[Apostol] p. 26Theorem I.29arch 9978
[Apostol] p. 28Exercise 2btwnz 10130
[Apostol] p. 28Exercise 3nnrecl 9979
[Apostol] p. 28Exercise 4rebtwnz 10331
[Apostol] p. 28Exercise 5zbtwnre 10330
[Apostol] p. 28Exercise 6qbtwnre 10542
[Apostol] p. 28Exercise 10(a)zneo 10110
[Apostol] p. 29Theorem I.35msqsqrd 11938  resqrth 11757  sqrth 11864  sqrthi 11870  sqsqrd 11937
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9765
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10300
[Apostol] p. 361Remarkcrreczi 11242
[Apostol] p. 363Remarkabsgt0i 11898
[Apostol] p. 363Exampleabssubd 11951  abssubi 11902
[Baer] p. 40Property (b)mapdord 32450
[Baer] p. 40Property (c)mapd11 32451
[Baer] p. 40Property (e)mapdin 32474  mapdlsm 32476
[Baer] p. 40Property (f)mapd0 32477
[Baer] p. 40Definition of projectivitydf-mapd 32437  mapd1o 32460
[Baer] p. 41Property (g)mapdat 32479
[Baer] p. 44Part (1)mapdpg 32518
[Baer] p. 45Part (2)hdmap1eq 32614  mapdheq 32540  mapdheq2 32541  mapdheq2biN 32542
[Baer] p. 45Part (3)baerlem3 32525
[Baer] p. 46Part (4)mapdheq4 32544  mapdheq4lem 32543
[Baer] p. 46Part (5)baerlem5a 32526  baerlem5abmN 32530  baerlem5amN 32528  baerlem5b 32527  baerlem5bmN 32529
[Baer] p. 47Part (6)hdmap1l6 32634  hdmap1l6a 32622  hdmap1l6e 32627  hdmap1l6f 32628  hdmap1l6g 32629  hdmap1l6lem1 32620  hdmap1l6lem2 32621  hdmap1p6N 32635  mapdh6N 32559  mapdh6aN 32547  mapdh6eN 32552  mapdh6fN 32553  mapdh6gN 32554  mapdh6lem1N 32545  mapdh6lem2N 32546
[Baer] p. 48Part 9hdmapval 32643
[Baer] p. 48Part 10hdmap10 32655
[Baer] p. 48Part 11hdmapadd 32658
[Baer] p. 48Part (6)hdmap1l6h 32630  mapdh6hN 32555
[Baer] p. 48Part (7)mapdh75cN 32565  mapdh75d 32566  mapdh75e 32564  mapdh75fN 32567  mapdh7cN 32561  mapdh7dN 32562  mapdh7eN 32560  mapdh7fN 32563
[Baer] p. 48Part (8)mapdh8 32601  mapdh8a 32587  mapdh8aa 32588  mapdh8ab 32589  mapdh8ac 32590  mapdh8ad 32591  mapdh8b 32592  mapdh8c 32593  mapdh8d 32595  mapdh8d0N 32594  mapdh8e 32596  mapdh8fN 32597  mapdh8g 32598  mapdh8i 32599  mapdh8j 32600
[Baer] p. 48Part (9)mapdh9a 32602
[Baer] p. 48Equation 10mapdhvmap 32581
[Baer] p. 49Part 12hdmap11 32663  hdmapeq0 32659  hdmapf1oN 32680  hdmapneg 32661  hdmaprnN 32679  hdmaprnlem1N 32664  hdmaprnlem3N 32665  hdmaprnlem3uN 32666  hdmaprnlem4N 32668  hdmaprnlem6N 32669  hdmaprnlem7N 32670  hdmaprnlem8N 32671  hdmaprnlem9N 32672  hdmapsub 32662
[Baer] p. 49Part 14hdmap14lem1 32683  hdmap14lem10 32692  hdmap14lem1a 32681  hdmap14lem2N 32684  hdmap14lem2a 32682  hdmap14lem3 32685  hdmap14lem8 32690  hdmap14lem9 32691
[Baer] p. 50Part 14hdmap14lem11 32693  hdmap14lem12 32694  hdmap14lem13 32695  hdmap14lem14 32696  hdmap14lem15 32697  hgmapval 32702
[Baer] p. 50Part 15hgmapadd 32709  hgmapmul 32710  hgmaprnlem2N 32712  hgmapvs 32706
[Baer] p. 50Part 16hgmaprnN 32716
[Baer] p. 110Lemma 1hdmapip0com 32732
[Baer] p. 110Line 27hdmapinvlem1 32733
[Baer] p. 110Line 28hdmapinvlem2 32734
[Baer] p. 110Line 30hdmapinvlem3 32735
[Baer] p. 110Part 1.2hdmapglem5 32737  hgmapvv 32741
[Baer] p. 110Proposition 1hdmapinvlem4 32736
[Baer] p. 111Line 10hgmapvvlem1 32738
[Baer] p. 111Line 15hdmapg 32745  hdmapglem7 32744
[BellMachover] p. 36Lemma 10.3id1 20
[BellMachover] p. 97Definition 10.1df-eu 2160
[BellMachover] p. 460Notationdf-mo 2161
[BellMachover] p. 460Definitionmo3 2187
[BellMachover] p. 461Axiom Extax-ext 2277
[BellMachover] p. 462Theorem 1.1bm1.1 2281
[BellMachover] p. 463Axiom Repaxrep5 4152
[BellMachover] p. 463Scheme Sepaxsep 4156
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4160
[BellMachover] p. 466Axiom Powaxpow3 4207
[BellMachover] p. 466Axiom Unionaxun2 4530
[BellMachover] p. 468Definitiondf-ord 4411
[BellMachover] p. 469Theorem 2.2(i)ordirr 4426
[BellMachover] p. 469Theorem 2.2(iii)onelon 4433
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4428
[BellMachover] p. 471Definition of Ndf-om 4673
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4613
[BellMachover] p. 471Definition of Limdf-lim 4413
[BellMachover] p. 472Axiom Infzfinf2 7359
[BellMachover] p. 473Theorem 2.8limom 4687
[BellMachover] p. 477Equation 3.1df-r1 7452
[BellMachover] p. 478Definitionrankval2 7506
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7470  r1ord3g 7467
[BellMachover] p. 480Axiom Regzfreg2 7326
[BellMachover] p. 488Axiom ACac5 8120  dfac4 7765
[BellMachover] p. 490Definition of alephalephval3 7753
[BeltramettiCassinelli] p. 98Remarkatlatmstc 30131
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22949
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22991  chirredi 22990
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22979
[Beran] p. 3Definition of joinsshjval3 21949
[Beran] p. 39Theorem 2.3(i)cmcm2 22211  cmcm2i 22188  cmcm2ii 22193  cmt2N 30062
[Beran] p. 40Theorem 2.3(iii)lecm 22212  lecmi 22197  lecmii 22198
[Beran] p. 45Theorem 3.4cmcmlem 22186
[Beran] p. 49Theorem 4.2cm2j 22215  cm2ji 22220  cm2mi 22221
[Beran] p. 95Definitiondf-sh 21802  issh2 21804
[Beran] p. 95Lemma 3.1(S5)his5 21681
[Beran] p. 95Lemma 3.1(S6)his6 21694
[Beran] p. 95Lemma 3.1(S7)his7 21685
[Beran] p. 95Lemma 3.2(S8)ho01i 22424
[Beran] p. 95Lemma 3.2(S9)hoeq1 22426
[Beran] p. 95Lemma 3.2(S10)ho02i 22425
[Beran] p. 95Lemma 3.2(S11)hoeq2 22427
[Beran] p. 95Postulate (S1)ax-his1 21677  his1i 21695
[Beran] p. 95Postulate (S2)ax-his2 21678
[Beran] p. 95Postulate (S3)ax-his3 21679
[Beran] p. 95Postulate (S4)ax-his4 21680
[Beran] p. 96Definition of normdf-hnorm 21564  dfhnorm2 21717  normval 21719
[Beran] p. 96Definition for Cauchy sequencehcau 21779
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21569
[Beran] p. 96Definition of complete subspaceisch3 21837
[Beran] p. 96Definition of convergedf-hlim 21568  hlimi 21783
[Beran] p. 97Theorem 3.3(i)norm-i-i 21728  norm-i 21724
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21732  norm-ii 21733  normlem0 21704  normlem1 21705  normlem2 21706  normlem3 21707  normlem4 21708  normlem5 21709  normlem6 21710  normlem7 21711  normlem7tALT 21714
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21734  norm-iii 21735
[Beran] p. 98Remark 3.4bcs 21776  bcsiALT 21774  bcsiHIL 21775
[Beran] p. 98Remark 3.4(B)normlem9at 21716  normpar 21750  normpari 21749
[Beran] p. 98Remark 3.4(C)normpyc 21741  normpyth 21740  normpythi 21737
[Beran] p. 99Remarklnfn0 22643  lnfn0i 22638  lnop0 22562  lnop0i 22566
[Beran] p. 99Theorem 3.5(i)nmcexi 22622  nmcfnex 22649  nmcfnexi 22647  nmcopex 22625  nmcopexi 22623
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22650  nmcfnlbi 22648  nmcoplb 22626  nmcoplbi 22624
[Beran] p. 99Theorem 3.5(iii)lnfncon 22652  lnfnconi 22651  lnopcon 22631  lnopconi 22630
[Beran] p. 100Lemma 3.6normpar2i 21751
[Beran] p. 101Lemma 3.6norm3adifi 21748  norm3adifii 21743  norm3dif 21745  norm3difi 21742
[Beran] p. 102Theorem 3.7(i)chocunii 21896  pjhth 21988  pjhtheu 21989  pjpjhth 22020  pjpjhthi 22021  pjth 18819
[Beran] p. 102Theorem 3.7(ii)ococ 22001  ococi 22000
[Beran] p. 103Remark 3.8nlelchi 22657
[Beran] p. 104Theorem 3.9riesz3i 22658  riesz4 22660  riesz4i 22659
[Beran] p. 104Theorem 3.10cnlnadj 22675  cnlnadjeu 22674  cnlnadjeui 22673  cnlnadji 22672  cnlnadjlem1 22663  nmopadjlei 22684
[Beran] p. 106Theorem 3.11(i)adjeq0 22687
[Beran] p. 106Theorem 3.11(v)nmopadji 22686
[Beran] p. 106Theorem 3.11(ii)adjmul 22688
[Beran] p. 106Theorem 3.11(iv)adjadj 22532
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22698  nmopcoadji 22697
[Beran] p. 106Theorem 3.11(iii)adjadd 22689
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22699
[Beran] p. 106Theorem 3.11(viii)adjcoi 22696  pjadj2coi 22800  pjadjcoi 22757
[Beran] p. 107Definitiondf-ch 21817  isch2 21819
[Beran] p. 107Remark 3.12choccl 21901  isch3 21837  occl 21899  ocsh 21878  shoccl 21900  shocsh 21879
[Beran] p. 107Remark 3.12(B)ococin 22003
[Beran] p. 108Theorem 3.13chintcl 21927
[Beran] p. 109Property (i)pjadj2 22783  pjadj3 22784  pjadji 22280  pjadjii 22269
[Beran] p. 109Property (ii)pjidmco 22777  pjidmcoi 22773  pjidmi 22268
[Beran] p. 110Definition of projector orderingpjordi 22769
[Beran] p. 111Remarkho0val 22346  pjch1 22265
[Beran] p. 111Definitiondf-hfmul 22330  df-hfsum 22329  df-hodif 22328  df-homul 22327  df-hosum 22326
[Beran] p. 111Lemma 4.4(i)pjo 22266
[Beran] p. 111Lemma 4.4(ii)pjch 22289  pjchi 22027
[Beran] p. 111Lemma 4.4(iii)pjoc2 22034  pjoc2i 22033
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22275
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22761  pjssmii 22276
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22760
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22759
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22764
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22762  pjssge0ii 22277
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22763  pjdifnormii 22278
[Bollobas] p. 4Definitiondf-wlk 28319
[Bollobas] p. 5Notationdf-pth 28321
[Bollobas] p. 5Definitiondf-crct 28323  df-cycl 28324  df-trail 28320  df-wlkon 28325
[BourbakiEns] p. Proposition 8fcof1 5813  fcofo 5814
[BourbakiFVR] p. Definition 1isder 25810
[BourbakiTop1] p. Remarkxnegmnf 10553  xnegpnf 10552
[BourbakiTop1] p. Remark rexneg 10554
[BourbakiTop1] p. Theoremneiss 16862
[BourbakiTop1] p. Axiom GT'tgpsubcn 17789
[BourbakiTop1] p. Example 1snfil 17575
[BourbakiTop1] p. Example 2neifil 17591
[BourbakiTop1] p. Definitionistgp 17776
[BourbakiTop1] p. Propositioncnpco 17012  ishmeo 17466  neips 16866
[BourbakiTop1] p. Definition 1filintn0 17572
[BourbakiTop1] p. Proposition 9cnpflf2 17711
[BourbakiTop1] p. Theorem 1 (d)iscncl 17014
[BourbakiTop1] p. Proposition Vissnei2 16869
[BourbakiTop1] p. Definition C'''df-cmp 17130
[BourbakiTop1] p. Proposition Viiinnei 16878
[BourbakiTop1] p. Proposition Vivneissex 16880
[BourbakiTop1] p. Proposition Viiielnei 16864  ssnei 16863
[BourbakiTop1] p. Remark below def. 1filn0 17573
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17557
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17574
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27916  stoweid 27915
[BrosowskiDeutsh] p. 89Theorem for the non-trivial casestoweidlem62 27914
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27853  stoweidlem10 27862  stoweidlem14 27866  stoweidlem15 27867  stoweidlem35 27887  stoweidlem36 27888  stoweidlem37 27889  stoweidlem38 27890  stoweidlem40 27892  stoweidlem41 27893  stoweidlem43 27895  stoweidlem44 27896  stoweidlem46 27898  stoweidlem5 27857  stoweidlem50 27902  stoweidlem52 27904  stoweidlem53 27905  stoweidlem55 27907  stoweidlem56 27908
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27875  stoweidlem24 27876  stoweidlem27 27879  stoweidlem28 27880  stoweidlem30 27882
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27897  stoweidlem49 27901  stoweidlem7 27859
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27883  stoweidlem39 27891  stoweidlem42 27894  stoweidlem48 27900  stoweidlem51 27903  stoweidlem54 27906  stoweidlem57 27909  stoweidlem58 27910
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27877
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27886
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27869
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27911
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27912
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27870
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27863  stoweidlem26 27878
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27865
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27913
[ChoquetDD] p. 2Definition of mappingdf-mpt 4095
[Clemente] p. 10Definition ITnatded 20806
[Clemente] p. 10Definition I` `m,nnatded 20806
[Clemente] p. 11Definition E=>m,nnatded 20806
[Clemente] p. 11Definition I=>m,nnatded 20806
[Clemente] p. 11Definition E` `(1)natded 20806
[Clemente] p. 11Definition E` `(2)natded 20806
[Clemente] p. 12Definition E` `m,n,pnatded 20806
[Clemente] p. 12Definition I` `n(1)natded 20806
[Clemente] p. 12Definition I` `n(2)natded 20806
[Clemente] p. 13Definition I` `m,n,pnatded 20806
[Clemente] p. 14Definition E` `nnatded 20806
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 20808  ex-natded5.2 20807
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 20811  ex-natded5.3 20810
[Clemente] p. 18Theorem 5.5ex-natded5.5 20813
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 20815  ex-natded5.7 20814
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 20817  ex-natded5.8 20816
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 20819  ex-natded5.13 20818
[Clemente] p. 32Definition I` `nnatded 20806
[Clemente] p. 32Definition E` `m,n,p,anatded 20806
[Clemente] p. 32Definition E` `n,tnatded 20806
[Clemente] p. 32Definition I` `n,tnatded 20806
[Clemente] p. 43Theorem 9.20ex-natded9.20 20820
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 20821
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 20823  ex-natded9.26 20822
[Cohen] p. 301Remarkrelogoprlem 19960
[Cohen] p. 301Property 2relogmul 19961  relogmuld 19992
[Cohen] p. 301Property 3relogdiv 19962  relogdivd 19993
[Cohen] p. 301Property 4relogexp 19965
[Cohen] p. 301Property 1alog1 19955
[Cohen] p. 301Property 1bloge 19956
[Cohn] p. 81Section II.5acsdomd 14300  acsinfd 14299  acsinfdimd 14301  acsmap2d 14298  acsmapd 14297
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10981
[Crawley] p. 1Definition of posetdf-poset 14096
[Crawley] p. 107Theorem 13.2hlsupr 30197
[Crawley] p. 110Theorem 13.3arglem1N 31001  dalaw 30697
[Crawley] p. 111Theorem 13.4hlathil 32776
[Crawley] p. 111Definition of set Wdf-watsN 30801
[Crawley] p. 111Definition of dilationdf-dilN 30917  df-ldil 30915  isldil 30921
[Crawley] p. 111Definition of translationdf-ltrn 30916  df-trnN 30918  isltrn 30930  ltrnu 30932
[Crawley] p. 112Lemma Acdlema1N 30602  cdlema2N 30603  exatleN 30215
[Crawley] p. 112Lemma B1cvrat 30287  cdlemb 30605  cdlemb2 30852  cdlemb3 31417  idltrn 30961  l1cvat 29867  lhpat 30854  lhpat2 30856  lshpat 29868  ltrnel 30950  ltrnmw 30962
[Crawley] p. 112Lemma Ccdlemc1 31002  cdlemc2 31003  ltrnnidn 30985  trlat 30980  trljat1 30977  trljat2 30978  trljat3 30979  trlne 30996  trlnidat 30984  trlnle 30997
[Crawley] p. 112Definition of automorphismdf-pautN 30802
[Crawley] p. 113Lemma Ccdlemc 31008  cdlemc3 31004  cdlemc4 31005
[Crawley] p. 113Lemma Dcdlemd 31018  cdlemd1 31009  cdlemd2 31010  cdlemd3 31011  cdlemd4 31012  cdlemd5 31013  cdlemd6 31014  cdlemd7 31015  cdlemd8 31016  cdlemd9 31017  cdleme31sde 31196  cdleme31se 31193  cdleme31se2 31194  cdleme31snd 31197  cdleme32a 31252  cdleme32b 31253  cdleme32c 31254  cdleme32d 31255  cdleme32e 31256  cdleme32f 31257  cdleme32fva 31248  cdleme32fva1 31249  cdleme32fvcl 31251  cdleme32le 31258  cdleme48fv 31310  cdleme4gfv 31318  cdleme50eq 31352  cdleme50f 31353  cdleme50f1 31354  cdleme50f1o 31357  cdleme50laut 31358  cdleme50ldil 31359  cdleme50lebi 31351  cdleme50rn 31356  cdleme50rnlem 31355  cdlemeg49le 31322  cdlemeg49lebilem 31350
[Crawley] p. 113Lemma Ecdleme 31371  cdleme00a 31020  cdleme01N 31032  cdleme02N 31033  cdleme0a 31022  cdleme0aa 31021  cdleme0b 31023  cdleme0c 31024  cdleme0cp 31025  cdleme0cq 31026  cdleme0dN 31027  cdleme0e 31028  cdleme0ex1N 31034  cdleme0ex2N 31035  cdleme0fN 31029  cdleme0gN 31030  cdleme0moN 31036  cdleme1 31038  cdleme10 31065  cdleme10tN 31069  cdleme11 31081  cdleme11a 31071  cdleme11c 31072  cdleme11dN 31073  cdleme11e 31074  cdleme11fN 31075  cdleme11g 31076  cdleme11h 31077  cdleme11j 31078  cdleme11k 31079  cdleme11l 31080  cdleme12 31082  cdleme13 31083  cdleme14 31084  cdleme15 31089  cdleme15a 31085  cdleme15b 31086  cdleme15c 31087  cdleme15d 31088  cdleme16 31096  cdleme16aN 31070  cdleme16b 31090  cdleme16c 31091  cdleme16d 31092  cdleme16e 31093  cdleme16f 31094  cdleme16g 31095  cdleme19a 31114  cdleme19b 31115  cdleme19c 31116  cdleme19d 31117  cdleme19e 31118  cdleme19f 31119  cdleme1b 31037  cdleme2 31039  cdleme20aN 31120  cdleme20bN 31121  cdleme20c 31122  cdleme20d 31123  cdleme20e 31124  cdleme20f 31125  cdleme20g 31126  cdleme20h 31127  cdleme20i 31128  cdleme20j 31129  cdleme20k 31130  cdleme20l 31133  cdleme20l1 31131  cdleme20l2 31132  cdleme20m 31134  cdleme20y 31113  cdleme20zN 31112  cdleme21 31148  cdleme21d 31141  cdleme21e 31142  cdleme22a 31151  cdleme22aa 31150  cdleme22b 31152  cdleme22cN 31153  cdleme22d 31154  cdleme22e 31155  cdleme22eALTN 31156  cdleme22f 31157  cdleme22f2 31158  cdleme22g 31159  cdleme23a 31160  cdleme23b 31161  cdleme23c 31162  cdleme26e 31170  cdleme26eALTN 31172  cdleme26ee 31171  cdleme26f 31174  cdleme26f2 31176  cdleme26f2ALTN 31175  cdleme26fALTN 31173  cdleme27N 31180  cdleme27a 31178  cdleme27cl 31177  cdleme28c 31183  cdleme3 31048  cdleme30a 31189  cdleme31fv 31201  cdleme31fv1 31202  cdleme31fv1s 31203  cdleme31fv2 31204  cdleme31id 31205  cdleme31sc 31195  cdleme31sdnN 31198  cdleme31sn 31191  cdleme31sn1 31192  cdleme31sn1c 31199  cdleme31sn2 31200  cdleme31so 31190  cdleme35a 31259  cdleme35b 31261  cdleme35c 31262  cdleme35d 31263  cdleme35e 31264  cdleme35f 31265  cdleme35fnpq 31260  cdleme35g 31266  cdleme35h 31267  cdleme35h2 31268  cdleme35sn2aw 31269  cdleme35sn3a 31270  cdleme36a 31271  cdleme36m 31272  cdleme37m 31273  cdleme38m 31274  cdleme38n 31275  cdleme39a 31276  cdleme39n 31277  cdleme3b 31040  cdleme3c 31041  cdleme3d 31042  cdleme3e 31043  cdleme3fN 31044  cdleme3fa 31047  cdleme3g 31045  cdleme3h 31046  cdleme4 31049  cdleme40m 31278  cdleme40n 31279  cdleme40v 31280  cdleme40w 31281  cdleme41fva11 31288  cdleme41sn3aw 31285  cdleme41sn4aw 31286  cdleme41snaw 31287  cdleme42a 31282  cdleme42b 31289  cdleme42c 31283  cdleme42d 31284  cdleme42e 31290  cdleme42f 31291  cdleme42g 31292  cdleme42h 31293  cdleme42i 31294  cdleme42k 31295  cdleme42ke 31296  cdleme42keg 31297  cdleme42mN 31298  cdleme42mgN 31299  cdleme43aN 31300  cdleme43bN 31301  cdleme43cN 31302  cdleme43dN 31303  cdleme5 31051  cdleme50ex 31370  cdleme50ltrn 31368  cdleme51finvN 31367  cdleme51finvfvN 31366  cdleme51finvtrN 31369  cdleme6 31052  cdleme7 31060  cdleme7a 31054  cdleme7aa 31053  cdleme7b 31055  cdleme7c 31056  cdleme7d 31057  cdleme7e 31058  cdleme7ga 31059  cdleme8 31061  cdleme8tN 31066  cdleme9 31064  cdleme9a 31062  cdleme9b 31063  cdleme9tN 31068  cdleme9taN 31067  cdlemeda 31109  cdlemedb 31108  cdlemednpq 31110  cdlemednuN 31111  cdlemefr27cl 31214  cdlemefr32fva1 31221  cdlemefr32fvaN 31220  cdlemefrs32fva 31211  cdlemefrs32fva1 31212  cdlemefs27cl 31224  cdlemefs32fva1 31234  cdlemefs32fvaN 31233  cdlemesner 31107  cdlemeulpq 31031
[Crawley] p. 114Lemma E4atex 30887  4atexlem7 30886  cdleme0nex 31101  cdleme17a 31097  cdleme17c 31099  cdleme17d 31309  cdleme17d1 31100  cdleme17d2 31306  cdleme18a 31102  cdleme18b 31103  cdleme18c 31104  cdleme18d 31106  cdleme4a 31050
[Crawley] p. 115Lemma Ecdleme21a 31136  cdleme21at 31139  cdleme21b 31137  cdleme21c 31138  cdleme21ct 31140  cdleme21f 31143  cdleme21g 31144  cdleme21h 31145  cdleme21i 31146  cdleme22gb 31105
[Crawley] p. 116Lemma Fcdlemf 31374  cdlemf1 31372  cdlemf2 31373
[Crawley] p. 116Lemma Gcdlemftr1 31378  cdlemg16 31468  cdlemg28 31515  cdlemg28a 31504  cdlemg28b 31514  cdlemg3a 31408  cdlemg42 31540  cdlemg43 31541  cdlemg44 31544  cdlemg44a 31542  cdlemg46 31546  cdlemg47 31547  cdlemg9 31445  ltrnco 31530  ltrncom 31549  tgrpabl 31562  trlco 31538
[Crawley] p. 116Definition of Gdf-tgrp 31554
[Crawley] p. 117Lemma Gcdlemg17 31488  cdlemg17b 31473
[Crawley] p. 117Definition of Edf-edring-rN 31567  df-edring 31568
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 31571
[Crawley] p. 118Remarktendopltp 31591
[Crawley] p. 118Lemma Hcdlemh 31628  cdlemh1 31626  cdlemh2 31627
[Crawley] p. 118Lemma Icdlemi 31631  cdlemi1 31629  cdlemi2 31630
[Crawley] p. 118Lemma Jcdlemj1 31632  cdlemj2 31633  cdlemj3 31634  tendocan 31635
[Crawley] p. 118Lemma Kcdlemk 31785  cdlemk1 31642  cdlemk10 31654  cdlemk11 31660  cdlemk11t 31757  cdlemk11ta 31740  cdlemk11tb 31742  cdlemk11tc 31756  cdlemk11u-2N 31700  cdlemk11u 31682  cdlemk12 31661  cdlemk12u-2N 31701  cdlemk12u 31683  cdlemk13-2N 31687  cdlemk13 31663  cdlemk14-2N 31689  cdlemk14 31665  cdlemk15-2N 31690  cdlemk15 31666  cdlemk16-2N 31691  cdlemk16 31668  cdlemk16a 31667  cdlemk17-2N 31692  cdlemk17 31669  cdlemk18-2N 31697  cdlemk18-3N 31711  cdlemk18 31679  cdlemk19-2N 31698  cdlemk19 31680  cdlemk19u 31781  cdlemk1u 31670  cdlemk2 31643  cdlemk20-2N 31703  cdlemk20 31685  cdlemk21-2N 31702  cdlemk21N 31684  cdlemk22-3 31712  cdlemk22 31704  cdlemk23-3 31713  cdlemk24-3 31714  cdlemk25-3 31715  cdlemk26-3 31717  cdlemk26b-3 31716  cdlemk27-3 31718  cdlemk28-3 31719  cdlemk29-3 31722  cdlemk3 31644  cdlemk30 31705  cdlemk31 31707  cdlemk32 31708  cdlemk33N 31720  cdlemk34 31721  cdlemk35 31723  cdlemk36 31724  cdlemk37 31725  cdlemk38 31726  cdlemk39 31727  cdlemk39u 31779  cdlemk4 31645  cdlemk41 31731  cdlemk42 31752  cdlemk42yN 31755  cdlemk43N 31774  cdlemk45 31758  cdlemk46 31759  cdlemk47 31760  cdlemk48 31761  cdlemk49 31762  cdlemk5 31647  cdlemk50 31763  cdlemk51 31764  cdlemk52 31765  cdlemk53 31768  cdlemk54 31769  cdlemk55 31772  cdlemk55u 31777  cdlemk56 31782  cdlemk5a 31646  cdlemk5auN 31671  cdlemk5u 31672  cdlemk6 31648  cdlemk6u 31673  cdlemk7 31659  cdlemk7u-2N 31699  cdlemk7u 31681  cdlemk8 31649  cdlemk9 31650  cdlemk9bN 31651  cdlemki 31652  cdlemkid 31747  cdlemkj-2N 31693  cdlemkj 31674  cdlemksat 31657  cdlemksel 31656  cdlemksv 31655  cdlemksv2 31658  cdlemkuat 31677  cdlemkuel-2N 31695  cdlemkuel-3 31709  cdlemkuel 31676  cdlemkuv-2N 31694  cdlemkuv2-2 31696  cdlemkuv2-3N 31710  cdlemkuv2 31678  cdlemkuvN 31675  cdlemkvcl 31653  cdlemky 31737  cdlemkyyN 31773  tendoex 31786
[Crawley] p. 120Remarkdva1dim 31796
[Crawley] p. 120Lemma Lcdleml1N 31787  cdleml2N 31788  cdleml3N 31789  cdleml4N 31790  cdleml5N 31791  cdleml6 31792  cdleml7 31793  cdleml8 31794  cdleml9 31795  dia1dim 31873
[Crawley] p. 120Lemma Mdia11N 31860  diaf11N 31861  dialss 31858  diaord 31859  dibf11N 31973  djajN 31949
[Crawley] p. 120Definition of isomorphism mapdiaval 31844
[Crawley] p. 121Lemma Mcdlemm10N 31930  dia2dimlem1 31876  dia2dimlem2 31877  dia2dimlem3 31878  dia2dimlem4 31879  dia2dimlem5 31880  diaf1oN 31942  diarnN 31941  dvheveccl 31924  dvhopN 31928
[Crawley] p. 121Lemma Ncdlemn 32024  cdlemn10 32018  cdlemn11 32023  cdlemn11a 32019  cdlemn11b 32020  cdlemn11c 32021  cdlemn11pre 32022  cdlemn2 32007  cdlemn2a 32008  cdlemn3 32009  cdlemn4 32010  cdlemn4a 32011  cdlemn5 32013  cdlemn5pre 32012  cdlemn6 32014  cdlemn7 32015  cdlemn8 32016  cdlemn9 32017  diclspsn 32006
[Crawley] p. 121Definition of phi(q)df-dic 31985
[Crawley] p. 122Lemma Ndih11 32077  dihf11 32079  dihjust 32029  dihjustlem 32028  dihord 32076  dihord1 32030  dihord10 32035  dihord11b 32034  dihord11c 32036  dihord2 32039  dihord2a 32031  dihord2b 32032  dihord2cN 32033  dihord2pre 32037  dihord2pre2 32038  dihordlem6 32025  dihordlem7 32026  dihordlem7b 32027
[Crawley] p. 122Definition of isomorphism mapdihffval 32042  dihfval 32043  dihval 32044
[Eisenberg] p. 67Definition 5.3df-dif 3168
[Eisenberg] p. 82Definition 6.3dfom3 7364
[Eisenberg] p. 125Definition 8.21df-map 6790
[Eisenberg] p. 216Example 13.2(4)omenps 7371
[Eisenberg] p. 310Theorem 19.8cardprc 7629
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8193
[Enderton] p. 18Axiom of Empty Setaxnul 4164
[Enderton] p. 19Definitiondf-tp 3661
[Enderton] p. 26Exercise 5unissb 3873
[Enderton] p. 26Exercise 10pwel 4241
[Enderton] p. 28Exercise 7(b)pwun 4318
[Enderton] p. 30Theorem "Distributive laws"iinin1 3989  iinin2 3988  iinun2 3984  iunin1 3983  iunin2 3982
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3987  iundif2 3985
[Enderton] p. 32Exercise 20unineq 3432
[Enderton] p. 33Exercise 23iinuni 4001
[Enderton] p. 33Exercise 25iununi 4002
[Enderton] p. 33Exercise 24(a)iinpw 4006
[Enderton] p. 33Exercise 24(b)iunpw 4586  iunpwss 4007
[Enderton] p. 36Definitionopthwiener 4284
[Enderton] p. 38Exercise 6(a)unipw 4240
[Enderton] p. 38Exercise 6(b)pwuni 4222
[Enderton] p. 41Lemma 3Dopeluu 4542  rnex 4958  rnexg 4956
[Enderton] p. 41Exercise 8dmuni 4904  rnuni 5108
[Enderton] p. 42Definition of a functiondffun7 5296  dffun8 5297
[Enderton] p. 43Definition of function valuefunfv2 5603
[Enderton] p. 43Definition of single-rootedfuncnv 5326
[Enderton] p. 44Definition (d)dfima2 5030  dfima3 5031
[Enderton] p. 47Theorem 3Hfvco2 5610
[Enderton] p. 49Axiom of Choice (first form)ac7 8116  ac7g 8117  df-ac 7759  dfac2 7773  dfac2a 7772  dfac3 7764  dfac7 7774
[Enderton] p. 50Theorem 3K(a)imauni 5788
[Enderton] p. 52Definitiondf-map 6790
[Enderton] p. 53Exercise 21coass 5207
[Enderton] p. 53Exercise 27dmco 5197
[Enderton] p. 53Exercise 14(a)funin 5335
[Enderton] p. 53Exercise 22(a)imass2 5065
[Enderton] p. 54Remarkixpf 6854  ixpssmap 6866
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6834
[Enderton] p. 55Axiom of Choice (second form)ac9 8126  ac9s 8136
[Enderton] p. 56Theorem 3Merref 6696
[Enderton] p. 57Lemma 3Nerthi 6722
[Enderton] p. 57Definitiondf-ec 6678
[Enderton] p. 58Definitiondf-qs 6682
[Enderton] p. 60Theorem 3Qth3q 6783  th3qcor 6782  th3qlem1 6780  th3qlem2 6781
[Enderton] p. 61Exercise 35df-ec 6678
[Enderton] p. 65Exercise 56(a)dmun 4901
[Enderton] p. 68Definition of successordf-suc 4414
[Enderton] p. 71Definitiondf-tr 4130  dftr4 4134
[Enderton] p. 72Theorem 4Eunisuc 4484
[Enderton] p. 73Exercise 6unisuc 4484
[Enderton] p. 73Exercise 5(a)truni 4143
[Enderton] p. 73Exercise 5(b)trint 4144  trintALT 28973
[Enderton] p. 79Theorem 4I(A1)nna0 6618
[Enderton] p. 79Theorem 4I(A2)nnasuc 6620  onasuc 6543
[Enderton] p. 79Definition of operation valuedf-ov 5877
[Enderton] p. 80Theorem 4J(A1)nnm0 6619
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6621  onmsuc 6544
[Enderton] p. 81Theorem 4K(1)nnaass 6636
[Enderton] p. 81Theorem 4K(2)nna0r 6623  nnacom 6631
[Enderton] p. 81Theorem 4K(3)nndi 6637
[Enderton] p. 81Theorem 4K(4)nnmass 6638
[Enderton] p. 81Theorem 4K(5)nnmcom 6640
[Enderton] p. 82Exercise 16nnm0r 6624  nnmsucr 6639
[Enderton] p. 88Exercise 23nnaordex 6652
[Enderton] p. 129Definitiondf-en 6880
[Enderton] p. 132Theorem 6B(b)canth 6310
[Enderton] p. 133Exercise 1xpomen 7659
[Enderton] p. 133Exercise 2qnnen 12508
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7061
[Enderton] p. 135Corollary 6Cphp3 7063
[Enderton] p. 136Corollary 6Enneneq 7060
[Enderton] p. 136Corollary 6D(a)pssinf 7089
[Enderton] p. 136Corollary 6D(b)ominf 7091
[Enderton] p. 137Lemma 6Fpssnn 7097
[Enderton] p. 138Corollary 6Gssfi 7099
[Enderton] p. 139Theorem 6H(c)mapen 7041
[Enderton] p. 142Theorem 6I(3)xpcdaen 7825
[Enderton] p. 142Theorem 6I(4)mapcdaen 7826
[Enderton] p. 143Theorem 6Jcda0en 7821  cda1en 7817
[Enderton] p. 144Exercise 13iunfi 7160  unifi 7161  unifi2 7162
[Enderton] p. 144Corollary 6Kundif2 3543  unfi 7140  unfi2 7142
[Enderton] p. 145Figure 38ffoss 5521
[Enderton] p. 145Definitiondf-dom 6881
[Enderton] p. 146Example 1domen 6891  domeng 6892
[Enderton] p. 146Example 3nndomo 7070  nnsdom 7370  nnsdomg 7132
[Enderton] p. 149Theorem 6L(a)cdadom2 7829
[Enderton] p. 149Theorem 6L(c)mapdom1 7042  xpdom1 6977  xpdom1g 6975  xpdom2g 6974
[Enderton] p. 149Theorem 6L(d)mapdom2 7048
[Enderton] p. 151Theorem 6Mzorn 8150  zorng 8147
[Enderton] p. 151Theorem 6M(4)ac8 8135  dfac5 7771
[Enderton] p. 159Theorem 6Qunictb 8213
[Enderton] p. 164Exampleinfdif 7851
[Enderton] p. 168Definitiondf-po 4330
[Enderton] p. 192Theorem 7M(a)oneli 4516
[Enderton] p. 192Theorem 7M(b)ontr1 4454
[Enderton] p. 192Theorem 7M(c)onirri 4515
[Enderton] p. 193Corollary 7N(b)0elon 4461
[Enderton] p. 193Corollary 7N(c)onsuci 4645
[Enderton] p. 193Corollary 7N(d)ssonunii 4595
[Enderton] p. 194Remarkonprc 4592
[Enderton] p. 194Exercise 16suc11 4512
[Enderton] p. 197Definitiondf-card 7588
[Enderton] p. 197Theorem 7Pcarden 8189
[Enderton] p. 200Exercise 25tfis 4661
[Enderton] p. 202Lemma 7Tr1tr 7464
[Enderton] p. 202Definitiondf-r1 7452
[Enderton] p. 202Theorem 7Qr1val1 7474
[Enderton] p. 204Theorem 7V(b)rankval4 7555
[Enderton] p. 206Theorem 7X(b)en2lp 7333
[Enderton] p. 207Exercise 30rankpr 7545  rankprb 7539  rankpw 7531  rankpwi 7511  rankuniss 7554
[Enderton] p. 207Exercise 34opthreg 7335
[Enderton] p. 208Exercise 35suc11reg 7336
[Enderton] p. 212Definition of alephalephval3 7753
[Enderton] p. 213Theorem 8A(a)alephord2 7719
[Enderton] p. 213Theorem 8A(b)cardalephex 7733
[Enderton] p. 218Theorem Schema 8Eonfununi 6374
[Enderton] p. 222Definition of kardkarden 7581  kardex 7580
[Enderton] p. 238Theorem 8Roeoa 6611
[Enderton] p. 238Theorem 8Soeoe 6613
[Enderton] p. 240Exercise 25oarec 6576
[Enderton] p. 257Definition of cofinalitycflm 7892
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13560
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13506
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14296  mrieqv2d 13557  mrieqvd 13556
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13561
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13566  mreexexlem2d 13563
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14302  mreexfidimd 13568
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18910
[Fremlin5] p. 213Lemma 565Cauniioovol 18950
[Fremlin5] p. 214Lemma 565Cauniioombl 18960
[FreydScedrov] p. 283Axiom of Infinityax-inf 7355  inf1 7339  inf2 7340
[Gleason] p. 117Proposition 9-2.1df-enq 8551  enqer 8561
[Gleason] p. 117Proposition 9-2.2df-1nq 8556  df-nq 8552
[Gleason] p. 117Proposition 9-2.3df-plpq 8548  df-plq 8554
[Gleason] p. 119Proposition 9-2.4caovmo 6073  df-mpq 8549  df-mq 8555
[Gleason] p. 119Proposition 9-2.5df-rq 8557
[Gleason] p. 119Proposition 9-2.6ltexnq 8615
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8616  ltbtwnnq 8618
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8611
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8612
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8619
[Gleason] p. 121Definition 9-3.1df-np 8621
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8633
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8635
[Gleason] p. 122Definitiondf-1p 8622
[Gleason] p. 122Remark (1)prub 8634
[Gleason] p. 122Lemma 9-3.4prlem934 8673
[Gleason] p. 122Proposition 9-3.2df-ltp 8625
[Gleason] p. 122Proposition 9-3.3ltsopr 8672  psslinpr 8671  supexpr 8694  suplem1pr 8692  suplem2pr 8693
[Gleason] p. 123Proposition 9-3.5addclpr 8658  addclprlem1 8656  addclprlem2 8657  df-plp 8623
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8662
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8661
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8674
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8683  ltexprlem1 8676  ltexprlem2 8677  ltexprlem3 8678  ltexprlem4 8679  ltexprlem5 8680  ltexprlem6 8681  ltexprlem7 8682
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8685  ltaprlem 8684
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8686
[Gleason] p. 124Lemma 9-3.6prlem936 8687
[Gleason] p. 124Proposition 9-3.7df-mp 8624  mulclpr 8660  mulclprlem 8659  reclem2pr 8688
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8669
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8664
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8663
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8668
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8691  reclem3pr 8689  reclem4pr 8690
[Gleason] p. 126Proposition 9-4.1df-enr 8697  df-mpr 8696  df-plpr 8695  enrer 8706
[Gleason] p. 126Proposition 9-4.2df-0r 8702  df-1r 8703  df-nr 8698
[Gleason] p. 126Proposition 9-4.3df-mr 8700  df-plr 8699  negexsr 8740  recexsr 8745  recexsrlem 8741
[Gleason] p. 127Proposition 9-4.4df-ltr 8701
[Gleason] p. 130Proposition 10-1.3creui 9757  creur 9756  cru 9754
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8826  axcnre 8802
[Gleason] p. 132Definition 10-3.1crim 11616  crimd 11733  crimi 11694  crre 11615  crred 11732  crrei 11693
[Gleason] p. 132Definition 10-3.2remim 11618  remimd 11699
[Gleason] p. 133Definition 10.36absval2 11785  absval2d 11943  absval2i 11896
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11642  cjaddd 11721  cjaddi 11689
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11643  cjmuld 11722  cjmuli 11690
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11641  cjcjd 11700  cjcji 11672
[Gleason] p. 133Proposition 10-3.4(f)cjre 11640  cjreb 11624  cjrebd 11703  cjrebi 11675  cjred 11727  rere 11623  rereb 11621  rerebd 11702  rerebi 11674  rered 11725
[Gleason] p. 133Proposition 10-3.4(h)addcj 11649  addcjd 11713  addcji 11684
[Gleason] p. 133Proposition 10-3.7(a)absval 11739
[Gleason] p. 133Proposition 10-3.7(b)abscj 11780  abscjd 11948  abscji 11900
[Gleason] p. 133Proposition 10-3.7(c)abs00 11790  abs00d 11944  abs00i 11897  absne0d 11945
[Gleason] p. 133Proposition 10-3.7(d)releabs 11821  releabsd 11949  releabsi 11901
[Gleason] p. 133Proposition 10-3.7(f)absmul 11795  absmuld 11952  absmuli 11903
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11783  sqabsaddi 11904
[Gleason] p. 133Proposition 10-3.7(h)abstri 11830  abstrid 11954  abstrii 11907
[Gleason] p. 134Definition 10-4.1df-exp 11121  exp0 11124  expp1 11126  expp1d 11262
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20042  cxpaddd 20080  expadd 11160  expaddd 11263  expaddz 11162
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20051  cxpmuld 20097  expmul 11163  expmuld 11264  expmulz 11164
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20048  mulcxpd 20091  mulexp 11157  mulexpd 11276  mulexpz 11158
[Gleason] p. 140Exercise 1znnen 12507
[Gleason] p. 141Definition 11-2.1fzval 10800
[Gleason] p. 168Proposition 12-2.1(a)climadd 12121  rlimadd 12132  rlimdiv 12135
[Gleason] p. 168Proposition 12-2.1(b)climsub 12123  rlimsub 12133
[Gleason] p. 168Proposition 12-2.1(c)climmul 12122  rlimmul 12134
[Gleason] p. 171Corollary 12-2.2climmulc2 12126
[Gleason] p. 172Corollary 12-2.5climrecl 12073
[Gleason] p. 172Proposition 12-2.4(c)climabs 12093  climcj 12094  climim 12096  climre 12095  rlimabs 12098  rlimcj 12099  rlimim 12101  rlimre 12100
[Gleason] p. 173Definition 12-3.1df-ltxr 8888  df-xr 8887  ltxr 10473
[Gleason] p. 175Definition 12-4.1df-limsup 11961  limsupval 11964
[Gleason] p. 180Theorem 12-5.1climsup 12159
[Gleason] p. 180Theorem 12-5.3caucvg 12167  caucvgb 12168  caucvgr 12164  climcau 12160
[Gleason] p. 182Exercise 3cvgcmp 12290
[Gleason] p. 182Exercise 4cvgrat 12355
[Gleason] p. 195Theorem 13-2.12abs1m 11835
[Gleason] p. 217Lemma 13-4.1btwnzge0 10969
[Gleason] p. 223Definition 14-1.1df-met 16390
[Gleason] p. 223Definition 14-1.1(a)met0 17924  xmet0 17923
[Gleason] p. 223Definition 14-1.1(b)metgt0 17939
[Gleason] p. 223Definition 14-1.1(c)metsym 17930
[Gleason] p. 223Definition 14-1.1(d)mettri 17932  mstri 18031  xmettri 17931  xmstri 18030
[Gleason] p. 225Definition 14-1.5xpsmet 17962
[Gleason] p. 230Proposition 14-2.6txlm 17358
[Gleason] p. 240Theorem 14-4.3metcnp4 18751
[Gleason] p. 240Proposition 14-4.2metcnp3 18102
[Gleason] p. 243Proposition 14-4.16addcn 18385  addcn2 12083  mulcn 18387  mulcn2 12085  subcn 18386  subcn2 12084
[Gleason] p. 295Remarkbcval3 11335  bcval4 11336
[Gleason] p. 295Equation 2bcpasc 11349
[Gleason] p. 295Definition of binomial coefficientbcval 11333  df-bc 11332
[Gleason] p. 296Remarkbcn0 11339  bcnn 11340
[Gleason] p. 296Theorem 15-2.8binom 12304
[Gleason] p. 308Equation 2ef0 12388
[Gleason] p. 308Equation 3efcj 12389
[Gleason] p. 309Corollary 15-4.3efne0 12393
[Gleason] p. 309Corollary 15-4.4efexp 12397
[Gleason] p. 310Equation 14sinadd 12460
[Gleason] p. 310Equation 15cosadd 12461
[Gleason] p. 311Equation 17sincossq 12472
[Gleason] p. 311Equation 18cosbnd 12477  sinbnd 12476
[Gleason] p. 311Lemma 15-4.7sqeqor 11233  sqeqori 11231
[Gleason] p. 311Definition of pidf-pi 12370
[Godowski] p. 730Equation SFgoeqi 22869
[GodowskiGreechie] p. 249Equation IV3oai 22263
[Gratzer] p. 23Section 0.6df-mre 13504
[Gratzer] p. 27Section 0.6df-mri 13506
[Halmos] p. 31Theorem 17.3riesz1 22661  riesz2 22662
[Halmos] p. 41Definition of Hermitianhmopadj2 22537
[Halmos] p. 42Definition of projector orderingpjordi 22769
[Halmos] p. 43Theorem 26.1elpjhmop 22781  elpjidm 22780  pjnmopi 22744
[Halmos] p. 44Remarkpjinormi 22282  pjinormii 22271
[Halmos] p. 44Theorem 26.2elpjch 22785  pjrn 22302  pjrni 22297  pjvec 22291
[Halmos] p. 44Theorem 26.3pjnorm2 22322
[Halmos] p. 44Theorem 26.4hmopidmpj 22750  hmopidmpji 22748
[Halmos] p. 45Theorem 27.1pjinvari 22787
[Halmos] p. 45Theorem 27.3pjoci 22776  pjocvec 22292
[Halmos] p. 45Theorem 27.4pjorthcoi 22765
[Halmos] p. 48Theorem 29.2pjssposi 22768
[Halmos] p. 48Theorem 29.3pjssdif1i 22771  pjssdif2i 22770
[Halmos] p. 50Definition of spectrumdf-spec 22451
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 20
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1536
[Hatcher] p. 25Definitiondf-phtpc 18506  df-phtpy 18485
[Hatcher] p. 26Definitiondf-pco 18519  df-pi1 18522
[Hatcher] p. 26Proposition 1.2phtpcer 18509
[Hatcher] p. 26Proposition 1.3pi1grp 18564
[Herstein] p. 54Exercise 28df-grpo 20874
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14514  grpoideu 20892  mndideu 14391
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14532  grpoinveu 20905
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14551  grpo2inv 20922
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14560  grpoinvop 20924
[Herstein] p. 57Exercise 1isgrp2d 20918  isgrp2i 20919
[Hitchcock] p. 5Rule A3mpto1 1523
[Hitchcock] p. 5Rule A4mpto2 1524
[Hitchcock] p. 5Rule A5mtp-xor 1526
[Holland] p. 1519Theorem 2sumdmdi 23016
[Holland] p. 1520Lemma 5cdj1i 23029  cdj3i 23037  cdj3lem1 23030  cdjreui 23028
[Holland] p. 1524Lemma 7mddmdin0i 23027
[Holland95] p. 13Theorem 3.6hlathil 32776
[Holland95] p. 14Line 15hgmapvs 32706
[Holland95] p. 14Line 16hdmaplkr 32728
[Holland95] p. 14Line 17hdmapellkr 32729
[Holland95] p. 14Line 19hdmapglnm2 32726
[Holland95] p. 14Line 20hdmapip0com 32732
[Holland95] p. 14Theorem 3.6hdmapevec2 32651
[Holland95] p. 14Lines 24 and 25hdmapoc 32746
[Holland95] p. 204Definition of involutiondf-srng 15627
[Holland95] p. 212Definition of subspacedf-psubsp 30314
[Holland95] p. 214Lemma 3.3lclkrlem2v 32340
[Holland95] p. 214Definition 3.2df-lpolN 32293
[Holland95] p. 214Definition of nonsingularpnonsingN 30744
[Holland95] p. 215Lemma 3.3(1)dihoml4 32189  poml4N 30764
[Holland95] p. 215Lemma 3.3(2)dochexmid 32280  pexmidALTN 30789  pexmidN 30780
[Holland95] p. 218Theorem 3.6lclkr 32345
[Holland95] p. 218Definition of dual vector spacedf-ldual 29936  ldualset 29937
[Holland95] p. 222Item 1df-lines 30312  df-pointsN 30313
[Holland95] p. 222Item 2df-polarityN 30714
[Holland95] p. 223Remarkispsubcl2N 30758  omllaw4 30058  pol1N 30721  polcon3N 30728
[Holland95] p. 223Definitiondf-psubclN 30746
[Holland95] p. 223Equation for polaritypolval2N 30717
[Hughes] p. 44Equation 1.21bax-his3 21679
[Hughes] p. 47Definition of projection operatordfpjop 22778
[Hughes] p. 49Equation 1.30eighmre 22559  eigre 22431  eigrei 22430
[Hughes] p. 49Equation 1.31eighmorth 22560  eigorth 22434  eigorthi 22433
[Hughes] p. 137Remark (ii)eigposi 22432
[Indrzejczak] p. 33Definition ` `Enatded 20806  natded 20806
[Indrzejczak] p. 33Definition ` `Inatded 20806
[Indrzejczak] p. 34Definition ` `Enatded 20806  natded 20806
[Indrzejczak] p. 34Definition ` `Inatded 20806
[Jech] p. 4Definition of classcv 1631  cvjust 2291
[Jech] p. 42Lemma 6.1alephexp1 8217
[Jech] p. 42Equation 6.1alephadd 8215  alephmul 8216
[Jech] p. 43Lemma 6.2infmap 8214  infmap2 7860
[Jech] p. 71Lemma 9.3jech9.3 7502
[Jech] p. 72Equation 9.3scott0 7572  scottex 7571
[Jech] p. 72Exercise 9.1rankval4 7555
[Jech] p. 72Scheme "Collection Principle"cp 7577
[Jech] p. 78Definition implied by the footnoteopthprc 4752
[JonesMatijasevic] p. 694Definition 2.3rmxyval 27103
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 27199
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 27200
[JonesMatijasevic] p. 695Equation 2.7rmxadd 27115
[JonesMatijasevic] p. 695Equation 2.8rmyadd 27119
[JonesMatijasevic] p. 695Equation 2.9rmxp1 27120  rmyp1 27121
[JonesMatijasevic] p. 695Equation 2.10rmxm1 27122  rmym1 27123
[JonesMatijasevic] p. 695Equation 2.11rmx0 27113  rmx1 27114  rmxluc 27124
[JonesMatijasevic] p. 695Equation 2.12rmy0 27117  rmy1 27118  rmyluc 27125
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 27127
[JonesMatijasevic] p. 695Equation 2.14rmydbl 27128
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 27150  jm2.17b 27151  jm2.17c 27152
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 27189
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 27193
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 27184
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 27153  jm2.24nn 27149
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 27198
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 27204  rmygeid 27154
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 27216
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1644
[KalishMontague] p. 85Lemma 2equid 1662
[KalishMontague] p. 85Lemma 3equcomi 1664
[KalishMontague] p. 86Lemma 7cbvalivw 1660  cbvaliw 1659
[KalishMontague] p. 87Lemma 8spimvw 1657  spimw 1656
[KalishMontague] p. 87Lemma 9spfw 1676  spw 1679
[Kalmbach] p. 14Definition of latticechabs1 22111  chabs1i 22113  chabs2 22112  chabs2i 22114  chjass 22128  chjassi 22081  latabs1 14209  latabs2 14210
[Kalmbach] p. 15Definition of atomdf-at 22934  ela 22935
[Kalmbach] p. 15Definition of coverscvbr2 22879  cvrval2 30086
[Kalmbach] p. 16Definitiondf-ol 29990  df-oml 29991
[Kalmbach] p. 20Definition of commutescmbr 22179  cmbri 22185  cmtvalN 30023  df-cm 22178  df-cmtN 29989
[Kalmbach] p. 22Remarkomllaw5N 30059  pjoml5 22208  pjoml5i 22183
[Kalmbach] p. 22Definitionpjoml2 22206  pjoml2i 22180
[Kalmbach] p. 22Theorem 2(v)cmcm 22209  cmcmi 22187  cmcmii 22192  cmtcomN 30061
[Kalmbach] p. 22Theorem 2(ii)omllaw3 30057  omlsi 21999  pjoml 22031  pjomli 22030
[Kalmbach] p. 22Definition of OML lawomllaw2N 30056
[Kalmbach] p. 23Remarkcmbr2i 22191  cmcm3 22210  cmcm3i 22189  cmcm3ii 22194  cmcm4i 22190  cmt3N 30063  cmt4N 30064  cmtbr2N 30065
[Kalmbach] p. 23Lemma 3cmbr3 22203  cmbr3i 22195  cmtbr3N 30066
[Kalmbach] p. 25Theorem 5fh1 22213  fh1i 22216  fh2 22214  fh2i 22217  omlfh1N 30070
[Kalmbach] p. 65Remarkchjatom 22953  chslej 22093  chsleji 22053  shslej 21975  shsleji 21965
[Kalmbach] p. 65Proposition 1chocin 22090  chocini 22049  chsupcl 21935  chsupval2 22005  h0elch 21850  helch 21839  hsupval2 22004  ocin 21891  ococss 21888  shococss 21889
[Kalmbach] p. 65Definition of subspace sumshsval 21907
[Kalmbach] p. 66Remarkdf-pjh 21990  pjssmi 22761  pjssmii 22276
[Kalmbach] p. 67Lemma 3osum 22240  osumi 22237
[Kalmbach] p. 67Lemma 4pjci 22796
[Kalmbach] p. 103Exercise 6atmd2 22996
[Kalmbach] p. 103Exercise 12mdsl0 22906
[Kalmbach] p. 140Remarkhatomic 22956  hatomici 22955  hatomistici 22958
[Kalmbach] p. 140Proposition 1atlatmstc 30131
[Kalmbach] p. 140Proposition 1(i)atexch 22977  lsatexch 29855
[Kalmbach] p. 140Proposition 1(ii)chcv1 22951  cvlcvr1 30151  cvr1 30221
[Kalmbach] p. 140Proposition 1(iii)cvexch 22970  cvexchi 22965  cvrexch 30231
[Kalmbach] p. 149Remark 2chrelati 22960  hlrelat 30213  hlrelat5N 30212  lrelat 29826
[Kalmbach] p. 153Exercise 5lsmcv 15910  lsmsatcv 29822  spansncv 22248  spansncvi 22247
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29841  spansncv2 22889
[Kalmbach] p. 266Definitiondf-st 22807
[Kalmbach2] p. 8Definition of adjointdf-adjh 22445
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8284  fpwwe2 8281
[KanamoriPincus] p. 416Corollary 1.3canth4 8285
[KanamoriPincus] p. 417Corollary 1.6canthp1 8292
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8287
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8289
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8302
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8306  gchxpidm 8307
[KanamoriPincus] p. 419Theorem 2.1gchacg 8310  gchhar 8309
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7858  unxpwdom 7319
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8312
[Kreyszig] p. 3Property M1metcl 17913  xmetcl 17912
[Kreyszig] p. 4Property M2meteq0 17920
[Kreyszig] p. 8Definition 1.1-8dscmet 18111
[Kreyszig] p. 12Equation 5conjmul 9493  muleqadd 9428
[Kreyszig] p. 18Definition 1.3-2mopnval 18000
[Kreyszig] p. 19Remarkmopntopon 18001
[Kreyszig] p. 19Theorem T1mopn0 18060  mopnm 18006
[Kreyszig] p. 19Theorem T2unimopn 18058
[Kreyszig] p. 19Definition of neighborhoodneibl 18063
[Kreyszig] p. 20Definition 1.3-3metcnp2 18104
[Kreyszig] p. 25Definition 1.4-1lmbr 17004  lmmbr 18700  lmmbr2 18701
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17124
[Kreyszig] p. 28Theorem 1.4-5lmcau 18754
[Kreyszig] p. 28Definition 1.4-3iscau 18718  iscmet2 18736
[Kreyszig] p. 30Theorem 1.4-7cmetss 18756
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17203  metelcls 18746
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18747  metcld2 18748
[Kreyszig] p. 51Equation 2clmvneg1 18605  lmodvneg1 15683  nvinv 21213  vcm 21143
[Kreyszig] p. 51Equation 1aclm0vs 18604  lmod0vs 15679  vc0 21141
[Kreyszig] p. 51Equation 1blmodvs0 15680  vcz 21142
[Kreyszig] p. 58Definition 2.2-1imsmet 21276
[Kreyszig] p. 59Equation 1imsdval 21271  imsdval2 21272
[Kreyszig] p. 63Problem 1nvnd 21273
[Kreyszig] p. 64Problem 2nvge0 21256  nvz 21251
[Kreyszig] p. 64Problem 3nvabs 21255
[Kreyszig] p. 91Definition 2.7-1isblo3i 21395
[Kreyszig] p. 92Equation 2df-nmoo 21339
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21401  blocni 21399
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21400
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18655  ipeq0 16558  ipz 21311
[Kreyszig] p. 135Problem 2pythi 21444
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21448
[Kreyszig] p. 144Equation 4supcvg 12330
[Kreyszig] p. 144Theorem 3.3-1minvec 18816  minveco 21479
[Kreyszig] p. 196Definition 3.9-1df-aj 21344
[Kreyszig] p. 247Theorem 4.7-2bcth 18767
[Kreyszig] p. 249Theorem 4.7-3ubth 21468
[Kreyszig] p. 470Definition of positive operator orderingleop 22719  leopg 22718
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22737
[Kreyszig] p. 525Theorem 10.1-1htth 21514
[Kunen] p. 10Axiom 0a9e 1904  axnul 4164
[Kunen] p. 11Axiom 3axnul 4164
[Kunen] p. 12Axiom 6zfrep6 5764
[Kunen] p. 24Definition 10.24mapval 6800  mapvalg 6798
[Kunen] p. 30Lemma 10.20fodom 8165
[Kunen] p. 31Definition 10.24mapex 6794
[Kunen] p. 95Definition 2.1df-r1 7452
[Kunen] p. 97Lemma 2.10r1elss 7494  r1elssi 7493
[Kunen] p. 107Exercise 4rankop 7546  rankopb 7540  rankuni 7551  rankxplim 7565  rankxpsuc 7568
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3931
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27654
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27649
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27655
[LeBlanc] p. 277Rule R2axnul 4164
[Levy] p. 338Axiomdf-clab 2283  df-clel 2292  df-cleq 2289
[Levy58] p. 2Definition Iisfin1-3 8028
[Levy58] p. 2Definition IIdf-fin2 7928
[Levy58] p. 2Definition Iadf-fin1a 7927
[Levy58] p. 2Definition IIIdf-fin3 7930
[Levy58] p. 3Definition Vdf-fin5 7931
[Levy58] p. 3Definition IVdf-fin4 7929
[Levy58] p. 4Definition VIdf-fin6 7932
[Levy58] p. 4Definition VIIdf-fin7 7933
[Levy58], p. 3Theorem 1fin1a2 8057
[Lopez-Astorga] p. 12Rule 1mpto1 1523
[Lopez-Astorga] p. 12Rule 2mpto2 1524
[Lopez-Astorga] p. 12Rule 3mtp-xor 1526
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 23004
[Maeda] p. 168Lemma 5mdsym 23008  mdsymi 23007
[Maeda] p. 168Lemma 4(i)mdsymlem4 23002  mdsymlem6 23004  mdsymlem7 23005
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23006
[MaedaMaeda] p. 1Remarkssdmd1 22909  ssdmd2 22910  ssmd1 22907  ssmd2 22908
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22905
[MaedaMaeda] p. 1Definition 1.1df-dmd 22877  df-md 22876  mdbr 22890
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22927  mdslj1i 22915  mdslj2i 22916  mdslle1i 22913  mdslle2i 22914  mdslmd1i 22925  mdslmd2i 22926
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22917  mdsl2bi 22919  mdsl2i 22918
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22931
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22928
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22929
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22906
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22911  mdsl3 22912
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22930
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23025
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 30133  hlrelat1 30211
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29851
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22932  cvmdi 22920  cvnbtwn4 22885  cvrnbtwn4 30091
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22933
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 30152  cvp 22971  cvrp 30227  lcvp 29852
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22995
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22994
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 30145  hlexch4N 30203
[MaedaMaeda] p. 34Exercise 7.1atabsi 22997
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 30254
[MaedaMaeda] p. 61Definition 15.10psubN 30560  atpsubN 30564  df-pointsN 30313  pointpsubN 30562
[MaedaMaeda] p. 62Theorem 15.5df-pmap 30315  pmap11 30573  pmaple 30572  pmapsub 30579  pmapval 30568
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 30576  pmap1N 30578
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 30581  pmapglb2N 30582  pmapglb2xN 30583  pmapglbx 30580
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30663
[MaedaMaeda] p. 67Postulate PS1ps-1 30288
[MaedaMaeda] p. 68Lemma 16.2df-padd 30607  paddclN 30653  paddidm 30652
[MaedaMaeda] p. 68Condition PS2ps-2 30289
[MaedaMaeda] p. 68Equation 16.2.1paddass 30649
[MaedaMaeda] p. 69Lemma 16.4ps-1 30288
[MaedaMaeda] p. 69Theorem 16.4ps-2 30289
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15000  lsmmod2 15001  lssats 29824  shatomici 22954  shatomistici 22957  shmodi 21985  shmodsi 21984
[MaedaMaeda] p. 130Remark 29.6dmdmd 22896  mdsymlem7 23005
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22184
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22088
[MaedaMaeda] p. 139Remarksumdmdii 23011
[Margaris] p. 40Rule Cexlimiv 1624
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 360  df-ex 1532  df-or 359  dfbi2 609
[Margaris] p. 51Theorem 1id1 20
[Margaris] p. 56Theorem 3syld 40
[Margaris] p. 59Section 14notnot2ALTVD 29007
[Margaris] p. 60Theorem 8mth8 138
[Margaris] p. 60Section 14con3ALTVD 29008
[Margaris] p. 79Rule Cexinst01 28702  exinst11 28703
[Margaris] p. 89Theorem 19.219.2 1648  19.2g 1792  r19.2z 3556
[Margaris] p. 89Theorem 19.319.3 1793  19.3v 1654  rr19.3v 2922
[Margaris] p. 89Theorem 19.5alcom 1723
[Margaris] p. 89Theorem 19.6alex 1562
[Margaris] p. 89Theorem 19.7alnex 1533
[Margaris] p. 89Theorem 19.819.8a 1730
[Margaris] p. 89Theorem 19.919.9 1795  19.9h 1739  19.9v 1653
[Margaris] p. 89Theorem 19.11excom 1798  excomim 1797
[Margaris] p. 89Theorem 19.1219.12 1746  r19.12 2669
[Margaris] p. 90Theorem 19.14exnal 1564
[Margaris] p. 90Theorem 19.152albi 27679  albi 1554  ralbi 2692
[Margaris] p. 90Theorem 19.1619.16 1799
[Margaris] p. 90Theorem 19.1719.17 1800
[Margaris] p. 90Theorem 19.182exbi 27681  exbi 1571
[Margaris] p. 90Theorem 19.1919.19 1801
[Margaris] p. 90Theorem 19.202alim 27678  alim 1548  alimd 1756  alimdh 1553  alimdv 1611  ralimdaa 2633  ralimdv 2635  ralimdva 2634  sbcimdv 3065
[Margaris] p. 90Theorem 19.2119.21-2 1804  19.21 1803  19.21bi 1806  19.21h 1743  19.21t 1802  19.21v 1843  19.21vv 27677  alrimd 1761  alrimdd 1760  alrimdh 1577  alrimdv 1623  alrimi 1757  alrimih 1555  alrimiv 1621  alrimivv 1622  r19.21 2642  r19.21be 2657  r19.21bi 2654  r19.21t 2641  r19.21v 2643  ralrimd 2644  ralrimdv 2645  ralrimdva 2646  ralrimdvv 2650  ralrimdvva 2651  ralrimi 2637  ralrimiv 2638  ralrimiva 2639  ralrimivv 2647  ralrimivva 2648  ralrimivvva 2649  ralrimivw 2640  rexlimi 2673
[Margaris] p. 90Theorem 19.222alimdv 1613  2exim 27680  2eximdv 1614  exim 1565  eximd 1762  eximdh 1578  eximdv 1612  rexim 2660  reximdai 2664  reximddv 23044  reximdv 2667  reximdv2 2665  reximdva 2668  reximdvai 2666  reximi2 2662
[Margaris] p. 90Theorem 19.2319.23 1809  19.23bi 1814  19.23h 1740  19.23t 1808  19.23v 1844  19.23vv 1845  exlimd 1815  exlimdh 1816  exlimdv 1626  exlimdvv 1627  exlimexi 28586  exlimi 1813  exlimih 1741  exlimiv 1624  exlimivv 1625  r19.23 2671  r19.23v 2672  rexlimd 2677  rexlimdv 2679  rexlimdv3a 2682  rexlimdva 2680  rexlimdvaa 2681  rexlimdvv 2686  rexlimdvva 2687  rexlimdvw 2683  rexlimiv 2674  rexlimiva 2675  rexlimivv 2685
[Margaris] p. 90Theorem 19.2419.24 1651
[Margaris] p. 90Theorem 19.2519.25 1593
[Margaris] p. 90Theorem 19.2619.26-2 1584  19.26-3an 1585  19.26 1583  r19.26-2 2689  r19.26-2a 25037  r19.26-3 2690  r19.26 2688  r19.26m 2691
[Margaris] p. 90Theorem 19.2719.27 1817  19.27v 1847  r19.27av 2694  r19.27z 3565  r19.27zv 3566
[Margaris] p. 90Theorem 19.2819.28 1818  19.28v 1848  19.28vv 27687  r19.28av 2695  r19.28z 3559  r19.28zv 3562  rr19.28v 2923
[Margaris] p. 90Theorem 19.2919.29 1586  19.29r 1587  19.29r2 1588  19.29x 1589  r19.29 2696  r19.29d2r 23197  r19.29r 2697
[Margaris] p. 90Theorem 19.3019.30 1594  r19.30 2698
[Margaris] p. 90Theorem 19.3119.31 1824  19.31vv 27685
[Margaris] p. 90Theorem 19.3219.32 1823  r19.32 28048  r19.32v 2699
[Margaris] p. 90Theorem 19.3319.33-2 27683  19.33 1597  19.33b 1598
[Margaris] p. 90Theorem 19.3419.34 1652
[Margaris] p. 90Theorem 19.3519.35 1590  19.35i 1591  19.35ri 1592  r19.35 2700
[Margaris] p. 90Theorem 19.3619.36 1819  19.36aiv 1850  19.36i 1820  19.36v 1849  19.36vv 27684  r19.36av 2701  r19.36zv 3567
[Margaris] p. 90Theorem 19.3719.37 1821  19.37aiv 1853  19.37v 1852  19.37vv 27686  r19.37 2702  r19.37av 2703  r19.37zv 3563
[Margaris] p. 90Theorem 19.3819.38 1822
[Margaris] p. 90Theorem 19.3919.39 1650
[Margaris] p. 90Theorem 19.4019.40-2 1600  19.40 1599  r19.40 2704
[Margaris] p. 90Theorem 19.4119.41 1827  19.41rg 28615  19.41v 1854  19.41vv 1855  19.41vvv 1856  19.41vvvv 1857  r19.41 2705  r19.41v 2706  r19.41vv 23179
[Margaris] p. 90Theorem 19.4219.42 1828  19.42v 1858  19.42vv 1860  19.42vvv 1861  r19.42v 2707
[Margaris] p. 90Theorem 19.4319.43 1595  r19.43 2708
[Margaris] p. 90Theorem 19.4419.44 1825  r19.44av 2709
[Margaris] p. 90Theorem 19.4519.45 1826  r19.45av 2710  r19.45zv 3564
[Margaris] p. 110Exercise 2(b)eu1 2177
[Mayet] p. 370Remarkjpi 22866  largei 22863  stri 22853
[Mayet3] p. 9Definition of CH-statesdf-hst 22808  ishst 22810
[Mayet3] p. 10Theoremhstrbi 22862  hstri 22861
[Mayet3] p. 1223Theorem 4.1mayete3i 22323
[Mayet3] p. 1240Theorem 7.1mayetes3i 22325
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22874
[MegPav2000] p. 2345Definition 3.4-1chintcl 21927  chsupcl 21935
[MegPav2000] p. 2345Definition 3.4-2hatomic 22956
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22950
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22977
[MegPav2000] p. 2366Figure 7pl42N 30794
[MegPav2002] p. 362Lemma 2.2latj31 14221  latj32 14219  latjass 14217
[Megill] p. 444Axiom C5ax-17 1606  ax17o 2109
[Megill] p. 444Section 7conventions 20805
[Megill] p. 445Lemma L12aecom-o 2103  aecom 1899  ax-10 2092
[Megill] p. 446Lemma L17equtrr 1672
[Megill] p. 446Lemma L18ax9from9o 2100
[Megill] p. 446Lemma L19hbnae-o 2131  hbnae 1908
[Megill] p. 447Remark 9.1df-sb 1639  sbid 1875  sbidd-misc 28443  sbidd 28442
[Megill] p. 448Remark 9.6ax15 1974
[Megill] p. 448Scheme C4'ax-5o 2088
[Megill] p. 448Scheme C5'ax-4 2087  sp 1728
[Megill] p. 448Scheme C6'ax-7 1720
[Megill] p. 448Scheme C7'ax-6o 2089
[Megill] p. 448Scheme C8'ax-8 1661
[Megill] p. 448Scheme C9'ax-12o 2094
[Megill] p. 448Scheme C10'ax-9 1644  ax-9o 2090
[Megill] p. 448Scheme C11'ax-10o 2091
[Megill] p. 448Scheme C12'ax-13 1698
[Megill] p. 448Scheme C13'ax-14 1700
[Megill] p. 448Scheme C14'ax-15 2095
[Megill] p. 448Scheme C15'ax-11o 2093
[Megill] p. 448Scheme C16'ax-16 2096
[Megill] p. 448Theorem 9.4dral1-o 2106  dral1 1918  dral2-o 2133  dral2 1919  drex1 1920  drex2 1921  drsb1 1975  drsb2 2014
[Megill] p. 448Theorem 9.7conventions 20805
[Megill] p. 449Theorem 9.7sbcom2 2066  sbequ 2013  sbid2v 2075
[Megill] p. 450Example in Appendixhba1-o 2101  hba1 1731
[Mendelson] p. 35Axiom A3hirstL-ax3 27963
[Mendelson] p. 36Lemma 1.8id1 20
[Mendelson] p. 69Axiom 4rspsbc 3082  rspsbca 3083  stdpc4 1977
[Mendelson] p. 69Axiom 5ax-5o 2088  ra5 3088  stdpc5 1805
[Mendelson] p. 81Rule Cexlimiv 1624
[Mendelson] p. 95Axiom 6stdpc6 1670
[Mendelson] p. 95Axiom 7stdpc7 1870
[Mendelson] p. 225Axiom system NBGru 3003
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4284
[Mendelson] p. 231Exercise 4.10(k)inv1 3494
[Mendelson] p. 231Exercise 4.10(l)unv 3495
[Mendelson] p. 231Exercise 4.10(n)dfin3 3421
[Mendelson] p. 231Exercise 4.10(o)df-nul 3469
[Mendelson] p. 231Exercise 4.10(q)dfin4 3422
[Mendelson] p. 231Exercise 4.10(s)ddif 3321
[Mendelson] p. 231Definition of uniondfun3 3420
[Mendelson] p. 235Exercise 4.12(c)univ 4581
[Mendelson] p. 235Exercise 4.12(d)pwv 3842
[Mendelson] p. 235Exercise 4.12(j)pwin 4313
[Mendelson] p. 235Exercise 4.12(k)pwunss 4314
[Mendelson] p. 235Exercise 4.12(l)pwssun 4315
[Mendelson] p. 235Exercise 4.12(n)uniin 3863
[Mendelson] p. 235Exercise 4.12(p)reli 4829
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5209
[Mendelson] p. 244Proposition 4.8(g)epweon 4591
[Mendelson] p. 246Definition of successordf-suc 4414
[Mendelson] p. 250Exercise 4.36oelim2 6609
[Mendelson] p. 254Proposition 4.22(b)xpen 7040
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6962  xpsneng 6963
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6969  xpcomeng 6970
[Mendelson] p. 254Proposition 4.22(e)xpassen 6972
[Mendelson] p. 255Definitionbrsdom 6900
[Mendelson] p. 255Exercise 4.39endisj 6965
[Mendelson] p. 255Exercise 4.41mapprc 6792
[Mendelson] p. 255Exercise 4.43mapsnen 6954
[Mendelson] p. 255Exercise 4.45mapunen 7046
[Mendelson] p. 255Exercise 4.47xpmapen 7045
[Mendelson] p. 255Exercise 4.42(a)map0e 6821
[Mendelson] p. 255Exercise 4.42(b)map1 6955
[Mendelson] p. 257Proposition 4.24(a)undom 6966
[Mendelson] p. 258Exercise 4.56(b)cdaen 7815
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7824  cdacomen 7823
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7828
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7822
[Mendelson] p. 258Definition of cardinal sumcdaval 7812  df-cda 7810
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6546
[Mendelson] p. 266Proposition 4.34(f)oaordex 6572
[Mendelson] p. 275Proposition 4.42(d)entri3 8197
[Mendelson] p. 281Definitiondf-r1 7452
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7501
[Mendelson] p. 287Axiom system MKru 3003
[MertziosUnger] p. 153Proposition 12pthfrgrarn 28433  2pthfrgrarn2 28434  n4cyclfrgra 28440
[Mittelstaedt] p. 9Definitiondf-oc 21847
[Monk1] p. 22Remarkconventions 20805
[Monk1] p. 22Theorem 3.1conventions 20805
[Monk1] p. 26Theorem 2.8(vii)ssin 3404
[Monk1] p. 33Theorem 3.2(i)ssrel 4792
[Monk1] p. 33Theorem 3.2(ii)eqrel 4793
[Monk1] p. 34Definition 3.3df-opab 4094
[Monk1] p. 36Theorem 3.7(i)coi1 5204  coi2 5205
[Monk1] p. 36Theorem 3.8(v)dm0 4908  rn0 4952
[Monk1] p. 36Theorem 3.7(ii)cnvi 5101
[Monk1] p. 37Theorem 3.13(i)relxp 4810
[Monk1] p. 37Theorem 3.13(x)dmxp 4913  rnxp 5122
[Monk1] p. 37Theorem 3.13(ii)xp0 5114  xp0r 4784
[Monk1] p. 38Theorem 3.16(ii)ima0 5046
[Monk1] p. 38Theorem 3.16(viii)imai 5043
[Monk1] p. 39Theorem 3.17imaexg 5042
[Monk1] p. 39Theorem 3.16(xi)imassrn 5041
[Monk1] p. 41Theorem 4.3(i)fnopfv 5676  funfvop 5653
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5582
[Monk1] p. 42Theorem 4.4(iii)fvelima 5590
[Monk1] p. 43Theorem 4.6funun 5312
[Monk1] p. 43Theorem 4.8(iv)dff13 5799  dff13f 5800
[Monk1] p. 46Theorem 4.15(v)funex 5759  funrnex 5763
[Monk1] p. 50Definition 5.4fniunfv 5789
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5172
[Monk1] p. 52Theorem 5.11(viii)ssint 3894
[Monk1] p. 52Definition 5.13 (i)1stval2 6153  df-1st 6138
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6154  df-2nd 6139
[Monk1] p. 112Theorem 15.17(v)ranksn 7542  ranksnb 7515
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7543
[Monk1] p. 112Theorem 15.17(iii)rankun 7544  rankunb 7538
[Monk1] p. 113Theorem 15.18r1val3 7526
[Monk1] p. 113Definition 15.19df-r1 7452  r1val2 7525
[Monk1] p. 117Lemmazorn2 8149  zorn2g 8146
[Monk1] p. 133Theorem 18.11cardom 7635
[Monk1] p. 133Theorem 18.12canth3 8199
[Monk1] p. 133Theorem 18.14carduni 7630
[Monk2] p. 105Axiom C4ax-5 1547
[Monk2] p. 105Axiom C7ax-8 1661
[Monk2] p. 105Axiom C8ax-11 1727  ax-11o 2093
[Monk2] p. 105Axiom (C8)ax11v 2049
[Monk2] p. 108Lemma 5ax-5o 2088
[Monk2] p. 109Lemma 12ax-7 1720
[Monk2] p. 109Lemma 15equvin 1954  equvini 1940  eqvinop 4267
[Monk2] p. 113Axiom C5-1ax-17 1606  ax17o 2109
[Monk2] p. 113Axiom C5-2ax-6 1715
[Monk2] p. 113Axiom C5-3ax-7 1720
[Monk2] p. 114Lemma 21sp 1728
[Monk2] p. 114Lemma 22ax5o 1729  hba1-o 2101  hba1 1731
[Monk2] p. 114Lemma 23nfia1 1790
[Monk2] p. 114Lemma 24nfa2 1789  nfra2 2610
[Moore] p. 53Part Idf-mre 13504
[Munkres] p. 77Example 2distop 16749  indistop 16755  indistopon 16754
[Munkres] p. 77Example 3fctop 16757  fctop2 16758
[Munkres] p. 77Example 4cctop 16759
[Munkres] p. 78Definition of basisdf-bases 16654  isbasis3g 16703
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13360  tgval2 16710
[Munkres] p. 79Remarktgcl 16723
[Munkres] p. 80Lemma 2.1tgval3 16717
[Munkres] p. 80Lemma 2.2tgss2 16741  tgss3 16740
[Munkres] p. 81Lemma 2.3basgen 16742  basgen2 16743
[Munkres] p. 89Definition of subspace topologyresttop 16907
[Munkres] p. 93Theorem 6.1(1)0cld 16791  topcld 16788
[Munkres] p. 93Theorem 6.1(2)iincld 16792
[Munkres] p. 93Theorem 6.1(3)uncld 16794
[Munkres] p. 94Definition of closureclsval 16790
[Munkres] p. 94Definition of interiorntrval 16789
[Munkres] p. 95Theorem 6.5(a)clsndisj 16828  elcls 16826
[Munkres] p. 95Theorem 6.5(b)elcls3 16836
[Munkres] p. 97Theorem 6.6clslp 16895  neindisj 16870
[Munkres] p. 97Corollary 6.7cldlp 16897
[Munkres] p. 97Definition of limit pointislp2 16893  lpval 16887
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17059
[Munkres] p. 102Definition of continuous functiondf-cn 16973  iscn 16981  iscn2 16984
[Munkres] p. 107Theorem 7.2(g)cncnp 17025  cncnp2 17026  cncnpi 17023  df-cnp 16974  iscnp 16983  iscnp2 16985
[Munkres] p. 127Theorem 10.1metcn 18105
[Munkres] p. 128Theorem 10.3metcn4 18752
[NielsenChuang] p. 195Equation 4.73unierri 22700
[Pfenning] p. 17Definition XMnatded 20806  natded 20806
[Pfenning] p. 17Definition NNCnatded 20806  notnotrd 105
[Pfenning] p. 17Definition ` `Cnatded 20806
[Pfenning] p. 18Rule"natded 20806
[Pfenning] p. 18Definition /\Inatded 20806
[Pfenning] p. 18Definition ` `Enatded 20806  natded 20806  natded 20806  natded 20806  natded 20806
[Pfenning] p. 18Definition ` `Inatded 20806  natded 20806  natded 20806  natded 20806  natded 20806
[Pfenning] p. 18Definition ` `ELnatded 20806
[Pfenning] p. 18Definition ` `ERnatded 20806
[Pfenning] p. 18Definition ` `Ea,unatded 20806
[Pfenning] p. 18Definition ` `IRnatded 20806
[Pfenning] p. 18Definition ` `Ianatded 20806
[Pfenning] p. 127Definition =Enatded 20806
[Pfenning] p. 127Definition =Inatded 20806
[Ponnusamy] p. 361Theorem 6.44cphip0l 18653  df-dip 21290  dip0l 21310  ip0l 16556
[Ponnusamy] p. 361Equation 6.45ipval 21292
[Ponnusamy] p. 362Equation I1dipcj 21306
[Ponnusamy] p. 362Equation I3cphdir 18656  dipdir 21436  ipdir 16559  ipdiri 21424
[Ponnusamy] p. 362Equation I4ipidsq 21302
[Ponnusamy] p. 362Equation 6.46ip0i 21419
[Ponnusamy] p. 362Equation 6.47ip1i 21421
[Ponnusamy] p. 362Equation 6.48ip2i 21422
[Ponnusamy] p. 363Equation I2cphass 18662  dipass 21439  ipass 16565  ipassi 21435
[Prugovecki] p. 186Definition of brabraval 22540  df-bra 22446
[Prugovecki] p. 376Equation 8.1df-kb 22447  kbval 22550
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22978
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30699
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22992  atcvat4i 22993  cvrat3 30253  cvrat4 30254  lsatcvat3 29864
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22878  cvrval 30081  df-cv 22875  df-lcv 29831  lspsncv0 15915
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30711
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30712
[Quine] p. 16Definition 2.1df-clab 2283  rabid 2729
[Quine] p. 17Definition 2.1''dfsb7 2071
[Quine] p. 18Definition 2.7df-cleq 2289
[Quine] p. 19Definition 2.9conventions 20805  df-v 2803
[Quine] p. 34Theorem 5.1abeq2 2401
[Quine] p. 35Theorem 5.2abid2 2413  abid2f 2457
[Quine] p. 40Theorem 6.1sb5 2052
[Quine] p. 40Theorem 6.2sb56 2050  sb6 2051
[Quine] p. 41Theorem 6.3df-clel 2292
[Quine] p. 41Theorem 6.4eqid 2296  eqid1 20856
[Quine] p. 41Theorem 6.5eqcom 2298
[Quine] p. 42Theorem 6.6df-sbc 3005
[Quine] p. 42Theorem 6.7dfsbcq 3006  dfsbcq2 3007
[Quine] p. 43Theorem 6.8vex 2804
[Quine] p. 43Theorem 6.9isset 2805
[Quine] p. 44Theorem 7.3spcgf 2876  spcgv 2881  spcimgf 2874
[Quine] p. 44Theorem 6.11spsbc 3016  spsbcd 3017
[Quine] p. 44Theorem 6.12elex 2809
[Quine] p. 44Theorem 6.13elab 2927  elabg 2928  elabgf 2925
[Quine] p. 44Theorem 6.14noel 3472
[Quine] p. 48Theorem 7.2snprc 3708
[Quine] p. 48Definition 7.1df-pr 3660  df-sn 3659
[Quine] p. 49Theorem 7.4snss 3761  snssg 3767
[Quine] p. 49Theorem 7.5prss 3785  prssg 3786
[Quine] p. 49Theorem 7.6prid1 3747  prid1g 3745  prid2 3748  prid2g 3746  snid 3680  snidg 3678
[Quine] p. 51Theorem 7.13prex 4233  snex 4232  snexALT 4212
[Quine] p. 53Theorem 8.2unisn 3859  unisnALT 29018  unisng 3860
[Quine] p. 53Theorem 8.3uniun 3862
[Quine] p. 54Theorem 8.6elssuni 3871
[Quine] p. 54Theorem 8.7uni0 3870
[Quine] p. 56Theorem 8.17uniabio 5245
[Quine] p. 56Definition 8.18dfiota2 5236
[Quine] p. 57Theorem 8.19iotaval 5246
[Quine] p. 57Theorem 8.22iotanul 5250
[Quine] p. 58Theorem 8.23iotaex 5252
[Quine] p. 58Definition 9.1df-op 3662
[Quine] p. 61Theorem 9.5opabid 4287  opelopab 4302  opelopaba 4297  opelopabaf 4304  opelopabf 4305  opelopabg 4299  opelopabga 4294  oprabid 5898
[Quine] p. 64Definition 9.11df-xp 4711
[Quine] p. 64Definition 9.12df-cnv 4713
[Quine] p. 64Definition 9.15df-id 4325
[Quine] p. 65Theorem 10.3fun0 5323
[Quine] p. 65Theorem 10.4funi 5300
[Quine] p. 65Theorem 10.5funsn 5316  funsng 5314
[Quine] p. 65Definition 10.1df-fun 5273
[Quine] p. 65Definition 10.2args 5057  dffv4 5538
[Quine] p. 68Definition 10.11conventions 20805  df-fv 5279  fv2 5536
[Quine] p. 124Theorem 17.3nn0opth2 11303  nn0opth2i 11302  nn0opthi 11301  omopthi 6671
[Quine] p. 177Definition 25.2df-rdg 6439
[Quine] p. 232Equation icarddom 8192
[Quine] p. 284Axiom 39(vi)funimaex 5346  funimaexg 5345
[Quine] p. 331Axiom system NFru 3003
[ReedSimon] p. 36Definition (iii)ax-his3 21679
[ReedSimon] p. 63Exercise 4(a)df-dip 21290  polid 21754  polid2i 21752  polidi 21753
[ReedSimon] p. 63Exercise 4(b)df-ph 21407
[ReedSimon] p. 195Remarklnophm 22615  lnophmi 22614
[Retherford] p. 49Exercise 1(i)leopadd 22728
[Retherford] p. 49Exercise 1(ii)leopmul 22730  leopmuli 22729
[Retherford] p. 49Exercise 1(iv)leoptr 22733
[Retherford] p. 49Definition VI.1df-leop 22448  leoppos 22722
[Retherford] p. 49Exercise 1(iii)leoptri 22732
[Retherford] p. 49Definition of operator orderingleop3 22721
[Rudin] p. 164Equation 27efcan 12392
[Rudin] p. 164Equation 30efzval 12398
[Rudin] p. 167Equation 48absefi 12492
[Sanford] p. 39Rule 3mtp-xor 1526
[Sanford] p. 39Rule 4mpto2 1524
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 8
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 167
[Sanford] p. 40Rule 1mpto1 1523
[Schechter] p. 51Definition of antisymmetryintasym 5074
[Schechter] p. 51Definition of irreflexivityintirr 5077
[Schechter] p. 51Definition of symmetrycnvsym 5073
[Schechter] p. 51Definition of transitivitycotr 5071
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13504
[Schechter] p. 79Definition of Moore closuredf-mrc 13505
[Schechter] p. 82Section 4.5df-mrc 13505
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13507
[Schechter] p. 139Definition AC3dfac9 7778
[Schechter] p. 141Definition (MC)dfac11 27263
[Schechter] p. 149Axiom DC1ax-dc 8088  axdc3 8096
[Schechter] p. 187Definition of ring with unitisrng 15361  isrngo 21061
[Schechter] p. 276Remark 11.6.espan0 22137
[Schechter] p. 276Definition of spandf-span 21904  spanval 21928
[Schechter] p. 428Definition 15.35bastop1 16747
[Schwabhauser] p. 10Axiom A1axcgrrflx 24614
[Schwabhauser] p. 10Axiom A2axcgrtr 24615
[Schwabhauser] p. 10Axiom A3axcgrid 24616
[Schwabhauser] p. 11Axiom A4axsegcon 24627
[Schwabhauser] p. 11Axiom A5ax5seg 24638
[Schwabhauser] p. 11Axiom A6axbtwnid 24639
[Schwabhauser] p. 12Axiom A7axpasch 24641
[Schwabhauser] p. 12Axiom A8axlowdim2 24660
[Schwabhauser] p. 13Axiom A10axeuclid 24663
[Schwabhauser] p. 13Axiom A11axcont 24676
[Schwabhauser] p. 27Theorem 2.1cgrrflx 24682
[Schwabhauser] p. 27Theorem 2.2cgrcomim 24684
[Schwabhauser] p. 27Theorem 2.3cgrtr 24687
[Schwabhauser] p. 27Theorem 2.4cgrcoml 24691
[Schwabhauser] p. 27Theorem 2.5cgrcomr 24692
[Schwabhauser] p. 28Theorem 2.8cgrtriv 24697
[Schwabhauser] p. 28Theorem 2.105segofs 24701
[Schwabhauser] p. 28Definition 2.10df-ofs 24678
[Schwabhauser] p. 29Theorem 2.11cgrextend 24703
[Schwabhauser] p. 29Theorem 2.12segconeq 24705
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24717  btwntriv2 24707
[Schwabhauser] p. 30Theorem 3.2btwncomim 24708
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24711
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24712
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24718  btwnintr 24714
[Schwabhauser] p. 30Theorem 3.6btwnexch 24720  btwnexch3 24715
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24719
[Schwabhauser] p. 32Theorem 3.13axlowdim1 24659
[Schwabhauser] p. 32Theorem 3.14btwndiff 24722
[Schwabhauser] p. 33Theorem 3.17trisegint 24723
[Schwabhauser] p. 34Theorem 4.2ifscgr 24739
[Schwabhauser] p. 34Definition 4.1df-ifs 24734
[Schwabhauser] p. 35Theorem 4.3cgrsub 24740
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24750
[Schwabhauser] p. 35Definition 4.4df-cgr3 24735
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24751
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24757  colinearperm2 24759  colinearperm3 24758  colinearperm4 24760  colinearperm5 24761
[Schwabhauser] p. 36Definition 4.10df-colinear 24736
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24762
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24770
[Schwabhauser] p. 37Theorem 4.14lineext 24771
[Schwabhauser] p. 37Theorem 4.16fscgr 24775
[Schwabhauser] p. 37Theorem 4.17linecgr 24776
[Schwabhauser] p. 37Definition 4.15df-fs 24737
[Schwabhauser] p. 38Theorem 4.18lineid 24778
[Schwabhauser] p. 38Theorem 4.19idinside 24779
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24796
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24797
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24798
[Schwabhauser] p. 41Theorem 5.5brsegle2 24804
[Schwabhauser] p. 41Definition 5.4df-segle 24802
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24805
[Schwabhauser] p. 42Theorem 5.7seglerflx 24807
[Schwabhauser] p. 42Theorem 5.8segletr 24809
[Schwabhauser] p. 42Theorem 5.9segleantisym 24810
[Schwabhauser] p. 42Theorem 5.10seglelin 24811
[Schwabhauser] p. 42Theorem 5.11seglemin 24808
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24813
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24820
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24821
[Schwabhauser] p. 43Theorem 6.4broutsideof 24816  df-outsideof 24815
[Schwabhauser] p. 43Definition 6.1broutsideof2 24817
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24822
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24823
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24824
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24826
[Schwabhauser] p. 44Definition 6.8df-ray 24833
[Schwabhauser] p. 45Part 2df-lines2 24834
[Schwabhauser] p. 45Theorem 6.13outsidele 24827
[Schwabhauser] p. 45Theorem 6.15lineunray 24842
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24843
[Schwabhauser] p. 45Theorem 6.17linecom 24845  linerflx1 24844  linerflx2 24846
[Schwabhauser] p. 45Theorem 6.18linethru 24848
[Schwabhauser] p. 45Definition 6.14df-line2 24832
[Schwabhauser] p. 46Theorem 6.19linethrueu 24851
[Schwabhauser] p. 46Theorem 6.21lineintmo 24852
[Shapiro] p. 230Theorem 6.5.1dchrhash 20526  dchrsum 20524  dchrsum2 20523  sumdchr 20527
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20528  sum2dchr 20529
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15317  ablfacrp2 15318
[Shapiro], p. 328Equation 9.2.4vmasum 20471
[Shapiro], p. 329Equation 9.2.7logfac2 20472
[Shapiro], p. 329Equation 9.2.9logfacrlim 20479
[Shapiro], p. 331Equation 9.2.13vmadivsum 20647
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20650
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20704  vmalogdivsum2 20703
[Shapiro], p. 375Theorem 9.4.1dirith 20694  dirith2 20693
[Shapiro], p. 375Equation 9.4.3rplogsum 20692  rpvmasum 20691  rpvmasum2 20677
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20652
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20690
[Shapiro], p. 377Lemma 9.4.1dchrisum 20657  dchrisumlem1 20654  dchrisumlem2 20655  dchrisumlem3 20656  dchrisumlema 20653
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20660
[Shapiro], p. 379Equation 9.4.16dchrmusum 20689  dchrmusumlem 20687  dchrvmasumlem 20688
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20659
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20661
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20685  dchrisum0re 20678  dchrisumn0 20686
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20671
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20675
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20676
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20731  pntrsumbnd2 20732  pntrsumo1 20730
[Shapiro], p. 405Equation 10.2.1mudivsum 20695
[Shapiro], p. 406Equation 10.2.6mulogsum 20697
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20699
[Shapiro], p. 407Equation 10.2.8mulog2sum 20702
[Shapiro], p. 418Equation 10.4.6logsqvma 20707
[Shapiro], p. 418Equation 10.4.8logsqvma2 20708
[Shapiro], p. 419Equation 10.4.10selberg 20713
[Shapiro], p. 420Equation 10.4.12selberg2lem 20715
[Shapiro], p. 420Equation 10.4.14selberg2 20716
[Shapiro], p. 422Equation 10.6.7selberg3 20724
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20725
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20722  selberg3lem2 20723
[Shapiro], p. 422Equation 10.4.23selberg4 20726
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20720
[Shapiro], p. 428Equation 10.6.2selbergr 20733
[Shapiro], p. 429Equation 10.6.8selberg3r 20734
[Shapiro], p. 430Equation 10.6.11selberg4r 20735
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20749
[Shapiro], p. 434Equation 10.6.27pntlema 20761  pntlemb 20762  pntlemc 20760  pntlemd 20759  pntlemg 20763
[Shapiro], p. 435Equation 10.6.29pntlema 20761
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20753
[Shapiro], p. 436Lemma 10.6.2pntibnd 20758
[Shapiro], p. 436Equation 10.6.34pntlema 20761
[Shapiro], p. 436Equation 10.6.35pntlem3 20774  pntleml 20776
[Stoll] p. 13Definition of symmetric differencesymdif1 3446
[Stoll] p. 16Exercise 4.40dif 3538  dif0 3537
[Stoll] p. 16Exercise 4.8difdifdir 3554
[Stoll] p. 17Theorem 5.1(5)undifv 3541
[Stoll] p. 19Theorem 5.2(13)undm 3439
[Stoll] p. 19Theorem 5.2(13')indm 3440
[Stoll] p. 20Remarkinvdif 3423
[Stoll] p. 25Definition of ordered tripledf-ot 3663
[Stoll] p. 43Definitionuniiun 3971
[Stoll] p. 44Definitionintiin 3972
[Stoll] p. 45Definitiondf-iin 3924
[Stoll] p. 45Definition indexed uniondf-iun 3923
[Stoll] p. 176Theorem 3.4(27)iman 413
[Stoll] p. 262Example 4.1symdif1 3446
[Strang] p. 242Section 6.3expgrowth 27655
[Suppes] p. 22Theorem 2eq0 3482
[Suppes] p. 22Theorem 4eqss 3207  eqssd 3209  eqssi 3208
[Suppes] p. 23Theorem 5ss0 3498  ss0b 3497
[Suppes] p. 23Theorem 6sstr 3200  sstrALT2 28927
[Suppes] p. 23Theorem 7pssirr 3289
[Suppes] p. 23Theorem 8pssn2lp 3290
[Suppes] p. 23Theorem 9psstr 3293
[Suppes] p. 23Theorem 10pssss 3284
[Suppes] p. 25Theorem 12elin 3371  elun 3329
[Suppes] p. 26Theorem 15inidm 3391
[Suppes] p. 26Theorem 16in0 3493
[Suppes] p. 27Theorem 23unidm 3331
[Suppes] p. 27Theorem 24un0 3492
[Suppes] p. 27Theorem 25ssun1 3351
[Suppes] p. 27Theorem 26ssequn1 3358
[Suppes] p. 27Theorem 27unss 3362
[Suppes] p. 27Theorem 28indir 3430
[Suppes] p. 27Theorem 29undir 3431
[Suppes] p. 28Theorem 32difid 3535  difidALT 3536
[Suppes] p. 29Theorem 33difin 3419
[Suppes] p. 29Theorem 34indif 3424
[Suppes] p. 29Theorem 35undif1 3542
[Suppes] p. 29Theorem 36difun2 3546
[Suppes] p. 29Theorem 37difin0 3540
[Suppes] p. 29Theorem 38disjdif 3539
[Suppes] p. 29Theorem 39difundi 3434
[Suppes] p. 29Theorem 40difindi 3436
[Suppes] p. 30Theorem 41nalset 4167
[Suppes] p. 39Theorem 61uniss 3864
[Suppes] p. 39Theorem 65uniop 4285
[Suppes] p. 41Theorem 70intsn 3914
[Suppes] p. 42Theorem 71intpr 3911  intprg 3912
[Suppes] p. 42Theorem 73op1stb 4585
[Suppes] p. 42Theorem 78intun 3910
[Suppes] p. 44Definition 15(a)dfiun2 3953  dfiun2g 3951
[Suppes] p. 44Definition 15(b)dfiin2 3954
[Suppes] p. 47Theorem 86elpw 3644  elpw2 4191  elpw2g 4190  elpwg 3645  elpwgdedVD 29009
[Suppes] p. 47Theorem 87pwid 3651
[Suppes] p. 47Theorem 89pw0 3778
[Suppes] p. 48Theorem 90pwpw0 3779
[Suppes] p. 52Theorem 101xpss12 4808
[Suppes] p. 52Theorem 102xpindi 4835  xpindir 4836
[Suppes] p. 52Theorem 103xpundi 4757  xpundir 4758
[Suppes] p. 54Theorem 105elirrv 7327
[Suppes] p. 58Theorem 2relss 4791
[Suppes] p. 59Theorem 4eldm 4892  eldm2 4893  eldm2g 4891  eldmg 4890
[Suppes] p. 59Definition 3df-dm 4715
[Suppes] p. 60Theorem 6dmin 4902
[Suppes] p. 60Theorem 8rnun 5105
[Suppes] p. 60Theorem 9rnin 5106
[Suppes] p. 60Definition 4dfrn2 4884
[Suppes] p. 61Theorem 11brcnv 4880  brcnvg 4878
[Suppes] p. 62Equation 5elcnv 4874  elcnv2 4875
[Suppes] p. 62Theorem 12relcnv 5067
[Suppes] p. 62Theorem 15cnvin 5104
[Suppes] p. 62Theorem 16cnvun 5102
[Suppes] p. 63Theorem 20co02 5202
[Suppes] p. 63Theorem 21dmcoss 4960
[Suppes] p. 63Definition 7df-co 4714
[Suppes] p. 64Theorem 26cnvco 4881
[Suppes] p. 64Theorem 27coass 5207
[Suppes] p. 65Theorem 31resundi 4985
[Suppes] p. 65Theorem 34elima 5033  elima2 5034  elima3 5035  elimag 5032
[Suppes] p. 65Theorem 35imaundi 5109
[Suppes] p. 66Theorem 40dminss 5111
[Suppes] p. 66Theorem 41imainss 5112
[Suppes] p. 67Exercise 11cnvxp 5113
[Suppes] p. 81Definition 34dfec2 6679
[Suppes] p. 82Theorem 72elec 6715  elecg 6714
[Suppes] p. 82Theorem 73erth 6720  erth2 6721
[Suppes] p. 83Theorem 74erdisj 6723
[Suppes] p. 89Theorem 96map0b 6822
[Suppes] p. 89Theorem 97map0 6824  map0g 6823
[Suppes] p. 89Theorem 98mapsn 6825
[Suppes] p. 89Theorem 99mapss 6826
[Suppes] p. 91Definition 12(ii)alephsuc 7711
[Suppes] p. 91Definition 12(iii)alephlim 7710
[Suppes] p. 92Theorem 1enref 6910  enrefg 6909
[Suppes] p. 92Theorem 2ensym 6926  ensymb 6925  ensymi 6927
[Suppes] p. 92Theorem 3entr 6929
[Suppes] p. 92Theorem 4unen 6959
[Suppes] p. 94Theorem 15endom 6904
[Suppes] p. 94Theorem 16ssdomg 6923
[Suppes] p. 94Theorem 17domtr 6930
[Suppes] p. 95Theorem 18sbth 6997
[Suppes] p. 97Theorem 23canth2 7030  canth2g 7031
[Suppes] p. 97Definition 3brsdom2 7001  df-sdom 6882  dfsdom2 7000
[Suppes] p. 97Theorem 21(i)sdomirr 7014
[Suppes] p. 97Theorem 22(i)domnsym 7003
[Suppes] p. 97Theorem 21(ii)sdomnsym 7002
[Suppes] p. 97Theorem 22(ii)domsdomtr 7012
[Suppes] p. 97Theorem 22(iv)brdom2 6907
[Suppes] p. 97Theorem 21(iii)sdomtr 7015
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7010
[Suppes] p. 98Exercise 4fundmen 6950  fundmeng 6951
[Suppes] p. 98Exercise 6xpdom3 6976
[Suppes] p. 98Exercise 11sdomentr 7011
[Suppes] p. 104Theorem 37fofi 7158
[Suppes] p. 104Theorem 38pwfi 7167
[Suppes] p. 105Theorem 40pwfi 7167
[Suppes] p. 111Axiom for cardinal numberscarden 8189
[Suppes] p. 130Definition 3df-tr 4130
[Suppes] p. 132Theorem 9ssonuni 4594
[Suppes] p. 134Definition 6df-suc 4414
[Suppes] p. 136Theorem Schema 22findes 4702  finds 4698  finds1 4701  finds2 4700
[Suppes] p. 151Theorem 42isfinite 7369  isfinite2 7131  isfiniteg 7133  unbnn 7129
[Suppes] p. 162Definition 5df-ltnq 8558  df-ltpq 8550
[Suppes] p. 197Theorem Schema 4tfindes 4669  tfinds 4666  tfinds2 4670
[Suppes] p. 209Theorem 18oaord1 6565
[Suppes] p. 209Theorem 21oaword2 6567
[Suppes] p. 211Theorem 25oaass 6575
[Suppes] p. 225Definition 8iscard2 7625
[Suppes] p. 227Theorem 56ondomon 8201
[Suppes] p. 228Theorem 59harcard 7627
[Suppes] p. 228Definition 12(i)aleph0 7709
[Suppes] p. 228Theorem Schema 61onintss 4458
[Suppes] p. 228Theorem Schema 62onminesb 4605  onminsb 4606
[Suppes] p. 229Theorem 64alephval2 8210
[Suppes] p. 229Theorem 65alephcard 7713
[Suppes] p. 229Theorem 66alephord2i 7720
[Suppes] p. 229Theorem 67alephnbtwn 7714
[Suppes] p. 229Definition 12df-aleph 7589
[Suppes] p. 242Theorem 6weth 8138
[Suppes] p. 242Theorem 8entric 8195
[Suppes] p. 242Theorem 9carden 8189
[TakeutiZaring] p. 8Axiom 1ax-ext 2277
[TakeutiZaring] p. 13Definition 4.5df-cleq 2289
[TakeutiZaring] p. 13Proposition 4.6df-clel 2292
[TakeutiZaring] p. 13Proposition 4.9cvjust 2291
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2313
[TakeutiZaring] p. 14Definition 4.16df-oprab 5878
[TakeutiZaring] p. 14Proposition 4.14ru 3003
[TakeutiZaring] p. 15Axiom 2zfpair 4228
[TakeutiZaring] p. 15Exercise 1elpr 3671  elpr2 3672  elprg 3670
[TakeutiZaring] p. 15Exercise 2elsn 3668  elsnc 3676  elsnc2 3682  elsnc2g 3681  elsncg 3675
[TakeutiZaring] p. 15Exercise 3elop 4255
[TakeutiZaring] p. 15Exercise 4sneq 3664  sneqr 3796
[TakeutiZaring] p. 15Definition 5.1dfpr2 3669  dfsn2 3667
[TakeutiZaring] p. 16Axiom 3uniex 4532
[TakeutiZaring] p. 16Exercise 6opth 4261
[TakeutiZaring] p. 16Exercise 7opex 4253
[TakeutiZaring] p. 16Exercise 8rext 4238
[TakeutiZaring] p. 16Corollary 5.8unex 4534  unexg 4537
[TakeutiZaring] p. 16Definition 5.3dftp2 3692
[TakeutiZaring] p. 16Definition 5.5df-uni 3844
[TakeutiZaring] p. 16Definition 5.6df-in 3172  df-un 3170
[TakeutiZaring] p. 16Proposition 5.7unipr 3857  uniprg 3858
[TakeutiZaring] p. 17Axiom 4pwex 4209  pwexg 4210
[TakeutiZaring] p. 17Exercise 1eltp 3691
[TakeutiZaring] p. 17Exercise 5elsuc 4477  elsucg 4475  sstr2 3199
[TakeutiZaring] p. 17Exercise 6uncom 3332
[TakeutiZaring] p. 17Exercise 7incom 3374
[TakeutiZaring] p. 17Exercise 8unass 3345
[TakeutiZaring] p. 17Exercise 9inass 3392
[TakeutiZaring] p. 17Exercise 10indi 3428
[TakeutiZaring] p. 17Exercise 11undi 3429
[TakeutiZaring] p. 17Definition 5.9df-pss 3181  dfss2 3182
[TakeutiZaring] p. 17Definition 5.10df-pw 3640
[TakeutiZaring] p. 18Exercise 7unss2 3359
[TakeutiZaring] p. 18Exercise 9df-ss 3179  sseqin2 3401
[TakeutiZaring] p. 18Exercise 10ssid 3210
[TakeutiZaring] p. 18Exercise 12inss1 3402  inss2 3403
[TakeutiZaring] p. 18Exercise 13nss 3249
[TakeutiZaring] p. 18Exercise 15unieq 3852
[TakeutiZaring] p. 18Exercise 18sspwb 4239  sspwimp 29010  sspwimpALT 29017  sspwimpALT2 29021  sspwimpcf 29012
[TakeutiZaring] p. 18Exercise 19pweqb 4246
[TakeutiZaring] p. 19Axiom 5ax-rep 4147
[TakeutiZaring] p. 20Definitiondf-rab 2565
[TakeutiZaring] p. 20Corollary 5.160ex 4166
[TakeutiZaring] p. 20Definition 5.12df-dif 3168
[TakeutiZaring] p. 20Definition 5.14dfnul2 3470
[TakeutiZaring] p. 20Proposition 5.15difid 3535  difidALT 3536
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3477  n0f 3476  neq0 3478
[TakeutiZaring] p. 21Axiom 6zfreg 7325
[TakeutiZaring] p. 21Axiom 6'zfregs 7430
[TakeutiZaring] p. 21Theorem 5.22setind 7435
[TakeutiZaring] p. 21Definition 5.20df-v 2803
[TakeutiZaring] p. 21Proposition 5.21vprc 4168
[TakeutiZaring] p. 22Exercise 10ss 3496
[TakeutiZaring] p. 22Exercise 3ssex 4174  ssexg 4176
[TakeutiZaring] p. 22Exercise 4inex1 4171
[TakeutiZaring] p. 22Exercise 5ruv 7330
[TakeutiZaring] p. 22Exercise 6elirr 7328
[TakeutiZaring] p. 22Exercise 7ssdif0 3526
[TakeutiZaring] p. 22Exercise 11difdif 3315
[TakeutiZaring] p. 22Exercise 13undif3 3442  undif3VD 28974
[TakeutiZaring] p. 22Exercise 14difss 3316
[TakeutiZaring] p. 22Exercise 15sscon 3323
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2561
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2562
[TakeutiZaring] p. 23Proposition 6.2xpex 4817  xpexg 4816  xpexgALT 6086
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4712
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5328
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5461  fun11 5331
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5283  svrelfun 5329
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4883
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4885
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4717
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4718
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4714
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5144  dfrel2 5140
[TakeutiZaring] p. 25Exercise 3xpss 4809
[TakeutiZaring] p. 25Exercise 5relun 4818
[TakeutiZaring] p. 25Exercise 6reluni 4824
[TakeutiZaring] p. 25Exercise 9inxp 4834
[TakeutiZaring] p. 25Exercise 12relres 4999
[TakeutiZaring] p. 25Exercise 13opelres 4976  opelresg 4978
[TakeutiZaring] p. 25Exercise 14dmres 4992
[TakeutiZaring] p. 25Exercise 15resss 4995
[TakeutiZaring] p. 25Exercise 17resabs1 5000
[TakeutiZaring] p. 25Exercise 18funres 5309
[TakeutiZaring] p. 25Exercise 24relco 5187
[TakeutiZaring] p. 25Exercise 29funco 5308
[TakeutiZaring] p. 25Exercise 30f1co 5462
[TakeutiZaring] p. 26Definition 6.10eu2 2181
[TakeutiZaring] p. 26Definition 6.11conventions 20805  df-fv 5279  fv3 5557
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5225  cnvexg 5224
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4957  dmexg 4955
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4958  rnexg 4956
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27761
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27762
[TakeutiZaring] p. 27Corollary 6.13fvex 5555
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 28142  tz6.12-1 5560  tz6.12-afv 28141  tz6.12 5561  tz6.12c 5563
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5532  tz6.12i 5564
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5274
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5275
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5277  wfo 5269
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5276  wf1 5268
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5278  wf1o 5270
[TakeutiZaring] p. 28Exercise 4eqfnfv 5638  eqfnfv2 5639  eqfnfv2f 5642
[TakeutiZaring] p. 28Exercise 5fvco 5611
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5757  fnexALT 5758
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5753  resfunexgALT 5754
[TakeutiZaring] p. 29Exercise 9funimaex 5346  funimaexg 5345
[TakeutiZaring] p. 29Definition 6.18df-br 4040
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4331
[TakeutiZaring] p. 30Definition 6.21dffr2 4374  dffr3 5061  eliniseg 5058  iniseg 5060
[TakeutiZaring] p. 30Definition 6.22df-eprel 4321
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4387  fr3nr 4587  frirr 4386
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4368
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4589
[TakeutiZaring] p. 31Exercise 1frss 4376
[TakeutiZaring] p. 31Exercise 4wess 4396
[TakeutiZaring] p. 31Proposition 6.26tz6.26 24276  tz6.26i 24277  wefrc 4403  wereu2 4406
[TakeutiZaring] p. 32Theorem 6.27wfi 24278  wfii 24279
[TakeutiZaring] p. 32Definition 6.28df-isom 5280
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5842
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5843
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5849
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5850
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5851
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5855
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5862
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5864
[TakeutiZaring] p. 35Notationwtr 4129
[TakeutiZaring] p. 35Theorem 7.2trelpss 27763  tz7.2 4393
[TakeutiZaring] p. 35Definition 7.1dftr3 4133
[TakeutiZaring] p. 36Proposition 7.4ordwe 4421
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4429
[TakeutiZaring] p. 36Proposition 7.6ordelord 4430  ordelordALT 28600  ordelordALTVD 28959
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4436  ordelssne 4435
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4434
[TakeutiZaring] p. 37Proposition 7.9ordin 4438
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4596
[TakeutiZaring] p. 38Corollary 7.15ordsson 4597
[TakeutiZaring] p. 38Definition 7.11df-on 4412
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4440
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28613  ordon 4590
[TakeutiZaring] p. 38Proposition 7.13onprc 4592
[TakeutiZaring] p. 39Theorem 7.17tfi 4660
[TakeutiZaring] p. 40Exercise 3ontr2 4455
[TakeutiZaring] p. 40Exercise 7dftr2 4131
[TakeutiZaring] p. 40Exercise 9onssmin 4604
[TakeutiZaring] p. 40Exercise 11unon 4638
[TakeutiZaring] p. 40Exercise 12ordun 4510
[TakeutiZaring] p. 40Exercise 14ordequn 4509
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4593
[TakeutiZaring] p. 40Proposition 7.20elssuni 3871
[TakeutiZaring] p. 41Definition 7.22df-suc 4414
[TakeutiZaring] p. 41Proposition 7.23sssucid 4485  sucidg 4486
[TakeutiZaring] p. 41Proposition 7.24suceloni 4620
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4500  ordnbtwn 4499
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4635
[TakeutiZaring] p. 42Exercise 1df-lim 4413
[TakeutiZaring] p. 42Exercise 4omssnlim 4686
[TakeutiZaring] p. 42Exercise 7ssnlim 4690
[TakeutiZaring] p. 42Exercise 8onsucssi 4648  ordelsuc 4627
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4629
[TakeutiZaring] p. 42Definition 7.27nlimon 4658
[TakeutiZaring] p. 42Definition 7.28dfom2 4674
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4691
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4692
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4693
[TakeutiZaring] p. 43Remarkomon 4683
[TakeutiZaring] p. 43Axiom 7inf3 7352  omex 7360
[TakeutiZaring] p. 43Theorem 7.32ordom 4681
[TakeutiZaring] p. 43Corollary 7.31find 4697
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4694
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4695
[TakeutiZaring] p. 44Exercise 1limomss 4677
[TakeutiZaring] p. 44Exercise 2int0 3892  trint0 4146
[TakeutiZaring] p. 44Exercise 4intss1 3893
[TakeutiZaring] p. 44Exercise 5intex 4183
[TakeutiZaring] p. 44Exercise 6oninton 4607
[TakeutiZaring] p. 44Exercise 11ordintdif 4457
[TakeutiZaring] p. 44Definition 7.35df-int 3879
[TakeutiZaring] p. 44Proposition 7.34noinfep 7376
[TakeutiZaring] p. 45Exercise 4onint 4602
[TakeutiZaring] p. 47Lemma 1tfrlem1 6407
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6429
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6430
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6431
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6435  tz7.44-2 6436  tz7.44-3 6437
[TakeutiZaring] p. 50Exercise 1smogt 6400
[TakeutiZaring] p. 50Exercise 3smoiso 6395
[TakeutiZaring] p. 50Definition 7.46df-smo 6379
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6473  tz7.49c 6474
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6471
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6470
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6472
[TakeutiZaring] p. 53Proposition 7.532eu5 2240
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7655
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7656
[TakeutiZaring] p. 56Definition 8.1oalim 6547  oasuc 6539
[TakeutiZaring] p. 57Remarktfindsg 4667
[TakeutiZaring] p. 57Proposition 8.2oacl 6550
[TakeutiZaring] p. 57Proposition 8.3oa0 6531  oa0r 6553
[TakeutiZaring] p. 57Proposition 8.16omcl 6551
[TakeutiZaring] p. 58Corollary 8.5oacan 6562
[TakeutiZaring] p. 58Proposition 8.4nnaord 6633  nnaordi 6632  oaord 6561  oaordi 6560
[TakeutiZaring] p. 59Proposition 8.6iunss2 3963  uniss2 3874
[TakeutiZaring] p. 59Proposition 8.7oawordri 6564
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6569  oawordex 6571
[TakeutiZaring] p. 59Proposition 8.9nnacl 6625
[TakeutiZaring] p. 59Proposition 8.10oaabs 6658
[TakeutiZaring] p. 60Remarkoancom 7368
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6574
[TakeutiZaring] p. 62Exercise 1nnarcl 6630
[TakeutiZaring] p. 62Exercise 5oaword1 6566
[TakeutiZaring] p. 62Definition 8.15om0 6532  om0x 6534  omlim 6548  omsuc 6541
[TakeutiZaring] p. 63Proposition 8.17nnecl 6627  nnmcl 6626
[TakeutiZaring] p. 63Proposition 8.19nnmord 6646  nnmordi 6645  omord 6582  omordi 6580
[TakeutiZaring] p. 63Proposition 8.20omcan 6583
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6650  omwordri 6586
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6554
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6556  om1r 6557
[TakeutiZaring] p. 64Proposition 8.22om00 6589
[TakeutiZaring] p. 64Proposition 8.23omordlim 6591
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6592
[TakeutiZaring] p. 64Proposition 8.25odi 6593
[TakeutiZaring] p. 65Theorem 8.26omass 6594
[TakeutiZaring] p. 67Definition 8.30nnesuc 6622  oe0 6537  oelim 6549  oesuc 6542  onesuc 6545
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6535
[TakeutiZaring] p. 67Proposition 8.32oen0 6600
[TakeutiZaring] p. 67Proposition 8.33oeordi 6601
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6536
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6559
[TakeutiZaring] p. 68Corollary 8.34oeord 6602
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6608
[TakeutiZaring] p. 68Proposition 8.35oewordri 6606
[TakeutiZaring] p. 68Proposition 8.37oeworde 6607
[TakeutiZaring] p. 69Proposition 8.41oeoa 6611
[TakeutiZaring] p. 70Proposition 8.42oeoe 6613
[TakeutiZaring] p. 73Theorem 9.1trcl 7426  tz9.1 7427
[TakeutiZaring] p. 76Definition 9.9df-r1 7452  r10 7456  r1lim 7460  r1limg 7459  r1suc 7458  r1sucg 7457
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7468  r1ord2 7469  r1ordg 7466
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7478
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7503  tz9.13 7479  tz9.13g 7480
[TakeutiZaring] p. 79Definition 9.14df-rank 7453  rankval 7504  rankvalb 7485  rankvalg 7505
[TakeutiZaring] p. 79Proposition 9.16rankel 7527  rankelb 7512
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7541  rankval3 7528  rankval3b 7514
[TakeutiZaring] p. 79Proposition 9.18rankonid 7517
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7483
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7522  rankr1c 7509  rankr1g 7520
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7523
[TakeutiZaring] p. 80Exercise 1rankss 7537  rankssb 7536
[TakeutiZaring] p. 80Exercise 2unbndrank 7530
[TakeutiZaring] p. 80Proposition 9.19bndrank 7529
[TakeutiZaring] p. 83Axiom of Choiceac4 8118  dfac3 7764
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7673  numth 8115  numth2 8114
[TakeutiZaring] p. 85Definition 10.4cardval 8184
[TakeutiZaring] p. 85Proposition 10.5cardid 8185  cardid2 7602
[TakeutiZaring] p. 85Proposition 10.9oncard 7609
[TakeutiZaring] p. 85Proposition 10.10carden 8189
[TakeutiZaring] p. 85Proposition 10.11cardidm 7608
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7593
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7614
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7606
[TakeutiZaring] p. 87Proposition 10.15pwen 7050
[TakeutiZaring] p. 88Exercise 1en0 6940
[TakeutiZaring] p. 88Exercise 7infensuc 7055
[TakeutiZaring] p. 89Exercise 10omxpen 6980
[TakeutiZaring] p. 90Corollary 10.23cardnn 7612
[TakeutiZaring] p. 90Definition 10.27alephiso 7741
[TakeutiZaring] p. 90Proposition 10.20nneneq 7060
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7066
[TakeutiZaring] p. 90Proposition 10.26alephprc 7742
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7065
[TakeutiZaring] p. 91Exercise 2alephle 7731
[TakeutiZaring] p. 91Exercise 3aleph0 7709
[TakeutiZaring] p. 91Exercise 4cardlim 7621
[TakeutiZaring] p. 91Exercise 7infpss 7859
[TakeutiZaring] p. 91Exercise 8infcntss 7146
[TakeutiZaring] p. 91Definition 10.29df-fin 6883  isfi 6901
[TakeutiZaring] p. 92Proposition 10.32onfin 7067
[TakeutiZaring] p. 92Proposition 10.34imadomg 8175
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6973
[TakeutiZaring] p. 93Proposition 10.35fodomb 8167
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7831  unxpdom 7086
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7623  cardsdomelir 7622
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7088
[TakeutiZaring] p. 94Proposition 10.39infxpen 7658
[TakeutiZaring] p. 95Definition 10.42df-map 6790
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8200  infxpidm2 7660
[TakeutiZaring] p. 95Proposition 10.41infcda 7850  infxp 7857  infxpg 25198
[TakeutiZaring] p. 96Proposition 10.44pw2en 6985  pw2f1o 6983
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7043
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8130
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8125  ac6s5 8134
[TakeutiZaring] p. 98Theorem 10.47unidom 8181
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8182  uniimadomf 8183
[TakeutiZaring] p. 100Definition 11.1cfcof 7916
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7911
[TakeutiZaring] p. 102Exercise 1cfle 7896
[TakeutiZaring] p. 102Exercise 2cf0 7893
[TakeutiZaring] p. 102Exercise 3cfsuc 7899
[TakeutiZaring] p. 102Exercise 4cfom 7906
[TakeutiZaring] p. 102Proposition 11.9coftr 7915
[TakeutiZaring] p. 103Theorem 11.15alephreg 8220
[TakeutiZaring] p. 103Proposition 11.11cardcf 7894
[TakeutiZaring] p. 103Proposition 11.13alephsing 7918
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7740
[TakeutiZaring] p. 104Proposition 11.16carduniima 7739
[TakeutiZaring] p. 104Proposition 11.18alephfp 7751  alephfp2 7752
[TakeutiZaring] p. 106Theorem 11.20gchina 8337
[TakeutiZaring] p. 106Theorem 11.21mappwen 7755
[TakeutiZaring] p. 107Theorem 11.26konigth 8207
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8221
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8222
[Tarski] p. 67Axiom B5ax-4 2087
[Tarski] p. 67Scheme B5sp 1728
[Tarski] p. 68Lemma 6avril1 20852  equid 1662  equid1 2110  equid1ALT 2128
[Tarski] p. 69Lemma 7equcomi 1664
[Tarski] p. 70Lemma 14spim 1928  spime 1929  spimeh 1734
[Tarski] p. 70Lemma 16ax-11 1727  ax-11o 2093  ax11i 1637
[Tarski] p. 70Lemmas 16 and 17sb6 2051
[Tarski] p. 75Axiom B7ax9v 1645
[Tarski] p. 75Scheme B7ax9vax9 29780
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1606  ax17o 2109
[Tarski], p. 75Scheme B8 of system S2ax-13 1698  ax-14 1700  ax-8 1661
[Truss] p. 114Theorem 5.18ruc 12537
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 499
[WhiteheadRussell] p. 96Axiom *1.3olc 373
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 375
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 508
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 814
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 160
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 108
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 76
[WhiteheadRussell] p. 100Theorem *2.05imim2 49
[WhiteheadRussell] p. 100Theorem *2.06imim1 70
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 406
[WhiteheadRussell] p. 101Theorem *2.06barbara 2253  syl 15
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 385
[WhiteheadRussell] p. 101Theorem *2.08id 19  id1 20
[WhiteheadRussell] p. 101Theorem *2.11exmid 404
[WhiteheadRussell] p. 101Theorem *2.12notnot1 114
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 407
[WhiteheadRussell] p. 102Theorem *2.14notnot2 104  notnot2ALT2 29019
[WhiteheadRussell] p. 102Theorem *2.15con1 120
[WhiteheadRussell] p. 103Theorem *2.16con3 126  con3th 924
[WhiteheadRussell] p. 103Theorem *2.17ax-3 7
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 102
[WhiteheadRussell] p. 104Theorem *2.2orc 374
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 555
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 100
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 101
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 393
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 853
[WhiteheadRussell] p. 104Theorem *2.27conventions 20805  pm2.27 35
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 511
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 512
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 816
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 817
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 815
[WhiteheadRussell] p. 105Definition *2.33df-3or 935
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 558
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 556
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 557
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 47
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 386
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 387
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 144
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 162
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 388
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 389
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 390
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 145
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 147
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 362
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 363
[WhiteheadRussell] p. 107Theorem *2.55orel1 371
[WhiteheadRussell] p. 107Theorem *2.56orel2 372
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 163
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 398
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 763
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 764
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 164
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 391  pm2.67 392
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 146
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 397
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 823
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 399
[WhiteheadRussell] p. 108Theorem *2.69looinv 174
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 818
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 819
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 822
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 821
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 824
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 825
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 71
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 826
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 94
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 484
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 434  pm3.2im 137
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 485
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 486
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 487
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 488
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 435
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 436
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 852
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 570
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 431
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 432
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 443  simplim 143
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 447  simprim 142
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 568
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 569
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 562
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 544
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 542
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 543
[WhiteheadRussell] p. 113Theorem *3.44jao 498  pm3.44 497
[WhiteheadRussell] p. 113Theorem *3.47prth 554
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 832
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 807
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 806
[WhiteheadRussell] p. 116Theorem *4.1con34b 283
[WhiteheadRussell] p. 117Theorem *4.2biid 227
[WhiteheadRussell] p. 117Theorem *4.11notbi 286
[WhiteheadRussell] p. 117Theorem *4.12con2bi 318
[WhiteheadRussell] p. 117Theorem *4.13notnot 282
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 561
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 564
[WhiteheadRussell] p. 117Theorem *4.21bicom 191
[WhiteheadRussell] p. 117Theorem *4.22biantr 897  bitr 689  wl-bitr 24992
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 624
[WhiteheadRussell] p. 117Theorem *4.25oridm 500  pm4.25 501
[WhiteheadRussell] p. 118Theorem *4.3ancom 437
[WhiteheadRussell] p. 118Theorem *4.4andi 837
[WhiteheadRussell] p. 118Theorem *4.31orcom 376
[WhiteheadRussell] p. 118Theorem *4.32anass 630
[WhiteheadRussell] p. 118Theorem *4.33orass 510
[WhiteheadRussell] p. 118Theorem *4.36anbi1 687
[WhiteheadRussell] p. 118Theorem *4.37orbi1 686
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 842
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 841
[WhiteheadRussell] p. 118Definition *4.34df-3an 936
[WhiteheadRussell] p. 119Theorem *4.41ordi 834
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 926
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 893
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 560
[WhiteheadRussell] p. 119Theorem *4.45orabs 828  pm4.45 669  pm4.45im 545
[WhiteheadRussell] p. 120Theorem *4.5anor 475
[WhiteheadRussell] p. 120Theorem *4.6imor 401
[WhiteheadRussell] p. 120Theorem *4.7anclb 530
[WhiteheadRussell] p. 120Theorem *4.51ianor 474
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 477
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 478
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 479
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 480
[WhiteheadRussell] p. 120Theorem *4.56ioran 476  pm4.56 481
[WhiteheadRussell] p. 120Theorem *4.57oran 482  pm4.57 483
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 415
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 408
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 410
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 361
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 416
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 409
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 417
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 611  pm4.71d 615  pm4.71i 613  pm4.71r 612  pm4.71rd 616  pm4.71ri 614
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 846
[WhiteheadRussell] p. 121Theorem *4.73iba 489
[WhiteheadRussell] p. 121Theorem *4.74biorf 394
[WhiteheadRussell] p. 121Theorem *4.76jcab 833  pm4.76 836
[WhiteheadRussell] p. 121Theorem *4.77jaob 758  pm4.77 762
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 565
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 566
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 354
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 355
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 894
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 895
[WhiteheadRussell] p. 122Theorem *4.84imbi1 313
[WhiteheadRussell] p. 122Theorem *4.85imbi2 314
[WhiteheadRussell] p. 122Theorem *4.86bibi1 317  wl-bibi1 24985
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 350  impexp 433  pm4.87 567
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 830
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 854
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 855
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 857
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 856
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 859
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 860
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 858
[WhiteheadRussell] p. 124Theorem *5.18nbbn 347  pm5.18 345
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 349
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 831
[WhiteheadRussell] p. 124Theorem *5.22xor 861
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 863
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 864
[WhiteheadRussell] p. 124Theorem *5.25dfor2 400
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 692
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 351
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 326
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 878
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 900
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 571
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 617
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 848
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 869
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 849
[WhiteheadRussell] p. 125Theorem *5.41imdi 352  pm5.41 353
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 531
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 877
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 771
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 870
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 867
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 693
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 889
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 890
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 902
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 330
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 235
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 903
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 27656
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27657
[WhiteheadRussell] p. 147Theorem *10.2219.26 1583
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27658
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27659
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27660
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1605
[WhiteheadRussell] p. 151Theorem *10.301albitr 27661
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27662
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27663
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27664
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27665
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27667
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27668
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27669
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27666
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27672
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2067
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27673
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27674
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1724
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27675
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27676
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27677
[WhiteheadRussell] p. 162Theorem *11.322alim 27678
[WhiteheadRussell] p. 162Theorem *11.332albi 27679
[WhiteheadRussell] p. 162Theorem *11.342exim 27680
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27682
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27681
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1600
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27684
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27685
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27683
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1563
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27686
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27687
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1570
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27688
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1846  pm11.53g 25067
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27689
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27694
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27690
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27691
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27692
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27693
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27698
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27695
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27696
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27697
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27699
[WhiteheadRussell] p. 175Definition *14.02df-eu 2160
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27710  pm13.13b 27711
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27712
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2531
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2532
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2921
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27718
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27719
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27713
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28617  pm13.193 27714
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27715
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27716
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27717
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27724
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27723
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27722
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3056
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27725  pm14.122b 27726  pm14.122c 27727
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27728  pm14.123b 27729  pm14.123c 27730
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27732
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27731
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27733
[WhiteheadRussell] p. 190Theorem *14.22iota4 5253
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27734
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5254
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27735
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27737
[WhiteheadRussell] p. 192Theorem *14.26eupick 2219  eupickbi 2222  sbaniota 27738
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27736
[WhiteheadRussell] p. 192Theorem *14.271eubi 27739
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27740
[WhiteheadRussell] p. 235Definition *30.01conventions 20805  df-fv 5279
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7649  pm54.43lem 7648
[Young] p. 141Definition of operator orderingleop2 22720
[Young] p. 142Example 12.2(i)0leop 22726  idleop 22727
[vandenDries] p. 42Lemma 61irrapx1 27016
[vandenDries] p. 43Theorem 62pellex 27023  pellexlem1 27017

This page was last updated on 8-Dec-2017.
Copyright terms: Public domain