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 13585
[Adamek] p. 29Proposition 3.14(1)invinv 13599
[Adamek] p. 29Proposition 3.14(2)invco 13600  isoco 13602
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25522
[AitkenIBCG] p. 3Definition 2df-angtrg 25518  df-trcng 25521
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25394  df-ig2 25393
[AitkenIBG] p. 2Definition 4df-li 25409
[AitkenIBG] p. 3Definition 5df-col 25423
[AitkenIBG] p. 3Definition 6df-con2 25428
[AitkenIBG] p. 3Proposition 4isconcl5a 25433  isconcl5ab 25434  isconcl6a 25435  isconcl6ab 25436
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25441
[AitkenIBG] p. 4Exercise 5tpne 25407
[AitkenIBG] p. 4Definition 8df-seg2 25463
[AitkenIBG] p. 4Definition 10df-sside 25495
[AitkenIBG] p. 4Definition 11df-ray2 25484
[AitkenIBG] p. 10Definition 17df-angle 25490
[AitkenIBG] p. 15Definition 23df-triangle 25492
[AitkenIBG] p. 15Definition 24df-cnvx 25511
[AitkenNG] p. 2Definition 1df-slices 25525
[AitkenNG] p. 2Definition 2df-Cut 25527
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25529
[AitkenNG] p. 4Definition 5df-crcl 25531
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18144  df-nmoo 21248
[AkhiezerGlazman] p. 64Theoremhmopidmch 22658  hmopidmchi 22656
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22706  pjcmul2i 22707
[AkhiezerGlazman] p. 72Theoremcnvunop 22423  unoplin 22425
[AkhiezerGlazman] p. 72Equation 2unopadj 22424  unopadj2 22443
[AkhiezerGlazman] p. 73Theoremelunop2 22518  lnopunii 22517
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22591
[Apostol] p. 18Theorem I.1addcan 8929  addcan2d 8949  addcan2i 8939  addcand 8948  addcani 8938
[Apostol] p. 18Theorem I.2negeu 8975
[Apostol] p. 18Theorem I.3negsub 9028  negsubd 9096  negsubi 9057
[Apostol] p. 18Theorem I.4negneg 9030  negnegd 9081  negnegi 9049
[Apostol] p. 18Theorem I.5subdi 9146  subdid 9168  subdii 9161  subdir 9147  subdird 9169  subdiri 9162
[Apostol] p. 18Theorem I.6mul01 8924  mul01d 8944  mul01i 8935  mul02 8923  mul02d 8943  mul02i 8934
[Apostol] p. 18Theorem I.7mulcan 9338  mulcan2d 9335  mulcand 9334  mulcani 9340
[Apostol] p. 18Theorem I.8receu 9346
[Apostol] p. 18Theorem I.9divrec 9373  divrecd 9472  divreci 9438  divreczi 9431
[Apostol] p. 18Theorem I.10recrec 9390  recreci 9425
[Apostol] p. 18Theorem I.11mul0or 9341  mul0ord 9351  mul0ori 9349
[Apostol] p. 18Theorem I.12mul2neg 9152  mul2negd 9167  mul2negi 9160  mulneg1 9149  mulneg1d 9165  mulneg1i 9158
[Apostol] p. 18Theorem I.13divadddiv 9408  divadddivd 9513  divadddivi 9455
[Apostol] p. 18Theorem I.14divmuldiv 9393  divmuldivd 9510  divmuldivi 9453
[Apostol] p. 18Theorem I.15divdivdiv 9394  divdivdivd 9516  divdivdivi 9456
[Apostol] p. 20Axiom 7rpaddcl 10306  rpaddcld 10337  rpmulcl 10307  rpmulcld 10338
[Apostol] p. 20Axiom 8rpneg 10315
[Apostol] p. 20Axiom 90nrp 10316
[Apostol] p. 20Theorem I.17lttri 8878
[Apostol] p. 20Theorem I.18ltadd1d 9298  ltadd1dd 9316  ltadd1i 9260
[Apostol] p. 20Theorem I.19ltmul1 9539  ltmul1a 9538  ltmul1i 9608  ltmul1ii 9618  ltmul2 9540  ltmul2d 10360  ltmul2dd 10374  ltmul2i 9611
[Apostol] p. 20Theorem I.20msqgt0 9227  msqgt0d 9273  msqgt0i 9243
[Apostol] p. 20Theorem I.210lt1 9229
[Apostol] p. 20Theorem I.23lt0neg1 9213  lt0neg1d 9275  ltneg 9207  ltnegd 9283  ltnegi 9250
[Apostol] p. 20Theorem I.25lt2add 9192  lt2addd 9327  lt2addi 9268
[Apostol] p. 20Definition of positive numbersdf-rp 10287
[Apostol] p. 21Exercise 4recgt0 9533  recgt0d 9624  recgt0i 9594  recgt0ii 9595
[Apostol] p. 22Definition of integersdf-z 9957
[Apostol] p. 22Definition of positive integersdfnn3 9693
[Apostol] p. 22Definition of rationalsdf-q 10249
[Apostol] p. 24Theorem I.26supeu 7138
[Apostol] p. 26Theorem I.28nnunb 9893
[Apostol] p. 26Theorem I.29arch 9894
[Apostol] p. 28Exercise 2btwnz 10046
[Apostol] p. 28Exercise 3nnrecl 9895
[Apostol] p. 28Exercise 4rebtwnz 10247
[Apostol] p. 28Exercise 5zbtwnre 10246
[Apostol] p. 28Exercise 6qbtwnre 10457
[Apostol] p. 28Exercise 10(a)zneo 10026
[Apostol] p. 29Theorem I.35msqsqrd 11852  resqrth 11671  sqrth 11778  sqrthi 11784  sqsqrd 11851
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9682
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10216
[Apostol] p. 361Remarkcrreczi 11157
[Apostol] p. 363Remarkabsgt0i 11812
[Apostol] p. 363Exampleabssubd 11865  abssubi 11816
[Baer] p. 40Property (b)mapdord 30958
[Baer] p. 40Property (c)mapd11 30959
[Baer] p. 40Property (e)mapdin 30982  mapdlsm 30984
[Baer] p. 40Property (f)mapd0 30985
[Baer] p. 40Definition of projectivitydf-mapd 30945  mapd1o 30968
[Baer] p. 41Property (g)mapdat 30987
[Baer] p. 44Part (1)mapdpg 31026
[Baer] p. 45Part (2)hdmap1eq 31122  mapdheq 31048  mapdheq2 31049  mapdheq2biN 31050
[Baer] p. 45Part (3)baerlem3 31033
[Baer] p. 46Part (4)mapdheq4 31052  mapdheq4lem 31051
[Baer] p. 46Part (5)baerlem5a 31034  baerlem5abmN 31038  baerlem5amN 31036  baerlem5b 31035  baerlem5bmN 31037
[Baer] p. 47Part (6)hdmap1l6 31142  hdmap1l6a 31130  hdmap1l6e 31135  hdmap1l6f 31136  hdmap1l6g 31137  hdmap1l6lem1 31128  hdmap1l6lem2 31129  hdmap1p6N 31143  mapdh6N 31067  mapdh6aN 31055  mapdh6eN 31060  mapdh6fN 31061  mapdh6gN 31062  mapdh6lem1N 31053  mapdh6lem2N 31054
[Baer] p. 48Part 9hdmapval 31151
[Baer] p. 48Part 10hdmap10 31163
[Baer] p. 48Part 11hdmapadd 31166
[Baer] p. 48Part (6)hdmap1l6h 31138  mapdh6hN 31063
[Baer] p. 48Part (7)mapdh75cN 31073  mapdh75d 31074  mapdh75e 31072  mapdh75fN 31075  mapdh7cN 31069  mapdh7dN 31070  mapdh7eN 31068  mapdh7fN 31071
[Baer] p. 48Part (8)mapdh8 31109  mapdh8a 31095  mapdh8aa 31096  mapdh8ab 31097  mapdh8ac 31098  mapdh8ad 31099  mapdh8b 31100  mapdh8c 31101  mapdh8d 31103  mapdh8d0N 31102  mapdh8e 31104  mapdh8fN 31105  mapdh8g 31106  mapdh8i 31107  mapdh8j 31108
[Baer] p. 48Part (9)mapdh9a 31110
[Baer] p. 48Equation 10mapdhvmap 31089
[Baer] p. 49Part 12hdmap11 31171  hdmapeq0 31167  hdmapf1oN 31188  hdmapneg 31169  hdmaprnN 31187  hdmaprnlem1N 31172  hdmaprnlem3N 31173  hdmaprnlem3uN 31174  hdmaprnlem4N 31176  hdmaprnlem6N 31177  hdmaprnlem7N 31178  hdmaprnlem8N 31179  hdmaprnlem9N 31180  hdmapsub 31170
[Baer] p. 49Part 14hdmap14lem1 31191  hdmap14lem10 31200  hdmap14lem1a 31189  hdmap14lem2N 31192  hdmap14lem2a 31190  hdmap14lem3 31193  hdmap14lem8 31198  hdmap14lem9 31199
[Baer] p. 50Part 14hdmap14lem11 31201  hdmap14lem12 31202  hdmap14lem13 31203  hdmap14lem14 31204  hdmap14lem15 31205  hgmapval 31210
[Baer] p. 50Part 15hgmapadd 31217  hgmapmul 31218  hgmaprnlem2N 31220  hgmapvs 31214
[Baer] p. 50Part 16hgmaprnN 31224
[Baer] p. 110Lemma 1hdmapip0com 31240
[Baer] p. 110Line 27hdmapinvlem1 31241
[Baer] p. 110Line 28hdmapinvlem2 31242
[Baer] p. 110Line 30hdmapinvlem3 31243
[Baer] p. 110Part 1.2hdmapglem5 31245  hgmapvv 31249
[Baer] p. 110Proposition 1hdmapinvlem4 31244
[Baer] p. 111Line 10hgmapvvlem1 31246
[Baer] p. 111Line 15hdmapg 31253  hdmapglem7 31252
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2121
[BellMachover] p. 460Notationdf-mo 2122
[BellMachover] p. 460Definitionmo3 2147
[BellMachover] p. 461Axiom Extax-ext 2237
[BellMachover] p. 462Theorem 1.1bm1.1 2241
[BellMachover] p. 463Axiom Repaxrep5 4076
[BellMachover] p. 463Scheme Sepaxsep 4080
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4084
[BellMachover] p. 466Axiom Powaxpow3 4129
[BellMachover] p. 466Axiom Unionaxun2 4451
[BellMachover] p. 468Definitiondf-ord 4332
[BellMachover] p. 469Theorem 2.2(i)ordirr 4347
[BellMachover] p. 469Theorem 2.2(iii)onelon 4354
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4349
[BellMachover] p. 471Definition of Ndf-om 4594
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4534
[BellMachover] p. 471Definition of Limdf-lim 4334
[BellMachover] p. 472Axiom Infzfinf2 7276
[BellMachover] p. 473Theorem 2.8limom 4608
[BellMachover] p. 477Equation 3.1df-r1 7369
[BellMachover] p. 478Definitionrankval2 7423
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7387  r1ord3g 7384
[BellMachover] p. 480Axiom Regzfreg2 7243
[BellMachover] p. 488Axiom ACac5 8037  dfac4 7682
[BellMachover] p. 490Definition of alephalephval3 7670
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28639
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22858
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22900  chirredi 22899
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22888
[Beran] p. 3Definition of joinsshjval3 21858
[Beran] p. 39Theorem 2.3(i)cmcm2 22138  cmcm2i 22115  cmcm2ii 22120  cmt2N 28570
[Beran] p. 40Theorem 2.3(iii)lecm 22139  lecmi 22124  lecmii 22125
[Beran] p. 45Theorem 3.4cmcmlem 22113
[Beran] p. 49Theorem 4.2cm2j 22142  cm2ji 22147  cm2mi 22148
[Beran] p. 95Definitiondf-sh 21711  issh2 21713
[Beran] p. 95Lemma 3.1(S5)his5 21590
[Beran] p. 95Lemma 3.1(S6)his6 21603
[Beran] p. 95Lemma 3.1(S7)his7 21594
[Beran] p. 95Lemma 3.2(S8)ho01i 22333
[Beran] p. 95Lemma 3.2(S9)hoeq1 22335
[Beran] p. 95Lemma 3.2(S10)ho02i 22334
[Beran] p. 95Lemma 3.2(S11)hoeq2 22336
[Beran] p. 95Postulate (S1)ax-his1 21586  his1i 21604
[Beran] p. 95Postulate (S2)ax-his2 21587
[Beran] p. 95Postulate (S3)ax-his3 21588
[Beran] p. 95Postulate (S4)ax-his4 21589
[Beran] p. 96Definition of normdf-hnorm 21473  dfhnorm2 21626  normval 21628
[Beran] p. 96Definition for Cauchy sequencehcau 21688
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21478
[Beran] p. 96Definition of complete subspaceisch3 21746
[Beran] p. 96Definition of convergedf-hlim 21477  hlimi 21692
[Beran] p. 97Theorem 3.3(i)norm-i-i 21637  norm-i 21633
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21641  norm-ii 21642  normlem0 21613  normlem1 21614  normlem2 21615  normlem3 21616  normlem4 21617  normlem5 21618  normlem6 21619  normlem7 21620  normlem7tALT 21623
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21643  norm-iii 21644
[Beran] p. 98Remark 3.4bcs 21685  bcsiALT 21683  bcsiHIL 21684
[Beran] p. 98Remark 3.4(B)normlem9at 21625  normpar 21659  normpari 21658
[Beran] p. 98Remark 3.4(C)normpyc 21650  normpyth 21649  normpythi 21646
[Beran] p. 99Remarklnfn0 22552  lnfn0i 22547  lnop0 22471  lnop0i 22475
[Beran] p. 99Theorem 3.5(i)nmcexi 22531  nmcfnex 22558  nmcfnexi 22556  nmcopex 22534  nmcopexi 22532
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22559  nmcfnlbi 22557  nmcoplb 22535  nmcoplbi 22533
[Beran] p. 99Theorem 3.5(iii)lnfncon 22561  lnfnconi 22560  lnopcon 22540  lnopconi 22539
[Beran] p. 100Lemma 3.6normpar2i 21660
[Beran] p. 101Lemma 3.6norm3adifi 21657  norm3adifii 21652  norm3dif 21654  norm3difi 21651
[Beran] p. 102Theorem 3.7(i)chocunii 21805  pjhth 21897  pjhtheu 21898  pjpjhth 21929  pjpjhthi 21930  pjth 18730
[Beran] p. 102Theorem 3.7(ii)ococ 21910  ococi 21909
[Beran] p. 103Remark 3.8nlelchi 22566
[Beran] p. 104Theorem 3.9riesz3i 22567  riesz4 22569  riesz4i 22568
[Beran] p. 104Theorem 3.10cnlnadj 22584  cnlnadjeu 22583  cnlnadjeui 22582  cnlnadji 22581  cnlnadjlem1 22572  nmopadjlei 22593
[Beran] p. 106Theorem 3.11(i)adjeq0 22596
[Beran] p. 106Theorem 3.11(v)nmopadji 22595
[Beran] p. 106Theorem 3.11(ii)adjmul 22597
[Beran] p. 106Theorem 3.11(iv)adjadj 22441
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22607  nmopcoadji 22606
[Beran] p. 106Theorem 3.11(iii)adjadd 22598
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22608
[Beran] p. 106Theorem 3.11(viii)adjcoi 22605  pjadj2coi 22709  pjadjcoi 22666
[Beran] p. 107Definitiondf-ch 21726  isch2 21728
[Beran] p. 107Remark 3.12choccl 21810  isch3 21746  occl 21808  ocsh 21787  shoccl 21809  shocsh 21788
[Beran] p. 107Remark 3.12(B)ococin 21912
[Beran] p. 108Theorem 3.13chintcl 21836
[Beran] p. 109Property (i)pjadj2 22692  pjadj3 22693  pjadji 22207  pjadjii 22196
[Beran] p. 109Property (ii)pjidmco 22686  pjidmcoi 22682  pjidmi 22195
[Beran] p. 110Definition of projector orderingpjordi 22678
[Beran] p. 111Remarkho0val 22255  pjch1 22192
[Beran] p. 111Definitiondf-hfmul 22091  df-hfsum 22090  df-hodif 22089  df-homul 22088  df-hosum 22087
[Beran] p. 111Lemma 4.4(i)pjo 22193
[Beran] p. 111Lemma 4.4(ii)pjch 22216  pjchi 21936
[Beran] p. 111Lemma 4.4(iii)pjoc2 21943  pjoc2i 21942
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22202
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22670  pjssmii 22203
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22669
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22668
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22673
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22671  pjssge0ii 22204
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22672  pjdifnormii 22205
[BourbakiEns] p. Proposition 8fcof1 5696  fcofo 5697
[BourbakiFVR] p. Definition 1isder 25039
[BourbakiTop1] p. Remarkxnegmnf 10468  xnegpnf 10467
[BourbakiTop1] p. Remark rexneg 10469
[BourbakiTop1] p. Theoremneiss 16773
[BourbakiTop1] p. Axiom GT'tgpsubcn 17700
[BourbakiTop1] p. Example 1snfil 17486
[BourbakiTop1] p. Example 2neifil 17502
[BourbakiTop1] p. Definitionistgp 17687
[BourbakiTop1] p. Propositioncnpco 16923  ishmeo 17377  neips 16777
[BourbakiTop1] p. Definition 1filintn0 17483
[BourbakiTop1] p. Proposition 9cnpflf2 17622
[BourbakiTop1] p. Theorem 1 (d)iscncl 16925
[BourbakiTop1] p. Proposition Vissnei2 16780
[BourbakiTop1] p. Definition C'''df-cmp 17041
[BourbakiTop1] p. Proposition Viiinnei 16789
[BourbakiTop1] p. Proposition Vivneissex 16791
[BourbakiTop1] p. Proposition Viiielnei 16775  ssnei 16774
[BourbakiTop1] p. Remark below def. 1filn0 17484
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17468
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17485
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27113  stoweid 27112
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27111
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27050  stoweidlem10 27059  stoweidlem14 27063  stoweidlem15 27064  stoweidlem35 27084  stoweidlem36 27085  stoweidlem37 27086  stoweidlem38 27087  stoweidlem40 27089  stoweidlem41 27090  stoweidlem43 27092  stoweidlem44 27093  stoweidlem46 27095  stoweidlem5 27054  stoweidlem50 27099  stoweidlem52 27101  stoweidlem53 27102  stoweidlem55 27104  stoweidlem56 27105
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27072  stoweidlem24 27073  stoweidlem27 27076  stoweidlem28 27077  stoweidlem30 27079
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27094  stoweidlem49 27098  stoweidlem7 27056
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27080  stoweidlem39 27088  stoweidlem42 27091  stoweidlem48 27097  stoweidlem51 27100  stoweidlem54 27103  stoweidlem57 27106  stoweidlem58 27107
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27074
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27083
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27066
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27108
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27109
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27067
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27060  stoweidlem26 27075
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27062
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27110
[ChoquetDD] p. 2Definition of mappingdf-mpt 4019
[Cohen] p. 301Remarkrelogoprlem 19871
[Cohen] p. 301Property 2relogmul 19872  relogmuld 19903
[Cohen] p. 301Property 3relogdiv 19873  relogdivd 19904
[Cohen] p. 301Property 4relogexp 19876
[Cohen] p. 301Property 1alog1 19866
[Cohen] p. 301Property 1bloge 19867
[Cohn] p. 81Section II.5acsdomd 14211  acsinfd 14210  acsinfdimd 14212  acsmap2d 14209  acsmapd 14208
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10896
[Crawley] p. 1Definition of posetdf-poset 14007
[Crawley] p. 107Theorem 13.2hlsupr 28705
[Crawley] p. 110Theorem 13.3arglem1N 29509  dalaw 29205
[Crawley] p. 111Theorem 13.4hlathil 31284
[Crawley] p. 111Definition of set Wdf-watsN 29309
[Crawley] p. 111Definition of dilationdf-dilN 29425  df-ldil 29423  isldil 29429
[Crawley] p. 111Definition of translationdf-ltrn 29424  df-trnN 29426  isltrn 29438  ltrnu 29440
[Crawley] p. 112Lemma Acdlema1N 29110  cdlema2N 29111  exatleN 28723
[Crawley] p. 112Lemma B1cvrat 28795  cdlemb 29113  cdlemb2 29360  cdlemb3 29925  idltrn 29469  l1cvat 28375  lhpat 29362  lhpat2 29364  lshpat 28376  ltrnel 29458  ltrnmw 29470
[Crawley] p. 112Lemma Ccdlemc1 29510  cdlemc2 29511  ltrnnidn 29493  trlat 29488  trljat1 29485  trljat2 29486  trljat3 29487  trlne 29504  trlnidat 29492  trlnle 29505
[Crawley] p. 112Definition of automorphismdf-pautN 29310
[Crawley] p. 113Lemma Ccdlemc 29516  cdlemc3 29512  cdlemc4 29513
[Crawley] p. 113Lemma Dcdlemd 29526  cdlemd1 29517  cdlemd2 29518  cdlemd3 29519  cdlemd4 29520  cdlemd5 29521  cdlemd6 29522  cdlemd7 29523  cdlemd8 29524  cdlemd9 29525  cdleme31sde 29704  cdleme31se 29701  cdleme31se2 29702  cdleme31snd 29705  cdleme32a 29760  cdleme32b 29761  cdleme32c 29762  cdleme32d 29763  cdleme32e 29764  cdleme32f 29765  cdleme32fva 29756  cdleme32fva1 29757  cdleme32fvcl 29759  cdleme32le 29766  cdleme48fv 29818  cdleme4gfv 29826  cdleme50eq 29860  cdleme50f 29861  cdleme50f1 29862  cdleme50f1o 29865  cdleme50laut 29866  cdleme50ldil 29867  cdleme50lebi 29859  cdleme50rn 29864  cdleme50rnlem 29863  cdlemeg49le 29830  cdlemeg49lebilem 29858
[Crawley] p. 113Lemma Ecdleme 29879  cdleme00a 29528  cdleme01N 29540  cdleme02N 29541  cdleme0a 29530  cdleme0aa 29529  cdleme0b 29531  cdleme0c 29532  cdleme0cp 29533  cdleme0cq 29534  cdleme0dN 29535  cdleme0e 29536  cdleme0ex1N 29542  cdleme0ex2N 29543  cdleme0fN 29537  cdleme0gN 29538  cdleme0moN 29544  cdleme1 29546  cdleme10 29573  cdleme10tN 29577  cdleme11 29589  cdleme11a 29579  cdleme11c 29580  cdleme11dN 29581  cdleme11e 29582  cdleme11fN 29583  cdleme11g 29584  cdleme11h 29585  cdleme11j 29586  cdleme11k 29587  cdleme11l 29588  cdleme12 29590  cdleme13 29591  cdleme14 29592  cdleme15 29597  cdleme15a 29593  cdleme15b 29594  cdleme15c 29595  cdleme15d 29596  cdleme16 29604  cdleme16aN 29578  cdleme16b 29598  cdleme16c 29599  cdleme16d 29600  cdleme16e 29601  cdleme16f 29602  cdleme16g 29603  cdleme19a 29622  cdleme19b 29623  cdleme19c 29624  cdleme19d 29625  cdleme19e 29626  cdleme19f 29627  cdleme1b 29545  cdleme2 29547  cdleme20aN 29628  cdleme20bN 29629  cdleme20c 29630  cdleme20d 29631  cdleme20e 29632  cdleme20f 29633  cdleme20g 29634  cdleme20h 29635  cdleme20i 29636  cdleme20j 29637  cdleme20k 29638  cdleme20l 29641  cdleme20l1 29639  cdleme20l2 29640  cdleme20m 29642  cdleme20y 29621  cdleme20zN 29620  cdleme21 29656  cdleme21d 29649  cdleme21e 29650  cdleme22a 29659  cdleme22aa 29658  cdleme22b 29660  cdleme22cN 29661  cdleme22d 29662  cdleme22e 29663  cdleme22eALTN 29664  cdleme22f 29665  cdleme22f2 29666  cdleme22g 29667  cdleme23a 29668  cdleme23b 29669  cdleme23c 29670  cdleme26e 29678  cdleme26eALTN 29680  cdleme26ee 29679  cdleme26f 29682  cdleme26f2 29684  cdleme26f2ALTN 29683  cdleme26fALTN 29681  cdleme27N 29688  cdleme27a 29686  cdleme27cl 29685  cdleme28c 29691  cdleme3 29556  cdleme30a 29697  cdleme31fv 29709  cdleme31fv1 29710  cdleme31fv1s 29711  cdleme31fv2 29712  cdleme31id 29713  cdleme31sc 29703  cdleme31sdnN 29706  cdleme31sn 29699  cdleme31sn1 29700  cdleme31sn1c 29707  cdleme31sn2 29708  cdleme31so 29698  cdleme35a 29767  cdleme35b 29769  cdleme35c 29770  cdleme35d 29771  cdleme35e 29772  cdleme35f 29773  cdleme35fnpq 29768  cdleme35g 29774  cdleme35h 29775  cdleme35h2 29776  cdleme35sn2aw 29777  cdleme35sn3a 29778  cdleme36a 29779  cdleme36m 29780  cdleme37m 29781  cdleme38m 29782  cdleme38n 29783  cdleme39a 29784  cdleme39n 29785  cdleme3b 29548  cdleme3c 29549  cdleme3d 29550  cdleme3e 29551  cdleme3fN 29552  cdleme3fa 29555  cdleme3g 29553  cdleme3h 29554  cdleme4 29557  cdleme40m 29786  cdleme40n 29787  cdleme40v 29788  cdleme40w 29789  cdleme41fva11 29796  cdleme41sn3aw 29793  cdleme41sn4aw 29794  cdleme41snaw 29795  cdleme42a 29790  cdleme42b 29797  cdleme42c 29791  cdleme42d 29792  cdleme42e 29798  cdleme42f 29799  cdleme42g 29800  cdleme42h 29801  cdleme42i 29802  cdleme42k 29803  cdleme42ke 29804  cdleme42keg 29805  cdleme42mN 29806  cdleme42mgN 29807  cdleme43aN 29808  cdleme43bN 29809  cdleme43cN 29810  cdleme43dN 29811  cdleme5 29559  cdleme50ex 29878  cdleme50ltrn 29876  cdleme51finvN 29875  cdleme51finvfvN 29874  cdleme51finvtrN 29877  cdleme6 29560  cdleme7 29568  cdleme7a 29562  cdleme7aa 29561  cdleme7b 29563  cdleme7c 29564  cdleme7d 29565  cdleme7e 29566  cdleme7ga 29567  cdleme8 29569  cdleme8tN 29574  cdleme9 29572  cdleme9a 29570  cdleme9b 29571  cdleme9tN 29576  cdleme9taN 29575  cdlemeda 29617  cdlemedb 29616  cdlemednpq 29618  cdlemednuN 29619  cdlemefr27cl 29722  cdlemefr32fva1 29729  cdlemefr32fvaN 29728  cdlemefrs32fva 29719  cdlemefrs32fva1 29720  cdlemefs27cl 29732  cdlemefs32fva1 29742  cdlemefs32fvaN 29741  cdlemesner 29615  cdlemeulpq 29539
[Crawley] p. 114Lemma E4atex 29395  4atexlem7 29394  cdleme0nex 29609  cdleme17a 29605  cdleme17c 29607  cdleme17d 29817  cdleme17d1 29608  cdleme17d2 29814  cdleme18a 29610  cdleme18b 29611  cdleme18c 29612  cdleme18d 29614  cdleme4a 29558
[Crawley] p. 115Lemma Ecdleme21a 29644  cdleme21at 29647  cdleme21b 29645  cdleme21c 29646  cdleme21ct 29648  cdleme21f 29651  cdleme21g 29652  cdleme21h 29653  cdleme21i 29654  cdleme22gb 29613
[Crawley] p. 116Lemma Fcdlemf 29882  cdlemf1 29880  cdlemf2 29881
[Crawley] p. 116Lemma Gcdlemftr1 29886  cdlemg16 29976  cdlemg28 30023  cdlemg28a 30012  cdlemg28b 30022  cdlemg3a 29916  cdlemg42 30048  cdlemg43 30049  cdlemg44 30052  cdlemg44a 30050  cdlemg46 30054  cdlemg47 30055  cdlemg9 29953  ltrnco 30038  ltrncom 30057  tgrpabl 30070  trlco 30046
[Crawley] p. 116Definition of Gdf-tgrp 30062
[Crawley] p. 117Lemma Gcdlemg17 29996  cdlemg17b 29981
[Crawley] p. 117Definition of Edf-edring-rN 30075  df-edring 30076
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30079
[Crawley] p. 118Remarktendopltp 30099
[Crawley] p. 118Lemma Hcdlemh 30136  cdlemh1 30134  cdlemh2 30135
[Crawley] p. 118Lemma Icdlemi 30139  cdlemi1 30137  cdlemi2 30138
[Crawley] p. 118Lemma Jcdlemj1 30140  cdlemj2 30141  cdlemj3 30142  tendocan 30143
[Crawley] p. 118Lemma Kcdlemk 30293  cdlemk1 30150  cdlemk10 30162  cdlemk11 30168  cdlemk11t 30265  cdlemk11ta 30248  cdlemk11tb 30250  cdlemk11tc 30264  cdlemk11u-2N 30208  cdlemk11u 30190  cdlemk12 30169  cdlemk12u-2N 30209  cdlemk12u 30191  cdlemk13-2N 30195  cdlemk13 30171  cdlemk14-2N 30197  cdlemk14 30173  cdlemk15-2N 30198  cdlemk15 30174  cdlemk16-2N 30199  cdlemk16 30176  cdlemk16a 30175  cdlemk17-2N 30200  cdlemk17 30177  cdlemk18-2N 30205  cdlemk18-3N 30219  cdlemk18 30187  cdlemk19-2N 30206  cdlemk19 30188  cdlemk19u 30289  cdlemk1u 30178  cdlemk2 30151  cdlemk20-2N 30211  cdlemk20 30193  cdlemk21-2N 30210  cdlemk21N 30192  cdlemk22-3 30220  cdlemk22 30212  cdlemk23-3 30221  cdlemk24-3 30222  cdlemk25-3 30223  cdlemk26-3 30225  cdlemk26b-3 30224  cdlemk27-3 30226  cdlemk28-3 30227  cdlemk29-3 30230  cdlemk3 30152  cdlemk30 30213  cdlemk31 30215  cdlemk32 30216  cdlemk33N 30228  cdlemk34 30229  cdlemk35 30231  cdlemk36 30232  cdlemk37 30233  cdlemk38 30234  cdlemk39 30235  cdlemk39u 30287  cdlemk4 30153  cdlemk41 30239  cdlemk42 30260  cdlemk42yN 30263  cdlemk43N 30282  cdlemk45 30266  cdlemk46 30267  cdlemk47 30268  cdlemk48 30269  cdlemk49 30270  cdlemk5 30155  cdlemk50 30271  cdlemk51 30272  cdlemk52 30273  cdlemk53 30276  cdlemk54 30277  cdlemk55 30280  cdlemk55u 30285  cdlemk56 30290  cdlemk5a 30154  cdlemk5auN 30179  cdlemk5u 30180  cdlemk6 30156  cdlemk6u 30181  cdlemk7 30167  cdlemk7u-2N 30207  cdlemk7u 30189  cdlemk8 30157  cdlemk9 30158  cdlemk9bN 30159  cdlemki 30160  cdlemkid 30255  cdlemkj-2N 30201  cdlemkj 30182  cdlemksat 30165  cdlemksel 30164  cdlemksv 30163  cdlemksv2 30166  cdlemkuat 30185  cdlemkuel-2N 30203  cdlemkuel-3 30217  cdlemkuel 30184  cdlemkuv-2N 30202  cdlemkuv2-2 30204  cdlemkuv2-3N 30218  cdlemkuv2 30186  cdlemkuvN 30183  cdlemkvcl 30161  cdlemky 30245  cdlemkyyN 30281  tendoex 30294
[Crawley] p. 120Remarkdva1dim 30304
[Crawley] p. 120Lemma Lcdleml1N 30295  cdleml2N 30296  cdleml3N 30297  cdleml4N 30298  cdleml5N 30299  cdleml6 30300  cdleml7 30301  cdleml8 30302  cdleml9 30303  dia1dim 30381
[Crawley] p. 120Lemma Mdia11N 30368  diaf11N 30369  dialss 30366  diaord 30367  dibf11N 30481  djajN 30457
[Crawley] p. 120Definition of isomorphism mapdiaval 30352
[Crawley] p. 121Lemma Mcdlemm10N 30438  dia2dimlem1 30384  dia2dimlem2 30385  dia2dimlem3 30386  dia2dimlem4 30387  dia2dimlem5 30388  diaf1oN 30450  diarnN 30449  dvheveccl 30432  dvhopN 30436
[Crawley] p. 121Lemma Ncdlemn 30532  cdlemn10 30526  cdlemn11 30531  cdlemn11a 30527  cdlemn11b 30528  cdlemn11c 30529  cdlemn11pre 30530  cdlemn2 30515  cdlemn2a 30516  cdlemn3 30517  cdlemn4 30518  cdlemn4a 30519  cdlemn5 30521  cdlemn5pre 30520  cdlemn6 30522  cdlemn7 30523  cdlemn8 30524  cdlemn9 30525  diclspsn 30514
[Crawley] p. 121Definition of phi(q)df-dic 30493
[Crawley] p. 122Lemma Ndih11 30585  dihf11 30587  dihjust 30537  dihjustlem 30536  dihord 30584  dihord1 30538  dihord10 30543  dihord11b 30542  dihord11c 30544  dihord2 30547  dihord2a 30539  dihord2b 30540  dihord2cN 30541  dihord2pre 30545  dihord2pre2 30546  dihordlem6 30533  dihordlem7 30534  dihordlem7b 30535
[Crawley] p. 122Definition of isomorphism mapdihffval 30550  dihfval 30551  dihval 30552
[Eisenberg] p. 67Definition 5.3df-dif 3097
[Eisenberg] p. 82Definition 6.3dfom3 7281
[Eisenberg] p. 125Definition 8.21df-map 6707
[Eisenberg] p. 216Example 13.2(4)omenps 7288
[Eisenberg] p. 310Theorem 19.8cardprc 7546
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8110
[Enderton] p. 18Axiom of Empty Setaxnul 4088
[Enderton] p. 19Definitiondf-tp 3589
[Enderton] p. 26Exercise 5unissb 3798
[Enderton] p. 26Exercise 10pwel 4163
[Enderton] p. 28Exercise 7(b)pwun 4239
[Enderton] p. 30Theorem "Distributive laws"iinin1 3914  iinin2 3913  iinun2 3909  iunin1 3908  iunin2 3907
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3912  iundif2 3910
[Enderton] p. 32Exercise 20unineq 3361
[Enderton] p. 33Exercise 23iinuni 3926
[Enderton] p. 33Exercise 25iununi 3927
[Enderton] p. 33Exercise 24(a)iinpw 3931
[Enderton] p. 33Exercise 24(b)iunpw 4507  iunpwss 3932
[Enderton] p. 36Definitionopthwiener 4205
[Enderton] p. 38Exercise 6(a)unipw 4162
[Enderton] p. 38Exercise 6(b)pwuni 4144
[Enderton] p. 41Lemma 3Dopeluu 4463  rnex 4895  rnexg 4893
[Enderton] p. 41Exercise 8dmuni 4841  rnuni 5045
[Enderton] p. 42Definition of a functiondffun7 5184  dffun8 5185
[Enderton] p. 43Definition of function valuefunfv2 5486
[Enderton] p. 43Definition of single-rootedfuncnv 5213
[Enderton] p. 44Definition (d)dfima2 4967  dfima3 4968
[Enderton] p. 47Theorem 3Hfvco2 5493
[Enderton] p. 49Axiom of Choice (first form)ac7 8033  ac7g 8034  df-ac 7676  dfac2 7690  dfac2a 7689  dfac3 7681  dfac7 7691
[Enderton] p. 50Theorem 3K(a)imauni 5671
[Enderton] p. 52Definitiondf-map 6707
[Enderton] p. 53Exercise 21coass 5143
[Enderton] p. 53Exercise 27dmco 5133
[Enderton] p. 53Exercise 14(a)funin 5222
[Enderton] p. 53Exercise 22(a)imass2 5002
[Enderton] p. 54Remarkixpf 6771  ixpssmap 6783
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6751
[Enderton] p. 55Axiom of Choice (second form)ac9 8043  ac9s 8053
[Enderton] p. 56Theorem 3Merref 6613
[Enderton] p. 57Lemma 3Nerthi 6639
[Enderton] p. 57Definitiondf-ec 6595
[Enderton] p. 58Definitiondf-qs 6599
[Enderton] p. 60Theorem 3Qth3q 6700  th3qcor 6699  th3qlem1 6697  th3qlem2 6698
[Enderton] p. 61Exercise 35df-ec 6595
[Enderton] p. 65Exercise 56(a)dmun 4838
[Enderton] p. 68Definition of successordf-suc 4335
[Enderton] p. 71Definitiondf-tr 4054  dftr4 4058
[Enderton] p. 72Theorem 4Eunisuc 4405
[Enderton] p. 73Exercise 6unisuc 4405
[Enderton] p. 73Exercise 5(a)truni 4067
[Enderton] p. 73Exercise 5(b)trint 4068  trintALT 27670
[Enderton] p. 79Theorem 4I(A1)nna0 6535
[Enderton] p. 79Theorem 4I(A2)nnasuc 6537  onasuc 6460
[Enderton] p. 79Definition of operation valuedf-ov 5760
[Enderton] p. 80Theorem 4J(A1)nnm0 6536
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6538  onmsuc 6461
[Enderton] p. 81Theorem 4K(1)nnaass 6553
[Enderton] p. 81Theorem 4K(2)nna0r 6540  nnacom 6548
[Enderton] p. 81Theorem 4K(3)nndi 6554
[Enderton] p. 81Theorem 4K(4)nnmass 6555
[Enderton] p. 81Theorem 4K(5)nnmcom 6557
[Enderton] p. 82Exercise 16nnm0r 6541  nnmsucr 6556
[Enderton] p. 88Exercise 23nnaordex 6569
[Enderton] p. 129Definitiondf-en 6797
[Enderton] p. 132Theorem 6B(b)canth 6225
[Enderton] p. 133Exercise 1xpomen 7576
[Enderton] p. 133Exercise 2qnnen 12419
[Enderton] p. 134Theorem (Pigeonhole Principle)php 6978
[Enderton] p. 135Corollary 6Cphp3 6980
[Enderton] p. 136Corollary 6Enneneq 6977
[Enderton] p. 136Corollary 6D(a)pssinf 7006
[Enderton] p. 136Corollary 6D(b)ominf 7008
[Enderton] p. 137Lemma 6Fpssnn 7014
[Enderton] p. 138Corollary 6Gssfi 7016
[Enderton] p. 139Theorem 6H(c)mapen 6958
[Enderton] p. 142Theorem 6I(3)xpcdaen 7742
[Enderton] p. 142Theorem 6I(4)mapcdaen 7743
[Enderton] p. 143Theorem 6Jcda0en 7738  cda1en 7734
[Enderton] p. 144Exercise 13iunfi 7077  unifi 7078  unifi2 7079
[Enderton] p. 144Corollary 6Kundif2 3472  unfi 7057  unfi2 7059
[Enderton] p. 145Figure 38ffoss 5408
[Enderton] p. 145Definitiondf-dom 6798
[Enderton] p. 146Example 1domen 6808  domeng 6809
[Enderton] p. 146Example 3nndomo 6987  nnsdom 7287  nnsdomg 7049
[Enderton] p. 149Theorem 6L(a)cdadom2 7746
[Enderton] p. 149Theorem 6L(c)mapdom1 6959  xpdom1 6894  xpdom1g 6892  xpdom2g 6891
[Enderton] p. 149Theorem 6L(d)mapdom2 6965
[Enderton] p. 151Theorem 6Mzorn 8067  zorng 8064
[Enderton] p. 151Theorem 6M(4)ac8 8052  dfac5 7688
[Enderton] p. 159Theorem 6Qunictb 8130
[Enderton] p. 164Exampleinfdif 7768
[Enderton] p. 168Definitiondf-po 4251
[Enderton] p. 192Theorem 7M(a)oneli 4437
[Enderton] p. 192Theorem 7M(b)ontr1 4375
[Enderton] p. 192Theorem 7M(c)onirri 4436
[Enderton] p. 193Corollary 7N(b)0elon 4382
[Enderton] p. 193Corollary 7N(c)onsuci 4566
[Enderton] p. 193Corollary 7N(d)ssonunii 4516
[Enderton] p. 194Remarkonprc 4513
[Enderton] p. 194Exercise 16suc11 4433
[Enderton] p. 197Definitiondf-card 7505
[Enderton] p. 197Theorem 7Pcarden 8106
[Enderton] p. 200Exercise 25tfis 4582
[Enderton] p. 202Lemma 7Tr1tr 7381
[Enderton] p. 202Definitiondf-r1 7369
[Enderton] p. 202Theorem 7Qr1val1 7391
[Enderton] p. 204Theorem 7V(b)rankval4 7472
[Enderton] p. 206Theorem 7X(b)en2lp 7250
[Enderton] p. 207Exercise 30rankpr 7462  rankprb 7456  rankpw 7448  rankpwi 7428  rankuniss 7471
[Enderton] p. 207Exercise 34opthreg 7252
[Enderton] p. 208Exercise 35suc11reg 7253
[Enderton] p. 212Definition of alephalephval3 7670
[Enderton] p. 213Theorem 8A(a)alephord2 7636
[Enderton] p. 213Theorem 8A(b)cardalephex 7650
[Enderton] p. 218Theorem Schema 8Eonfununi 6291
[Enderton] p. 222Definition of kardkarden 7498  kardex 7497
[Enderton] p. 238Theorem 8Roeoa 6528
[Enderton] p. 238Theorem 8Soeoe 6530
[Enderton] p. 240Exercise 25oarec 6493
[Enderton] p. 257Definition of cofinalitycflm 7809
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13471
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13417
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14207  mrieqv2d 13468  mrieqvd 13467
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13472
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13477  mreexexlem2d 13474
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14213  mreexfidimd 13479
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18821
[Fremlin5] p. 213Lemma 565Cauniioovol 18861
[Fremlin5] p. 214Lemma 565Cauniioombl 18871
[FreydScedrov] p. 283Axiom of Infinityax-inf 7272  inf1 7256  inf2 7257
[Gleason] p. 117Proposition 9-2.1df-enq 8468  enqer 8478
[Gleason] p. 117Proposition 9-2.2df-1nq 8473  df-nq 8469
[Gleason] p. 117Proposition 9-2.3df-plpq 8465  df-plq 8471
[Gleason] p. 119Proposition 9-2.4caovmo 5956  df-mpq 8466  df-mq 8472
[Gleason] p. 119Proposition 9-2.5df-rq 8474
[Gleason] p. 119Proposition 9-2.6ltexnq 8532
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8533  ltbtwnnq 8535
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8528
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8529
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8536
[Gleason] p. 121Definition 9-3.1df-np 8538
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8550
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8552
[Gleason] p. 122Definitiondf-1p 8539
[Gleason] p. 122Remark (1)prub 8551
[Gleason] p. 122Lemma 9-3.4prlem934 8590
[Gleason] p. 122Proposition 9-3.2df-ltp 8542
[Gleason] p. 122Proposition 9-3.3ltsopr 8589  psslinpr 8588  supexpr 8611  suplem1pr 8609  suplem2pr 8610
[Gleason] p. 123Proposition 9-3.5addclpr 8575  addclprlem1 8573  addclprlem2 8574  df-plp 8540
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8579
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8578
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8591
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8600  ltexprlem1 8593  ltexprlem2 8594  ltexprlem3 8595  ltexprlem4 8596  ltexprlem5 8597  ltexprlem6 8598  ltexprlem7 8599
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8602  ltaprlem 8601
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8603
[Gleason] p. 124Lemma 9-3.6prlem936 8604
[Gleason] p. 124Proposition 9-3.7df-mp 8541  mulclpr 8577  mulclprlem 8576  reclem2pr 8605
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8586
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8581
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8580
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8585
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8608  reclem3pr 8606  reclem4pr 8607
[Gleason] p. 126Proposition 9-4.1df-enr 8614  df-mpr 8613  df-plpr 8612  enrer 8623
[Gleason] p. 126Proposition 9-4.2df-0r 8619  df-1r 8620  df-nr 8615
[Gleason] p. 126Proposition 9-4.3df-mr 8617  df-plr 8616  negexsr 8657  recexsr 8662  recexsrlem 8658
[Gleason] p. 127Proposition 9-4.4df-ltr 8618
[Gleason] p. 130Proposition 10-1.3creui 9674  creur 9673  cru 9671
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8743  axcnre 8719
[Gleason] p. 132Definition 10-3.1crim 11530  crimd 11647  crimi 11608  crre 11529  crred 11646  crrei 11607
[Gleason] p. 132Definition 10-3.2remim 11532  remimd 11613
[Gleason] p. 133Definition 10.36absval2 11699  absval2d 11857  absval2i 11810
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11556  cjaddd 11635  cjaddi 11603
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11557  cjmuld 11636  cjmuli 11604
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11555  cjcjd 11614  cjcji 11586
[Gleason] p. 133Proposition 10-3.4(f)cjre 11554  cjreb 11538  cjrebd 11617  cjrebi 11589  cjred 11641  rere 11537  rereb 11535  rerebd 11616  rerebi 11588  rered 11639
[Gleason] p. 133Proposition 10-3.4(h)addcj 11563  addcjd 11627  addcji 11598
[Gleason] p. 133Proposition 10-3.7(a)absval 11653
[Gleason] p. 133Proposition 10-3.7(b)abscj 11694  abscjd 11862  abscji 11814
[Gleason] p. 133Proposition 10-3.7(c)abs00 11704  abs00d 11858  abs00i 11811  absne0d 11859
[Gleason] p. 133Proposition 10-3.7(d)releabs 11735  releabsd 11863  releabsi 11815
[Gleason] p. 133Proposition 10-3.7(f)absmul 11709  absmuld 11866  absmuli 11817
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11697  sqabsaddi 11818
[Gleason] p. 133Proposition 10-3.7(h)abstri 11744  abstrid 11868  abstrii 11821
[Gleason] p. 134Definition 10-4.1df-exp 11036  exp0 11039  expp1 11041  expp1d 11177
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19953  cxpaddd 19991  expadd 11075  expaddd 11178  expaddz 11077
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19962  cxpmuld 20008  expmul 11078  expmuld 11179  expmulz 11079
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19959  mulcxpd 20002  mulexp 11072  mulexpd 11191  mulexpz 11073
[Gleason] p. 140Exercise 1znnen 12418
[Gleason] p. 141Definition 11-2.1fzval 10715
[Gleason] p. 168Proposition 12-2.1(a)climadd 12035  rlimadd 12046  rlimdiv 12049
[Gleason] p. 168Proposition 12-2.1(b)climsub 12037  rlimsub 12047
[Gleason] p. 168Proposition 12-2.1(c)climmul 12036  rlimmul 12048
[Gleason] p. 171Corollary 12-2.2climmulc2 12040
[Gleason] p. 172Corollary 12-2.5climrecl 11987
[Gleason] p. 172Proposition 12-2.4(c)climabs 12007  climcj 12008  climim 12010  climre 12009  rlimabs 12012  rlimcj 12013  rlimim 12015  rlimre 12014
[Gleason] p. 173Definition 12-3.1df-ltxr 8805  df-xr 8804  ltxr 10389
[Gleason] p. 175Definition 12-4.1df-limsup 11875  limsupval 11878
[Gleason] p. 180Theorem 12-5.1climsup 12073
[Gleason] p. 180Theorem 12-5.3caucvg 12081  caucvgb 12082  caucvgr 12078  climcau 12074
[Gleason] p. 182Exercise 3cvgcmp 12204
[Gleason] p. 182Exercise 4cvgrat 12266
[Gleason] p. 195Theorem 13-2.12abs1m 11749
[Gleason] p. 217Lemma 13-4.1btwnzge0 10884
[Gleason] p. 223Definition 14-1.1df-met 16301
[Gleason] p. 223Definition 14-1.1(a)met0 17835  xmet0 17834
[Gleason] p. 223Definition 14-1.1(b)metgt0 17850
[Gleason] p. 223Definition 14-1.1(c)metsym 17841
[Gleason] p. 223Definition 14-1.1(d)mettri 17843  mstri 17942  xmettri 17842  xmstri 17941
[Gleason] p. 225Definition 14-1.5xpsmet 17873
[Gleason] p. 230Proposition 14-2.6txlm 17269
[Gleason] p. 240Theorem 14-4.3metcnp4 18662
[Gleason] p. 240Proposition 14-4.2metcnp3 18013
[Gleason] p. 243Proposition 14-4.16addcn 18296  addcn2 11997  mulcn 18298  mulcn2 11999  subcn 18297  subcn2 11998
[Gleason] p. 295Remarkbcval3 11250  bcval4 11251
[Gleason] p. 295Equation 2bcpasc 11264
[Gleason] p. 295Definition of binomial coefficientbcval 11248  df-bc 11247
[Gleason] p. 296Remarkbcn0 11254  bcnn 11255
[Gleason] p. 296Theorem 15-2.8binom 12218
[Gleason] p. 308Equation 2ef0 12299
[Gleason] p. 308Equation 3efcj 12300
[Gleason] p. 309Corollary 15-4.3efne0 12304
[Gleason] p. 309Corollary 15-4.4efexp 12308
[Gleason] p. 310Equation 14sinadd 12371
[Gleason] p. 310Equation 15cosadd 12372
[Gleason] p. 311Equation 17sincossq 12383
[Gleason] p. 311Equation 18cosbnd 12388  sinbnd 12387
[Gleason] p. 311Lemma 15-4.7sqeqor 11148  sqeqori 11146
[Gleason] p. 311Definition of pidf-pi 12281
[Godowski] p. 730Equation SFgoeqi 22778
[GodowskiGreechie] p. 249Equation IV3oai 22190
[Gratzer] p. 23Section 0.6df-mre 13415
[Gratzer] p. 27Section 0.6df-mri 13417
[Halmos] p. 31Theorem 17.3riesz1 22570  riesz2 22571
[Halmos] p. 41Definition of Hermitianhmopadj2 22446
[Halmos] p. 42Definition of projector orderingpjordi 22678
[Halmos] p. 43Theorem 26.1elpjhmop 22690  elpjidm 22689  pjnmopi 22653
[Halmos] p. 44Remarkpjinormi 22209  pjinormii 22198
[Halmos] p. 44Theorem 26.2elpjch 22694  pjrn 22229  pjrni 22224  pjvec 22218
[Halmos] p. 44Theorem 26.3pjnorm2 22249
[Halmos] p. 44Theorem 26.4hmopidmpj 22659  hmopidmpji 22657
[Halmos] p. 45Theorem 27.1pjinvari 22696
[Halmos] p. 45Theorem 27.3pjoci 22685  pjocvec 22219
[Halmos] p. 45Theorem 27.4pjorthcoi 22674
[Halmos] p. 48Theorem 29.2pjssposi 22677
[Halmos] p. 48Theorem 29.3pjssdif1i 22680  pjssdif2i 22679
[Halmos] p. 50Definition of spectrumdf-spec 22360
[Hamilton] p. 28Definition 2.1ax-1 7
[Hamilton] p. 31Example 2.7(a)id1 22
[Hamilton] p. 73Rule 1ax-mp 10
[Hamilton] p. 74Rule 2ax-gen 1536
[Hatcher] p. 25Definitiondf-phtpc 18417  df-phtpy 18396
[Hatcher] p. 26Definitiondf-pco 18430  df-pi1 18433
[Hatcher] p. 26Proposition 1.2phtpcer 18420
[Hatcher] p. 26Proposition 1.3pi1grp 18475
[Herstein] p. 54Exercise 28df-grpo 20783
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14425  grpoideu 20801  mndideu 14302
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14443  grpoinveu 20814
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14462  grpo2inv 20831
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14471  grpoinvop 20833
[Herstein] p. 57Exercise 1isgrp2d 20827  isgrp2i 20828
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22925
[Holland] p. 1520Lemma 5cdj1i 22938  cdj3i 22946  cdj3lem1 22939  cdjreui 22937
[Holland] p. 1524Lemma 7mddmdin0i 22936
[Holland95] p. 13Theorem 3.6hlathil 31284
[Holland95] p. 14Line 15hgmapvs 31214
[Holland95] p. 14Line 16hdmaplkr 31236
[Holland95] p. 14Line 17hdmapellkr 31237
[Holland95] p. 14Line 19hdmapglnm2 31234
[Holland95] p. 14Line 20hdmapip0com 31240
[Holland95] p. 14Theorem 3.6hdmapevec2 31159
[Holland95] p. 14Lines 24 and 25hdmapoc 31254
[Holland95] p. 204Definition of involutiondf-srng 15538
[Holland95] p. 212Definition of subspacedf-psubsp 28822
[Holland95] p. 214Lemma 3.3lclkrlem2v 30848
[Holland95] p. 214Definition 3.2df-lpolN 30801
[Holland95] p. 214Definition of nonsingularpnonsingN 29252
[Holland95] p. 215Lemma 3.3(1)dihoml4 30697  poml4N 29272
[Holland95] p. 215Lemma 3.3(2)dochexmid 30788  pexmidALTN 29297  pexmidN 29288
[Holland95] p. 218Theorem 3.6lclkr 30853
[Holland95] p. 218Definition of dual vector spacedf-ldual 28444  ldualset 28445
[Holland95] p. 222Item 1df-lines 28820  df-pointsN 28821
[Holland95] p. 222Item 2df-polarityN 29222
[Holland95] p. 223Remarkispsubcl2N 29266  omllaw4 28566  pol1N 29229  polcon3N 29236
[Holland95] p. 223Definitiondf-psubclN 29254
[Holland95] p. 223Equation for polaritypolval2N 29225
[Hughes] p. 44Equation 1.21bax-his3 21588
[Hughes] p. 47Definition of projection operatordfpjop 22687
[Hughes] p. 49Equation 1.30eighmre 22468  eigre 22340  eigrei 22339
[Hughes] p. 49Equation 1.31eighmorth 22469  eigorth 22343  eigorthi 22342
[Hughes] p. 137Remark (ii)eigposi 22341
[Indrzejczak] p. 33Definition ` `Enatded 4  natded 4
[Indrzejczak] p. 33Definition ` `Inatded 4
[Indrzejczak] p. 34Definition ` `Enatded 4  natded 4
[Indrzejczak] p. 34Definition ` `Inatded 4
[Jech] p. 4Definition of classcv 1618  cvjust 2251
[Jech] p. 42Lemma 6.1alephexp1 8134
[Jech] p. 42Equation 6.1alephadd 8132  alephmul 8133
[Jech] p. 43Lemma 6.2infmap 8131  infmap2 7777
[Jech] p. 71Lemma 9.3jech9.3 7419
[Jech] p. 72Equation 9.3scott0 7489  scottex 7488
[Jech] p. 72Exercise 9.1rankval4 7472
[Jech] p. 72Scheme "Collection Principle"cp 7494
[Jech] p. 78Definition implied by the footnoteopthprc 4689
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26332
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26428
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26429
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26344
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26348
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26349  rmyp1 26350
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26351  rmym1 26352
[JonesMatijasevic] p. 695Equation 2.11rmx0 26342  rmx1 26343  rmxluc 26353
[JonesMatijasevic] p. 695Equation 2.12rmy0 26346  rmy1 26347  rmyluc 26354
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26356
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26357
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26379  jm2.17b 26380  jm2.17c 26381
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26418
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26422
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26413
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26382  jm2.24nn 26378
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26427
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26433  rmygeid 26383
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26445
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[KalishMontague] p. 81Schemes B4 through B8equidK 28115
[KalishMontague] p. 85Lemma 2equidK 28115
[KalishMontague] p. 85Lemma 3equcomiK 28116
[KalishMontague] p. 85Theorem 1equidK 28115
[KalishMontague] p. 86Lemma 5albiiK 28122  alimdK 28123  alimdvK 28124
[KalishMontague] p. 86Lemma 7cbvaliK 28139  cbvalivK 28140
[KalishMontague] p. 86Lemma 9ax4wK 28132  ax4wfK 28131  equidK 28115
[KalishMontague] p. 87Lemma 8a4imK 28129  a4imvK 28130
[Kalmbach] p. 14Definition of latticechabs1 22020  chabs1i 22022  chabs2 22021  chabs2i 22023  chjass 22037  chjassi 21990  latabs1 14120  latabs2 14121
[Kalmbach] p. 15Definition of atomdf-at 22843  ela 22844
[Kalmbach] p. 15Definition of coverscvbr2 22788  cvrval2 28594
[Kalmbach] p. 16Definitiondf-ol 28498  df-oml 28499
[Kalmbach] p. 20Definition of commutescmbr 22106  cmbri 22112  cmtvalN 28531  df-cm 22105  df-cmtN 28497
[Kalmbach] p. 22Remarkomllaw5N 28567  pjoml5 22135  pjoml5i 22110
[Kalmbach] p. 22Definitionpjoml2 22133  pjoml2i 22107
[Kalmbach] p. 22Theorem 2(v)cmcm 22136  cmcmi 22114  cmcmii 22119  cmtcomN 28569
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28565  omlsi 21908  pjoml 21940  pjomli 21939
[Kalmbach] p. 22Definition of OML lawomllaw2N 28564
[Kalmbach] p. 23Remarkcmbr2i 22118  cmcm3 22137  cmcm3i 22116  cmcm3ii 22121  cmcm4i 22117  cmt3N 28571  cmt4N 28572  cmtbr2N 28573
[Kalmbach] p. 23Lemma 3cmbr3 22130  cmbr3i 22122  cmtbr3N 28574
[Kalmbach] p. 25Theorem 5fh1 22140  fh1i 22143  fh2 22141  fh2i 22144  omlfh1N 28578
[Kalmbach] p. 65Remarkchjatom 22862  chslej 22002  chsleji 21962  shslej 21884  shsleji 21874
[Kalmbach] p. 65Proposition 1chocin 21999  chocini 21958  chsupcl 21844  chsupval2 21914  h0elch 21759  helch 21748  hsupval2 21913  ocin 21800  ococss 21797  shococss 21798
[Kalmbach] p. 65Definition of subspace sumshsval 21816
[Kalmbach] p. 66Remarkdf-pjh 21899  pjssmi 22670  pjssmii 22203
[Kalmbach] p. 67Lemma 3osum 22167  osumi 22164
[Kalmbach] p. 67Lemma 4pjci 22705
[Kalmbach] p. 103Exercise 6atmd2 22905
[Kalmbach] p. 103Exercise 12mdsl0 22815
[Kalmbach] p. 140Remarkhatomic 22865  hatomici 22864  hatomistici 22867
[Kalmbach] p. 140Proposition 1atlatmstc 28639
[Kalmbach] p. 140Proposition 1(i)atexch 22886  lsatexch 28363
[Kalmbach] p. 140Proposition 1(ii)chcv1 22860  cvlcvr1 28659  cvr1 28729
[Kalmbach] p. 140Proposition 1(iii)cvexch 22879  cvexchi 22874  cvrexch 28739
[Kalmbach] p. 149Remark 2chrelati 22869  hlrelat 28721  hlrelat5N 28720  lrelat 28334
[Kalmbach] p. 153Exercise 5lsmcv 15821  lsmsatcv 28330  spansncv 22175  spansncvi 22174
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 28349  spansncv2 22798
[Kalmbach] p. 266Definitiondf-st 22716
[Kalmbach2] p. 8Definition of adjointdf-adjh 22354
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8201  fpwwe2 8198
[KanamoriPincus] p. 416Corollary 1.3canth4 8202
[KanamoriPincus] p. 417Corollary 1.6canthp1 8209
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8204
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8206
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8219
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8223  gchxpidm 8224
[KanamoriPincus] p. 419Theorem 2.1gchacg 8227  gchhar 8226
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7775  unxpwdom 7236
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8229
[Kreyszig] p. 3Property M1metcl 17824  xmetcl 17823
[Kreyszig] p. 4Property M2meteq0 17831
[Kreyszig] p. 8Definition 1.1-8dscmet 18022
[Kreyszig] p. 12Equation 5conjmul 9410  muleqadd 9345
[Kreyszig] p. 18Definition 1.3-2mopnval 17911
[Kreyszig] p. 19Remarkmopntopon 17912
[Kreyszig] p. 19Theorem T1mopn0 17971  mopnm 17917
[Kreyszig] p. 19Theorem T2unimopn 17969
[Kreyszig] p. 19Definition of neighborhoodneibl 17974
[Kreyszig] p. 20Definition 1.3-3metcnp2 18015
[Kreyszig] p. 25Definition 1.4-1lmbr 16915  lmmbr 18611  lmmbr2 18612
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17035
[Kreyszig] p. 28Theorem 1.4-5lmcau 18665
[Kreyszig] p. 28Definition 1.4-3iscau 18629  iscmet2 18647
[Kreyszig] p. 30Theorem 1.4-7cmetss 18667
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17114  metelcls 18657
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18658  metcld2 18659
[Kreyszig] p. 51Equation 2clmvneg1 18516  lmodvneg1 15594  nvinv 21122  vcm 21052
[Kreyszig] p. 51Equation 1aclm0vs 18515  lmod0vs 15590  vc0 21050
[Kreyszig] p. 51Equation 1blmodvs0 15591  vcz 21051
[Kreyszig] p. 58Definition 2.2-1imsmet 21185
[Kreyszig] p. 59Equation 1imsdval 21180  imsdval2 21181
[Kreyszig] p. 63Problem 1nvnd 21182
[Kreyszig] p. 64Problem 2nvge0 21165  nvz 21160
[Kreyszig] p. 64Problem 3nvabs 21164
[Kreyszig] p. 91Definition 2.7-1isblo3i 21304
[Kreyszig] p. 92Equation 2df-nmoo 21248
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21310  blocni 21308
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21309
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18566  ipeq0 16469  ipz 21220
[Kreyszig] p. 135Problem 2pythi 21353
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21357
[Kreyszig] p. 144Equation 4supcvg 12241
[Kreyszig] p. 144Theorem 3.3-1minvec 18727  minveco 21388
[Kreyszig] p. 196Definition 3.9-1df-aj 21253
[Kreyszig] p. 247Theorem 4.7-2bcth 18678
[Kreyszig] p. 249Theorem 4.7-3ubth 21377
[Kreyszig] p. 470Definition of positive operator orderingleop 22628  leopg 22627
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22646
[Kreyszig] p. 525Theorem 10.1-1htth 21423
[Kunen] p. 10Axiom 0a9e 1817  axnul 4088
[Kunen] p. 11Axiom 3axnul 4088
[Kunen] p. 12Axiom 6zfrep6 5647
[Kunen] p. 24Definition 10.24mapval 6717  mapvalg 6715
[Kunen] p. 30Lemma 10.20fodom 8082
[Kunen] p. 31Definition 10.24mapex 6711
[Kunen] p. 95Definition 2.1df-r1 7369
[Kunen] p. 97Lemma 2.10r1elss 7411  r1elssi 7410
[Kunen] p. 107Exercise 4rankop 7463  rankopb 7457  rankuni 7468  rankxplim 7482  rankxpsuc 7485
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3856
[Laboreo] p. 10Definition ITnatded 4
[Laboreo] p. 10Definition I` `m,nnatded 4
[Laboreo] p. 11Definition E=>m,nnatded 4
[Laboreo] p. 11Definition I=>m,nnatded 4
[Laboreo] p. 11Definition E` `(1)natded 4
[Laboreo] p. 11Definition E` `(2)natded 4
[Laboreo] p. 12Definition E` `m,n,pnatded 4
[Laboreo] p. 12Definition I` `n(1)natded 4
[Laboreo] p. 12Definition I` `n(2)natded 4
[Laboreo] p. 13Definition I` `m,n,pnatded 4
[Laboreo] p. 14Definition E` `nnatded 4
[Laboreo] p. 15Theorem 5.2ex-natded5.2-2 20745  ex-natded5.2 20744
[Laboreo] p. 16Theorem 5.3ex-natded5.3-2 20748  ex-natded5.3 20747
[Laboreo] p. 18Theorem 5.5ex-natded5.5 20750
[Laboreo] p. 19Theorem 5.7ex-natded5.7-2 20752  ex-natded5.7 20751
[Laboreo] p. 20Theorem 5.8ex-natded5.8-2 20754  ex-natded5.8 20753
[Laboreo] p. 20Theorem 5.13ex-natded5.13-2 20756  ex-natded5.13 20755
[Laboreo] p. 32Definition I` `nnatded 4
[Laboreo] p. 32Definition E` `m,n,p,anatded 4
[Laboreo] p. 32Definition E` `n,tnatded 4
[Laboreo] p. 32Definition I` `n,tnatded 4
[Laboreo] p. 43Theorem 9.20ex-natded9.20 20757
[Laboreo] p. 45Theorem 9.20ex-natded9.20-2 20758
[Laboreo] p. 45Theorem 9.26ex-natded9.26-2 20760  ex-natded9.26 20759
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26883
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26878
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26884
[LeBlanc] p. 277Rule R2axnul 4088
[Levy] p. 338Axiomdf-clab 2243  df-clel 2252  df-cleq 2249
[Levy58] p. 2Definition Iisfin1-3 7945
[Levy58] p. 2Definition IIdf-fin2 7845
[Levy58] p. 2Definition Iadf-fin1a 7844
[Levy58] p. 2Definition IIIdf-fin3 7847
[Levy58] p. 3Definition Vdf-fin5 7848
[Levy58] p. 3Definition IVdf-fin4 7846
[Levy58] p. 4Definition VIdf-fin6 7849
[Levy58] p. 4Definition VIIdf-fin7 7850
[Levy58], p. 3Theorem 1fin1a2 7974
[Lopez-Astorga] p. 12Rule 1mpto1 1528
[Lopez-Astorga] p. 12Rule 2mpto2 1529
[Lopez-Astorga] p. 12Rule 3mtp-xor 1530
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 22913
[Maeda] p. 168Lemma 5mdsym 22917  mdsymi 22916
[Maeda] p. 168Lemma 4(i)mdsymlem4 22911  mdsymlem6 22913  mdsymlem7 22914
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22915
[MaedaMaeda] p. 1Remarkssdmd1 22818  ssdmd2 22819  ssmd1 22816  ssmd2 22817
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22814
[MaedaMaeda] p. 1Definition 1.1df-dmd 22786  df-md 22785  mdbr 22799
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22836  mdslj1i 22824  mdslj2i 22825  mdslle1i 22822  mdslle2i 22823  mdslmd1i 22834  mdslmd2i 22835
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22826  mdsl2bi 22828  mdsl2i 22827
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22840
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22837
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22838
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22815
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22820  mdsl3 22821
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22839
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22934
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28641  hlrelat1 28719
[MaedaMaeda] p. 31Lemma 7.5lcvexch 28359
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22841  cvmdi 22829  cvnbtwn4 22794  cvrnbtwn4 28599
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22842
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28660  cvp 22880  cvrp 28735  lcvp 28360
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22904
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22903
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28653  hlexch4N 28711
[MaedaMaeda] p. 34Exercise 7.1atabsi 22906
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28762
[MaedaMaeda] p. 61Definition 15.10psubN 29068  atpsubN 29072  df-pointsN 28821  pointpsubN 29070
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28823  pmap11 29081  pmaple 29080  pmapsub 29087  pmapval 29076
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29084  pmap1N 29086
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29089  pmapglb2N 29090  pmapglb2xN 29091  pmapglbx 29088
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29171
[MaedaMaeda] p. 67Postulate PS1ps-1 28796
[MaedaMaeda] p. 68Lemma 16.2df-padd 29115  paddclN 29161  paddidm 29160
[MaedaMaeda] p. 68Condition PS2ps-2 28797
[MaedaMaeda] p. 68Equation 16.2.1paddass 29157
[MaedaMaeda] p. 69Lemma 16.4ps-1 28796
[MaedaMaeda] p. 69Theorem 16.4ps-2 28797
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14911  lsmmod2 14912  lssats 28332  shatomici 22863  shatomistici 22866  shmodi 21894  shmodsi 21893
[MaedaMaeda] p. 130Remark 29.6dmdmd 22805  mdsymlem7 22914
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22111
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 21997
[MaedaMaeda] p. 139Remarksumdmdii 22920
[Margaris] p. 40Rule Cexlimiv 2024
[Margaris] p. 49Axiom A1ax-1 7
[Margaris] p. 49Axiom A2ax-2 8
[Margaris] p. 49Axiom A3ax-3 9
[Margaris] p. 49Definitiondf-an 362  df-ex 1538  df-or 361  dfbi2 612
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 27704
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27705
[Margaris] p. 79Rule Cexinst01 27410  exinst11 27411
[Margaris] p. 89Theorem 19.219.2 1759  19.2K 28138  r19.2z 3485
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2860
[Margaris] p. 89Theorem 19.5alcom 1568
[Margaris] p. 89Theorem 19.6alex 1570
[Margaris] p. 89Theorem 19.7alnex 1569
[Margaris] p. 89Theorem 19.819.8a 1758
[Margaris] p. 89Theorem 19.919.9 1762  19.9v 2011
[Margaris] p. 89Theorem 19.11excom 1765  excomim 1764
[Margaris] p. 89Theorem 19.1219.12 1766  r19.12 2627
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26908  albi 1552  ralbi 2650
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26910  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26907  alim 1548  alimd 1705  alimdh 1551  alimdv 2018  ralimdaa 2591  ralimdv 2593  ralimdva 2592  sbcimdv 2996
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2012  19.21vv 26906  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2015  alrimi 1706  alrimih 1553  alrimiv 2013  alrimivv 2014  r19.21 2600  r19.21be 2615  r19.21bi 2612  r19.21t 2599  r19.21v 2601  ralrimd 2602  ralrimdv 2603  ralrimdva 2604  ralrimdvv 2608  ralrimdvva 2609  ralrimi 2595  ralrimiv 2596  ralrimiva 2597  ralrimivv 2605  ralrimivva 2606  ralrimivvva 2607  ralrimivw 2598  rexlimi 2631
[Margaris] p. 90Theorem 19.222alimdv 2020  2exim 26909  2eximdv 2021  exim 1573  eximd 1711  eximdh 1586  eximdv 2019  rexim 2618  reximdai 2622  reximddv 22953  reximdv 2625  reximdv2 2623  reximdva 2626  reximdvai 2624  reximi2 2620
[Margaris] p. 90Theorem 19.2319.23 1777  19.23bi 1783  19.23t 1776  19.23v 2022  19.23vv 2023  exlimd 1784  exlimdh 1785  exlimdv 1933  exlimdvv 2027  exlimexi 27303  exlimi 1781  exlimih 1782  exlimiv 2024  exlimivv 2026  r19.23 2629  r19.23v 2630  rexlimd 2635  rexlimdv 2637  rexlimdv3a 2640  rexlimdva 2638  rexlimdvaa 2639  rexlimdvv 2644  rexlimdvva 2645  rexlimdvw 2641  rexlimiv 2632  rexlimiva 2633  rexlimivv 2643
[Margaris] p. 90Theorem 19.2419.24 1793
[Margaris] p. 90Theorem 19.2519.25 1602
[Margaris] p. 90Theorem 19.2619.26-2 1593  19.26-3an 1594  19.26 1592  r19.26-2 2647  r19.26-2a 24265  r19.26-3 2648  r19.26 2646  r19.26m 2649
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2028  r19.27av 2652  r19.27z 3494  r19.27zv 3495
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2029  19.28vv 26916  r19.28av 2653  r19.28z 3488  r19.28zv 3491  rr19.28v 2861
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2654  r19.29r 2655
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2656
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26914
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32v 2657
[Margaris] p. 90Theorem 19.3319.33-2 26912  19.33 1606  19.33b 1607
[Margaris] p. 90Theorem 19.3419.34 1798
[Margaris] p. 90Theorem 19.3519.35 1599  19.35i 1600  19.35ri 1601  r19.35 2658
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2031  19.36i 1789  19.36v 2030  19.36vv 26913  r19.36av 2659  r19.36zv 3496
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2034  19.37v 2033  19.37vv 26915  r19.37 2660  r19.37av 2661  r19.37zv 3492
[Margaris] p. 90Theorem 19.3819.38 1791
[Margaris] p. 90Theorem 19.3919.39 1792
[Margaris] p. 90Theorem 19.4019.40-2 1609  19.40 1608  r19.40 2662
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 27332  19.41v 2035  19.41vv 2036  19.41vvv 2037  19.41vvvv 2038  r19.41 2663  r19.41v 2664
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2039  19.42vv 2041  19.42vvv 2042  r19.42v 2665
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2666
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2667
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2668  r19.45zv 3493
[Margaris] p. 110Exercise 2(b)eu1 2137
[Mayet] p. 370Remarkjpi 22775  largei 22772  stri 22762
[Mayet3] p. 9Definition of CH-statesdf-hst 22717  ishst 22719
[Mayet3] p. 10Theoremhstrbi 22771  hstri 22770
[Mayet3] p. 1223Theorem 4.1mayete3i 22250
[Mayet3] p. 1240Theorem 7.1mayetes3i 22252
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22783
[MegPav2000] p. 2345Definition 3.4-1chintcl 21836  chsupcl 21844
[MegPav2000] p. 2345Definition 3.4-2hatomic 22865
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22859
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22886
[MegPav2000] p. 2366Figure 7pl42N 29302
[MegPav2002] p. 362Lemma 2.2latj31 14132  latj32 14130  latjass 14128
[Megill] p. 444Axiom C5ax-17 1628
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1838  alequcom 1680  alequcomX 28229  ax-10 1678
[Megill] p. 446Lemma L17equtrr 1827
[Megill] p. 446Lemma L18ax9from9o 1816
[Megill] p. 446Lemma L19hbnae-o 1846  hbnae 1845
[Megill] p. 447Remark 9.1df-sb 1884  sbid 1896  sbidd-misc 27201  sbidd 27200
[Megill] p. 448Remark 9.6ax15 2104
[Megill] p. 448Scheme C4'ax-5o 1694
[Megill] p. 448Scheme C5'ax-4 1692
[Megill] p. 448Scheme C6'ax-7 1535
[Megill] p. 448Scheme C7'ax-6o 1697
[Megill] p. 448Scheme C8'ax-8 1623
[Megill] p. 448Scheme C9'ax-12o 1664
[Megill] p. 448Scheme C10'ax-9 1684  ax-9o 1815
[Megill] p. 448Scheme C11'ax-10o 1836
[Megill] p. 448Scheme C12'ax-13 1625
[Megill] p. 448Scheme C13'ax-14 1626
[Megill] p. 448Scheme C14'ax-15 2105
[Megill] p. 448Scheme C15'ax-11o 1941
[Megill] p. 448Scheme C16'ax-16 1927
[Megill] p. 448Theorem 9.4dral1-o 1857  dral1 1856  dral2-o 1859  dral2 1858  drex1 1860  drex2 1861  drsb1 1887  drsb2 1954
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2077  sbequ 1953  sbid2v 2086
[Megill] p. 450Example in Appendixhba1 1718
[Mendelson] p. 35Axiom A3hirstL-ax3 27114
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 3013  ra4sbca 3014  stdpc4 1897
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3019  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2024
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1892
[Mendelson] p. 225Axiom system NBGru 2934
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4205
[Mendelson] p. 231Exercise 4.10(k)inv1 3423
[Mendelson] p. 231Exercise 4.10(l)unv 3424
[Mendelson] p. 231Exercise 4.10(n)dfin3 3350
[Mendelson] p. 231Exercise 4.10(o)df-nul 3398
[Mendelson] p. 231Exercise 4.10(q)dfin4 3351
[Mendelson] p. 231Exercise 4.10(s)ddif 3250
[Mendelson] p. 231Definition of uniondfun3 3349
[Mendelson] p. 235Exercise 4.12(c)univ 4502
[Mendelson] p. 235Exercise 4.12(d)pwv 3767
[Mendelson] p. 235Exercise 4.12(j)pwin 4234
[Mendelson] p. 235Exercise 4.12(k)pwunss 4235
[Mendelson] p. 235Exercise 4.12(l)pwssun 4236
[Mendelson] p. 235Exercise 4.12(n)uniin 3788
[Mendelson] p. 235Exercise 4.12(p)reli 4766
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5145
[Mendelson] p. 244Proposition 4.8(g)epweon 4512
[Mendelson] p. 246Definition of successordf-suc 4335
[Mendelson] p. 250Exercise 4.36oelim2 6526
[Mendelson] p. 254Proposition 4.22(b)xpen 6957
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6879  xpsneng 6880
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6886  xpcomeng 6887
[Mendelson] p. 254Proposition 4.22(e)xpassen 6889
[Mendelson] p. 255Definitionbrsdom 6817
[Mendelson] p. 255Exercise 4.39endisj 6882
[Mendelson] p. 255Exercise 4.41mapprc 6709
[Mendelson] p. 255Exercise 4.43mapsnen 6871
[Mendelson] p. 255Exercise 4.45mapunen 6963
[Mendelson] p. 255Exercise 4.47xpmapen 6962
[Mendelson] p. 255Exercise 4.42(a)map0e 6738
[Mendelson] p. 255Exercise 4.42(b)map1 6872
[Mendelson] p. 257Proposition 4.24(a)undom 6883
[Mendelson] p. 258Exercise 4.56(b)cdaen 7732
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7741  cdacomen 7740
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7745
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7739
[Mendelson] p. 258Definition of cardinal sumcdaval 7729  df-cda 7727
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6463
[Mendelson] p. 266Proposition 4.34(f)oaordex 6489
[Mendelson] p. 275Proposition 4.42(d)entri3 8114
[Mendelson] p. 281Definitiondf-r1 7369
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7418
[Mendelson] p. 287Axiom system MKru 2934
[Mittelstaedt] p. 9Definitiondf-oc 21756
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3333
[Monk1] p. 33Theorem 3.2(i)ssrel 4729
[Monk1] p. 33Theorem 3.2(ii)eqrel 4730
[Monk1] p. 34Definition 3.3df-opab 4018
[Monk1] p. 36Theorem 3.7(i)coi1 5140  coi2 5141
[Monk1] p. 36Theorem 3.8(v)dm0 4845  rn0 4889
[Monk1] p. 36Theorem 3.7(ii)cnvi 5038
[Monk1] p. 37Theorem 3.13(i)relxp 4747
[Monk1] p. 37Theorem 3.13(x)dmxp 4850  rnxp 5059
[Monk1] p. 37Theorem 3.13(ii)xp0 5051  xp0r 4721
[Monk1] p. 38Theorem 3.16(ii)ima0 4983
[Monk1] p. 38Theorem 3.16(viii)imai 4980
[Monk1] p. 39Theorem 3.17imaexg 4979
[Monk1] p. 39Theorem 3.16(xi)imassrn 4978
[Monk1] p. 41Theorem 4.3(i)fnopfv 5559  funfvop 5536
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5465
[Monk1] p. 42Theorem 4.4(iii)fvelima 5473
[Monk1] p. 43Theorem 4.6funun 5199
[Monk1] p. 43Theorem 4.8(iv)dff13 5682  dff13f 5683
[Monk1] p. 46Theorem 4.15(v)funex 5642  funrnex 5646
[Monk1] p. 50Definition 5.4fniunfv 5672
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5108
[Monk1] p. 52Theorem 5.11(viii)ssint 3819
[Monk1] p. 52Definition 5.13 (i)1stval2 6036  df-1st 6021
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6037  df-2nd 6022
[Monk1] p. 112Theorem 15.17(v)ranksn 7459  ranksnb 7432
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7460
[Monk1] p. 112Theorem 15.17(iii)rankun 7461  rankunb 7455
[Monk1] p. 113Theorem 15.18r1val3 7443
[Monk1] p. 113Definition 15.19df-r1 7369  r1val2 7442
[Monk1] p. 117Lemmazorn2 8066  zorn2g 8063
[Monk1] p. 133Theorem 18.11cardom 7552
[Monk1] p. 133Theorem 18.12canth3 8116
[Monk1] p. 133Theorem 18.14carduni 7547
[Monk2] p. 105Axiom C4ax-5 1533
[Monk2] p. 105Axiom C7ax-8 1623
[Monk2] p. 105Axiom C8ax-11 1624  ax-11o 1941
[Monk2] p. 105Axiom (C8)ax11v 1991
[Monk2] p. 108Lemma 5ax-5o 1694
[Monk2] p. 109Lemma 12ax-7 1535
[Monk2] p. 109Lemma 15equvin 2000  equvini 1880  eqvinop 4188
[Monk2] p. 113Axiom C5-1ax-17 1628
[Monk2] p. 113Axiom C5-2ax-6 1534
[Monk2] p. 113Axiom C5-3ax-7 1535
[Monk2] p. 114Lemma 21ax4 1691
[Monk2] p. 114Lemma 22ax5o 1693  hba1 1718
[Monk2] p. 114Lemma 23nfia1 1745
[Monk2] p. 114Lemma 24nfa2 1744  nfra2 2568
[Moore] p. 53Part Idf-mre 13415
[Munkres] p. 77Example 2distop 16660  indistop 16666  indistopon 16665
[Munkres] p. 77Example 3fctop 16668  fctop2 16669
[Munkres] p. 77Example 4cctop 16670
[Munkres] p. 78Definition of basisdf-bases 16565  isbasis3g 16614
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13271  tgval2 16621
[Munkres] p. 79Remarktgcl 16634
[Munkres] p. 80Lemma 2.1tgval3 16628
[Munkres] p. 80Lemma 2.2tgss2 16652  tgss3 16651
[Munkres] p. 81Lemma 2.3basgen 16653  basgen2 16654
[Munkres] p. 89Definition of subspace topologyresttop 16818
[Munkres] p. 93Theorem 6.1(1)0cld 16702  topcld 16699
[Munkres] p. 93Theorem 6.1(2)iincld 16703
[Munkres] p. 93Theorem 6.1(3)uncld 16705
[Munkres] p. 94Definition of closureclsval 16701
[Munkres] p. 94Definition of interiorntrval 16700
[Munkres] p. 95Theorem 6.5(a)clsndisj 16739  elcls 16737
[Munkres] p. 95Theorem 6.5(b)elcls3 16747
[Munkres] p. 97Theorem 6.6clslp 16806  neindisj 16781
[Munkres] p. 97Corollary 6.7cldlp 16808
[Munkres] p. 97Definition of limit pointislp2 16804  lpval 16798
[Munkres] p. 98Definition of Hausdorff spacedf-haus 16970
[Munkres] p. 102Definition of continuous functiondf-cn 16884  iscn 16892  iscn2 16895
[Munkres] p. 107Theorem 7.2(g)cncnp 16936  cncnp2 16937  cncnpi 16934  df-cnp 16885  iscnp 16894  iscnp2 16896
[Munkres] p. 127Theorem 10.1metcn 18016
[Munkres] p. 128Theorem 10.3metcn4 18663
[NielsenChuang] p. 195Equation 4.73unierri 22609
[Pfenning] p. 17Definition XMnatded 4  natded 4
[Pfenning] p. 17Definition NNCnatded 4  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 4
[Pfenning] p. 18Rule"natded 4
[Pfenning] p. 18Definition /\Inatded 4
[Pfenning] p. 18Definition ` `Enatded 4  natded 4  natded 4  natded 4  natded 4
[Pfenning] p. 18Definition ` `Inatded 4  natded 4  natded 4  natded 4  natded 4
[Pfenning] p. 18Definition ` `ELnatded 4
[Pfenning] p. 18Definition ` `ERnatded 4
[Pfenning] p. 18Definition ` `Ea,unatded 4
[Pfenning] p. 18Definition ` `IRnatded 4
[Pfenning] p. 18Definition ` `Ianatded 4
[Pfenning] p. 127Definition =Enatded 4
[Pfenning] p. 127Definition =Inatded 4
[Ponnusamy] p. 361Theorem 6.44cphip0l 18564  df-dip 21199  dip0l 21219  ip0l 16467
[Ponnusamy] p. 361Equation 6.45ipval 21201
[Ponnusamy] p. 362Equation I1dipcj 21215
[Ponnusamy] p. 362Equation I3cphdir 18567  dipdir 21345  ipdir 16470  ipdiri 21333
[Ponnusamy] p. 362Equation I4ipidsq 21211
[Ponnusamy] p. 362Equation 6.46ip0i 21328
[Ponnusamy] p. 362Equation 6.47ip1i 21330
[Ponnusamy] p. 362Equation 6.48ip2i 21331
[Ponnusamy] p. 363Equation I2cphass 18573  dipass 21348  ipass 16476  ipassi 21344
[Prugovecki] p. 186Definition of brabraval 22449  df-bra 22355
[Prugovecki] p. 376Equation 8.1df-kb 22356  kbval 22459
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22887
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 29207
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22901  atcvat4i 22902  cvrat3 28761  cvrat4 28762  lsatcvat3 28372
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22787  cvrval 28589  df-cv 22784  df-lcv 28339  lspsncv0 15826
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 29219
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 29220
[Quine] p. 16Definition 2.1df-clab 2243  rabid 2684
[Quine] p. 17Definition 2.1''dfsb7 2082
[Quine] p. 18Definition 2.7df-cleq 2249
[Quine] p. 19Definition 2.9conventions 3  df-v 2742
[Quine] p. 34Theorem 5.1abeq2 2361
[Quine] p. 35Theorem 5.2abid2 2373  abid2f 2417
[Quine] p. 40Theorem 6.1sb5 1994
[Quine] p. 40Theorem 6.2sb56 1992  sb6 1993
[Quine] p. 41Theorem 6.3df-clel 2252
[Quine] p. 41Theorem 6.4eqid 2256  eqid1 20765
[Quine] p. 41Theorem 6.5eqcom 2258
[Quine] p. 42Theorem 6.6df-sbc 2936
[Quine] p. 42Theorem 6.7dfsbcq 2937  dfsbcq2 2938
[Quine] p. 43Theorem 6.8vex 2743
[Quine] p. 43Theorem 6.9isset 2744
[Quine] p. 44Theorem 7.3cla4gf 2814  cla4gv 2819  cla4imgf 2812
[Quine] p. 44Theorem 6.11a4sbc 2947  a4sbcd 2948
[Quine] p. 44Theorem 6.12elex 2748
[Quine] p. 44Theorem 6.13elab 2865  elabg 2866  elabgf 2863
[Quine] p. 44Theorem 6.14noel 3401
[Quine] p. 48Theorem 7.2snprc 3636
[Quine] p. 48Definition 7.1df-pr 3588  df-sn 3587
[Quine] p. 49Theorem 7.4snss 3689  snssg 3695
[Quine] p. 49Theorem 7.5prss 3710  prssg 3711
[Quine] p. 49Theorem 7.6prid1 3675  prid1g 3673  prid2 3676  prid2g 3674  snid 3608  snidg 3606
[Quine] p. 51Theorem 7.13prex 4155  snex 4154  snexALT 4134
[Quine] p. 53Theorem 8.2unisn 3784  unisnALT 27715  unisng 3785
[Quine] p. 53Theorem 8.3uniun 3787
[Quine] p. 54Theorem 8.6elssuni 3796
[Quine] p. 54Theorem 8.7uni0 3795
[Quine] p. 56Theorem 8.17uniabio 6200
[Quine] p. 56Definition 8.18dfiota2 6191
[Quine] p. 57Theorem 8.19iotaval 6201
[Quine] p. 57Theorem 8.22iotanul 6205
[Quine] p. 58Theorem 8.23iotaex 6207
[Quine] p. 58Definition 9.1df-op 3590
[Quine] p. 61Theorem 9.5opabid 4208  opelopab 4223  opelopaba 4218  opelopabaf 4225  opelopabf 4226  opelopabg 4220  opelopabga 4215  oprabid 5781
[Quine] p. 64Definition 9.11df-xp 4640
[Quine] p. 64Definition 9.12df-cnv 4642
[Quine] p. 64Definition 9.15df-id 4246
[Quine] p. 65Theorem 10.3fun0 5210
[Quine] p. 65Theorem 10.4funi 5188
[Quine] p. 65Theorem 10.5funsn 5203  funsng 5201
[Quine] p. 65Definition 10.1df-fun 4648
[Quine] p. 65Definition 10.2args 4994  df-fv 4654
[Quine] p. 68Definition 10.11conventions 3  df-fv 4654  fv2 5419
[Quine] p. 124Theorem 17.3nn0opth2 11218  nn0opth2i 11217  nn0opthi 11216  omopthi 6588
[Quine] p. 177Definition 25.2df-rdg 6356
[Quine] p. 232Equation icarddom 8109
[Quine] p. 284Axiom 39(vi)funimaex 5233  funimaexg 5232
[Quine] p. 331Axiom system NFru 2934
[ReedSimon] p. 36Definition (iii)ax-his3 21588
[ReedSimon] p. 63Exercise 4(a)df-dip 21199  polid 21663  polid2i 21661  polidi 21662
[ReedSimon] p. 63Exercise 4(b)df-ph 21316
[ReedSimon] p. 195Remarklnophm 22524  lnophmi 22523
[Retherford] p. 49Exercise 1(i)leopadd 22637
[Retherford] p. 49Exercise 1(ii)leopmul 22639  leopmuli 22638
[Retherford] p. 49Exercise 1(iv)leoptr 22642
[Retherford] p. 49Definition VI.1df-leop 22357  leoppos 22631
[Retherford] p. 49Exercise 1(iii)leoptri 22641
[Retherford] p. 49Definition of operator orderingleop3 22630
[Rudin] p. 164Equation 27efcan 12303
[Rudin] p. 164Equation 30efzval 12309
[Rudin] p. 167Equation 48absefi 12403
[Sanford] p. 39Rule 3mtp-xor 1530
[Sanford] p. 39Rule 4mpto2 1529
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 10
[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 169
[Sanford] p. 40Rule 1mpto1 1528
[Schechter] p. 51Definition of antisymmetryintasym 5011
[Schechter] p. 51Definition of irreflexivityintirr 5014
[Schechter] p. 51Definition of symmetrycnvsym 5010
[Schechter] p. 51Definition of transitivitycotr 5008
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13415
[Schechter] p. 79Definition of Moore closuredf-mrc 13416
[Schechter] p. 82Section 4.5df-mrc 13416
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13418
[Schechter] p. 139Definition AC3dfac9 7695
[Schechter] p. 141Definition (MC)dfac11 26492
[Schechter] p. 149Axiom DC1ax-dc 8005  axdc3 8013
[Schechter] p. 187Definition of ring with unitisrng 15272  isrngo 20970
[Schechter] p. 276Remark 11.6.espan0 22046
[Schechter] p. 276Definition of spandf-span 21813  spanval 21837
[Schechter] p. 428Definition 15.35bastop1 16658
[Schwabhauser] p. 10Axiom A1axcgrrflx 23882
[Schwabhauser] p. 10Axiom A2axcgrtr 23883
[Schwabhauser] p. 10Axiom A3axcgrid 23884
[Schwabhauser] p. 11Axiom A4axsegcon 23895
[Schwabhauser] p. 11Axiom A5ax5seg 23906
[Schwabhauser] p. 11Axiom A6axbtwnid 23907
[Schwabhauser] p. 12Axiom A7axpasch 23909
[Schwabhauser] p. 12Axiom A8axlowdim2 23928
[Schwabhauser] p. 13Axiom A10axeuclid 23931
[Schwabhauser] p. 13Axiom A11axcont 23944
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23950
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23952
[Schwabhauser] p. 27Theorem 2.3cgrtr 23955
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23959
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23960
[Schwabhauser] p. 28Theorem 2.8cgrtriv 23965
[Schwabhauser] p. 28Theorem 2.105segofs 23969
[Schwabhauser] p. 28Definition 2.10df-ofs 23946
[Schwabhauser] p. 29Theorem 2.11cgrextend 23971
[Schwabhauser] p. 29Theorem 2.12segconeq 23973
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 23985  btwntriv2 23975
[Schwabhauser] p. 30Theorem 3.2btwncomim 23976
[Schwabhauser] p. 30Theorem 3.3btwntriv1 23979
[Schwabhauser] p. 30Theorem 3.4btwnswapid 23980
[Schwabhauser] p. 30Theorem 3.5btwnexch2 23986  btwnintr 23982
[Schwabhauser] p. 30Theorem 3.6btwnexch 23988  btwnexch3 23983
[Schwabhauser] p. 30Theorem 3.7btwnouttr 23987
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23927
[Schwabhauser] p. 32Theorem 3.14btwndiff 23990
[Schwabhauser] p. 33Theorem 3.17trisegint 23991
[Schwabhauser] p. 34Theorem 4.2ifscgr 24007
[Schwabhauser] p. 34Definition 4.1df-ifs 24002
[Schwabhauser] p. 35Theorem 4.3cgrsub 24008
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24018
[Schwabhauser] p. 35Definition 4.4df-cgr3 24003
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24019
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24025  colinearperm2 24027  colinearperm3 24026  colinearperm4 24028  colinearperm5 24029
[Schwabhauser] p. 36Definition 4.10df-colinear 24004
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24030
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24038
[Schwabhauser] p. 37Theorem 4.14lineext 24039
[Schwabhauser] p. 37Theorem 4.16fscgr 24043
[Schwabhauser] p. 37Theorem 4.17linecgr 24044
[Schwabhauser] p. 37Definition 4.15df-fs 24005
[Schwabhauser] p. 38Theorem 4.18lineid 24046
[Schwabhauser] p. 38Theorem 4.19idinside 24047
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24064
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24065
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24066
[Schwabhauser] p. 41Theorem 5.5brsegle2 24072
[Schwabhauser] p. 41Definition 5.4df-segle 24070
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24073
[Schwabhauser] p. 42Theorem 5.7seglerflx 24075
[Schwabhauser] p. 42Theorem 5.8segletr 24077
[Schwabhauser] p. 42Theorem 5.9segleantisym 24078
[Schwabhauser] p. 42Theorem 5.10seglelin 24079
[Schwabhauser] p. 42Theorem 5.11seglemin 24076
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24081
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24088
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24089
[Schwabhauser] p. 43Theorem 6.4broutsideof 24084  df-outsideof 24083
[Schwabhauser] p. 43Definition 6.1broutsideof2 24085
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24090
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24091
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24092
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24094
[Schwabhauser] p. 44Definition 6.8df-ray 24101
[Schwabhauser] p. 45Part 2df-lines2 24102
[Schwabhauser] p. 45Theorem 6.13outsidele 24095
[Schwabhauser] p. 45Theorem 6.15lineunray 24110
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24111
[Schwabhauser] p. 45Theorem 6.17linecom 24113  linerflx1 24112  linerflx2 24114
[Schwabhauser] p. 45Theorem 6.18linethru 24116
[Schwabhauser] p. 45Definition 6.14df-line2 24100
[Schwabhauser] p. 46Theorem 6.19linethrueu 24119
[Schwabhauser] p. 46Theorem 6.21lineintmo 24120
[Shapiro] p. 230Theorem 6.5.1dchrhash 20437  dchrsum 20435  dchrsum2 20434  sumdchr 20438
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20439  sum2dchr 20440
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15228  ablfacrp2 15229
[Shapiro], p. 328Equation 9.2.4vmasum 20382
[Shapiro], p. 329Equation 9.2.7logfac2 20383
[Shapiro], p. 329Equation 9.2.9logfacrlim 20390
[Shapiro], p. 331Equation 9.2.13vmadivsum 20558
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20561
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20615  vmalogdivsum2 20614
[Shapiro], p. 375Theorem 9.4.1dirith 20605  dirith2 20604
[Shapiro], p. 375Equation 9.4.3rplogsum 20603  rpvmasum 20602  rpvmasum2 20588
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20563
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20601
[Shapiro], p. 377Lemma 9.4.1dchrisum 20568  dchrisumlem1 20565  dchrisumlem2 20566  dchrisumlem3 20567  dchrisumlema 20564
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20571
[Shapiro], p. 379Equation 9.4.16dchrmusum 20600  dchrmusumlem 20598  dchrvmasumlem 20599
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20570
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20572
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20596  dchrisum0re 20589  dchrisumn0 20597
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20582
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20586
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20587
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20642  pntrsumbnd2 20643  pntrsumo1 20641
[Shapiro], p. 405Equation 10.2.1mudivsum 20606
[Shapiro], p. 406Equation 10.2.6mulogsum 20608
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20610
[Shapiro], p. 407Equation 10.2.8mulog2sum 20613
[Shapiro], p. 418Equation 10.4.6logsqvma 20618
[Shapiro], p. 418Equation 10.4.8logsqvma2 20619
[Shapiro], p. 419Equation 10.4.10selberg 20624
[Shapiro], p. 420Equation 10.4.12selberg2lem 20626
[Shapiro], p. 420Equation 10.4.14selberg2 20627
[Shapiro], p. 422Equation 10.6.7selberg3 20635
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20636
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20633  selberg3lem2 20634
[Shapiro], p. 422Equation 10.4.23selberg4 20637
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20631
[Shapiro], p. 428Equation 10.6.2selbergr 20644
[Shapiro], p. 429Equation 10.6.8selberg3r 20645
[Shapiro], p. 430Equation 10.6.11selberg4r 20646
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20660
[Shapiro], p. 434Equation 10.6.27pntlema 20672  pntlemb 20673  pntlemc 20671  pntlemd 20670  pntlemg 20674
[Shapiro], p. 435Equation 10.6.29pntlema 20672
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20664
[Shapiro], p. 436Lemma 10.6.2pntibnd 20669
[Shapiro], p. 436Equation 10.6.34pntlema 20672
[Shapiro], p. 436Equation 10.6.35pntlem3 20685  pntleml 20687
[Stoll] p. 13Definition of symmetric differencesymdif1 3375
[Stoll] p. 16Exercise 4.40dif 3467  dif0 3466
[Stoll] p. 16Exercise 4.8difdifdir 3483
[Stoll] p. 17Theorem 5.1(5)undifv 3470
[Stoll] p. 19Theorem 5.2(13)undm 3368
[Stoll] p. 19Theorem 5.2(13')indm 3369
[Stoll] p. 20Remarkinvdif 3352
[Stoll] p. 25Definition of ordered tripledf-ot 3591
[Stoll] p. 43Definitionuniiun 3896
[Stoll] p. 44Definitionintiin 3897
[Stoll] p. 45Definitiondf-iin 3849
[Stoll] p. 45Definition indexed uniondf-iun 3848
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3375
[Strang] p. 242Section 6.3expgrowth 26884
[Suppes] p. 22Theorem 2eq0 3411
[Suppes] p. 22Theorem 4eqss 3136  eqssd 3138  eqssi 3137
[Suppes] p. 23Theorem 5ss0 3427  ss0b 3426
[Suppes] p. 23Theorem 6sstr 3129  sstrALT2 27624
[Suppes] p. 23Theorem 7pssirr 3218
[Suppes] p. 23Theorem 8pssn2lp 3219
[Suppes] p. 23Theorem 9psstr 3222
[Suppes] p. 23Theorem 10pssss 3213
[Suppes] p. 25Theorem 12elin 3300  elun 3258
[Suppes] p. 26Theorem 15inidm 3320
[Suppes] p. 26Theorem 16in0 3422
[Suppes] p. 27Theorem 23unidm 3260
[Suppes] p. 27Theorem 24un0 3421
[Suppes] p. 27Theorem 25ssun1 3280
[Suppes] p. 27Theorem 26ssequn1 3287
[Suppes] p. 27Theorem 27unss 3291
[Suppes] p. 27Theorem 28indir 3359
[Suppes] p. 27Theorem 29undir 3360
[Suppes] p. 28Theorem 32difid 3464  difidALT 3465
[Suppes] p. 29Theorem 33difin 3348
[Suppes] p. 29Theorem 34indif 3353
[Suppes] p. 29Theorem 35undif1 3471
[Suppes] p. 29Theorem 36difun2 3475
[Suppes] p. 29Theorem 37difin0 3469
[Suppes] p. 29Theorem 38disjdif 3468
[Suppes] p. 29Theorem 39difundi 3363
[Suppes] p. 29Theorem 40difindi 3365
[Suppes] p. 30Theorem 41nalset 4091
[Suppes] p. 39Theorem 61uniss 3789
[Suppes] p. 39Theorem 65uniop 4206
[Suppes] p. 41Theorem 70intsn 3839
[Suppes] p. 42Theorem 71intpr 3836  intprg 3837
[Suppes] p. 42Theorem 73op1stb 4506
[Suppes] p. 42Theorem 78intun 3835
[Suppes] p. 44Definition 15(a)dfiun2 3878  dfiun2g 3876
[Suppes] p. 44Definition 15(b)dfiin2 3879
[Suppes] p. 47Theorem 86elpw 3572  elpw2 4108  elpw2g 4107  elpwg 3573  elpwgdedVD 27706
[Suppes] p. 47Theorem 87pwid 3579
[Suppes] p. 47Theorem 89pw0 3703
[Suppes] p. 48Theorem 90pwpw0 3704
[Suppes] p. 52Theorem 101xpss12 4745
[Suppes] p. 52Theorem 102xpindi 4772  xpindir 4773
[Suppes] p. 52Theorem 103xpundi 4694  xpundir 4695
[Suppes] p. 54Theorem 105elirrv 7244
[Suppes] p. 58Theorem 2relss 4728
[Suppes] p. 59Theorem 4eldm 4829  eldm2 4830  eldm2g 4828  eldmg 4827
[Suppes] p. 59Definition 3df-dm 4644
[Suppes] p. 60Theorem 6dmin 4839
[Suppes] p. 60Theorem 8rnun 5042
[Suppes] p. 60Theorem 9rnin 5043
[Suppes] p. 60Definition 4dfrn2 4821
[Suppes] p. 61Theorem 11brcnv 4817  brcnvg 4815
[Suppes] p. 62Equation 5elcnv 4811  elcnv2 4812
[Suppes] p. 62Theorem 12relcnv 5004
[Suppes] p. 62Theorem 15cnvin 5041
[Suppes] p. 62Theorem 16cnvun 5039
[Suppes] p. 63Theorem 20co02 5138
[Suppes] p. 63Theorem 21dmcoss 4897
[Suppes] p. 63Definition 7df-co 4643
[Suppes] p. 64Theorem 26cnvco 4818
[Suppes] p. 64Theorem 27coass 5143
[Suppes] p. 65Theorem 31resundi 4922
[Suppes] p. 65Theorem 34elima 4970  elima2 4971  elima3 4972  elimag 4969
[Suppes] p. 65Theorem 35imaundi 5046
[Suppes] p. 66Theorem 40dminss 5048
[Suppes] p. 66Theorem 41imainss 5049
[Suppes] p. 67Exercise 11cnvxp 5050
[Suppes] p. 81Definition 34dfec2 6596
[Suppes] p. 82Theorem 72elec 6632  elecg 6631
[Suppes] p. 82Theorem 73erth 6637  erth2 6638
[Suppes] p. 83Theorem 74erdisj 6640
[Suppes] p. 89Theorem 96map0b 6739
[Suppes] p. 89Theorem 97map0 6741  map0g 6740
[Suppes] p. 89Theorem 98mapsn 6742
[Suppes] p. 89Theorem 99mapss 6743
[Suppes] p. 91Definition 12(ii)alephsuc 7628
[Suppes] p. 91Definition 12(iii)alephlim 7627
[Suppes] p. 92Theorem 1enref 6827  enrefg 6826
[Suppes] p. 92Theorem 2ensym 6843  ensymb 6842  ensymi 6844
[Suppes] p. 92Theorem 3entr 6846
[Suppes] p. 92Theorem 4unen 6876
[Suppes] p. 94Theorem 15endom 6821
[Suppes] p. 94Theorem 16ssdomg 6840
[Suppes] p. 94Theorem 17domtr 6847
[Suppes] p. 95Theorem 18sbth 6914
[Suppes] p. 97Theorem 23canth2 6947  canth2g 6948
[Suppes] p. 97Definition 3brsdom2 6918  df-sdom 6799  dfsdom2 6917
[Suppes] p. 97Theorem 21(i)sdomirr 6931
[Suppes] p. 97Theorem 22(i)domnsym 6920
[Suppes] p. 97Theorem 21(ii)sdomnsym 6919
[Suppes] p. 97Theorem 22(ii)domsdomtr 6929
[Suppes] p. 97Theorem 22(iv)brdom2 6824
[Suppes] p. 97Theorem 21(iii)sdomtr 6932
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6927
[Suppes] p. 98Exercise 4fundmen 6867  fundmeng 6868
[Suppes] p. 98Exercise 6xpdom3 6893
[Suppes] p. 98Exercise 11sdomentr 6928
[Suppes] p. 104Theorem 37fofi 7075
[Suppes] p. 104Theorem 38pwfi 7084
[Suppes] p. 105Theorem 40pwfi 7084
[Suppes] p. 111Axiom for cardinal numberscarden 8106
[Suppes] p. 130Definition 3df-tr 4054
[Suppes] p. 132Theorem 9ssonuni 4515
[Suppes] p. 134Definition 6df-suc 4335
[Suppes] p. 136Theorem Schema 22findes 4623  finds 4619  finds1 4622  finds2 4621
[Suppes] p. 151Theorem 42isfinite 7286  isfinite2 7048  isfiniteg 7050  unbnn 7046
[Suppes] p. 162Definition 5df-ltnq 8475  df-ltpq 8467
[Suppes] p. 197Theorem Schema 4tfindes 4590  tfinds 4587  tfinds2 4591
[Suppes] p. 209Theorem 18oaord1 6482
[Suppes] p. 209Theorem 21oaword2 6484
[Suppes] p. 211Theorem 25oaass 6492
[Suppes] p. 225Definition 8iscard2 7542
[Suppes] p. 227Theorem 56ondomon 8118
[Suppes] p. 228Theorem 59harcard 7544
[Suppes] p. 228Definition 12(i)aleph0 7626
[Suppes] p. 228Theorem Schema 61onintss 4379
[Suppes] p. 228Theorem Schema 62onminesb 4526  onminsb 4527
[Suppes] p. 229Theorem 64alephval2 8127
[Suppes] p. 229Theorem 65alephcard 7630
[Suppes] p. 229Theorem 66alephord2i 7637
[Suppes] p. 229Theorem 67alephnbtwn 7631
[Suppes] p. 229Definition 12df-aleph 7506
[Suppes] p. 242Theorem 6weth 8055
[Suppes] p. 242Theorem 8entric 8112
[Suppes] p. 242Theorem 9carden 8106
[TakeutiZaring] p. 8Axiom 1ax-ext 2237
[TakeutiZaring] p. 13Definition 4.5df-cleq 2249
[TakeutiZaring] p. 13Proposition 4.6df-clel 2252
[TakeutiZaring] p. 13Proposition 4.9cvjust 2251
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2273
[TakeutiZaring] p. 14Definition 4.16df-oprab 5761
[TakeutiZaring] p. 14Proposition 4.14ru 2934
[TakeutiZaring] p. 15Axiom 2zfpair 4150
[TakeutiZaring] p. 15Exercise 1elpr 3599  elpr2 3600  elprg 3598
[TakeutiZaring] p. 15Exercise 2elsn 3596  elsnc 3604  elsnc2 3610  elsnc2g 3609  elsncg 3603
[TakeutiZaring] p. 15Exercise 3elop 4176
[TakeutiZaring] p. 15Exercise 4sneq 3592  sneqr 3721
[TakeutiZaring] p. 15Definition 5.1dfpr2 3597  dfsn2 3595
[TakeutiZaring] p. 16Axiom 3uniex 4453
[TakeutiZaring] p. 16Exercise 6opth 4182
[TakeutiZaring] p. 16Exercise 7opex 4174
[TakeutiZaring] p. 16Exercise 8rext 4160
[TakeutiZaring] p. 16Corollary 5.8unex 4455  unexg 4458
[TakeutiZaring] p. 16Definition 5.3dftp2 3620
[TakeutiZaring] p. 16Definition 5.5df-uni 3769
[TakeutiZaring] p. 16Definition 5.6df-in 3101  df-un 3099
[TakeutiZaring] p. 16Proposition 5.7unipr 3782  uniprg 3783
[TakeutiZaring] p. 17Axiom 4pwex 4131  pwexg 4132
[TakeutiZaring] p. 17Exercise 1eltp 3619
[TakeutiZaring] p. 17Exercise 5elsuc 4398  elsucg 4396  sstr2 3128
[TakeutiZaring] p. 17Exercise 6uncom 3261
[TakeutiZaring] p. 17Exercise 7incom 3303
[TakeutiZaring] p. 17Exercise 8unass 3274
[TakeutiZaring] p. 17Exercise 9inass 3321
[TakeutiZaring] p. 17Exercise 10indi 3357
[TakeutiZaring] p. 17Exercise 11undi 3358
[TakeutiZaring] p. 17Definition 5.9df-pss 3110  dfss2 3111
[TakeutiZaring] p. 17Definition 5.10df-pw 3568
[TakeutiZaring] p. 18Exercise 7unss2 3288
[TakeutiZaring] p. 18Exercise 9df-ss 3108  sseqin2 3330
[TakeutiZaring] p. 18Exercise 10ssid 3139
[TakeutiZaring] p. 18Exercise 12inss1 3331  inss2 3332
[TakeutiZaring] p. 18Exercise 13nss 3178
[TakeutiZaring] p. 18Exercise 15unieq 3777
[TakeutiZaring] p. 18Exercise 18sspwb 4161  sspwimp 27707  sspwimpALT 27714  sspwimpALT2 27718  sspwimpcf 27709
[TakeutiZaring] p. 18Exercise 19pweqb 4168
[TakeutiZaring] p. 19Axiom 5ax-rep 4071
[TakeutiZaring] p. 20Definitiondf-rab 2523
[TakeutiZaring] p. 20Corollary 5.160ex 4090
[TakeutiZaring] p. 20Definition 5.12df-dif 3097
[TakeutiZaring] p. 20Definition 5.14dfnul2 3399
[TakeutiZaring] p. 20Proposition 5.15difid 3464  difidALT 3465
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3406  n0f 3405  neq0 3407
[TakeutiZaring] p. 21Axiom 6zfreg 7242
[TakeutiZaring] p. 21Axiom 6'zfregs 7347
[TakeutiZaring] p. 21Theorem 5.22setind 7352
[TakeutiZaring] p. 21Definition 5.20df-v 2742
[TakeutiZaring] p. 21Proposition 5.21vprc 4092
[TakeutiZaring] p. 22Exercise 10ss 3425
[TakeutiZaring] p. 22Exercise 3ssex 4098  ssexg 4100
[TakeutiZaring] p. 22Exercise 4inex1 4095
[TakeutiZaring] p. 22Exercise 5ruv 7247
[TakeutiZaring] p. 22Exercise 6elirr 7245
[TakeutiZaring] p. 22Exercise 7ssdif0 3455
[TakeutiZaring] p. 22Exercise 11difdif 3244
[TakeutiZaring] p. 22Exercise 13undif3 3371  undif3VD 27671
[TakeutiZaring] p. 22Exercise 14difss 3245
[TakeutiZaring] p. 22Exercise 15sscon 3252
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2520
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2521
[TakeutiZaring] p. 23Proposition 6.2xpex 4754  xpexg 4753  xpexgALT 5969
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4641
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5215
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5348  fun11 5218
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5171  svrelfun 5216
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4820
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4822
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4646
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4647
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4643
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5081  dfrel2 5077
[TakeutiZaring] p. 25Exercise 3xpss 4746
[TakeutiZaring] p. 25Exercise 5relun 4755
[TakeutiZaring] p. 25Exercise 6reluni 4761
[TakeutiZaring] p. 25Exercise 9inxp 4771
[TakeutiZaring] p. 25Exercise 12relres 4936
[TakeutiZaring] p. 25Exercise 13opelres 4913  opelresg 4915
[TakeutiZaring] p. 25Exercise 14dmres 4929
[TakeutiZaring] p. 25Exercise 15resss 4932
[TakeutiZaring] p. 25Exercise 17resabs1 4937
[TakeutiZaring] p. 25Exercise 18funres 5196
[TakeutiZaring] p. 25Exercise 24relco 5123
[TakeutiZaring] p. 25Exercise 29funco 5195
[TakeutiZaring] p. 25Exercise 30f1co 5349
[TakeutiZaring] p. 26Definition 6.10eu2 2141
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4654  fv3 5439
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5161  cnvexg 5160
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4894  dmexg 4892
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4895  rnexg 4893
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 26991
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 26992
[TakeutiZaring] p. 27Corollary 6.13fvex 5437
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5442  tz6.12 5443  tz6.12c 5446
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5445  tz6.12i 5447
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4649
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4650
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4652  wfo 4636
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4651  wf1 4635
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4653  wf1o 4637
[TakeutiZaring] p. 28Exercise 4eqfnfv 5521  eqfnfv2 5522  eqfnfv2f 5525
[TakeutiZaring] p. 28Exercise 5fvco 5494
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5640  fnexALT 5641
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5636  resfunexgALT 5637
[TakeutiZaring] p. 29Exercise 9funimaex 5233  funimaexg 5232
[TakeutiZaring] p. 29Definition 6.18df-br 3964
[TakeutiZaring] p. 30Definition 6.21dffr2 4295  dffr3 4998  eliniseg 4995  iniseg 4997
[TakeutiZaring] p. 30Definition 6.22df-eprel 4242
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4308  fr3nr 4508  frirr 4307
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4289
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4510
[TakeutiZaring] p. 31Exercise 1frss 4297
[TakeutiZaring] p. 31Exercise 4wess 4317
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23539  tz6.26i 23540  wefrc 4324  wereu2 4327
[TakeutiZaring] p. 32Theorem 6.27wfi 23541  wfii 23542
[TakeutiZaring] p. 32Definition 6.28df-isom 4655
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5725
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5726
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5732
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5733
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5734
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5738
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5745
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5747
[TakeutiZaring] p. 35Notationwtr 4053
[TakeutiZaring] p. 35Theorem 7.2trelpss 26993  tz7.2 4314
[TakeutiZaring] p. 35Definition 7.1dftr3 4057
[TakeutiZaring] p. 36Proposition 7.4ordwe 4342
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4350
[TakeutiZaring] p. 36Proposition 7.6ordelord 4351  ordelordALT 27317  ordelordALTVD 27656
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4357  ordelssne 4356
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4355
[TakeutiZaring] p. 37Proposition 7.9ordin 4359
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4517
[TakeutiZaring] p. 38Corollary 7.15ordsson 4518
[TakeutiZaring] p. 38Definition 7.11df-on 4333
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4361
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27330  ordon 4511
[TakeutiZaring] p. 38Proposition 7.13onprc 4513
[TakeutiZaring] p. 39Theorem 7.17tfi 4581
[TakeutiZaring] p. 40Exercise 3ontr2 4376
[TakeutiZaring] p. 40Exercise 7dftr2 4055
[TakeutiZaring] p. 40Exercise 9onssmin 4525
[TakeutiZaring] p. 40Exercise 11unon 4559
[TakeutiZaring] p. 40Exercise 12ordun 4431
[TakeutiZaring] p. 40Exercise 14ordequn 4430
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4514
[TakeutiZaring] p. 40Proposition 7.20elssuni 3796
[TakeutiZaring] p. 41Definition 7.22df-suc 4335
[TakeutiZaring] p. 41Proposition 7.23sssucid 4406  sucidg 4407
[TakeutiZaring] p. 41Proposition 7.24suceloni 4541
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4421  ordnbtwn 4420
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4556
[TakeutiZaring] p. 42Exercise 1df-lim 4334
[TakeutiZaring] p. 42Exercise 4omssnlim 4607
[TakeutiZaring] p. 42Exercise 7ssnlim 4611
[TakeutiZaring] p. 42Exercise 8onsucssi 4569  ordelsuc 4548
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4550
[TakeutiZaring] p. 42Definition 7.27nlimon 4579
[TakeutiZaring] p. 42Definition 7.28dfom2 4595
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4612
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4613
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4614
[TakeutiZaring] p. 43Remarkomon 4604
[TakeutiZaring] p. 43Axiom 7inf3 7269  omex 7277
[TakeutiZaring] p. 43Theorem 7.32ordom 4602
[TakeutiZaring] p. 43Corollary 7.31find 4618
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4615
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4616
[TakeutiZaring] p. 44Exercise 1limomss 4598
[TakeutiZaring] p. 44Exercise 2int0 3817  trint0 4070
[TakeutiZaring] p. 44Exercise 4intss1 3818
[TakeutiZaring] p. 44Exercise 5intex 4109
[TakeutiZaring] p. 44Exercise 6oninton 4528
[TakeutiZaring] p. 44Exercise 11ordintdif 4378
[TakeutiZaring] p. 44Definition 7.35df-int 3804
[TakeutiZaring] p. 44Proposition 7.34noinfep 7293
[TakeutiZaring] p. 45Exercise 4onint 4523
[TakeutiZaring] p. 47Lemma 1tfrlem1 6324
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6346
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6347
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6348
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6352  tz7.44-2 6353  tz7.44-3 6354
[TakeutiZaring] p. 50Exercise 1smogt 6317
[TakeutiZaring] p. 50Exercise 3smoiso 6312
[TakeutiZaring] p. 50Definition 7.46df-smo 6296
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6390  tz7.49c 6391
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6388
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6387
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6389
[TakeutiZaring] p. 53Proposition 7.532eu5 2200
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7572
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7573
[TakeutiZaring] p. 56Definition 8.1oalim 6464  oasuc 6456
[TakeutiZaring] p. 57Remarktfindsg 4588
[TakeutiZaring] p. 57Proposition 8.2oacl 6467
[TakeutiZaring] p. 57Proposition 8.3oa0 6448  oa0r 6470
[TakeutiZaring] p. 57Proposition 8.16omcl 6468
[TakeutiZaring] p. 58Corollary 8.5oacan 6479
[TakeutiZaring] p. 58Proposition 8.4nnaord 6550  nnaordi 6549  oaord 6478  oaordi 6477
[TakeutiZaring] p. 59Proposition 8.6iunss2 3888  uniss2 3799
[TakeutiZaring] p. 59Proposition 8.7oawordri 6481
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6486  oawordex 6488
[TakeutiZaring] p. 59Proposition 8.9nnacl 6542
[TakeutiZaring] p. 59Proposition 8.10oaabs 6575
[TakeutiZaring] p. 60Remarkoancom 7285
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6491
[TakeutiZaring] p. 62Exercise 1nnarcl 6547
[TakeutiZaring] p. 62Exercise 5oaword1 6483
[TakeutiZaring] p. 62Definition 8.15om0 6449  om0x 6451  omlim 6465  omsuc 6458
[TakeutiZaring] p. 63Proposition 8.17nnecl 6544  nnmcl 6543
[TakeutiZaring] p. 63Proposition 8.19nnmord 6563  nnmordi 6562  omord 6499  omordi 6497
[TakeutiZaring] p. 63Proposition 8.20omcan 6500
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6567  omwordri 6503
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6471
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6473  om1r 6474
[TakeutiZaring] p. 64Proposition 8.22om00 6506
[TakeutiZaring] p. 64Proposition 8.23omordlim 6508
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6509
[TakeutiZaring] p. 64Proposition 8.25odi 6510
[TakeutiZaring] p. 65Theorem 8.26omass 6511
[TakeutiZaring] p. 67Definition 8.30nnesuc 6539  oe0 6454  oelim 6466  oesuc 6459  onesuc 6462
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6452
[TakeutiZaring] p. 67Proposition 8.32oen0 6517
[TakeutiZaring] p. 67Proposition 8.33oeordi 6518
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6453
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6476
[TakeutiZaring] p. 68Corollary 8.34oeord 6519
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6525
[TakeutiZaring] p. 68Proposition 8.35oewordri 6523
[TakeutiZaring] p. 68Proposition 8.37oeworde 6524
[TakeutiZaring] p. 69Proposition 8.41oeoa 6528
[TakeutiZaring] p. 70Proposition 8.42oeoe 6530
[TakeutiZaring] p. 73Theorem 9.1trcl 7343  tz9.1 7344
[TakeutiZaring] p. 76Definition 9.9df-r1 7369  r10 7373  r1lim 7377  r1limg 7376  r1suc 7375  r1sucg 7374
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7385  r1ord2 7386  r1ordg 7383
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7395
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7420  tz9.13 7396  tz9.13g 7397
[TakeutiZaring] p. 79Definition 9.14df-rank 7370  rankval 7421  rankvalb 7402  rankvalg 7422
[TakeutiZaring] p. 79Proposition 9.16rankel 7444  rankelb 7429
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7458  rankval3 7445  rankval3b 7431
[TakeutiZaring] p. 79Proposition 9.18rankonid 7434
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7400
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7439  rankr1c 7426  rankr1g 7437
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7440
[TakeutiZaring] p. 80Exercise 1rankss 7454  rankssb 7453
[TakeutiZaring] p. 80Exercise 2unbndrank 7447
[TakeutiZaring] p. 80Proposition 9.19bndrank 7446
[TakeutiZaring] p. 83Axiom of Choiceac4 8035  dfac3 7681
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7590  numth 8032  numth2 8031
[TakeutiZaring] p. 85Definition 10.4cardval 8101
[TakeutiZaring] p. 85Proposition 10.5cardid 8102  cardid2 7519
[TakeutiZaring] p. 85Proposition 10.9oncard 7526
[TakeutiZaring] p. 85Proposition 10.10carden 8106
[TakeutiZaring] p. 85Proposition 10.11cardidm 7525
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7510
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7531
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7523
[TakeutiZaring] p. 87Proposition 10.15pwen 6967
[TakeutiZaring] p. 88Exercise 1en0 6857
[TakeutiZaring] p. 88Exercise 7infensuc 6972
[TakeutiZaring] p. 89Exercise 10omxpen 6897
[TakeutiZaring] p. 90Corollary 10.23cardnn 7529
[TakeutiZaring] p. 90Definition 10.27alephiso 7658
[TakeutiZaring] p. 90Proposition 10.20nneneq 6977
[TakeutiZaring] p. 90Proposition 10.22onomeneq 6983
[TakeutiZaring] p. 90Proposition 10.26alephprc 7659
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6982
[TakeutiZaring] p. 91Exercise 2alephle 7648
[TakeutiZaring] p. 91Exercise 3aleph0 7626
[TakeutiZaring] p. 91Exercise 4cardlim 7538
[TakeutiZaring] p. 91Exercise 7infpss 7776
[TakeutiZaring] p. 91Exercise 8infcntss 7063
[TakeutiZaring] p. 91Definition 10.29df-fin 6800  isfi 6818
[TakeutiZaring] p. 92Proposition 10.32onfin 6984
[TakeutiZaring] p. 92Proposition 10.34imadomg 8092
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6890
[TakeutiZaring] p. 93Proposition 10.35fodomb 8084
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7748  unxpdom 7003
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7540  cardsdomelir 7539
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7005
[TakeutiZaring] p. 94Proposition 10.39infxpen 7575
[TakeutiZaring] p. 95Definition 10.42df-map 6707
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8117  infxpidm2 7577
[TakeutiZaring] p. 95Proposition 10.41infcda 7767  infxp 7774  infxpg 24426
[TakeutiZaring] p. 96Proposition 10.44pw2en 6902  pw2f1o 6900
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6960
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8047
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8042  ac6s5 8051
[TakeutiZaring] p. 98Theorem 10.47unidom 8098
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8099  uniimadomf 8100
[TakeutiZaring] p. 100Definition 11.1cfcof 7833
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7828
[TakeutiZaring] p. 102Exercise 1cfle 7813
[TakeutiZaring] p. 102Exercise 2cf0 7810
[TakeutiZaring] p. 102Exercise 3cfsuc 7816
[TakeutiZaring] p. 102Exercise 4cfom 7823
[TakeutiZaring] p. 102Proposition 11.9coftr 7832
[TakeutiZaring] p. 103Theorem 11.15alephreg 8137
[TakeutiZaring] p. 103Proposition 11.11cardcf 7811
[TakeutiZaring] p. 103Proposition 11.13alephsing 7835
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7657
[TakeutiZaring] p. 104Proposition 11.16carduniima 7656
[TakeutiZaring] p. 104Proposition 11.18alephfp 7668  alephfp2 7669
[TakeutiZaring] p. 106Theorem 11.20gchina 8254
[TakeutiZaring] p. 106Theorem 11.21mappwen 7672
[TakeutiZaring] p. 107Theorem 11.26konigth 8124
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8138
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8139
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20761  equid 1818  equid1 1820  equidALT 1819
[Tarski] p. 69Lemma 7equcomi-o 1823  equcomi 1822
[Tarski] p. 70Lemma 14a4im 1868  a4ime 1869
[Tarski] p. 70Lemma 16ax-11 1624  ax-11o 1941  ax11i 1833
[Tarski] p. 70Lemmas 16 and 17sb6 1993
[Tarski] p. 75Axiom B8ax-9v 1632
[Tarski] p. 75Scheme B7ax9vax9 28288
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1628
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1625  ax-14 1626
[Truss] p. 114Theorem 5.18ruc 12448
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 501
[WhiteheadRussell] p. 96Axiom *1.3olc 375
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 377
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 510
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 817
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 162
[WhiteheadRussell] p. 100Theorem *2.02ax-1 7
[WhiteheadRussell] p. 100Theorem *2.03con2 110
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 78
[WhiteheadRussell] p. 100Theorem *2.05imim2 51
[WhiteheadRussell] p. 100Theorem *2.06imim1 72
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 408
[WhiteheadRussell] p. 101Theorem *2.06barbara 2213  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 387
[WhiteheadRussell] p. 101Theorem *2.08id 21  id1 22
[WhiteheadRussell] p. 101Theorem *2.11exmid 406
[WhiteheadRussell] p. 101Theorem *2.12notnot1 116
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 409
[WhiteheadRussell] p. 102Theorem *2.14notnot2 106  notnot2ALT2 27716
[WhiteheadRussell] p. 102Theorem *2.15con1 122
[WhiteheadRussell] p. 103Theorem *2.16con3 128  con3th 929
[WhiteheadRussell] p. 103Theorem *2.17ax-3 9
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 104
[WhiteheadRussell] p. 104Theorem *2.2orc 376
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 558
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 102
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 103
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 395
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 858
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 37
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 513
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 514
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 819
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 820
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 818
[WhiteheadRussell] p. 105Definition *2.33df-3or 940
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 561
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 559
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 560
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 49
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 388
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 389
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 146
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 164
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 390
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 391
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 392
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 147
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 149
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 364
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 365
[WhiteheadRussell] p. 107Theorem *2.55orel1 373
[WhiteheadRussell] p. 107Theorem *2.56orel2 374
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 165
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 400
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 766
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 767
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 166
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 393  pm2.67 394
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 148
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 399
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 826
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 401
[WhiteheadRussell] p. 108Theorem *2.69looinv 176
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 821
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 822
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 825
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 824
[WhiteheadRussell] p. 108Theorem *2.77ax-2 8
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 827
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 828
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 73
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 829
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 96
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 486
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 436  pm3.2im 139
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 487
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 488
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 489
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 490
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 437
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 438
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 857
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 573
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 433
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 434
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 445  simplim 145
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 449  simprim 144
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 571
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 572
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 565
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 546
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 544
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 545
[WhiteheadRussell] p. 113Theorem *3.44jao 500  pm3.44 499
[WhiteheadRussell] p. 113Theorem *3.47prth 557
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 835
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 810
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 809
[WhiteheadRussell] p. 116Theorem *4.1con34b 285
[WhiteheadRussell] p. 117Theorem *4.2biid 229
[WhiteheadRussell] p. 117Theorem *4.11notbi 288
[WhiteheadRussell] p. 117Theorem *4.12con2bi 320
[WhiteheadRussell] p. 117Theorem *4.13notnot 284
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 564
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 567
[WhiteheadRussell] p. 117Theorem *4.21bicom 193
[WhiteheadRussell] p. 117Theorem *4.22biantr 902  bitr 692  wl-bitr 24260
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 627
[WhiteheadRussell] p. 117Theorem *4.25oridm 502  pm4.25 503
[WhiteheadRussell] p. 118Theorem *4.3ancom 439
[WhiteheadRussell] p. 118Theorem *4.4andi 842
[WhiteheadRussell] p. 118Theorem *4.31orcom 378
[WhiteheadRussell] p. 118Theorem *4.32anass 633
[WhiteheadRussell] p. 118Theorem *4.33orass 512
[WhiteheadRussell] p. 118Theorem *4.36anbi1 690
[WhiteheadRussell] p. 118Theorem *4.37orbi1 689
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 847
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 846
[WhiteheadRussell] p. 118Definition *4.34df-3an 941
[WhiteheadRussell] p. 119Theorem *4.41ordi 837
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 931
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 898
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 563
[WhiteheadRussell] p. 119Theorem *4.45orabs 831  pm4.45 672  pm4.45im 547
[WhiteheadRussell] p. 120Theorem *4.5anor 477
[WhiteheadRussell] p. 120Theorem *4.6imor 403
[WhiteheadRussell] p. 120Theorem *4.7anclb 532
[WhiteheadRussell] p. 120Theorem *4.51ianor 476
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 479
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 480
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 481
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 482
[WhiteheadRussell] p. 120Theorem *4.56ioran 478  pm4.56 483
[WhiteheadRussell] p. 120Theorem *4.57oran 484  pm4.57 485
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 417
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 410
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 412
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 363
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 418
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 411
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 419
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 614  pm4.71d 618  pm4.71i 616  pm4.71r 615  pm4.71rd 619  pm4.71ri 617
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 851
[WhiteheadRussell] p. 121Theorem *4.73iba 491
[WhiteheadRussell] p. 121Theorem *4.74biorf 396
[WhiteheadRussell] p. 121Theorem *4.76jcab 836  pm4.76 841
[WhiteheadRussell] p. 121Theorem *4.77jaob 761  pm4.77 765
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 568
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 569
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 356
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 357
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 899
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 900
[WhiteheadRussell] p. 122Theorem *4.84imbi1 315
[WhiteheadRussell] p. 122Theorem *4.85imbi2 316
[WhiteheadRussell] p. 122Theorem *4.86bibi1 319  wl-bibi1 24253
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 352  impexp 435  pm4.87 570
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 833
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 859
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 860
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 862
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 861
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 864
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 865
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 863
[WhiteheadRussell] p. 124Theorem *5.18nbbn 349  pm5.18 347
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 351
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 834
[WhiteheadRussell] p. 124Theorem *5.22xor 866
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 868
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 869
[WhiteheadRussell] p. 124Theorem *5.25dfor2 402
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 695
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 353
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 328
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 883
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 905
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 574
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 620
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 853
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 874
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 854
[WhiteheadRussell] p. 125Theorem *5.41imdi 354  pm5.41 355
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 533
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 882
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 774
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 875
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 872
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 696
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 894
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 895
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 907
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 332
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 237
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 908
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 26885
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26886
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26887
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26888
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26889
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26890
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26891
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26892
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26893
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26894
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26896
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26897
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26898
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26895
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26901
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2078
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26902
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26903
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26904
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26905
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26906
[WhiteheadRussell] p. 162Theorem *11.322alim 26907
[WhiteheadRussell] p. 162Theorem *11.332albi 26908
[WhiteheadRussell] p. 162Theorem *11.342exim 26909
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26911
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26910
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26913
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26914
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26912
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26915
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26916
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26917
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2025  pm11.53g 24295
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26918
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26923
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26919
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26920
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26921
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26922
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26927
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26924
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26925
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26926
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26928
[WhiteheadRussell] p. 175Definition *14.02df-eu 2121
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26940  pm13.13b 26941
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26942
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2491
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2492
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2859
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26948
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26949
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26943
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27334  pm13.193 26944
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26945
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26946
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26947
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26954
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26953
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26952
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2987
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26955  pm14.122b 26956  pm14.122c 26957
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26958  pm14.123b 26959  pm14.123c 26960
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26962
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26961
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26963
[WhiteheadRussell] p. 190Theorem *14.22iota4 6208
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26964
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6209
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 26965
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 26967
[WhiteheadRussell] p. 192Theorem *14.26eupick 2179  eupickbi 2182  sbaniota 26968
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 26966
[WhiteheadRussell] p. 192Theorem *14.271eubi 26969
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 26970
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4654
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7566  pm54.43lem 7565
[Young] p. 141Definition of operator orderingleop2 22629
[Young] p. 142Example 12.2(i)0leop 22635  idleop 22636
[vandenDries] p. 42Lemma 61irrapx1 26245
[vandenDries] p. 43Theorem 62pellex 26252  pellexlem1 26246

This page was last updated on 19-May-2017.
Copyright terms: Public domain