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 13620
[Adamek] p. 29Proposition 3.14(1)invinv 13634
[Adamek] p. 29Proposition 3.14(2)invco 13635  isoco 13637
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25557
[AitkenIBCG] p. 3Definition 2df-angtrg 25553  df-trcng 25556
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25429  df-ig2 25428
[AitkenIBG] p. 2Definition 4df-li 25444
[AitkenIBG] p. 3Definition 5df-col 25458
[AitkenIBG] p. 3Definition 6df-con2 25463
[AitkenIBG] p. 3Proposition 4isconcl5a 25468  isconcl5ab 25469  isconcl6a 25470  isconcl6ab 25471
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25476
[AitkenIBG] p. 4Exercise 5tpne 25442
[AitkenIBG] p. 4Definition 8df-seg2 25498
[AitkenIBG] p. 4Definition 10df-sside 25530
[AitkenIBG] p. 4Definition 11df-ray2 25519
[AitkenIBG] p. 10Definition 17df-angle 25525
[AitkenIBG] p. 15Definition 23df-triangle 25527
[AitkenIBG] p. 15Definition 24df-cnvx 25546
[AitkenNG] p. 2Definition 1df-slices 25560
[AitkenNG] p. 2Definition 2df-Cut 25562
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25564
[AitkenNG] p. 4Definition 5df-crcl 25566
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18179  df-nmoo 21283
[AkhiezerGlazman] p. 64Theoremhmopidmch 22693  hmopidmchi 22691
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22741  pjcmul2i 22742
[AkhiezerGlazman] p. 72Theoremcnvunop 22458  unoplin 22460
[AkhiezerGlazman] p. 72Equation 2unopadj 22459  unopadj2 22478
[AkhiezerGlazman] p. 73Theoremelunop2 22553  lnopunii 22552
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22626
[Apostol] p. 18Theorem I.1addcan 8964  addcan2d 8984  addcan2i 8974  addcand 8983  addcani 8973
[Apostol] p. 18Theorem I.2negeu 9010
[Apostol] p. 18Theorem I.3negsub 9063  negsubd 9131  negsubi 9092
[Apostol] p. 18Theorem I.4negneg 9065  negnegd 9116  negnegi 9084
[Apostol] p. 18Theorem I.5subdi 9181  subdid 9203  subdii 9196  subdir 9182  subdird 9204  subdiri 9197
[Apostol] p. 18Theorem I.6mul01 8959  mul01d 8979  mul01i 8970  mul02 8958  mul02d 8978  mul02i 8969
[Apostol] p. 18Theorem I.7mulcan 9373  mulcan2d 9370  mulcand 9369  mulcani 9375
[Apostol] p. 18Theorem I.8receu 9381
[Apostol] p. 18Theorem I.9divrec 9408  divrecd 9507  divreci 9473  divreczi 9466
[Apostol] p. 18Theorem I.10recrec 9425  recreci 9460
[Apostol] p. 18Theorem I.11mul0or 9376  mul0ord 9386  mul0ori 9384
[Apostol] p. 18Theorem I.12mul2neg 9187  mul2negd 9202  mul2negi 9195  mulneg1 9184  mulneg1d 9200  mulneg1i 9193
[Apostol] p. 18Theorem I.13divadddiv 9443  divadddivd 9548  divadddivi 9490
[Apostol] p. 18Theorem I.14divmuldiv 9428  divmuldivd 9545  divmuldivi 9488
[Apostol] p. 18Theorem I.15divdivdiv 9429  divdivdivd 9551  divdivdivi 9491
[Apostol] p. 20Axiom 7rpaddcl 10341  rpaddcld 10372  rpmulcl 10342  rpmulcld 10373
[Apostol] p. 20Axiom 8rpneg 10350
[Apostol] p. 20Axiom 90nrp 10351
[Apostol] p. 20Theorem I.17lttri 8913
[Apostol] p. 20Theorem I.18ltadd1d 9333  ltadd1dd 9351  ltadd1i 9295
[Apostol] p. 20Theorem I.19ltmul1 9574  ltmul1a 9573  ltmul1i 9643  ltmul1ii 9653  ltmul2 9575  ltmul2d 10395  ltmul2dd 10409  ltmul2i 9646
[Apostol] p. 20Theorem I.20msqgt0 9262  msqgt0d 9308  msqgt0i 9278
[Apostol] p. 20Theorem I.210lt1 9264
[Apostol] p. 20Theorem I.23lt0neg1 9248  lt0neg1d 9310  ltneg 9242  ltnegd 9318  ltnegi 9285
[Apostol] p. 20Theorem I.25lt2add 9227  lt2addd 9362  lt2addi 9303
[Apostol] p. 20Definition of positive numbersdf-rp 10322
[Apostol] p. 21Exercise 4recgt0 9568  recgt0d 9659  recgt0i 9629  recgt0ii 9630
[Apostol] p. 22Definition of integersdf-z 9992
[Apostol] p. 22Definition of positive integersdfnn3 9728
[Apostol] p. 22Definition of rationalsdf-q 10284
[Apostol] p. 24Theorem I.26supeu 7173
[Apostol] p. 26Theorem I.28nnunb 9928
[Apostol] p. 26Theorem I.29arch 9929
[Apostol] p. 28Exercise 2btwnz 10081
[Apostol] p. 28Exercise 3nnrecl 9930
[Apostol] p. 28Exercise 4rebtwnz 10282
[Apostol] p. 28Exercise 5zbtwnre 10281
[Apostol] p. 28Exercise 6qbtwnre 10492
[Apostol] p. 28Exercise 10(a)zneo 10061
[Apostol] p. 29Theorem I.35msqsqrd 11887  resqrth 11706  sqrth 11813  sqrthi 11819  sqsqrd 11886
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9717
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10251
[Apostol] p. 361Remarkcrreczi 11192
[Apostol] p. 363Remarkabsgt0i 11847
[Apostol] p. 363Exampleabssubd 11900  abssubi 11851
[Baer] p. 40Property (b)mapdord 30995
[Baer] p. 40Property (c)mapd11 30996
[Baer] p. 40Property (e)mapdin 31019  mapdlsm 31021
[Baer] p. 40Property (f)mapd0 31022
[Baer] p. 40Definition of projectivitydf-mapd 30982  mapd1o 31005
[Baer] p. 41Property (g)mapdat 31024
[Baer] p. 44Part (1)mapdpg 31063
[Baer] p. 45Part (2)hdmap1eq 31159  mapdheq 31085  mapdheq2 31086  mapdheq2biN 31087
[Baer] p. 45Part (3)baerlem3 31070
[Baer] p. 46Part (4)mapdheq4 31089  mapdheq4lem 31088
[Baer] p. 46Part (5)baerlem5a 31071  baerlem5abmN 31075  baerlem5amN 31073  baerlem5b 31072  baerlem5bmN 31074
[Baer] p. 47Part (6)hdmap1l6 31179  hdmap1l6a 31167  hdmap1l6e 31172  hdmap1l6f 31173  hdmap1l6g 31174  hdmap1l6lem1 31165  hdmap1l6lem2 31166  hdmap1p6N 31180  mapdh6N 31104  mapdh6aN 31092  mapdh6eN 31097  mapdh6fN 31098  mapdh6gN 31099  mapdh6lem1N 31090  mapdh6lem2N 31091
[Baer] p. 48Part 9hdmapval 31188
[Baer] p. 48Part 10hdmap10 31200
[Baer] p. 48Part 11hdmapadd 31203
[Baer] p. 48Part (6)hdmap1l6h 31175  mapdh6hN 31100
[Baer] p. 48Part (7)mapdh75cN 31110  mapdh75d 31111  mapdh75e 31109  mapdh75fN 31112  mapdh7cN 31106  mapdh7dN 31107  mapdh7eN 31105  mapdh7fN 31108
[Baer] p. 48Part (8)mapdh8 31146  mapdh8a 31132  mapdh8aa 31133  mapdh8ab 31134  mapdh8ac 31135  mapdh8ad 31136  mapdh8b 31137  mapdh8c 31138  mapdh8d 31140  mapdh8d0N 31139  mapdh8e 31141  mapdh8fN 31142  mapdh8g 31143  mapdh8i 31144  mapdh8j 31145
[Baer] p. 48Part (9)mapdh9a 31147
[Baer] p. 48Equation 10mapdhvmap 31126
[Baer] p. 49Part 12hdmap11 31208  hdmapeq0 31204  hdmapf1oN 31225  hdmapneg 31206  hdmaprnN 31224  hdmaprnlem1N 31209  hdmaprnlem3N 31210  hdmaprnlem3uN 31211  hdmaprnlem4N 31213  hdmaprnlem6N 31214  hdmaprnlem7N 31215  hdmaprnlem8N 31216  hdmaprnlem9N 31217  hdmapsub 31207
[Baer] p. 49Part 14hdmap14lem1 31228  hdmap14lem10 31237  hdmap14lem1a 31226  hdmap14lem2N 31229  hdmap14lem2a 31227  hdmap14lem3 31230  hdmap14lem8 31235  hdmap14lem9 31236
[Baer] p. 50Part 14hdmap14lem11 31238  hdmap14lem12 31239  hdmap14lem13 31240  hdmap14lem14 31241  hdmap14lem15 31242  hgmapval 31247
[Baer] p. 50Part 15hgmapadd 31254  hgmapmul 31255  hgmaprnlem2N 31257  hgmapvs 31251
[Baer] p. 50Part 16hgmaprnN 31261
[Baer] p. 110Lemma 1hdmapip0com 31277
[Baer] p. 110Line 27hdmapinvlem1 31278
[Baer] p. 110Line 28hdmapinvlem2 31279
[Baer] p. 110Line 30hdmapinvlem3 31280
[Baer] p. 110Part 1.2hdmapglem5 31282  hgmapvv 31286
[Baer] p. 110Proposition 1hdmapinvlem4 31281
[Baer] p. 111Line 10hgmapvvlem1 31283
[Baer] p. 111Line 15hdmapg 31290  hdmapglem7 31289
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2122
[BellMachover] p. 460Notationdf-mo 2123
[BellMachover] p. 460Definitionmo3 2149
[BellMachover] p. 461Axiom Extax-ext 2239
[BellMachover] p. 462Theorem 1.1bm1.1 2243
[BellMachover] p. 463Axiom Repaxrep5 4110
[BellMachover] p. 463Scheme Sepaxsep 4114
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4118
[BellMachover] p. 466Axiom Powaxpow3 4163
[BellMachover] p. 466Axiom Unionaxun2 4486
[BellMachover] p. 468Definitiondf-ord 4367
[BellMachover] p. 469Theorem 2.2(i)ordirr 4382
[BellMachover] p. 469Theorem 2.2(iii)onelon 4389
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4384
[BellMachover] p. 471Definition of Ndf-om 4629
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4569
[BellMachover] p. 471Definition of Limdf-lim 4369
[BellMachover] p. 472Axiom Infzfinf2 7311
[BellMachover] p. 473Theorem 2.8limom 4643
[BellMachover] p. 477Equation 3.1df-r1 7404
[BellMachover] p. 478Definitionrankval2 7458
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7422  r1ord3g 7419
[BellMachover] p. 480Axiom Regzfreg2 7278
[BellMachover] p. 488Axiom ACac5 8072  dfac4 7717
[BellMachover] p. 490Definition of alephalephval3 7705
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28676
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22893
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22935  chirredi 22934
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22923
[Beran] p. 3Definition of joinsshjval3 21893
[Beran] p. 39Theorem 2.3(i)cmcm2 22155  cmcm2i 22132  cmcm2ii 22137  cmt2N 28607
[Beran] p. 40Theorem 2.3(iii)lecm 22156  lecmi 22141  lecmii 22142
[Beran] p. 45Theorem 3.4cmcmlem 22130
[Beran] p. 49Theorem 4.2cm2j 22159  cm2ji 22164  cm2mi 22165
[Beran] p. 95Definitiondf-sh 21746  issh2 21748
[Beran] p. 95Lemma 3.1(S5)his5 21625
[Beran] p. 95Lemma 3.1(S6)his6 21638
[Beran] p. 95Lemma 3.1(S7)his7 21629
[Beran] p. 95Lemma 3.2(S8)ho01i 22368
[Beran] p. 95Lemma 3.2(S9)hoeq1 22370
[Beran] p. 95Lemma 3.2(S10)ho02i 22369
[Beran] p. 95Lemma 3.2(S11)hoeq2 22371
[Beran] p. 95Postulate (S1)ax-his1 21621  his1i 21639
[Beran] p. 95Postulate (S2)ax-his2 21622
[Beran] p. 95Postulate (S3)ax-his3 21623
[Beran] p. 95Postulate (S4)ax-his4 21624
[Beran] p. 96Definition of normdf-hnorm 21508  dfhnorm2 21661  normval 21663
[Beran] p. 96Definition for Cauchy sequencehcau 21723
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21513
[Beran] p. 96Definition of complete subspaceisch3 21781
[Beran] p. 96Definition of convergedf-hlim 21512  hlimi 21727
[Beran] p. 97Theorem 3.3(i)norm-i-i 21672  norm-i 21668
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21676  norm-ii 21677  normlem0 21648  normlem1 21649  normlem2 21650  normlem3 21651  normlem4 21652  normlem5 21653  normlem6 21654  normlem7 21655  normlem7tALT 21658
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21678  norm-iii 21679
[Beran] p. 98Remark 3.4bcs 21720  bcsiALT 21718  bcsiHIL 21719
[Beran] p. 98Remark 3.4(B)normlem9at 21660  normpar 21694  normpari 21693
[Beran] p. 98Remark 3.4(C)normpyc 21685  normpyth 21684  normpythi 21681
[Beran] p. 99Remarklnfn0 22587  lnfn0i 22582  lnop0 22506  lnop0i 22510
[Beran] p. 99Theorem 3.5(i)nmcexi 22566  nmcfnex 22593  nmcfnexi 22591  nmcopex 22569  nmcopexi 22567
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22594  nmcfnlbi 22592  nmcoplb 22570  nmcoplbi 22568
[Beran] p. 99Theorem 3.5(iii)lnfncon 22596  lnfnconi 22595  lnopcon 22575  lnopconi 22574
[Beran] p. 100Lemma 3.6normpar2i 21695
[Beran] p. 101Lemma 3.6norm3adifi 21692  norm3adifii 21687  norm3dif 21689  norm3difi 21686
[Beran] p. 102Theorem 3.7(i)chocunii 21840  pjhth 21932  pjhtheu 21933  pjpjhth 21964  pjpjhthi 21965  pjth 18765
[Beran] p. 102Theorem 3.7(ii)ococ 21945  ococi 21944
[Beran] p. 103Remark 3.8nlelchi 22601
[Beran] p. 104Theorem 3.9riesz3i 22602  riesz4 22604  riesz4i 22603
[Beran] p. 104Theorem 3.10cnlnadj 22619  cnlnadjeu 22618  cnlnadjeui 22617  cnlnadji 22616  cnlnadjlem1 22607  nmopadjlei 22628
[Beran] p. 106Theorem 3.11(i)adjeq0 22631
[Beran] p. 106Theorem 3.11(v)nmopadji 22630
[Beran] p. 106Theorem 3.11(ii)adjmul 22632
[Beran] p. 106Theorem 3.11(iv)adjadj 22476
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22642  nmopcoadji 22641
[Beran] p. 106Theorem 3.11(iii)adjadd 22633
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22643
[Beran] p. 106Theorem 3.11(viii)adjcoi 22640  pjadj2coi 22744  pjadjcoi 22701
[Beran] p. 107Definitiondf-ch 21761  isch2 21763
[Beran] p. 107Remark 3.12choccl 21845  isch3 21781  occl 21843  ocsh 21822  shoccl 21844  shocsh 21823
[Beran] p. 107Remark 3.12(B)ococin 21947
[Beran] p. 108Theorem 3.13chintcl 21871
[Beran] p. 109Property (i)pjadj2 22727  pjadj3 22728  pjadji 22224  pjadjii 22213
[Beran] p. 109Property (ii)pjidmco 22721  pjidmcoi 22717  pjidmi 22212
[Beran] p. 110Definition of projector orderingpjordi 22713
[Beran] p. 111Remarkho0val 22290  pjch1 22209
[Beran] p. 111Definitiondf-hfmul 22274  df-hfsum 22273  df-hodif 22272  df-homul 22271  df-hosum 22270
[Beran] p. 111Lemma 4.4(i)pjo 22210
[Beran] p. 111Lemma 4.4(ii)pjch 22233  pjchi 21971
[Beran] p. 111Lemma 4.4(iii)pjoc2 21978  pjoc2i 21977
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22219
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22705  pjssmii 22220
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22704
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22703
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22708
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22706  pjssge0ii 22221
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22707  pjdifnormii 22222
[BourbakiEns] p. Proposition 8fcof1 5731  fcofo 5732
[BourbakiFVR] p. Definition 1isder 25074
[BourbakiTop1] p. Remarkxnegmnf 10503  xnegpnf 10502
[BourbakiTop1] p. Remark rexneg 10504
[BourbakiTop1] p. Theoremneiss 16808
[BourbakiTop1] p. Axiom GT'tgpsubcn 17735
[BourbakiTop1] p. Example 1snfil 17521
[BourbakiTop1] p. Example 2neifil 17537
[BourbakiTop1] p. Definitionistgp 17722
[BourbakiTop1] p. Propositioncnpco 16958  ishmeo 17412  neips 16812
[BourbakiTop1] p. Definition 1filintn0 17518
[BourbakiTop1] p. Proposition 9cnpflf2 17657
[BourbakiTop1] p. Theorem 1 (d)iscncl 16960
[BourbakiTop1] p. Proposition Vissnei2 16815
[BourbakiTop1] p. Definition C'''df-cmp 17076
[BourbakiTop1] p. Proposition Viiinnei 16824
[BourbakiTop1] p. Proposition Vivneissex 16826
[BourbakiTop1] p. Proposition Viiielnei 16810  ssnei 16809
[BourbakiTop1] p. Remark below def. 1filn0 17519
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17503
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17520
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27148  stoweid 27147
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27146
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27085  stoweidlem10 27094  stoweidlem14 27098  stoweidlem15 27099  stoweidlem35 27119  stoweidlem36 27120  stoweidlem37 27121  stoweidlem38 27122  stoweidlem40 27124  stoweidlem41 27125  stoweidlem43 27127  stoweidlem44 27128  stoweidlem46 27130  stoweidlem5 27089  stoweidlem50 27134  stoweidlem52 27136  stoweidlem53 27137  stoweidlem55 27139  stoweidlem56 27140
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27107  stoweidlem24 27108  stoweidlem27 27111  stoweidlem28 27112  stoweidlem30 27114
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27129  stoweidlem49 27133  stoweidlem7 27091
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27115  stoweidlem39 27123  stoweidlem42 27126  stoweidlem48 27132  stoweidlem51 27135  stoweidlem54 27138  stoweidlem57 27141  stoweidlem58 27142
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27109
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27118
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27101
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27143
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27144
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27102
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27095  stoweidlem26 27110
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27097
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27145
[ChoquetDD] p. 2Definition of mappingdf-mpt 4053
[Cohen] p. 301Remarkrelogoprlem 19906
[Cohen] p. 301Property 2relogmul 19907  relogmuld 19938
[Cohen] p. 301Property 3relogdiv 19908  relogdivd 19939
[Cohen] p. 301Property 4relogexp 19911
[Cohen] p. 301Property 1alog1 19901
[Cohen] p. 301Property 1bloge 19902
[Cohn] p. 81Section II.5acsdomd 14246  acsinfd 14245  acsinfdimd 14247  acsmap2d 14244  acsmapd 14243
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10931
[Crawley] p. 1Definition of posetdf-poset 14042
[Crawley] p. 107Theorem 13.2hlsupr 28742
[Crawley] p. 110Theorem 13.3arglem1N 29546  dalaw 29242
[Crawley] p. 111Theorem 13.4hlathil 31321
[Crawley] p. 111Definition of set Wdf-watsN 29346
[Crawley] p. 111Definition of dilationdf-dilN 29462  df-ldil 29460  isldil 29466
[Crawley] p. 111Definition of translationdf-ltrn 29461  df-trnN 29463  isltrn 29475  ltrnu 29477
[Crawley] p. 112Lemma Acdlema1N 29147  cdlema2N 29148  exatleN 28760
[Crawley] p. 112Lemma B1cvrat 28832  cdlemb 29150  cdlemb2 29397  cdlemb3 29962  idltrn 29506  l1cvat 28412  lhpat 29399  lhpat2 29401  lshpat 28413  ltrnel 29495  ltrnmw 29507
[Crawley] p. 112Lemma Ccdlemc1 29547  cdlemc2 29548  ltrnnidn 29530  trlat 29525  trljat1 29522  trljat2 29523  trljat3 29524  trlne 29541  trlnidat 29529  trlnle 29542
[Crawley] p. 112Definition of automorphismdf-pautN 29347
[Crawley] p. 113Lemma Ccdlemc 29553  cdlemc3 29549  cdlemc4 29550
[Crawley] p. 113Lemma Dcdlemd 29563  cdlemd1 29554  cdlemd2 29555  cdlemd3 29556  cdlemd4 29557  cdlemd5 29558  cdlemd6 29559  cdlemd7 29560  cdlemd8 29561  cdlemd9 29562  cdleme31sde 29741  cdleme31se 29738  cdleme31se2 29739  cdleme31snd 29742  cdleme32a 29797  cdleme32b 29798  cdleme32c 29799  cdleme32d 29800  cdleme32e 29801  cdleme32f 29802  cdleme32fva 29793  cdleme32fva1 29794  cdleme32fvcl 29796  cdleme32le 29803  cdleme48fv 29855  cdleme4gfv 29863  cdleme50eq 29897  cdleme50f 29898  cdleme50f1 29899  cdleme50f1o 29902  cdleme50laut 29903  cdleme50ldil 29904  cdleme50lebi 29896  cdleme50rn 29901  cdleme50rnlem 29900  cdlemeg49le 29867  cdlemeg49lebilem 29895
[Crawley] p. 113Lemma Ecdleme 29916  cdleme00a 29565  cdleme01N 29577  cdleme02N 29578  cdleme0a 29567  cdleme0aa 29566  cdleme0b 29568  cdleme0c 29569  cdleme0cp 29570  cdleme0cq 29571  cdleme0dN 29572  cdleme0e 29573  cdleme0ex1N 29579  cdleme0ex2N 29580  cdleme0fN 29574  cdleme0gN 29575  cdleme0moN 29581  cdleme1 29583  cdleme10 29610  cdleme10tN 29614  cdleme11 29626  cdleme11a 29616  cdleme11c 29617  cdleme11dN 29618  cdleme11e 29619  cdleme11fN 29620  cdleme11g 29621  cdleme11h 29622  cdleme11j 29623  cdleme11k 29624  cdleme11l 29625  cdleme12 29627  cdleme13 29628  cdleme14 29629  cdleme15 29634  cdleme15a 29630  cdleme15b 29631  cdleme15c 29632  cdleme15d 29633  cdleme16 29641  cdleme16aN 29615  cdleme16b 29635  cdleme16c 29636  cdleme16d 29637  cdleme16e 29638  cdleme16f 29639  cdleme16g 29640  cdleme19a 29659  cdleme19b 29660  cdleme19c 29661  cdleme19d 29662  cdleme19e 29663  cdleme19f 29664  cdleme1b 29582  cdleme2 29584  cdleme20aN 29665  cdleme20bN 29666  cdleme20c 29667  cdleme20d 29668  cdleme20e 29669  cdleme20f 29670  cdleme20g 29671  cdleme20h 29672  cdleme20i 29673  cdleme20j 29674  cdleme20k 29675  cdleme20l 29678  cdleme20l1 29676  cdleme20l2 29677  cdleme20m 29679  cdleme20y 29658  cdleme20zN 29657  cdleme21 29693  cdleme21d 29686  cdleme21e 29687  cdleme22a 29696  cdleme22aa 29695  cdleme22b 29697  cdleme22cN 29698  cdleme22d 29699  cdleme22e 29700  cdleme22eALTN 29701  cdleme22f 29702  cdleme22f2 29703  cdleme22g 29704  cdleme23a 29705  cdleme23b 29706  cdleme23c 29707  cdleme26e 29715  cdleme26eALTN 29717  cdleme26ee 29716  cdleme26f 29719  cdleme26f2 29721  cdleme26f2ALTN 29720  cdleme26fALTN 29718  cdleme27N 29725  cdleme27a 29723  cdleme27cl 29722  cdleme28c 29728  cdleme3 29593  cdleme30a 29734  cdleme31fv 29746  cdleme31fv1 29747  cdleme31fv1s 29748  cdleme31fv2 29749  cdleme31id 29750  cdleme31sc 29740  cdleme31sdnN 29743  cdleme31sn 29736  cdleme31sn1 29737  cdleme31sn1c 29744  cdleme31sn2 29745  cdleme31so 29735  cdleme35a 29804  cdleme35b 29806  cdleme35c 29807  cdleme35d 29808  cdleme35e 29809  cdleme35f 29810  cdleme35fnpq 29805  cdleme35g 29811  cdleme35h 29812  cdleme35h2 29813  cdleme35sn2aw 29814  cdleme35sn3a 29815  cdleme36a 29816  cdleme36m 29817  cdleme37m 29818  cdleme38m 29819  cdleme38n 29820  cdleme39a 29821  cdleme39n 29822  cdleme3b 29585  cdleme3c 29586  cdleme3d 29587  cdleme3e 29588  cdleme3fN 29589  cdleme3fa 29592  cdleme3g 29590  cdleme3h 29591  cdleme4 29594  cdleme40m 29823  cdleme40n 29824  cdleme40v 29825  cdleme40w 29826  cdleme41fva11 29833  cdleme41sn3aw 29830  cdleme41sn4aw 29831  cdleme41snaw 29832  cdleme42a 29827  cdleme42b 29834  cdleme42c 29828  cdleme42d 29829  cdleme42e 29835  cdleme42f 29836  cdleme42g 29837  cdleme42h 29838  cdleme42i 29839  cdleme42k 29840  cdleme42ke 29841  cdleme42keg 29842  cdleme42mN 29843  cdleme42mgN 29844  cdleme43aN 29845  cdleme43bN 29846  cdleme43cN 29847  cdleme43dN 29848  cdleme5 29596  cdleme50ex 29915  cdleme50ltrn 29913  cdleme51finvN 29912  cdleme51finvfvN 29911  cdleme51finvtrN 29914  cdleme6 29597  cdleme7 29605  cdleme7a 29599  cdleme7aa 29598  cdleme7b 29600  cdleme7c 29601  cdleme7d 29602  cdleme7e 29603  cdleme7ga 29604  cdleme8 29606  cdleme8tN 29611  cdleme9 29609  cdleme9a 29607  cdleme9b 29608  cdleme9tN 29613  cdleme9taN 29612  cdlemeda 29654  cdlemedb 29653  cdlemednpq 29655  cdlemednuN 29656  cdlemefr27cl 29759  cdlemefr32fva1 29766  cdlemefr32fvaN 29765  cdlemefrs32fva 29756  cdlemefrs32fva1 29757  cdlemefs27cl 29769  cdlemefs32fva1 29779  cdlemefs32fvaN 29778  cdlemesner 29652  cdlemeulpq 29576
[Crawley] p. 114Lemma E4atex 29432  4atexlem7 29431  cdleme0nex 29646  cdleme17a 29642  cdleme17c 29644  cdleme17d 29854  cdleme17d1 29645  cdleme17d2 29851  cdleme18a 29647  cdleme18b 29648  cdleme18c 29649  cdleme18d 29651  cdleme4a 29595
[Crawley] p. 115Lemma Ecdleme21a 29681  cdleme21at 29684  cdleme21b 29682  cdleme21c 29683  cdleme21ct 29685  cdleme21f 29688  cdleme21g 29689  cdleme21h 29690  cdleme21i 29691  cdleme22gb 29650
[Crawley] p. 116Lemma Fcdlemf 29919  cdlemf1 29917  cdlemf2 29918
[Crawley] p. 116Lemma Gcdlemftr1 29923  cdlemg16 30013  cdlemg28 30060  cdlemg28a 30049  cdlemg28b 30059  cdlemg3a 29953  cdlemg42 30085  cdlemg43 30086  cdlemg44 30089  cdlemg44a 30087  cdlemg46 30091  cdlemg47 30092  cdlemg9 29990  ltrnco 30075  ltrncom 30094  tgrpabl 30107  trlco 30083
[Crawley] p. 116Definition of Gdf-tgrp 30099
[Crawley] p. 117Lemma Gcdlemg17 30033  cdlemg17b 30018
[Crawley] p. 117Definition of Edf-edring-rN 30112  df-edring 30113
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30116
[Crawley] p. 118Remarktendopltp 30136
[Crawley] p. 118Lemma Hcdlemh 30173  cdlemh1 30171  cdlemh2 30172
[Crawley] p. 118Lemma Icdlemi 30176  cdlemi1 30174  cdlemi2 30175
[Crawley] p. 118Lemma Jcdlemj1 30177  cdlemj2 30178  cdlemj3 30179  tendocan 30180
[Crawley] p. 118Lemma Kcdlemk 30330  cdlemk1 30187  cdlemk10 30199  cdlemk11 30205  cdlemk11t 30302  cdlemk11ta 30285  cdlemk11tb 30287  cdlemk11tc 30301  cdlemk11u-2N 30245  cdlemk11u 30227  cdlemk12 30206  cdlemk12u-2N 30246  cdlemk12u 30228  cdlemk13-2N 30232  cdlemk13 30208  cdlemk14-2N 30234  cdlemk14 30210  cdlemk15-2N 30235  cdlemk15 30211  cdlemk16-2N 30236  cdlemk16 30213  cdlemk16a 30212  cdlemk17-2N 30237  cdlemk17 30214  cdlemk18-2N 30242  cdlemk18-3N 30256  cdlemk18 30224  cdlemk19-2N 30243  cdlemk19 30225  cdlemk19u 30326  cdlemk1u 30215  cdlemk2 30188  cdlemk20-2N 30248  cdlemk20 30230  cdlemk21-2N 30247  cdlemk21N 30229  cdlemk22-3 30257  cdlemk22 30249  cdlemk23-3 30258  cdlemk24-3 30259  cdlemk25-3 30260  cdlemk26-3 30262  cdlemk26b-3 30261  cdlemk27-3 30263  cdlemk28-3 30264  cdlemk29-3 30267  cdlemk3 30189  cdlemk30 30250  cdlemk31 30252  cdlemk32 30253  cdlemk33N 30265  cdlemk34 30266  cdlemk35 30268  cdlemk36 30269  cdlemk37 30270  cdlemk38 30271  cdlemk39 30272  cdlemk39u 30324  cdlemk4 30190  cdlemk41 30276  cdlemk42 30297  cdlemk42yN 30300  cdlemk43N 30319  cdlemk45 30303  cdlemk46 30304  cdlemk47 30305  cdlemk48 30306  cdlemk49 30307  cdlemk5 30192  cdlemk50 30308  cdlemk51 30309  cdlemk52 30310  cdlemk53 30313  cdlemk54 30314  cdlemk55 30317  cdlemk55u 30322  cdlemk56 30327  cdlemk5a 30191  cdlemk5auN 30216  cdlemk5u 30217  cdlemk6 30193  cdlemk6u 30218  cdlemk7 30204  cdlemk7u-2N 30244  cdlemk7u 30226  cdlemk8 30194  cdlemk9 30195  cdlemk9bN 30196  cdlemki 30197  cdlemkid 30292  cdlemkj-2N 30238  cdlemkj 30219  cdlemksat 30202  cdlemksel 30201  cdlemksv 30200  cdlemksv2 30203  cdlemkuat 30222  cdlemkuel-2N 30240  cdlemkuel-3 30254  cdlemkuel 30221  cdlemkuv-2N 30239  cdlemkuv2-2 30241  cdlemkuv2-3N 30255  cdlemkuv2 30223  cdlemkuvN 30220  cdlemkvcl 30198  cdlemky 30282  cdlemkyyN 30318  tendoex 30331
[Crawley] p. 120Remarkdva1dim 30341
[Crawley] p. 120Lemma Lcdleml1N 30332  cdleml2N 30333  cdleml3N 30334  cdleml4N 30335  cdleml5N 30336  cdleml6 30337  cdleml7 30338  cdleml8 30339  cdleml9 30340  dia1dim 30418
[Crawley] p. 120Lemma Mdia11N 30405  diaf11N 30406  dialss 30403  diaord 30404  dibf11N 30518  djajN 30494
[Crawley] p. 120Definition of isomorphism mapdiaval 30389
[Crawley] p. 121Lemma Mcdlemm10N 30475  dia2dimlem1 30421  dia2dimlem2 30422  dia2dimlem3 30423  dia2dimlem4 30424  dia2dimlem5 30425  diaf1oN 30487  diarnN 30486  dvheveccl 30469  dvhopN 30473
[Crawley] p. 121Lemma Ncdlemn 30569  cdlemn10 30563  cdlemn11 30568  cdlemn11a 30564  cdlemn11b 30565  cdlemn11c 30566  cdlemn11pre 30567  cdlemn2 30552  cdlemn2a 30553  cdlemn3 30554  cdlemn4 30555  cdlemn4a 30556  cdlemn5 30558  cdlemn5pre 30557  cdlemn6 30559  cdlemn7 30560  cdlemn8 30561  cdlemn9 30562  diclspsn 30551
[Crawley] p. 121Definition of phi(q)df-dic 30530
[Crawley] p. 122Lemma Ndih11 30622  dihf11 30624  dihjust 30574  dihjustlem 30573  dihord 30621  dihord1 30575  dihord10 30580  dihord11b 30579  dihord11c 30581  dihord2 30584  dihord2a 30576  dihord2b 30577  dihord2cN 30578  dihord2pre 30582  dihord2pre2 30583  dihordlem6 30570  dihordlem7 30571  dihordlem7b 30572
[Crawley] p. 122Definition of isomorphism mapdihffval 30587  dihfval 30588  dihval 30589
[Eisenberg] p. 67Definition 5.3df-dif 3130
[Eisenberg] p. 82Definition 6.3dfom3 7316
[Eisenberg] p. 125Definition 8.21df-map 6742
[Eisenberg] p. 216Example 13.2(4)omenps 7323
[Eisenberg] p. 310Theorem 19.8cardprc 7581
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8145
[Enderton] p. 18Axiom of Empty Setaxnul 4122
[Enderton] p. 19Definitiondf-tp 3622
[Enderton] p. 26Exercise 5unissb 3831
[Enderton] p. 26Exercise 10pwel 4197
[Enderton] p. 28Exercise 7(b)pwun 4274
[Enderton] p. 30Theorem "Distributive laws"iinin1 3947  iinin2 3946  iinun2 3942  iunin1 3941  iunin2 3940
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3945  iundif2 3943
[Enderton] p. 32Exercise 20unineq 3394
[Enderton] p. 33Exercise 23iinuni 3959
[Enderton] p. 33Exercise 25iununi 3960
[Enderton] p. 33Exercise 24(a)iinpw 3964
[Enderton] p. 33Exercise 24(b)iunpw 4542  iunpwss 3965
[Enderton] p. 36Definitionopthwiener 4240
[Enderton] p. 38Exercise 6(a)unipw 4196
[Enderton] p. 38Exercise 6(b)pwuni 4178
[Enderton] p. 41Lemma 3Dopeluu 4498  rnex 4930  rnexg 4928
[Enderton] p. 41Exercise 8dmuni 4876  rnuni 5080
[Enderton] p. 42Definition of a functiondffun7 5219  dffun8 5220
[Enderton] p. 43Definition of function valuefunfv2 5521
[Enderton] p. 43Definition of single-rootedfuncnv 5248
[Enderton] p. 44Definition (d)dfima2 5002  dfima3 5003
[Enderton] p. 47Theorem 3Hfvco2 5528
[Enderton] p. 49Axiom of Choice (first form)ac7 8068  ac7g 8069  df-ac 7711  dfac2 7725  dfac2a 7724  dfac3 7716  dfac7 7726
[Enderton] p. 50Theorem 3K(a)imauni 5706
[Enderton] p. 52Definitiondf-map 6742
[Enderton] p. 53Exercise 21coass 5178
[Enderton] p. 53Exercise 27dmco 5168
[Enderton] p. 53Exercise 14(a)funin 5257
[Enderton] p. 53Exercise 22(a)imass2 5037
[Enderton] p. 54Remarkixpf 6806  ixpssmap 6818
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6786
[Enderton] p. 55Axiom of Choice (second form)ac9 8078  ac9s 8088
[Enderton] p. 56Theorem 3Merref 6648
[Enderton] p. 57Lemma 3Nerthi 6674
[Enderton] p. 57Definitiondf-ec 6630
[Enderton] p. 58Definitiondf-qs 6634
[Enderton] p. 60Theorem 3Qth3q 6735  th3qcor 6734  th3qlem1 6732  th3qlem2 6733
[Enderton] p. 61Exercise 35df-ec 6630
[Enderton] p. 65Exercise 56(a)dmun 4873
[Enderton] p. 68Definition of successordf-suc 4370
[Enderton] p. 71Definitiondf-tr 4088  dftr4 4092
[Enderton] p. 72Theorem 4Eunisuc 4440
[Enderton] p. 73Exercise 6unisuc 4440
[Enderton] p. 73Exercise 5(a)truni 4101
[Enderton] p. 73Exercise 5(b)trint 4102  trintALT 27707
[Enderton] p. 79Theorem 4I(A1)nna0 6570
[Enderton] p. 79Theorem 4I(A2)nnasuc 6572  onasuc 6495
[Enderton] p. 79Definition of operation valuedf-ov 5795
[Enderton] p. 80Theorem 4J(A1)nnm0 6571
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6573  onmsuc 6496
[Enderton] p. 81Theorem 4K(1)nnaass 6588
[Enderton] p. 81Theorem 4K(2)nna0r 6575  nnacom 6583
[Enderton] p. 81Theorem 4K(3)nndi 6589
[Enderton] p. 81Theorem 4K(4)nnmass 6590
[Enderton] p. 81Theorem 4K(5)nnmcom 6592
[Enderton] p. 82Exercise 16nnm0r 6576  nnmsucr 6591
[Enderton] p. 88Exercise 23nnaordex 6604
[Enderton] p. 129Definitiondf-en 6832
[Enderton] p. 132Theorem 6B(b)canth 6260
[Enderton] p. 133Exercise 1xpomen 7611
[Enderton] p. 133Exercise 2qnnen 12454
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7013
[Enderton] p. 135Corollary 6Cphp3 7015
[Enderton] p. 136Corollary 6Enneneq 7012
[Enderton] p. 136Corollary 6D(a)pssinf 7041
[Enderton] p. 136Corollary 6D(b)ominf 7043
[Enderton] p. 137Lemma 6Fpssnn 7049
[Enderton] p. 138Corollary 6Gssfi 7051
[Enderton] p. 139Theorem 6H(c)mapen 6993
[Enderton] p. 142Theorem 6I(3)xpcdaen 7777
[Enderton] p. 142Theorem 6I(4)mapcdaen 7778
[Enderton] p. 143Theorem 6Jcda0en 7773  cda1en 7769
[Enderton] p. 144Exercise 13iunfi 7112  unifi 7113  unifi2 7114
[Enderton] p. 144Corollary 6Kundif2 3505  unfi 7092  unfi2 7094
[Enderton] p. 145Figure 38ffoss 5443
[Enderton] p. 145Definitiondf-dom 6833
[Enderton] p. 146Example 1domen 6843  domeng 6844
[Enderton] p. 146Example 3nndomo 7022  nnsdom 7322  nnsdomg 7084
[Enderton] p. 149Theorem 6L(a)cdadom2 7781
[Enderton] p. 149Theorem 6L(c)mapdom1 6994  xpdom1 6929  xpdom1g 6927  xpdom2g 6926
[Enderton] p. 149Theorem 6L(d)mapdom2 7000
[Enderton] p. 151Theorem 6Mzorn 8102  zorng 8099
[Enderton] p. 151Theorem 6M(4)ac8 8087  dfac5 7723
[Enderton] p. 159Theorem 6Qunictb 8165
[Enderton] p. 164Exampleinfdif 7803
[Enderton] p. 168Definitiondf-po 4286
[Enderton] p. 192Theorem 7M(a)oneli 4472
[Enderton] p. 192Theorem 7M(b)ontr1 4410
[Enderton] p. 192Theorem 7M(c)onirri 4471
[Enderton] p. 193Corollary 7N(b)0elon 4417
[Enderton] p. 193Corollary 7N(c)onsuci 4601
[Enderton] p. 193Corollary 7N(d)ssonunii 4551
[Enderton] p. 194Remarkonprc 4548
[Enderton] p. 194Exercise 16suc11 4468
[Enderton] p. 197Definitiondf-card 7540
[Enderton] p. 197Theorem 7Pcarden 8141
[Enderton] p. 200Exercise 25tfis 4617
[Enderton] p. 202Lemma 7Tr1tr 7416
[Enderton] p. 202Definitiondf-r1 7404
[Enderton] p. 202Theorem 7Qr1val1 7426
[Enderton] p. 204Theorem 7V(b)rankval4 7507
[Enderton] p. 206Theorem 7X(b)en2lp 7285
[Enderton] p. 207Exercise 30rankpr 7497  rankprb 7491  rankpw 7483  rankpwi 7463  rankuniss 7506
[Enderton] p. 207Exercise 34opthreg 7287
[Enderton] p. 208Exercise 35suc11reg 7288
[Enderton] p. 212Definition of alephalephval3 7705
[Enderton] p. 213Theorem 8A(a)alephord2 7671
[Enderton] p. 213Theorem 8A(b)cardalephex 7685
[Enderton] p. 218Theorem Schema 8Eonfununi 6326
[Enderton] p. 222Definition of kardkarden 7533  kardex 7532
[Enderton] p. 238Theorem 8Roeoa 6563
[Enderton] p. 238Theorem 8Soeoe 6565
[Enderton] p. 240Exercise 25oarec 6528
[Enderton] p. 257Definition of cofinalitycflm 7844
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13506
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13452
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14242  mrieqv2d 13503  mrieqvd 13502
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13507
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13512  mreexexlem2d 13509
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14248  mreexfidimd 13514
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18856
[Fremlin5] p. 213Lemma 565Cauniioovol 18896
[Fremlin5] p. 214Lemma 565Cauniioombl 18906
[FreydScedrov] p. 283Axiom of Infinityax-inf 7307  inf1 7291  inf2 7292
[Gleason] p. 117Proposition 9-2.1df-enq 8503  enqer 8513
[Gleason] p. 117Proposition 9-2.2df-1nq 8508  df-nq 8504
[Gleason] p. 117Proposition 9-2.3df-plpq 8500  df-plq 8506
[Gleason] p. 119Proposition 9-2.4caovmo 5991  df-mpq 8501  df-mq 8507
[Gleason] p. 119Proposition 9-2.5df-rq 8509
[Gleason] p. 119Proposition 9-2.6ltexnq 8567
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8568  ltbtwnnq 8570
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8563
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8564
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8571
[Gleason] p. 121Definition 9-3.1df-np 8573
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8585
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8587
[Gleason] p. 122Definitiondf-1p 8574
[Gleason] p. 122Remark (1)prub 8586
[Gleason] p. 122Lemma 9-3.4prlem934 8625
[Gleason] p. 122Proposition 9-3.2df-ltp 8577
[Gleason] p. 122Proposition 9-3.3ltsopr 8624  psslinpr 8623  supexpr 8646  suplem1pr 8644  suplem2pr 8645
[Gleason] p. 123Proposition 9-3.5addclpr 8610  addclprlem1 8608  addclprlem2 8609  df-plp 8575
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8614
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8613
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8626
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8635  ltexprlem1 8628  ltexprlem2 8629  ltexprlem3 8630  ltexprlem4 8631  ltexprlem5 8632  ltexprlem6 8633  ltexprlem7 8634
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8637  ltaprlem 8636
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8638
[Gleason] p. 124Lemma 9-3.6prlem936 8639
[Gleason] p. 124Proposition 9-3.7df-mp 8576  mulclpr 8612  mulclprlem 8611  reclem2pr 8640
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8621
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8616
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8615
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8620
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8643  reclem3pr 8641  reclem4pr 8642
[Gleason] p. 126Proposition 9-4.1df-enr 8649  df-mpr 8648  df-plpr 8647  enrer 8658
[Gleason] p. 126Proposition 9-4.2df-0r 8654  df-1r 8655  df-nr 8650
[Gleason] p. 126Proposition 9-4.3df-mr 8652  df-plr 8651  negexsr 8692  recexsr 8697  recexsrlem 8693
[Gleason] p. 127Proposition 9-4.4df-ltr 8653
[Gleason] p. 130Proposition 10-1.3creui 9709  creur 9708  cru 9706
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8778  axcnre 8754
[Gleason] p. 132Definition 10-3.1crim 11565  crimd 11682  crimi 11643  crre 11564  crred 11681  crrei 11642
[Gleason] p. 132Definition 10-3.2remim 11567  remimd 11648
[Gleason] p. 133Definition 10.36absval2 11734  absval2d 11892  absval2i 11845
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11591  cjaddd 11670  cjaddi 11638
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11592  cjmuld 11671  cjmuli 11639
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11590  cjcjd 11649  cjcji 11621
[Gleason] p. 133Proposition 10-3.4(f)cjre 11589  cjreb 11573  cjrebd 11652  cjrebi 11624  cjred 11676  rere 11572  rereb 11570  rerebd 11651  rerebi 11623  rered 11674
[Gleason] p. 133Proposition 10-3.4(h)addcj 11598  addcjd 11662  addcji 11633
[Gleason] p. 133Proposition 10-3.7(a)absval 11688
[Gleason] p. 133Proposition 10-3.7(b)abscj 11729  abscjd 11897  abscji 11849
[Gleason] p. 133Proposition 10-3.7(c)abs00 11739  abs00d 11893  abs00i 11846  absne0d 11894
[Gleason] p. 133Proposition 10-3.7(d)releabs 11770  releabsd 11898  releabsi 11850
[Gleason] p. 133Proposition 10-3.7(f)absmul 11744  absmuld 11901  absmuli 11852
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11732  sqabsaddi 11853
[Gleason] p. 133Proposition 10-3.7(h)abstri 11779  abstrid 11903  abstrii 11856
[Gleason] p. 134Definition 10-4.1df-exp 11071  exp0 11074  expp1 11076  expp1d 11212
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19988  cxpaddd 20026  expadd 11110  expaddd 11213  expaddz 11112
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19997  cxpmuld 20043  expmul 11113  expmuld 11214  expmulz 11114
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19994  mulcxpd 20037  mulexp 11107  mulexpd 11226  mulexpz 11108
[Gleason] p. 140Exercise 1znnen 12453
[Gleason] p. 141Definition 11-2.1fzval 10750
[Gleason] p. 168Proposition 12-2.1(a)climadd 12070  rlimadd 12081  rlimdiv 12084
[Gleason] p. 168Proposition 12-2.1(b)climsub 12072  rlimsub 12082
[Gleason] p. 168Proposition 12-2.1(c)climmul 12071  rlimmul 12083
[Gleason] p. 171Corollary 12-2.2climmulc2 12075
[Gleason] p. 172Corollary 12-2.5climrecl 12022
[Gleason] p. 172Proposition 12-2.4(c)climabs 12042  climcj 12043  climim 12045  climre 12044  rlimabs 12047  rlimcj 12048  rlimim 12050  rlimre 12049
[Gleason] p. 173Definition 12-3.1df-ltxr 8840  df-xr 8839  ltxr 10424
[Gleason] p. 175Definition 12-4.1df-limsup 11910  limsupval 11913
[Gleason] p. 180Theorem 12-5.1climsup 12108
[Gleason] p. 180Theorem 12-5.3caucvg 12116  caucvgb 12117  caucvgr 12113  climcau 12109
[Gleason] p. 182Exercise 3cvgcmp 12239
[Gleason] p. 182Exercise 4cvgrat 12301
[Gleason] p. 195Theorem 13-2.12abs1m 11784
[Gleason] p. 217Lemma 13-4.1btwnzge0 10919
[Gleason] p. 223Definition 14-1.1df-met 16336
[Gleason] p. 223Definition 14-1.1(a)met0 17870  xmet0 17869
[Gleason] p. 223Definition 14-1.1(b)metgt0 17885
[Gleason] p. 223Definition 14-1.1(c)metsym 17876
[Gleason] p. 223Definition 14-1.1(d)mettri 17878  mstri 17977  xmettri 17877  xmstri 17976
[Gleason] p. 225Definition 14-1.5xpsmet 17908
[Gleason] p. 230Proposition 14-2.6txlm 17304
[Gleason] p. 240Theorem 14-4.3metcnp4 18697
[Gleason] p. 240Proposition 14-4.2metcnp3 18048
[Gleason] p. 243Proposition 14-4.16addcn 18331  addcn2 12032  mulcn 18333  mulcn2 12034  subcn 18332  subcn2 12033
[Gleason] p. 295Remarkbcval3 11285  bcval4 11286
[Gleason] p. 295Equation 2bcpasc 11299
[Gleason] p. 295Definition of binomial coefficientbcval 11283  df-bc 11282
[Gleason] p. 296Remarkbcn0 11289  bcnn 11290
[Gleason] p. 296Theorem 15-2.8binom 12253
[Gleason] p. 308Equation 2ef0 12334
[Gleason] p. 308Equation 3efcj 12335
[Gleason] p. 309Corollary 15-4.3efne0 12339
[Gleason] p. 309Corollary 15-4.4efexp 12343
[Gleason] p. 310Equation 14sinadd 12406
[Gleason] p. 310Equation 15cosadd 12407
[Gleason] p. 311Equation 17sincossq 12418
[Gleason] p. 311Equation 18cosbnd 12423  sinbnd 12422
[Gleason] p. 311Lemma 15-4.7sqeqor 11183  sqeqori 11181
[Gleason] p. 311Definition of pidf-pi 12316
[Godowski] p. 730Equation SFgoeqi 22813
[GodowskiGreechie] p. 249Equation IV3oai 22207
[Gratzer] p. 23Section 0.6df-mre 13450
[Gratzer] p. 27Section 0.6df-mri 13452
[Halmos] p. 31Theorem 17.3riesz1 22605  riesz2 22606
[Halmos] p. 41Definition of Hermitianhmopadj2 22481
[Halmos] p. 42Definition of projector orderingpjordi 22713
[Halmos] p. 43Theorem 26.1elpjhmop 22725  elpjidm 22724  pjnmopi 22688
[Halmos] p. 44Remarkpjinormi 22226  pjinormii 22215
[Halmos] p. 44Theorem 26.2elpjch 22729  pjrn 22246  pjrni 22241  pjvec 22235
[Halmos] p. 44Theorem 26.3pjnorm2 22266
[Halmos] p. 44Theorem 26.4hmopidmpj 22694  hmopidmpji 22692
[Halmos] p. 45Theorem 27.1pjinvari 22731
[Halmos] p. 45Theorem 27.3pjoci 22720  pjocvec 22236
[Halmos] p. 45Theorem 27.4pjorthcoi 22709
[Halmos] p. 48Theorem 29.2pjssposi 22712
[Halmos] p. 48Theorem 29.3pjssdif1i 22715  pjssdif2i 22714
[Halmos] p. 50Definition of spectrumdf-spec 22395
[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 18452  df-phtpy 18431
[Hatcher] p. 26Definitiondf-pco 18465  df-pi1 18468
[Hatcher] p. 26Proposition 1.2phtpcer 18455
[Hatcher] p. 26Proposition 1.3pi1grp 18510
[Herstein] p. 54Exercise 28df-grpo 20818
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14460  grpoideu 20836  mndideu 14337
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14478  grpoinveu 20849
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14497  grpo2inv 20866
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14506  grpoinvop 20868
[Herstein] p. 57Exercise 1isgrp2d 20862  isgrp2i 20863
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22960
[Holland] p. 1520Lemma 5cdj1i 22973  cdj3i 22981  cdj3lem1 22974  cdjreui 22972
[Holland] p. 1524Lemma 7mddmdin0i 22971
[Holland95] p. 13Theorem 3.6hlathil 31321
[Holland95] p. 14Line 15hgmapvs 31251
[Holland95] p. 14Line 16hdmaplkr 31273
[Holland95] p. 14Line 17hdmapellkr 31274
[Holland95] p. 14Line 19hdmapglnm2 31271
[Holland95] p. 14Line 20hdmapip0com 31277
[Holland95] p. 14Theorem 3.6hdmapevec2 31196
[Holland95] p. 14Lines 24 and 25hdmapoc 31291
[Holland95] p. 204Definition of involutiondf-srng 15573
[Holland95] p. 212Definition of subspacedf-psubsp 28859
[Holland95] p. 214Lemma 3.3lclkrlem2v 30885
[Holland95] p. 214Definition 3.2df-lpolN 30838
[Holland95] p. 214Definition of nonsingularpnonsingN 29289
[Holland95] p. 215Lemma 3.3(1)dihoml4 30734  poml4N 29309
[Holland95] p. 215Lemma 3.3(2)dochexmid 30825  pexmidALTN 29334  pexmidN 29325
[Holland95] p. 218Theorem 3.6lclkr 30890
[Holland95] p. 218Definition of dual vector spacedf-ldual 28481  ldualset 28482
[Holland95] p. 222Item 1df-lines 28857  df-pointsN 28858
[Holland95] p. 222Item 2df-polarityN 29259
[Holland95] p. 223Remarkispsubcl2N 29303  omllaw4 28603  pol1N 29266  polcon3N 29273
[Holland95] p. 223Definitiondf-psubclN 29291
[Holland95] p. 223Equation for polaritypolval2N 29262
[Hughes] p. 44Equation 1.21bax-his3 21623
[Hughes] p. 47Definition of projection operatordfpjop 22722
[Hughes] p. 49Equation 1.30eighmre 22503  eigre 22375  eigrei 22374
[Hughes] p. 49Equation 1.31eighmorth 22504  eigorth 22378  eigorthi 22377
[Hughes] p. 137Remark (ii)eigposi 22376
[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 2253
[Jech] p. 42Lemma 6.1alephexp1 8169
[Jech] p. 42Equation 6.1alephadd 8167  alephmul 8168
[Jech] p. 43Lemma 6.2infmap 8166  infmap2 7812
[Jech] p. 71Lemma 9.3jech9.3 7454
[Jech] p. 72Equation 9.3scott0 7524  scottex 7523
[Jech] p. 72Exercise 9.1rankval4 7507
[Jech] p. 72Scheme "Collection Principle"cp 7529
[Jech] p. 78Definition implied by the footnoteopthprc 4724
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26367
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26463
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26464
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26379
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26383
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26384  rmyp1 26385
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26386  rmym1 26387
[JonesMatijasevic] p. 695Equation 2.11rmx0 26377  rmx1 26378  rmxluc 26388
[JonesMatijasevic] p. 695Equation 2.12rmy0 26381  rmy1 26382  rmyluc 26389
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26391
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26392
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26414  jm2.17b 26415  jm2.17c 26416
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26453
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26457
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26448
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26417  jm2.24nn 26413
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26462
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26468  rmygeid 26418
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26480
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[KalishMontague] p. 81Schemes B4 through B8equidK 28152
[KalishMontague] p. 85Lemma 2equidK 28152
[KalishMontague] p. 85Lemma 3equcomiK 28153
[KalishMontague] p. 85Theorem 1equidK 28152
[KalishMontague] p. 86Lemma 5albiiK 28159  alimdK 28160  alimdvK 28161
[KalishMontague] p. 86Lemma 7cbvaliK 28176  cbvalivK 28177
[KalishMontague] p. 86Lemma 9ax4wK 28169  ax4wfK 28168  equidK 28152
[KalishMontague] p. 87Lemma 8a4imK 28166  a4imvK 28167
[Kalmbach] p. 14Definition of latticechabs1 22055  chabs1i 22057  chabs2 22056  chabs2i 22058  chjass 22072  chjassi 22025  latabs1 14155  latabs2 14156
[Kalmbach] p. 15Definition of atomdf-at 22878  ela 22879
[Kalmbach] p. 15Definition of coverscvbr2 22823  cvrval2 28631
[Kalmbach] p. 16Definitiondf-ol 28535  df-oml 28536
[Kalmbach] p. 20Definition of commutescmbr 22123  cmbri 22129  cmtvalN 28568  df-cm 22122  df-cmtN 28534
[Kalmbach] p. 22Remarkomllaw5N 28604  pjoml5 22152  pjoml5i 22127
[Kalmbach] p. 22Definitionpjoml2 22150  pjoml2i 22124
[Kalmbach] p. 22Theorem 2(v)cmcm 22153  cmcmi 22131  cmcmii 22136  cmtcomN 28606
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28602  omlsi 21943  pjoml 21975  pjomli 21974
[Kalmbach] p. 22Definition of OML lawomllaw2N 28601
[Kalmbach] p. 23Remarkcmbr2i 22135  cmcm3 22154  cmcm3i 22133  cmcm3ii 22138  cmcm4i 22134  cmt3N 28608  cmt4N 28609  cmtbr2N 28610
[Kalmbach] p. 23Lemma 3cmbr3 22147  cmbr3i 22139  cmtbr3N 28611
[Kalmbach] p. 25Theorem 5fh1 22157  fh1i 22160  fh2 22158  fh2i 22161  omlfh1N 28615
[Kalmbach] p. 65Remarkchjatom 22897  chslej 22037  chsleji 21997  shslej 21919  shsleji 21909
[Kalmbach] p. 65Proposition 1chocin 22034  chocini 21993  chsupcl 21879  chsupval2 21949  h0elch 21794  helch 21783  hsupval2 21948  ocin 21835  ococss 21832  shococss 21833
[Kalmbach] p. 65Definition of subspace sumshsval 21851
[Kalmbach] p. 66Remarkdf-pjh 21934  pjssmi 22705  pjssmii 22220
[Kalmbach] p. 67Lemma 3osum 22184  osumi 22181
[Kalmbach] p. 67Lemma 4pjci 22740
[Kalmbach] p. 103Exercise 6atmd2 22940
[Kalmbach] p. 103Exercise 12mdsl0 22850
[Kalmbach] p. 140Remarkhatomic 22900  hatomici 22899  hatomistici 22902
[Kalmbach] p. 140Proposition 1atlatmstc 28676
[Kalmbach] p. 140Proposition 1(i)atexch 22921  lsatexch 28400
[Kalmbach] p. 140Proposition 1(ii)chcv1 22895  cvlcvr1 28696  cvr1 28766
[Kalmbach] p. 140Proposition 1(iii)cvexch 22914  cvexchi 22909  cvrexch 28776
[Kalmbach] p. 149Remark 2chrelati 22904  hlrelat 28758  hlrelat5N 28757  lrelat 28371
[Kalmbach] p. 153Exercise 5lsmcv 15856  lsmsatcv 28367  spansncv 22192  spansncvi 22191
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 28386  spansncv2 22833
[Kalmbach] p. 266Definitiondf-st 22751
[Kalmbach2] p. 8Definition of adjointdf-adjh 22389
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8236  fpwwe2 8233
[KanamoriPincus] p. 416Corollary 1.3canth4 8237
[KanamoriPincus] p. 417Corollary 1.6canthp1 8244
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8239
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8241
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8254
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8258  gchxpidm 8259
[KanamoriPincus] p. 419Theorem 2.1gchacg 8262  gchhar 8261
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7810  unxpwdom 7271
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8264
[Kreyszig] p. 3Property M1metcl 17859  xmetcl 17858
[Kreyszig] p. 4Property M2meteq0 17866
[Kreyszig] p. 8Definition 1.1-8dscmet 18057
[Kreyszig] p. 12Equation 5conjmul 9445  muleqadd 9380
[Kreyszig] p. 18Definition 1.3-2mopnval 17946
[Kreyszig] p. 19Remarkmopntopon 17947
[Kreyszig] p. 19Theorem T1mopn0 18006  mopnm 17952
[Kreyszig] p. 19Theorem T2unimopn 18004
[Kreyszig] p. 19Definition of neighborhoodneibl 18009
[Kreyszig] p. 20Definition 1.3-3metcnp2 18050
[Kreyszig] p. 25Definition 1.4-1lmbr 16950  lmmbr 18646  lmmbr2 18647
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17070
[Kreyszig] p. 28Theorem 1.4-5lmcau 18700
[Kreyszig] p. 28Definition 1.4-3iscau 18664  iscmet2 18682
[Kreyszig] p. 30Theorem 1.4-7cmetss 18702
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17149  metelcls 18692
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18693  metcld2 18694
[Kreyszig] p. 51Equation 2clmvneg1 18551  lmodvneg1 15629  nvinv 21157  vcm 21087
[Kreyszig] p. 51Equation 1aclm0vs 18550  lmod0vs 15625  vc0 21085
[Kreyszig] p. 51Equation 1blmodvs0 15626  vcz 21086
[Kreyszig] p. 58Definition 2.2-1imsmet 21220
[Kreyszig] p. 59Equation 1imsdval 21215  imsdval2 21216
[Kreyszig] p. 63Problem 1nvnd 21217
[Kreyszig] p. 64Problem 2nvge0 21200  nvz 21195
[Kreyszig] p. 64Problem 3nvabs 21199
[Kreyszig] p. 91Definition 2.7-1isblo3i 21339
[Kreyszig] p. 92Equation 2df-nmoo 21283
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21345  blocni 21343
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21344
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18601  ipeq0 16504  ipz 21255
[Kreyszig] p. 135Problem 2pythi 21388
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21392
[Kreyszig] p. 144Equation 4supcvg 12276
[Kreyszig] p. 144Theorem 3.3-1minvec 18762  minveco 21423
[Kreyszig] p. 196Definition 3.9-1df-aj 21288
[Kreyszig] p. 247Theorem 4.7-2bcth 18713
[Kreyszig] p. 249Theorem 4.7-3ubth 21412
[Kreyszig] p. 470Definition of positive operator orderingleop 22663  leopg 22662
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22681
[Kreyszig] p. 525Theorem 10.1-1htth 21458
[Kunen] p. 10Axiom 0a9e 1817  axnul 4122
[Kunen] p. 11Axiom 3axnul 4122
[Kunen] p. 12Axiom 6zfrep6 5682
[Kunen] p. 24Definition 10.24mapval 6752  mapvalg 6750
[Kunen] p. 30Lemma 10.20fodom 8117
[Kunen] p. 31Definition 10.24mapex 6746
[Kunen] p. 95Definition 2.1df-r1 7404
[Kunen] p. 97Lemma 2.10r1elss 7446  r1elssi 7445
[Kunen] p. 107Exercise 4rankop 7498  rankopb 7492  rankuni 7503  rankxplim 7517  rankxpsuc 7520
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3889
[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 20780  ex-natded5.2 20779
[Laboreo] p. 16Theorem 5.3ex-natded5.3-2 20783  ex-natded5.3 20782
[Laboreo] p. 18Theorem 5.5ex-natded5.5 20785
[Laboreo] p. 19Theorem 5.7ex-natded5.7-2 20787  ex-natded5.7 20786
[Laboreo] p. 20Theorem 5.8ex-natded5.8-2 20789  ex-natded5.8 20788
[Laboreo] p. 20Theorem 5.13ex-natded5.13-2 20791  ex-natded5.13 20790
[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 20792
[Laboreo] p. 45Theorem 9.20ex-natded9.20-2 20793
[Laboreo] p. 45Theorem 9.26ex-natded9.26-2 20795  ex-natded9.26 20794
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26918
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26913
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26919
[LeBlanc] p. 277Rule R2axnul 4122
[Levy] p. 338Axiomdf-clab 2245  df-clel 2254  df-cleq 2251
[Levy58] p. 2Definition Iisfin1-3 7980
[Levy58] p. 2Definition IIdf-fin2 7880
[Levy58] p. 2Definition Iadf-fin1a 7879
[Levy58] p. 2Definition IIIdf-fin3 7882
[Levy58] p. 3Definition Vdf-fin5 7883
[Levy58] p. 3Definition IVdf-fin4 7881
[Levy58] p. 4Definition VIdf-fin6 7884
[Levy58] p. 4Definition VIIdf-fin7 7885
[Levy58], p. 3Theorem 1fin1a2 8009
[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 22948
[Maeda] p. 168Lemma 5mdsym 22952  mdsymi 22951
[Maeda] p. 168Lemma 4(i)mdsymlem4 22946  mdsymlem6 22948  mdsymlem7 22949
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22950
[MaedaMaeda] p. 1Remarkssdmd1 22853  ssdmd2 22854  ssmd1 22851  ssmd2 22852
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22849
[MaedaMaeda] p. 1Definition 1.1df-dmd 22821  df-md 22820  mdbr 22834
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22871  mdslj1i 22859  mdslj2i 22860  mdslle1i 22857  mdslle2i 22858  mdslmd1i 22869  mdslmd2i 22870
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22861  mdsl2bi 22863  mdsl2i 22862
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22875
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22872
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22873
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22850
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22855  mdsl3 22856
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22874
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22969
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28678  hlrelat1 28756
[MaedaMaeda] p. 31Lemma 7.5lcvexch 28396
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22876  cvmdi 22864  cvnbtwn4 22829  cvrnbtwn4 28636
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22877
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28697  cvp 22915  cvrp 28772  lcvp 28397
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22939
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22938
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28690  hlexch4N 28748
[MaedaMaeda] p. 34Exercise 7.1atabsi 22941
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28799
[MaedaMaeda] p. 61Definition 15.10psubN 29105  atpsubN 29109  df-pointsN 28858  pointpsubN 29107
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28860  pmap11 29118  pmaple 29117  pmapsub 29124  pmapval 29113
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29121  pmap1N 29123
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29126  pmapglb2N 29127  pmapglb2xN 29128  pmapglbx 29125
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29208
[MaedaMaeda] p. 67Postulate PS1ps-1 28833
[MaedaMaeda] p. 68Lemma 16.2df-padd 29152  paddclN 29198  paddidm 29197
[MaedaMaeda] p. 68Condition PS2ps-2 28834
[MaedaMaeda] p. 68Equation 16.2.1paddass 29194
[MaedaMaeda] p. 69Lemma 16.4ps-1 28833
[MaedaMaeda] p. 69Theorem 16.4ps-2 28834
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14946  lsmmod2 14947  lssats 28369  shatomici 22898  shatomistici 22901  shmodi 21929  shmodsi 21928
[MaedaMaeda] p. 130Remark 29.6dmdmd 22840  mdsymlem7 22949
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22128
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22032
[MaedaMaeda] p. 139Remarksumdmdii 22955
[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 27741
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27742
[Margaris] p. 79Rule Cexinst01 27447  exinst11 27448
[Margaris] p. 89Theorem 19.219.2 1759  19.2K 28175  r19.2z 3518
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2884
[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 2631
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26943  albi 1552  ralbi 2654
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26945  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26942  alim 1548  alimd 1705  alimdh 1551  alimdv 2018  ralimdaa 2595  ralimdv 2597  ralimdva 2596  sbcimdv 3027
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2012  19.21vv 26941  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2015  alrimi 1706  alrimih 1553  alrimiv 2013  alrimivv 2014  r19.21 2604  r19.21be 2619  r19.21bi 2616  r19.21t 2603  r19.21v 2605  ralrimd 2606  ralrimdv 2607  ralrimdva 2608  ralrimdvv 2612  ralrimdvva 2613  ralrimi 2599  ralrimiv 2600  ralrimiva 2601  ralrimivv 2609  ralrimivva 2610  ralrimivvva 2611  ralrimivw 2602  rexlimi 2635
[Margaris] p. 90Theorem 19.222alimdv 2020  2exim 26944  2eximdv 2021  exim 1573  eximd 1711  eximdh 1586  eximdv 2019  rexim 2622  reximdai 2626  reximddv 22988  reximdv 2629  reximdv2 2627  reximdva 2630  reximdvai 2628  reximi2 2624
[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 27340  exlimi 1781  exlimih 1782  exlimiv 2024  exlimivv 2026  r19.23 2633  r19.23v 2634  rexlimd 2639  rexlimdv 2641  rexlimdv3a 2644  rexlimdva 2642  rexlimdvaa 2643  rexlimdvv 2648  rexlimdvva 2649  rexlimdvw 2645  rexlimiv 2636  rexlimiva 2637  rexlimivv 2647
[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 2651  r19.26-2a 24300  r19.26-3 2652  r19.26 2650  r19.26m 2653
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2028  r19.27av 2656  r19.27z 3527  r19.27zv 3528
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2029  19.28vv 26951  r19.28av 2657  r19.28z 3521  r19.28zv 3524  rr19.28v 2885
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2658  r19.29r 2659
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2660
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26949
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32v 2661
[Margaris] p. 90Theorem 19.3319.33-2 26947  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 2662
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2031  19.36i 1789  19.36v 2030  19.36vv 26948  r19.36av 2663  r19.36zv 3529
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2034  19.37v 2033  19.37vv 26950  r19.37 2664  r19.37av 2665  r19.37zv 3525
[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 2666
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 27369  19.41v 2035  19.41vv 2036  19.41vvv 2037  19.41vvvv 2038  r19.41 2667  r19.41v 2668
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2039  19.42vv 2041  19.42vvv 2042  r19.42v 2669
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2670
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2671
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2672  r19.45zv 3526
[Margaris] p. 110Exercise 2(b)eu1 2139
[Mayet] p. 370Remarkjpi 22810  largei 22807  stri 22797
[Mayet3] p. 9Definition of CH-statesdf-hst 22752  ishst 22754
[Mayet3] p. 10Theoremhstrbi 22806  hstri 22805
[Mayet3] p. 1223Theorem 4.1mayete3i 22267
[Mayet3] p. 1240Theorem 7.1mayetes3i 22269
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22818
[MegPav2000] p. 2345Definition 3.4-1chintcl 21871  chsupcl 21879
[MegPav2000] p. 2345Definition 3.4-2hatomic 22900
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22894
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22921
[MegPav2000] p. 2366Figure 7pl42N 29339
[MegPav2002] p. 362Lemma 2.2latj31 14167  latj32 14165  latjass 14163
[Megill] p. 444Axiom C5ax-17 1628
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1838  alequcom 1680  alequcomX 28266  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 27238  sbidd 27237
[Megill] p. 448Remark 9.6ax15 2105
[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 2106
[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 27149
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 3044  ra4sbca 3045  stdpc4 1897
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3050  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2024
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1892
[Mendelson] p. 225Axiom system NBGru 2965
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4240
[Mendelson] p. 231Exercise 4.10(k)inv1 3456
[Mendelson] p. 231Exercise 4.10(l)unv 3457
[Mendelson] p. 231Exercise 4.10(n)dfin3 3383
[Mendelson] p. 231Exercise 4.10(o)df-nul 3431
[Mendelson] p. 231Exercise 4.10(q)dfin4 3384
[Mendelson] p. 231Exercise 4.10(s)ddif 3283
[Mendelson] p. 231Definition of uniondfun3 3382
[Mendelson] p. 235Exercise 4.12(c)univ 4537
[Mendelson] p. 235Exercise 4.12(d)pwv 3800
[Mendelson] p. 235Exercise 4.12(j)pwin 4269
[Mendelson] p. 235Exercise 4.12(k)pwunss 4270
[Mendelson] p. 235Exercise 4.12(l)pwssun 4271
[Mendelson] p. 235Exercise 4.12(n)uniin 3821
[Mendelson] p. 235Exercise 4.12(p)reli 4801
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5180
[Mendelson] p. 244Proposition 4.8(g)epweon 4547
[Mendelson] p. 246Definition of successordf-suc 4370
[Mendelson] p. 250Exercise 4.36oelim2 6561
[Mendelson] p. 254Proposition 4.22(b)xpen 6992
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6914  xpsneng 6915
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6921  xpcomeng 6922
[Mendelson] p. 254Proposition 4.22(e)xpassen 6924
[Mendelson] p. 255Definitionbrsdom 6852
[Mendelson] p. 255Exercise 4.39endisj 6917
[Mendelson] p. 255Exercise 4.41mapprc 6744
[Mendelson] p. 255Exercise 4.43mapsnen 6906
[Mendelson] p. 255Exercise 4.45mapunen 6998
[Mendelson] p. 255Exercise 4.47xpmapen 6997
[Mendelson] p. 255Exercise 4.42(a)map0e 6773
[Mendelson] p. 255Exercise 4.42(b)map1 6907
[Mendelson] p. 257Proposition 4.24(a)undom 6918
[Mendelson] p. 258Exercise 4.56(b)cdaen 7767
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7776  cdacomen 7775
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7780
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7774
[Mendelson] p. 258Definition of cardinal sumcdaval 7764  df-cda 7762
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6498
[Mendelson] p. 266Proposition 4.34(f)oaordex 6524
[Mendelson] p. 275Proposition 4.42(d)entri3 8149
[Mendelson] p. 281Definitiondf-r1 7404
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7453
[Mendelson] p. 287Axiom system MKru 2965
[Mittelstaedt] p. 9Definitiondf-oc 21791
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3366
[Monk1] p. 33Theorem 3.2(i)ssrel 4764
[Monk1] p. 33Theorem 3.2(ii)eqrel 4765
[Monk1] p. 34Definition 3.3df-opab 4052
[Monk1] p. 36Theorem 3.7(i)coi1 5175  coi2 5176
[Monk1] p. 36Theorem 3.8(v)dm0 4880  rn0 4924
[Monk1] p. 36Theorem 3.7(ii)cnvi 5073
[Monk1] p. 37Theorem 3.13(i)relxp 4782
[Monk1] p. 37Theorem 3.13(x)dmxp 4885  rnxp 5094
[Monk1] p. 37Theorem 3.13(ii)xp0 5086  xp0r 4756
[Monk1] p. 38Theorem 3.16(ii)ima0 5018
[Monk1] p. 38Theorem 3.16(viii)imai 5015
[Monk1] p. 39Theorem 3.17imaexg 5014
[Monk1] p. 39Theorem 3.16(xi)imassrn 5013
[Monk1] p. 41Theorem 4.3(i)fnopfv 5594  funfvop 5571
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5500
[Monk1] p. 42Theorem 4.4(iii)fvelima 5508
[Monk1] p. 43Theorem 4.6funun 5234
[Monk1] p. 43Theorem 4.8(iv)dff13 5717  dff13f 5718
[Monk1] p. 46Theorem 4.15(v)funex 5677  funrnex 5681
[Monk1] p. 50Definition 5.4fniunfv 5707
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5143
[Monk1] p. 52Theorem 5.11(viii)ssint 3852
[Monk1] p. 52Definition 5.13 (i)1stval2 6071  df-1st 6056
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6072  df-2nd 6057
[Monk1] p. 112Theorem 15.17(v)ranksn 7494  ranksnb 7467
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7495
[Monk1] p. 112Theorem 15.17(iii)rankun 7496  rankunb 7490
[Monk1] p. 113Theorem 15.18r1val3 7478
[Monk1] p. 113Definition 15.19df-r1 7404  r1val2 7477
[Monk1] p. 117Lemmazorn2 8101  zorn2g 8098
[Monk1] p. 133Theorem 18.11cardom 7587
[Monk1] p. 133Theorem 18.12canth3 8151
[Monk1] p. 133Theorem 18.14carduni 7582
[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 4223
[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 2572
[Moore] p. 53Part Idf-mre 13450
[Munkres] p. 77Example 2distop 16695  indistop 16701  indistopon 16700
[Munkres] p. 77Example 3fctop 16703  fctop2 16704
[Munkres] p. 77Example 4cctop 16705
[Munkres] p. 78Definition of basisdf-bases 16600  isbasis3g 16649
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13306  tgval2 16656
[Munkres] p. 79Remarktgcl 16669
[Munkres] p. 80Lemma 2.1tgval3 16663
[Munkres] p. 80Lemma 2.2tgss2 16687  tgss3 16686
[Munkres] p. 81Lemma 2.3basgen 16688  basgen2 16689
[Munkres] p. 89Definition of subspace topologyresttop 16853
[Munkres] p. 93Theorem 6.1(1)0cld 16737  topcld 16734
[Munkres] p. 93Theorem 6.1(2)iincld 16738
[Munkres] p. 93Theorem 6.1(3)uncld 16740
[Munkres] p. 94Definition of closureclsval 16736
[Munkres] p. 94Definition of interiorntrval 16735
[Munkres] p. 95Theorem 6.5(a)clsndisj 16774  elcls 16772
[Munkres] p. 95Theorem 6.5(b)elcls3 16782
[Munkres] p. 97Theorem 6.6clslp 16841  neindisj 16816
[Munkres] p. 97Corollary 6.7cldlp 16843
[Munkres] p. 97Definition of limit pointislp2 16839  lpval 16833
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17005
[Munkres] p. 102Definition of continuous functiondf-cn 16919  iscn 16927  iscn2 16930
[Munkres] p. 107Theorem 7.2(g)cncnp 16971  cncnp2 16972  cncnpi 16969  df-cnp 16920  iscnp 16929  iscnp2 16931
[Munkres] p. 127Theorem 10.1metcn 18051
[Munkres] p. 128Theorem 10.3metcn4 18698
[NielsenChuang] p. 195Equation 4.73unierri 22644
[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 18599  df-dip 21234  dip0l 21254  ip0l 16502
[Ponnusamy] p. 361Equation 6.45ipval 21236
[Ponnusamy] p. 362Equation I1dipcj 21250
[Ponnusamy] p. 362Equation I3cphdir 18602  dipdir 21380  ipdir 16505  ipdiri 21368
[Ponnusamy] p. 362Equation I4ipidsq 21246
[Ponnusamy] p. 362Equation 6.46ip0i 21363
[Ponnusamy] p. 362Equation 6.47ip1i 21365
[Ponnusamy] p. 362Equation 6.48ip2i 21366
[Ponnusamy] p. 363Equation I2cphass 18608  dipass 21383  ipass 16511  ipassi 21379
[Prugovecki] p. 186Definition of brabraval 22484  df-bra 22390
[Prugovecki] p. 376Equation 8.1df-kb 22391  kbval 22494
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22922
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 29244
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22936  atcvat4i 22937  cvrat3 28798  cvrat4 28799  lsatcvat3 28409
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22822  cvrval 28626  df-cv 22819  df-lcv 28376  lspsncv0 15861
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 29256
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 29257
[Quine] p. 16Definition 2.1df-clab 2245  rabid 2691
[Quine] p. 17Definition 2.1''dfsb7 2082
[Quine] p. 18Definition 2.7df-cleq 2251
[Quine] p. 19Definition 2.9conventions 3  df-v 2765
[Quine] p. 34Theorem 5.1abeq2 2363
[Quine] p. 35Theorem 5.2abid2 2375  abid2f 2419
[Quine] p. 40Theorem 6.1sb5 1994
[Quine] p. 40Theorem 6.2sb56 1992  sb6 1993
[Quine] p. 41Theorem 6.3df-clel 2254
[Quine] p. 41Theorem 6.4eqid 2258  eqid1 20800
[Quine] p. 41Theorem 6.5eqcom 2260
[Quine] p. 42Theorem 6.6df-sbc 2967
[Quine] p. 42Theorem 6.7dfsbcq 2968  dfsbcq2 2969
[Quine] p. 43Theorem 6.8vex 2766
[Quine] p. 43Theorem 6.9isset 2767
[Quine] p. 44Theorem 7.3cla4gf 2838  cla4gv 2843  cla4imgf 2836
[Quine] p. 44Theorem 6.11a4sbc 2978  a4sbcd 2979
[Quine] p. 44Theorem 6.12elex 2771
[Quine] p. 44Theorem 6.13elab 2889  elabg 2890  elabgf 2887
[Quine] p. 44Theorem 6.14noel 3434
[Quine] p. 48Theorem 7.2snprc 3669
[Quine] p. 48Definition 7.1df-pr 3621  df-sn 3620
[Quine] p. 49Theorem 7.4snss 3722  snssg 3728
[Quine] p. 49Theorem 7.5prss 3743  prssg 3744
[Quine] p. 49Theorem 7.6prid1 3708  prid1g 3706  prid2 3709  prid2g 3707  snid 3641  snidg 3639
[Quine] p. 51Theorem 7.13prex 4189  snex 4188  snexALT 4168
[Quine] p. 53Theorem 8.2unisn 3817  unisnALT 27752  unisng 3818
[Quine] p. 53Theorem 8.3uniun 3820
[Quine] p. 54Theorem 8.6elssuni 3829
[Quine] p. 54Theorem 8.7uni0 3828
[Quine] p. 56Theorem 8.17uniabio 6235
[Quine] p. 56Definition 8.18dfiota2 6226
[Quine] p. 57Theorem 8.19iotaval 6236
[Quine] p. 57Theorem 8.22iotanul 6240
[Quine] p. 58Theorem 8.23iotaex 6242
[Quine] p. 58Definition 9.1df-op 3623
[Quine] p. 61Theorem 9.5opabid 4243  opelopab 4258  opelopaba 4253  opelopabaf 4260  opelopabf 4261  opelopabg 4255  opelopabga 4250  oprabid 5816
[Quine] p. 64Definition 9.11df-xp 4675
[Quine] p. 64Definition 9.12df-cnv 4677
[Quine] p. 64Definition 9.15df-id 4281
[Quine] p. 65Theorem 10.3fun0 5245
[Quine] p. 65Theorem 10.4funi 5223
[Quine] p. 65Theorem 10.5funsn 5238  funsng 5236
[Quine] p. 65Definition 10.1df-fun 4683
[Quine] p. 65Definition 10.2args 5029  df-fv 4689
[Quine] p. 68Definition 10.11conventions 3  df-fv 4689  fv2 5454
[Quine] p. 124Theorem 17.3nn0opth2 11253  nn0opth2i 11252  nn0opthi 11251  omopthi 6623
[Quine] p. 177Definition 25.2df-rdg 6391
[Quine] p. 232Equation icarddom 8144
[Quine] p. 284Axiom 39(vi)funimaex 5268  funimaexg 5267
[Quine] p. 331Axiom system NFru 2965
[ReedSimon] p. 36Definition (iii)ax-his3 21623
[ReedSimon] p. 63Exercise 4(a)df-dip 21234  polid 21698  polid2i 21696  polidi 21697
[ReedSimon] p. 63Exercise 4(b)df-ph 21351
[ReedSimon] p. 195Remarklnophm 22559  lnophmi 22558
[Retherford] p. 49Exercise 1(i)leopadd 22672
[Retherford] p. 49Exercise 1(ii)leopmul 22674  leopmuli 22673
[Retherford] p. 49Exercise 1(iv)leoptr 22677
[Retherford] p. 49Definition VI.1df-leop 22392  leoppos 22666
[Retherford] p. 49Exercise 1(iii)leoptri 22676
[Retherford] p. 49Definition of operator orderingleop3 22665
[Rudin] p. 164Equation 27efcan 12338
[Rudin] p. 164Equation 30efzval 12344
[Rudin] p. 167Equation 48absefi 12438
[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 5046
[Schechter] p. 51Definition of irreflexivityintirr 5049
[Schechter] p. 51Definition of symmetrycnvsym 5045
[Schechter] p. 51Definition of transitivitycotr 5043
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13450
[Schechter] p. 79Definition of Moore closuredf-mrc 13451
[Schechter] p. 82Section 4.5df-mrc 13451
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13453
[Schechter] p. 139Definition AC3dfac9 7730
[Schechter] p. 141Definition (MC)dfac11 26527
[Schechter] p. 149Axiom DC1ax-dc 8040  axdc3 8048
[Schechter] p. 187Definition of ring with unitisrng 15307  isrngo 21005
[Schechter] p. 276Remark 11.6.espan0 22081
[Schechter] p. 276Definition of spandf-span 21848  spanval 21872
[Schechter] p. 428Definition 15.35bastop1 16693
[Schwabhauser] p. 10Axiom A1axcgrrflx 23917
[Schwabhauser] p. 10Axiom A2axcgrtr 23918
[Schwabhauser] p. 10Axiom A3axcgrid 23919
[Schwabhauser] p. 11Axiom A4axsegcon 23930
[Schwabhauser] p. 11Axiom A5ax5seg 23941
[Schwabhauser] p. 11Axiom A6axbtwnid 23942
[Schwabhauser] p. 12Axiom A7axpasch 23944
[Schwabhauser] p. 12Axiom A8axlowdim2 23963
[Schwabhauser] p. 13Axiom A10axeuclid 23966
[Schwabhauser] p. 13Axiom A11axcont 23979
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23985
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23987
[Schwabhauser] p. 27Theorem 2.3cgrtr 23990
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23994
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23995
[Schwabhauser] p. 28Theorem 2.8cgrtriv 24000
[Schwabhauser] p. 28Theorem 2.105segofs 24004
[Schwabhauser] p. 28Definition 2.10df-ofs 23981
[Schwabhauser] p. 29Theorem 2.11cgrextend 24006
[Schwabhauser] p. 29Theorem 2.12segconeq 24008
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24020  btwntriv2 24010
[Schwabhauser] p. 30Theorem 3.2btwncomim 24011
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24014
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24015
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24021  btwnintr 24017
[Schwabhauser] p. 30Theorem 3.6btwnexch 24023  btwnexch3 24018
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24022
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23962
[Schwabhauser] p. 32Theorem 3.14btwndiff 24025
[Schwabhauser] p. 33Theorem 3.17trisegint 24026
[Schwabhauser] p. 34Theorem 4.2ifscgr 24042
[Schwabhauser] p. 34Definition 4.1df-ifs 24037
[Schwabhauser] p. 35Theorem 4.3cgrsub 24043
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24053
[Schwabhauser] p. 35Definition 4.4df-cgr3 24038
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24054
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24060  colinearperm2 24062  colinearperm3 24061  colinearperm4 24063  colinearperm5 24064
[Schwabhauser] p. 36Definition 4.10df-colinear 24039
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24065
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24073
[Schwabhauser] p. 37Theorem 4.14lineext 24074
[Schwabhauser] p. 37Theorem 4.16fscgr 24078
[Schwabhauser] p. 37Theorem 4.17linecgr 24079
[Schwabhauser] p. 37Definition 4.15df-fs 24040
[Schwabhauser] p. 38Theorem 4.18lineid 24081
[Schwabhauser] p. 38Theorem 4.19idinside 24082
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24099
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24100
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24101
[Schwabhauser] p. 41Theorem 5.5brsegle2 24107
[Schwabhauser] p. 41Definition 5.4df-segle 24105
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24108
[Schwabhauser] p. 42Theorem 5.7seglerflx 24110
[Schwabhauser] p. 42Theorem 5.8segletr 24112
[Schwabhauser] p. 42Theorem 5.9segleantisym 24113
[Schwabhauser] p. 42Theorem 5.10seglelin 24114
[Schwabhauser] p. 42Theorem 5.11seglemin 24111
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24116
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24123
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24124
[Schwabhauser] p. 43Theorem 6.4broutsideof 24119  df-outsideof 24118
[Schwabhauser] p. 43Definition 6.1broutsideof2 24120
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24125
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24126
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24127
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24129
[Schwabhauser] p. 44Definition 6.8df-ray 24136
[Schwabhauser] p. 45Part 2df-lines2 24137
[Schwabhauser] p. 45Theorem 6.13outsidele 24130
[Schwabhauser] p. 45Theorem 6.15lineunray 24145
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24146
[Schwabhauser] p. 45Theorem 6.17linecom 24148  linerflx1 24147  linerflx2 24149
[Schwabhauser] p. 45Theorem 6.18linethru 24151
[Schwabhauser] p. 45Definition 6.14df-line2 24135
[Schwabhauser] p. 46Theorem 6.19linethrueu 24154
[Schwabhauser] p. 46Theorem 6.21lineintmo 24155
[Shapiro] p. 230Theorem 6.5.1dchrhash 20472  dchrsum 20470  dchrsum2 20469  sumdchr 20473
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20474  sum2dchr 20475
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15263  ablfacrp2 15264
[Shapiro], p. 328Equation 9.2.4vmasum 20417
[Shapiro], p. 329Equation 9.2.7logfac2 20418
[Shapiro], p. 329Equation 9.2.9logfacrlim 20425
[Shapiro], p. 331Equation 9.2.13vmadivsum 20593
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20596
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20650  vmalogdivsum2 20649
[Shapiro], p. 375Theorem 9.4.1dirith 20640  dirith2 20639
[Shapiro], p. 375Equation 9.4.3rplogsum 20638  rpvmasum 20637  rpvmasum2 20623
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20598
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20636
[Shapiro], p. 377Lemma 9.4.1dchrisum 20603  dchrisumlem1 20600  dchrisumlem2 20601  dchrisumlem3 20602  dchrisumlema 20599
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20606
[Shapiro], p. 379Equation 9.4.16dchrmusum 20635  dchrmusumlem 20633  dchrvmasumlem 20634
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20605
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20607
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20631  dchrisum0re 20624  dchrisumn0 20632
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20617
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20621
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20622
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20677  pntrsumbnd2 20678  pntrsumo1 20676
[Shapiro], p. 405Equation 10.2.1mudivsum 20641
[Shapiro], p. 406Equation 10.2.6mulogsum 20643
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20645
[Shapiro], p. 407Equation 10.2.8mulog2sum 20648
[Shapiro], p. 418Equation 10.4.6logsqvma 20653
[Shapiro], p. 418Equation 10.4.8logsqvma2 20654
[Shapiro], p. 419Equation 10.4.10selberg 20659
[Shapiro], p. 420Equation 10.4.12selberg2lem 20661
[Shapiro], p. 420Equation 10.4.14selberg2 20662
[Shapiro], p. 422Equation 10.6.7selberg3 20670
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20671
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20668  selberg3lem2 20669
[Shapiro], p. 422Equation 10.4.23selberg4 20672
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20666
[Shapiro], p. 428Equation 10.6.2selbergr 20679
[Shapiro], p. 429Equation 10.6.8selberg3r 20680
[Shapiro], p. 430Equation 10.6.11selberg4r 20681
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20695
[Shapiro], p. 434Equation 10.6.27pntlema 20707  pntlemb 20708  pntlemc 20706  pntlemd 20705  pntlemg 20709
[Shapiro], p. 435Equation 10.6.29pntlema 20707
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20699
[Shapiro], p. 436Lemma 10.6.2pntibnd 20704
[Shapiro], p. 436Equation 10.6.34pntlema 20707
[Shapiro], p. 436Equation 10.6.35pntlem3 20720  pntleml 20722
[Stoll] p. 13Definition of symmetric differencesymdif1 3408
[Stoll] p. 16Exercise 4.40dif 3500  dif0 3499
[Stoll] p. 16Exercise 4.8difdifdir 3516
[Stoll] p. 17Theorem 5.1(5)undifv 3503
[Stoll] p. 19Theorem 5.2(13)undm 3401
[Stoll] p. 19Theorem 5.2(13')indm 3402
[Stoll] p. 20Remarkinvdif 3385
[Stoll] p. 25Definition of ordered tripledf-ot 3624
[Stoll] p. 43Definitionuniiun 3929
[Stoll] p. 44Definitionintiin 3930
[Stoll] p. 45Definitiondf-iin 3882
[Stoll] p. 45Definition indexed uniondf-iun 3881
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3408
[Strang] p. 242Section 6.3expgrowth 26919
[Suppes] p. 22Theorem 2eq0 3444
[Suppes] p. 22Theorem 4eqss 3169  eqssd 3171  eqssi 3170
[Suppes] p. 23Theorem 5ss0 3460  ss0b 3459
[Suppes] p. 23Theorem 6sstr 3162  sstrALT2 27661
[Suppes] p. 23Theorem 7pssirr 3251
[Suppes] p. 23Theorem 8pssn2lp 3252
[Suppes] p. 23Theorem 9psstr 3255
[Suppes] p. 23Theorem 10pssss 3246
[Suppes] p. 25Theorem 12elin 3333  elun 3291
[Suppes] p. 26Theorem 15inidm 3353
[Suppes] p. 26Theorem 16in0 3455
[Suppes] p. 27Theorem 23unidm 3293
[Suppes] p. 27Theorem 24un0 3454
[Suppes] p. 27Theorem 25ssun1 3313
[Suppes] p. 27Theorem 26ssequn1 3320
[Suppes] p. 27Theorem 27unss 3324
[Suppes] p. 27Theorem 28indir 3392
[Suppes] p. 27Theorem 29undir 3393
[Suppes] p. 28Theorem 32difid 3497  difidALT 3498
[Suppes] p. 29Theorem 33difin 3381
[Suppes] p. 29Theorem 34indif 3386
[Suppes] p. 29Theorem 35undif1 3504
[Suppes] p. 29Theorem 36difun2 3508
[Suppes] p. 29Theorem 37difin0 3502
[Suppes] p. 29Theorem 38disjdif 3501
[Suppes] p. 29Theorem 39difundi 3396
[Suppes] p. 29Theorem 40difindi 3398
[Suppes] p. 30Theorem 41nalset 4125
[Suppes] p. 39Theorem 61uniss 3822
[Suppes] p. 39Theorem 65uniop 4241
[Suppes] p. 41Theorem 70intsn 3872
[Suppes] p. 42Theorem 71intpr 3869  intprg 3870
[Suppes] p. 42Theorem 73op1stb 4541
[Suppes] p. 42Theorem 78intun 3868
[Suppes] p. 44Definition 15(a)dfiun2 3911  dfiun2g 3909
[Suppes] p. 44Definition 15(b)dfiin2 3912
[Suppes] p. 47Theorem 86elpw 3605  elpw2 4142  elpw2g 4141  elpwg 3606  elpwgdedVD 27743
[Suppes] p. 47Theorem 87pwid 3612
[Suppes] p. 47Theorem 89pw0 3736
[Suppes] p. 48Theorem 90pwpw0 3737
[Suppes] p. 52Theorem 101xpss12 4780
[Suppes] p. 52Theorem 102xpindi 4807  xpindir 4808
[Suppes] p. 52Theorem 103xpundi 4729  xpundir 4730
[Suppes] p. 54Theorem 105elirrv 7279
[Suppes] p. 58Theorem 2relss 4763
[Suppes] p. 59Theorem 4eldm 4864  eldm2 4865  eldm2g 4863  eldmg 4862
[Suppes] p. 59Definition 3df-dm 4679
[Suppes] p. 60Theorem 6dmin 4874
[Suppes] p. 60Theorem 8rnun 5077
[Suppes] p. 60Theorem 9rnin 5078
[Suppes] p. 60Definition 4dfrn2 4856
[Suppes] p. 61Theorem 11brcnv 4852  brcnvg 4850
[Suppes] p. 62Equation 5elcnv 4846  elcnv2 4847
[Suppes] p. 62Theorem 12relcnv 5039
[Suppes] p. 62Theorem 15cnvin 5076
[Suppes] p. 62Theorem 16cnvun 5074
[Suppes] p. 63Theorem 20co02 5173
[Suppes] p. 63Theorem 21dmcoss 4932
[Suppes] p. 63Definition 7df-co 4678
[Suppes] p. 64Theorem 26cnvco 4853
[Suppes] p. 64Theorem 27coass 5178
[Suppes] p. 65Theorem 31resundi 4957
[Suppes] p. 65Theorem 34elima 5005  elima2 5006  elima3 5007  elimag 5004
[Suppes] p. 65Theorem 35imaundi 5081
[Suppes] p. 66Theorem 40dminss 5083
[Suppes] p. 66Theorem 41imainss 5084
[Suppes] p. 67Exercise 11cnvxp 5085
[Suppes] p. 81Definition 34dfec2 6631
[Suppes] p. 82Theorem 72elec 6667  elecg 6666
[Suppes] p. 82Theorem 73erth 6672  erth2 6673
[Suppes] p. 83Theorem 74erdisj 6675
[Suppes] p. 89Theorem 96map0b 6774
[Suppes] p. 89Theorem 97map0 6776  map0g 6775
[Suppes] p. 89Theorem 98mapsn 6777
[Suppes] p. 89Theorem 99mapss 6778
[Suppes] p. 91Definition 12(ii)alephsuc 7663
[Suppes] p. 91Definition 12(iii)alephlim 7662
[Suppes] p. 92Theorem 1enref 6862  enrefg 6861
[Suppes] p. 92Theorem 2ensym 6878  ensymb 6877  ensymi 6879
[Suppes] p. 92Theorem 3entr 6881
[Suppes] p. 92Theorem 4unen 6911
[Suppes] p. 94Theorem 15endom 6856
[Suppes] p. 94Theorem 16ssdomg 6875
[Suppes] p. 94Theorem 17domtr 6882
[Suppes] p. 95Theorem 18sbth 6949
[Suppes] p. 97Theorem 23canth2 6982  canth2g 6983
[Suppes] p. 97Definition 3brsdom2 6953  df-sdom 6834  dfsdom2 6952
[Suppes] p. 97Theorem 21(i)sdomirr 6966
[Suppes] p. 97Theorem 22(i)domnsym 6955
[Suppes] p. 97Theorem 21(ii)sdomnsym 6954
[Suppes] p. 97Theorem 22(ii)domsdomtr 6964
[Suppes] p. 97Theorem 22(iv)brdom2 6859
[Suppes] p. 97Theorem 21(iii)sdomtr 6967
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6962
[Suppes] p. 98Exercise 4fundmen 6902  fundmeng 6903
[Suppes] p. 98Exercise 6xpdom3 6928
[Suppes] p. 98Exercise 11sdomentr 6963
[Suppes] p. 104Theorem 37fofi 7110
[Suppes] p. 104Theorem 38pwfi 7119
[Suppes] p. 105Theorem 40pwfi 7119
[Suppes] p. 111Axiom for cardinal numberscarden 8141
[Suppes] p. 130Definition 3df-tr 4088
[Suppes] p. 132Theorem 9ssonuni 4550
[Suppes] p. 134Definition 6df-suc 4370
[Suppes] p. 136Theorem Schema 22findes 4658  finds 4654  finds1 4657  finds2 4656
[Suppes] p. 151Theorem 42isfinite 7321  isfinite2 7083  isfiniteg 7085  unbnn 7081
[Suppes] p. 162Definition 5df-ltnq 8510  df-ltpq 8502
[Suppes] p. 197Theorem Schema 4tfindes 4625  tfinds 4622  tfinds2 4626
[Suppes] p. 209Theorem 18oaord1 6517
[Suppes] p. 209Theorem 21oaword2 6519
[Suppes] p. 211Theorem 25oaass 6527
[Suppes] p. 225Definition 8iscard2 7577
[Suppes] p. 227Theorem 56ondomon 8153
[Suppes] p. 228Theorem 59harcard 7579
[Suppes] p. 228Definition 12(i)aleph0 7661
[Suppes] p. 228Theorem Schema 61onintss 4414
[Suppes] p. 228Theorem Schema 62onminesb 4561  onminsb 4562
[Suppes] p. 229Theorem 64alephval2 8162
[Suppes] p. 229Theorem 65alephcard 7665
[Suppes] p. 229Theorem 66alephord2i 7672
[Suppes] p. 229Theorem 67alephnbtwn 7666
[Suppes] p. 229Definition 12df-aleph 7541
[Suppes] p. 242Theorem 6weth 8090
[Suppes] p. 242Theorem 8entric 8147
[Suppes] p. 242Theorem 9carden 8141
[TakeutiZaring] p. 8Axiom 1ax-ext 2239
[TakeutiZaring] p. 13Definition 4.5df-cleq 2251
[TakeutiZaring] p. 13Proposition 4.6df-clel 2254
[TakeutiZaring] p. 13Proposition 4.9cvjust 2253
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2275
[TakeutiZaring] p. 14Definition 4.16df-oprab 5796
[TakeutiZaring] p. 14Proposition 4.14ru 2965
[TakeutiZaring] p. 15Axiom 2zfpair 4184
[TakeutiZaring] p. 15Exercise 1elpr 3632  elpr2 3633  elprg 3631
[TakeutiZaring] p. 15Exercise 2elsn 3629  elsnc 3637  elsnc2 3643  elsnc2g 3642  elsncg 3636
[TakeutiZaring] p. 15Exercise 3elop 4211
[TakeutiZaring] p. 15Exercise 4sneq 3625  sneqr 3754
[TakeutiZaring] p. 15Definition 5.1dfpr2 3630  dfsn2 3628
[TakeutiZaring] p. 16Axiom 3uniex 4488
[TakeutiZaring] p. 16Exercise 6opth 4217
[TakeutiZaring] p. 16Exercise 7opex 4209
[TakeutiZaring] p. 16Exercise 8rext 4194
[TakeutiZaring] p. 16Corollary 5.8unex 4490  unexg 4493
[TakeutiZaring] p. 16Definition 5.3dftp2 3653
[TakeutiZaring] p. 16Definition 5.5df-uni 3802
[TakeutiZaring] p. 16Definition 5.6df-in 3134  df-un 3132
[TakeutiZaring] p. 16Proposition 5.7unipr 3815  uniprg 3816
[TakeutiZaring] p. 17Axiom 4pwex 4165  pwexg 4166
[TakeutiZaring] p. 17Exercise 1eltp 3652
[TakeutiZaring] p. 17Exercise 5elsuc 4433  elsucg 4431  sstr2 3161
[TakeutiZaring] p. 17Exercise 6uncom 3294
[TakeutiZaring] p. 17Exercise 7incom 3336
[TakeutiZaring] p. 17Exercise 8unass 3307
[TakeutiZaring] p. 17Exercise 9inass 3354
[TakeutiZaring] p. 17Exercise 10indi 3390
[TakeutiZaring] p. 17Exercise 11undi 3391
[TakeutiZaring] p. 17Definition 5.9df-pss 3143  dfss2 3144
[TakeutiZaring] p. 17Definition 5.10df-pw 3601
[TakeutiZaring] p. 18Exercise 7unss2 3321
[TakeutiZaring] p. 18Exercise 9df-ss 3141  sseqin2 3363
[TakeutiZaring] p. 18Exercise 10ssid 3172
[TakeutiZaring] p. 18Exercise 12inss1 3364  inss2 3365
[TakeutiZaring] p. 18Exercise 13nss 3211
[TakeutiZaring] p. 18Exercise 15unieq 3810
[TakeutiZaring] p. 18Exercise 18sspwb 4195  sspwimp 27744  sspwimpALT 27751  sspwimpALT2 27755  sspwimpcf 27746
[TakeutiZaring] p. 18Exercise 19pweqb 4202
[TakeutiZaring] p. 19Axiom 5ax-rep 4105
[TakeutiZaring] p. 20Definitiondf-rab 2527
[TakeutiZaring] p. 20Corollary 5.160ex 4124
[TakeutiZaring] p. 20Definition 5.12df-dif 3130
[TakeutiZaring] p. 20Definition 5.14dfnul2 3432
[TakeutiZaring] p. 20Proposition 5.15difid 3497  difidALT 3498
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3439  n0f 3438  neq0 3440
[TakeutiZaring] p. 21Axiom 6zfreg 7277
[TakeutiZaring] p. 21Axiom 6'zfregs 7382
[TakeutiZaring] p. 21Theorem 5.22setind 7387
[TakeutiZaring] p. 21Definition 5.20df-v 2765
[TakeutiZaring] p. 21Proposition 5.21vprc 4126
[TakeutiZaring] p. 22Exercise 10ss 3458
[TakeutiZaring] p. 22Exercise 3ssex 4132  ssexg 4134
[TakeutiZaring] p. 22Exercise 4inex1 4129
[TakeutiZaring] p. 22Exercise 5ruv 7282
[TakeutiZaring] p. 22Exercise 6elirr 7280
[TakeutiZaring] p. 22Exercise 7ssdif0 3488
[TakeutiZaring] p. 22Exercise 11difdif 3277
[TakeutiZaring] p. 22Exercise 13undif3 3404  undif3VD 27708
[TakeutiZaring] p. 22Exercise 14difss 3278
[TakeutiZaring] p. 22Exercise 15sscon 3285
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2523
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2524
[TakeutiZaring] p. 23Proposition 6.2xpex 4789  xpexg 4788  xpexgALT 6004
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4676
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5250
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5383  fun11 5253
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5206  svrelfun 5251
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4855
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4857
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4681
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4682
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4678
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5116  dfrel2 5112
[TakeutiZaring] p. 25Exercise 3xpss 4781
[TakeutiZaring] p. 25Exercise 5relun 4790
[TakeutiZaring] p. 25Exercise 6reluni 4796
[TakeutiZaring] p. 25Exercise 9inxp 4806
[TakeutiZaring] p. 25Exercise 12relres 4971
[TakeutiZaring] p. 25Exercise 13opelres 4948  opelresg 4950
[TakeutiZaring] p. 25Exercise 14dmres 4964
[TakeutiZaring] p. 25Exercise 15resss 4967
[TakeutiZaring] p. 25Exercise 17resabs1 4972
[TakeutiZaring] p. 25Exercise 18funres 5231
[TakeutiZaring] p. 25Exercise 24relco 5158
[TakeutiZaring] p. 25Exercise 29funco 5230
[TakeutiZaring] p. 25Exercise 30f1co 5384
[TakeutiZaring] p. 26Definition 6.10eu2 2143
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4689  fv3 5474
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5196  cnvexg 5195
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4929  dmexg 4927
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4930  rnexg 4928
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27026
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27027
[TakeutiZaring] p. 27Corollary 6.13fvex 5472
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5477  tz6.12 5478  tz6.12c 5481
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5480  tz6.12i 5482
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4684
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4685
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4687  wfo 4671
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4686  wf1 4670
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4688  wf1o 4672
[TakeutiZaring] p. 28Exercise 4eqfnfv 5556  eqfnfv2 5557  eqfnfv2f 5560
[TakeutiZaring] p. 28Exercise 5fvco 5529
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5675  fnexALT 5676
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5671  resfunexgALT 5672
[TakeutiZaring] p. 29Exercise 9funimaex 5268  funimaexg 5267
[TakeutiZaring] p. 29Definition 6.18df-br 3998
[TakeutiZaring] p. 30Definition 6.21dffr2 4330  dffr3 5033  eliniseg 5030  iniseg 5032
[TakeutiZaring] p. 30Definition 6.22df-eprel 4277
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4343  fr3nr 4543  frirr 4342
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4324
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4545
[TakeutiZaring] p. 31Exercise 1frss 4332
[TakeutiZaring] p. 31Exercise 4wess 4352
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23574  tz6.26i 23575  wefrc 4359  wereu2 4362
[TakeutiZaring] p. 32Theorem 6.27wfi 23576  wfii 23577
[TakeutiZaring] p. 32Definition 6.28df-isom 4690
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5760
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5761
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5767
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5768
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5769
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5773
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5780
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5782
[TakeutiZaring] p. 35Notationwtr 4087
[TakeutiZaring] p. 35Theorem 7.2trelpss 27028  tz7.2 4349
[TakeutiZaring] p. 35Definition 7.1dftr3 4091
[TakeutiZaring] p. 36Proposition 7.4ordwe 4377
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4385
[TakeutiZaring] p. 36Proposition 7.6ordelord 4386  ordelordALT 27354  ordelordALTVD 27693
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4392  ordelssne 4391
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4390
[TakeutiZaring] p. 37Proposition 7.9ordin 4394
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4552
[TakeutiZaring] p. 38Corollary 7.15ordsson 4553
[TakeutiZaring] p. 38Definition 7.11df-on 4368
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4396
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27367  ordon 4546
[TakeutiZaring] p. 38Proposition 7.13onprc 4548
[TakeutiZaring] p. 39Theorem 7.17tfi 4616
[TakeutiZaring] p. 40Exercise 3ontr2 4411
[TakeutiZaring] p. 40Exercise 7dftr2 4089
[TakeutiZaring] p. 40Exercise 9onssmin 4560
[TakeutiZaring] p. 40Exercise 11unon 4594
[TakeutiZaring] p. 40Exercise 12ordun 4466
[TakeutiZaring] p. 40Exercise 14ordequn 4465
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4549
[TakeutiZaring] p. 40Proposition 7.20elssuni 3829
[TakeutiZaring] p. 41Definition 7.22df-suc 4370
[TakeutiZaring] p. 41Proposition 7.23sssucid 4441  sucidg 4442
[TakeutiZaring] p. 41Proposition 7.24suceloni 4576
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4456  ordnbtwn 4455
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4591
[TakeutiZaring] p. 42Exercise 1df-lim 4369
[TakeutiZaring] p. 42Exercise 4omssnlim 4642
[TakeutiZaring] p. 42Exercise 7ssnlim 4646
[TakeutiZaring] p. 42Exercise 8onsucssi 4604  ordelsuc 4583
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4585
[TakeutiZaring] p. 42Definition 7.27nlimon 4614
[TakeutiZaring] p. 42Definition 7.28dfom2 4630
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4647
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4648
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4649
[TakeutiZaring] p. 43Remarkomon 4639
[TakeutiZaring] p. 43Axiom 7inf3 7304  omex 7312
[TakeutiZaring] p. 43Theorem 7.32ordom 4637
[TakeutiZaring] p. 43Corollary 7.31find 4653
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4650
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4651
[TakeutiZaring] p. 44Exercise 1limomss 4633
[TakeutiZaring] p. 44Exercise 2int0 3850  trint0 4104
[TakeutiZaring] p. 44Exercise 4intss1 3851
[TakeutiZaring] p. 44Exercise 5intex 4143
[TakeutiZaring] p. 44Exercise 6oninton 4563
[TakeutiZaring] p. 44Exercise 11ordintdif 4413
[TakeutiZaring] p. 44Definition 7.35df-int 3837
[TakeutiZaring] p. 44Proposition 7.34noinfep 7328
[TakeutiZaring] p. 45Exercise 4onint 4558
[TakeutiZaring] p. 47Lemma 1tfrlem1 6359
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6381
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6382
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6383
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6387  tz7.44-2 6388  tz7.44-3 6389
[TakeutiZaring] p. 50Exercise 1smogt 6352
[TakeutiZaring] p. 50Exercise 3smoiso 6347
[TakeutiZaring] p. 50Definition 7.46df-smo 6331
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6425  tz7.49c 6426
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6423
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6422
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6424
[TakeutiZaring] p. 53Proposition 7.532eu5 2202
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7607
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7608
[TakeutiZaring] p. 56Definition 8.1oalim 6499  oasuc 6491
[TakeutiZaring] p. 57Remarktfindsg 4623
[TakeutiZaring] p. 57Proposition 8.2oacl 6502
[TakeutiZaring] p. 57Proposition 8.3oa0 6483  oa0r 6505
[TakeutiZaring] p. 57Proposition 8.16omcl 6503
[TakeutiZaring] p. 58Corollary 8.5oacan 6514
[TakeutiZaring] p. 58Proposition 8.4nnaord 6585  nnaordi 6584  oaord 6513  oaordi 6512
[TakeutiZaring] p. 59Proposition 8.6iunss2 3921  uniss2 3832
[TakeutiZaring] p. 59Proposition 8.7oawordri 6516
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6521  oawordex 6523
[TakeutiZaring] p. 59Proposition 8.9nnacl 6577
[TakeutiZaring] p. 59Proposition 8.10oaabs 6610
[TakeutiZaring] p. 60Remarkoancom 7320
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6526
[TakeutiZaring] p. 62Exercise 1nnarcl 6582
[TakeutiZaring] p. 62Exercise 5oaword1 6518
[TakeutiZaring] p. 62Definition 8.15om0 6484  om0x 6486  omlim 6500  omsuc 6493
[TakeutiZaring] p. 63Proposition 8.17nnecl 6579  nnmcl 6578
[TakeutiZaring] p. 63Proposition 8.19nnmord 6598  nnmordi 6597  omord 6534  omordi 6532
[TakeutiZaring] p. 63Proposition 8.20omcan 6535
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6602  omwordri 6538
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6506
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6508  om1r 6509
[TakeutiZaring] p. 64Proposition 8.22om00 6541
[TakeutiZaring] p. 64Proposition 8.23omordlim 6543
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6544
[TakeutiZaring] p. 64Proposition 8.25odi 6545
[TakeutiZaring] p. 65Theorem 8.26omass 6546
[TakeutiZaring] p. 67Definition 8.30nnesuc 6574  oe0 6489  oelim 6501  oesuc 6494  onesuc 6497
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6487
[TakeutiZaring] p. 67Proposition 8.32oen0 6552
[TakeutiZaring] p. 67Proposition 8.33oeordi 6553
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6488
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6511
[TakeutiZaring] p. 68Corollary 8.34oeord 6554
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6560
[TakeutiZaring] p. 68Proposition 8.35oewordri 6558
[TakeutiZaring] p. 68Proposition 8.37oeworde 6559
[TakeutiZaring] p. 69Proposition 8.41oeoa 6563
[TakeutiZaring] p. 70Proposition 8.42oeoe 6565
[TakeutiZaring] p. 73Theorem 9.1trcl 7378  tz9.1 7379
[TakeutiZaring] p. 76Definition 9.9df-r1 7404  r10 7408  r1lim 7412  r1limg 7411  r1suc 7410  r1sucg 7409
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7420  r1ord2 7421  r1ordg 7418
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7430
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7455  tz9.13 7431  tz9.13g 7432
[TakeutiZaring] p. 79Definition 9.14df-rank 7405  rankval 7456  rankvalb 7437  rankvalg 7457
[TakeutiZaring] p. 79Proposition 9.16rankel 7479  rankelb 7464
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7493  rankval3 7480  rankval3b 7466
[TakeutiZaring] p. 79Proposition 9.18rankonid 7469
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7435
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7474  rankr1c 7461  rankr1g 7472
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7475
[TakeutiZaring] p. 80Exercise 1rankss 7489  rankssb 7488
[TakeutiZaring] p. 80Exercise 2unbndrank 7482
[TakeutiZaring] p. 80Proposition 9.19bndrank 7481
[TakeutiZaring] p. 83Axiom of Choiceac4 8070  dfac3 7716
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7625  numth 8067  numth2 8066
[TakeutiZaring] p. 85Definition 10.4cardval 8136
[TakeutiZaring] p. 85Proposition 10.5cardid 8137  cardid2 7554
[TakeutiZaring] p. 85Proposition 10.9oncard 7561
[TakeutiZaring] p. 85Proposition 10.10carden 8141
[TakeutiZaring] p. 85Proposition 10.11cardidm 7560
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7545
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7566
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7558
[TakeutiZaring] p. 87Proposition 10.15pwen 7002
[TakeutiZaring] p. 88Exercise 1en0 6892
[TakeutiZaring] p. 88Exercise 7infensuc 7007
[TakeutiZaring] p. 89Exercise 10omxpen 6932
[TakeutiZaring] p. 90Corollary 10.23cardnn 7564
[TakeutiZaring] p. 90Definition 10.27alephiso 7693
[TakeutiZaring] p. 90Proposition 10.20nneneq 7012
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7018
[TakeutiZaring] p. 90Proposition 10.26alephprc 7694
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7017
[TakeutiZaring] p. 91Exercise 2alephle 7683
[TakeutiZaring] p. 91Exercise 3aleph0 7661
[TakeutiZaring] p. 91Exercise 4cardlim 7573
[TakeutiZaring] p. 91Exercise 7infpss 7811
[TakeutiZaring] p. 91Exercise 8infcntss 7098
[TakeutiZaring] p. 91Definition 10.29df-fin 6835  isfi 6853
[TakeutiZaring] p. 92Proposition 10.32onfin 7019
[TakeutiZaring] p. 92Proposition 10.34imadomg 8127
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6925
[TakeutiZaring] p. 93Proposition 10.35fodomb 8119
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7783  unxpdom 7038
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7575  cardsdomelir 7574
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7040
[TakeutiZaring] p. 94Proposition 10.39infxpen 7610
[TakeutiZaring] p. 95Definition 10.42df-map 6742
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8152  infxpidm2 7612
[TakeutiZaring] p. 95Proposition 10.41infcda 7802  infxp 7809  infxpg 24461
[TakeutiZaring] p. 96Proposition 10.44pw2en 6937  pw2f1o 6935
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6995
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8082
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8077  ac6s5 8086
[TakeutiZaring] p. 98Theorem 10.47unidom 8133
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8134  uniimadomf 8135
[TakeutiZaring] p. 100Definition 11.1cfcof 7868
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7863
[TakeutiZaring] p. 102Exercise 1cfle 7848
[TakeutiZaring] p. 102Exercise 2cf0 7845
[TakeutiZaring] p. 102Exercise 3cfsuc 7851
[TakeutiZaring] p. 102Exercise 4cfom 7858
[TakeutiZaring] p. 102Proposition 11.9coftr 7867
[TakeutiZaring] p. 103Theorem 11.15alephreg 8172
[TakeutiZaring] p. 103Proposition 11.11cardcf 7846
[TakeutiZaring] p. 103Proposition 11.13alephsing 7870
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7692
[TakeutiZaring] p. 104Proposition 11.16carduniima 7691
[TakeutiZaring] p. 104Proposition 11.18alephfp 7703  alephfp2 7704
[TakeutiZaring] p. 106Theorem 11.20gchina 8289
[TakeutiZaring] p. 106Theorem 11.21mappwen 7707
[TakeutiZaring] p. 107Theorem 11.26konigth 8159
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8173
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8174
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20796  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 28325
[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 12483
[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 2215  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 27753
[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 24295
[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 24288
[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 26920
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26921
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26922
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26923
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26924
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26925
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26926
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26927
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26928
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26929
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26931
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26932
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26933
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26930
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26936
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2078
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26937
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26938
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26939
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26940
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26941
[WhiteheadRussell] p. 162Theorem *11.322alim 26942
[WhiteheadRussell] p. 162Theorem *11.332albi 26943
[WhiteheadRussell] p. 162Theorem *11.342exim 26944
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26946
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26945
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26948
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26949
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26947
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26950
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26951
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26952
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2025  pm11.53g 24330
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26953
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26958
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26954
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26955
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26956
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26957
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26962
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26959
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26960
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26961
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26963
[WhiteheadRussell] p. 175Definition *14.02df-eu 2122
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26975  pm13.13b 26976
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26977
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2493
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2494
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2883
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26983
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26984
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26978
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27371  pm13.193 26979
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26980
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26981
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26982
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26989
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26988
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26987
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3018
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26990  pm14.122b 26991  pm14.122c 26992
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26993  pm14.123b 26994  pm14.123c 26995
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26997
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26996
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26998
[WhiteheadRussell] p. 190Theorem *14.22iota4 6243
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26999
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6244
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27000
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27002
[WhiteheadRussell] p. 192Theorem *14.26eupick 2181  eupickbi 2184  sbaniota 27003
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27001
[WhiteheadRussell] p. 192Theorem *14.271eubi 27004
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27005
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4689
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7601  pm54.43lem 7600
[Young] p. 141Definition of operator orderingleop2 22664
[Young] p. 142Example 12.2(i)0leop 22670  idleop 22671
[vandenDries] p. 42Lemma 61irrapx1 26280
[vandenDries] p. 43Theorem 62pellex 26287  pellexlem1 26281

This page was last updated on 25-Jun-2017.
Copyright terms: Public domain