Metamath Proof Explorer Home Metamath Proof Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  MPE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Metamath Proof Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular set theory book, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic ReferenceDescriptionMetamath Proof Explorer Page(s)
[Adamek] p. 21Definition 3.1df-cat 17842
[Adamek] p. 21Condition 3.1(b)df-cat 17842
[Adamek] p. 22Example 3.3(1)df-setc 18251
[Adamek] p. 24Example 3.3(4.c)0cat 17863  0funcg 50193  df-termc 50581
[Adamek] p. 24Example 3.3(4.d)df-prstc 50658  prsthinc 50572
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50686  df-mndtc 50686
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50682
[Adamek] p. 25Definition 3.5df-oppc 17886
[Adamek] p. 25Example 3.6(1)oduoppcciso 50674
[Adamek] p. 25Example 3.6(2)oppgoppcco 50699  oppgoppchom 50698  oppgoppcid 50700
[Adamek] p. 28Remark 3.9oppciso 17956
[Adamek] p. 28Remark 3.12invf1o 17944  invisoinvl 17965
[Adamek] p. 28Example 3.13idinv 17964  idiso 17963
[Adamek] p. 28Corollary 3.11inveq 17949
[Adamek] p. 28Definition 3.8df-inv 17923  df-iso 17924  dfiso2 17947
[Adamek] p. 28Proposition 3.10sectcan 17930
[Adamek] p. 29Remark 3.16cicer 17981  cicerALT 50154
[Adamek] p. 29Definition 3.15cic 17974  df-cic 17971
[Adamek] p. 29Definition 3.17df-func 18033
[Adamek] p. 29Proposition 3.14(1)invinv 17945
[Adamek] p. 29Proposition 3.14(2)invco 17946  isoco 17952
[Adamek] p. 30Remark 3.19df-func 18033
[Adamek] p. 30Example 3.20(1)idfucl 18056
[Adamek] p. 30Example 3.20(2)diag1 50412
[Adamek] p. 32Proposition 3.21funciso 18049
[Adamek] p. 33Example 3.26(1)discsnterm 50682  discthing 50569
[Adamek] p. 33Example 3.26(2)df-thinc 50526  prsthinc 50572  thincciso 50561  thincciso2 50563  thincciso3 50564  thinccisod 50562
[Adamek] p. 33Example 3.26(3)df-mndtc 50686
[Adamek] p. 33Proposition 3.23cofucl 18063  cofucla 50204
[Adamek] p. 34Remark 3.28(1)cofidfth 50270
[Adamek] p. 34Remark 3.28(2)catciso 18286  catcisoi 50508
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18341
[Adamek] p. 34Definition 3.27(2)df-fth 18082
[Adamek] p. 34Definition 3.27(3)df-full 18081
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18341
[Adamek] p. 35Corollary 3.32ffthiso 18106
[Adamek] p. 35Proposition 3.30(c)cofth 18112
[Adamek] p. 35Proposition 3.30(d)cofull 18111
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18326
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18326
[Adamek] p. 39Remark 3.422oppf 50240
[Adamek] p. 39Definition 3.41df-oppf 50231  funcoppc 18050
[Adamek] p. 39Definition 3.44.df-catc 18274  elcatchom 50505
[Adamek] p. 39Proposition 3.43(c)fthoppc 18100  fthoppf 50272
[Adamek] p. 39Proposition 3.43(d)fulloppc 18099  fulloppf 50271
[Adamek] p. 40Remark 3.48catccat 18283
[Adamek] p. 40Definition 3.470funcg 50193  df-catc 18274
[Adamek] p. 45Exercise 3Gincat 50709
[Adamek] p. 48Remark 4.2(2)cnelsubc 50712  nelsubc3 50179
[Adamek] p. 48Remark 4.2(3)imasubc 50259  imasubc2 50260  imasubc3 50264
[Adamek] p. 48Example 4.3(1.a)0subcat 18013
[Adamek] p. 48Example 4.3(1.b)catsubcat 18014
[Adamek] p. 48Definition 4.1(1)nelsubc3 50179
[Adamek] p. 48Definition 4.1(2)fullsubc 18025
[Adamek] p. 48Definition 4.1(a)df-subc 17987
[Adamek] p. 49Remark 4.4idsubc 50268
[Adamek] p. 49Remark 4.4(1)idemb 50267
[Adamek] p. 49Remark 4.4(2)idfullsubc 50269  ressffth 18115
[Adamek] p. 58Exercise 4Asetc1onsubc 50710
[Adamek] p. 83Definition 6.1df-nat 18121
[Adamek] p. 87Remark 6.14(a)fuccocl 18142
[Adamek] p. 87Remark 6.14(b)fucass 18146
[Adamek] p. 87Definition 6.15df-fuc 18122
[Adamek] p. 88Remark 6.16fuccat 18148
[Adamek] p. 101Definition 7.10funcg 50193  df-inito 18159
[Adamek] p. 101Example 7.2(3)0funcg 50193  df-termc 50581  initc 50199
[Adamek] p. 101Example 7.2 (6)irinitoringc 21785
[Adamek] p. 102Definition 7.4df-termo 18160  oppctermo 50344
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18187
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18191
[Adamek] p. 103Remark 7.8oppczeroo 50345
[Adamek] p. 103Definition 7.7df-zeroo 18161
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21786
[Adamek] p. 103Proposition 7.6termoeu1w 18194
[Adamek] p. 106Definition 7.19df-sect 17922
[Adamek] p. 107Example 7.20(7)thincinv 50577
[Adamek] p. 108Example 7.25(4)thincsect2 50576
[Adamek] p. 110Example 7.33(9)thincmon 50541
[Adamek] p. 110Proposition 7.35sectmon 17957
[Adamek] p. 112Proposition 7.42sectepi 17959
[Adamek] p. 185Section 10.67updjud 10015
[Adamek] p. 193Definition 11.1(1)df-lmd 50753
[Adamek] p. 193Definition 11.3(1)df-lmd 50753
[Adamek] p. 194Definition 11.3(2)df-lmd 50753
[Adamek] p. 202Definition 11.27(1)df-cmd 50754
[Adamek] p. 202Definition 11.27(2)df-cmd 50754
[Adamek] p. 478Item Rngdf-ringc 20898
[AhoHopUll] p. 2Section 1.1df-bigo 49660
[AhoHopUll] p. 12Section 1.3df-blen 49682
[AhoHopUll] p. 318Section 9.1df-concat 14716  df-pfx 14821  df-substr 14789  df-word 14659  lencl 14678  wrd0 14684
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 25027  df-nmoo 31347
[AkhiezerGlazman] p. 64Theoremhmopidmch 32755  hmopidmchi 32753
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32803  pjcmul2i 32804
[AkhiezerGlazman] p. 72Theoremcnvunop 32520  unoplin 32522
[AkhiezerGlazman] p. 72Equation 2unopadj 32521  unopadj2 32540
[AkhiezerGlazman] p. 73Theoremelunop2 32615  lnopunii 32614
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32688
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28313
[Alling] p. 184Axiom Bbdayfo 28034
[Alling] p. 184Axiom Oltsso 28033
[Alling] p. 184Axiom SDnodense 28049
[Alling] p. 185Lemma 0nocvxmin 28141
[Alling] p. 185Theoremconway 28165
[Alling] p. 185Axiom FEnoeta 28100
[Alling] p. 186Theorem 4lesrec 28185  lesrecd 28186
[Alling], p. 2Definitionrp-brsslt 44424
[Alling], p. 3Notenla0001 44427  nla0002 44425  nla0003 44426
[Apostol] p. 18Theorem I.1addcan 11494  addcan2d 11514  addcan2i 11504  addcand 11513  addcani 11503
[Apostol] p. 18Theorem I.2negeu 11547
[Apostol] p. 18Theorem I.3negsub 11606  negsubd 11675  negsubi 11636
[Apostol] p. 18Theorem I.4negneg 11608  negnegd 11660  negnegi 11628
[Apostol] p. 18Theorem I.5subdi 11749  subdid 11772  subdii 11765  subdir 11750  subdird 11773  subdiri 11766
[Apostol] p. 18Theorem I.6mul01 11489  mul01d 11509  mul01i 11500  mul02 11488  mul02d 11508  mul02i 11499
[Apostol] p. 18Theorem I.7mulcan 11953  mulcan2d 11950  mulcand 11949  mulcani 11955
[Apostol] p. 18Theorem I.8receu 11961  xreceu 33488
[Apostol] p. 18Theorem I.9divrec 11990  divrecd 12096  divreci 12062  divreczi 12055
[Apostol] p. 18Theorem I.10recrec 12014  recreci 12049
[Apostol] p. 18Theorem I.11mul0or 11956  mul0ord 11964  mul0ori 11963
[Apostol] p. 18Theorem I.12mul2neg 11755  mul2negd 11771  mul2negi 11764  mulneg1 11752  mulneg1d 11769  mulneg1i 11762
[Apostol] p. 18Theorem I.13divadddiv 12032  divadddivd 12137  divadddivi 12079
[Apostol] p. 18Theorem I.14divmuldiv 12017  divmuldivd 12134  divmuldivi 12077  rdivmuldivd 20643
[Apostol] p. 18Theorem I.15divdivdiv 12018  divdivdivd 12140  divdivdivi 12080
[Apostol] p. 20Axiom 7rpaddcl 13144  rpaddcld 13179  rpmulcl 13145  rpmulcld 13180
[Apostol] p. 20Axiom 8rpneg 13154
[Apostol] p. 20Axiom 90nrp 13157
[Apostol] p. 20Theorem I.17lttri 11436
[Apostol] p. 20Theorem I.18ltadd1d 11909  ltadd1dd 11927  ltadd1i 11870
[Apostol] p. 20Theorem I.19ltmul1 12167  ltmul1a 12166  ltmul1i 12235  ltmul1ii 12245  ltmul2 12168  ltmul2d 13206  ltmul2dd 13220  ltmul2i 12238
[Apostol] p. 20Theorem I.20msqgt0 11836  msqgt0d 11883  msqgt0i 11853
[Apostol] p. 20Theorem I.210lt1 11838
[Apostol] p. 20Theorem I.23lt0neg1 11822  lt0neg1d 11885  ltneg 11816  ltnegd 11894  ltnegi 11860
[Apostol] p. 20Theorem I.25lt2add 11801  lt2addd 11939  lt2addi 11878
[Apostol] p. 20Definition of positive numbersdf-rp 13121
[Apostol] p. 21Exercise 4recgt0 12163  recgt0d 12251  recgt0i 12222  recgt0ii 12223
[Apostol] p. 22Definition of integersdf-z 12694
[Apostol] p. 22Definition of positive integersdfnn3 12349
[Apostol] p. 22Definition of rationalsdf-q 13076
[Apostol] p. 24Theorem I.26supeu 9446
[Apostol] p. 26Theorem I.28nnunb 12602
[Apostol] p. 26Theorem I.29arch 12603  archd 46177
[Apostol] p. 28Exercise 2btwnz 12802
[Apostol] p. 28Exercise 3nnrecl 12604
[Apostol] p. 28Exercise 4rebtwnz 13074
[Apostol] p. 28Exercise 5zbtwnre 13073
[Apostol] p. 28Exercise 6qbtwnre 13329
[Apostol] p. 28Exercise 10(a)zeneo 16509  zneo 12782  zneoALTV 48767
[Apostol] p. 29Theorem I.35cxpsqrtth 27058  msqsqrtd 15610  resqrtth 15422  sqrtth 15532  sqrtthi 15538  sqsqrtd 15609
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12338
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 13040
[Apostol] p. 361Remarkcrreczi 14372
[Apostol] p. 363Remarkabsgt0i 15567
[Apostol] p. 363Exampleabssubd 15623  abssubi 15571
[ApostolNT] p. 7Remarkfmtno0 48625  fmtno1 48626  fmtno2 48635  fmtno3 48636  fmtno4 48637  fmtno5fac 48667  fmtnofz04prm 48662
[ApostolNT] p. 7Definitiondf-fmtno 48613
[ApostolNT] p. 8Definitiondf-ppi 27427
[ApostolNT] p. 14Definitiondf-dvds 16423
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16439
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16464
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16459
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16452
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16454
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16440
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16441
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16446
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16481
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16483
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16485
[ApostolNT] p. 15Definitiondf-gcd 16665  dfgcd2 16719
[ApostolNT] p. 16Definitionisprm2 16857
[ApostolNT] p. 16Theorem 1.5coprmdvds 16828
[ApostolNT] p. 16Theorem 1.7prminf 17093
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16685
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16720
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16722
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16701
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16692
[ApostolNT] p. 17Theorem 1.8coprm 16887
[ApostolNT] p. 17Theorem 1.9euclemma 16889
[ApostolNT] p. 17Theorem 1.101arith2 17106
[ApostolNT] p. 18Theorem 1.13prmrec 17100
[ApostolNT] p. 19Theorem 1.14divalg 16573
[ApostolNT] p. 20Theorem 1.15eucalg 16762
[ApostolNT] p. 24Definitiondf-mu 27428
[ApostolNT] p. 25Definitiondf-phi 16943
[ApostolNT] p. 25Theorem 2.1musum 27518
[ApostolNT] p. 26Theorem 2.2phisum 16968
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16953
[ApostolNT] p. 28Theorem 2.5(c)phimul 16957
[ApostolNT] p. 32Definitiondf-vma 27425
[ApostolNT] p. 32Theorem 2.9muinv 27520
[ApostolNT] p. 32Theorem 2.10vmasum 27543
[ApostolNT] p. 38Remarkdf-sgm 27429
[ApostolNT] p. 38Definitiondf-sgm 27429
[ApostolNT] p. 75Definitiondf-chp 27426  df-cht 27424
[ApostolNT] p. 104Definitioncongr 16839
[ApostolNT] p. 106Remarkdvdsval3 16426
[ApostolNT] p. 106Definitionmoddvds 16433
[ApostolNT] p. 107Example 2mod2eq0even 16516
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16517
[ApostolNT] p. 107Example 4zmod1congr 14028
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 14068
[ApostolNT] p. 107Theorem 5.2(c)modexp 14382
[ApostolNT] p. 108Theorem 5.3modmulconst 16458
[ApostolNT] p. 109Theorem 5.4cncongr1 16842
[ApostolNT] p. 109Theorem 5.6gcdmodi 17252
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16844
[ApostolNT] p. 113Theorem 5.17eulerth 16960
[ApostolNT] p. 113Theorem 5.18vfermltl 16979
[ApostolNT] p. 114Theorem 5.19fermltl 16961
[ApostolNT] p. 116Theorem 5.24wilthimp 27399
[ApostolNT] p. 179Definitiondf-lgs 27622  lgsprme0 27666
[ApostolNT] p. 180Example 11lgs 27667
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27643
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27658
[ApostolNT] p. 181Theorem 9.4m1lgs 27715
[ApostolNT] p. 181Theorem 9.52lgs 27734  2lgsoddprm 27743
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27701
[ApostolNT] p. 185Theorem 9.8lgsquad 27710
[ApostolNT] p. 188Definitiondf-lgs 27622  lgs1 27668
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27659
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27661
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27669
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27670
[Baer] p. 40Property (b)mapdord 42696
[Baer] p. 40Property (c)mapd11 42697
[Baer] p. 40Property (e)mapdin 42720  mapdlsm 42722
[Baer] p. 40Property (f)mapd0 42723
[Baer] p. 40Definition of projectivitydf-mapd 42683  mapd1o 42706
[Baer] p. 41Property (g)mapdat 42725
[Baer] p. 44Part (1)mapdpg 42764
[Baer] p. 45Part (2)hdmap1eq 42859  mapdheq 42786  mapdheq2 42787  mapdheq2biN 42788
[Baer] p. 45Part (3)baerlem3 42771
[Baer] p. 46Part (4)mapdheq4 42790  mapdheq4lem 42789
[Baer] p. 46Part (5)baerlem5a 42772  baerlem5abmN 42776  baerlem5amN 42774  baerlem5b 42773  baerlem5bmN 42775
[Baer] p. 47Part (6)hdmap1l6 42879  hdmap1l6a 42867  hdmap1l6e 42872  hdmap1l6f 42873  hdmap1l6g 42874  hdmap1l6lem1 42865  hdmap1l6lem2 42866  mapdh6N 42805  mapdh6aN 42793  mapdh6eN 42798  mapdh6fN 42799  mapdh6gN 42800  mapdh6lem1N 42791  mapdh6lem2N 42792
[Baer] p. 48Part 9hdmapval 42886
[Baer] p. 48Part 10hdmap10 42898
[Baer] p. 48Part 11hdmapadd 42901
[Baer] p. 48Part (6)hdmap1l6h 42875  mapdh6hN 42801
[Baer] p. 48Part (7)mapdh75cN 42811  mapdh75d 42812  mapdh75e 42810  mapdh75fN 42813  mapdh7cN 42807  mapdh7dN 42808  mapdh7eN 42806  mapdh7fN 42809
[Baer] p. 48Part (8)mapdh8 42846  mapdh8a 42833  mapdh8aa 42834  mapdh8ab 42835  mapdh8ac 42836  mapdh8ad 42837  mapdh8b 42838  mapdh8c 42839  mapdh8d 42841  mapdh8d0N 42840  mapdh8e 42842  mapdh8g 42843  mapdh8i 42844  mapdh8j 42845
[Baer] p. 48Part (9)mapdh9a 42847
[Baer] p. 48Equation 10mapdhvmap 42827
[Baer] p. 49Part 12hdmap11 42906  hdmapeq0 42902  hdmapf1oN 42923  hdmapneg 42904  hdmaprnN 42922  hdmaprnlem1N 42907  hdmaprnlem3N 42908  hdmaprnlem3uN 42909  hdmaprnlem4N 42911  hdmaprnlem6N 42912  hdmaprnlem7N 42913  hdmaprnlem8N 42914  hdmaprnlem9N 42915  hdmapsub 42905
[Baer] p. 49Part 14hdmap14lem1 42926  hdmap14lem10 42935  hdmap14lem1a 42924  hdmap14lem2N 42927  hdmap14lem2a 42925  hdmap14lem3 42928  hdmap14lem8 42933  hdmap14lem9 42934
[Baer] p. 50Part 14hdmap14lem11 42936  hdmap14lem12 42937  hdmap14lem13 42938  hdmap14lem14 42939  hdmap14lem15 42940  hgmapval 42945
[Baer] p. 50Part 15hgmapadd 42952  hgmapmul 42953  hgmaprnlem2N 42955  hgmapvs 42949
[Baer] p. 50Part 16hgmaprnN 42959
[Baer] p. 110Lemma 1hdmapip0com 42975
[Baer] p. 110Line 27hdmapinvlem1 42976
[Baer] p. 110Line 28hdmapinvlem2 42977
[Baer] p. 110Line 30hdmapinvlem3 42978
[Baer] p. 110Part 1.2hdmapglem5 42980  hgmapvv 42984
[Baer] p. 110Proposition 1hdmapinvlem4 42979
[Baer] p. 111Line 10hgmapvvlem1 42981
[Baer] p. 111Line 15hdmapg 42988  hdmapglem7 42987
[Bauer], p. 483Theorem 1.22irrexpq 27059  2irrexpqALT 27128
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2595
[BellMachover] p. 460Notationdf-mo 2565
[BellMachover] p. 460Definitionmo3 2590
[BellMachover] p. 461Axiom Extax-ext 2733
[BellMachover] p. 462Theorem 1.1axextmo 2737
[BellMachover] p. 463Axiom Repaxrep5 5239
[BellMachover] p. 463Scheme Sepax-sep 5249
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37979  sepex 5255
[BellMachover] p. 466Problemaxpow2 5329
[BellMachover] p. 466Axiom Powaxpow3 5330
[BellMachover] p. 466Axiom Unionaxun2 7753
[BellMachover] p. 468Definitiondf-ord 6365
[BellMachover] p. 469Theorem 2.2(i)ordirr 6380
[BellMachover] p. 469Theorem 2.2(iii)onelon 6387  onelond 36948
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6382
[BellMachover] p. 471Definition of Ndf-om 7878
[BellMachover] p. 471Problem 2.5(ii)uniordint 7815
[BellMachover] p. 471Definition of Limdf-lim 6367
[BellMachover] p. 472Axiom Infzfinf2 9643
[BellMachover] p. 473Theorem 2.8limom 7893
[BellMachover] p. 477Equation 3.1df-r1 9768
[BellMachover] p. 478Definitionrankval2 9827  rankval2b 9835
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9789  r1ord3g 9786
[BellMachover] p. 480Axiom Regzfreg 9590
[BellMachover] p. 488Axiom ACac5 10555  dfac4 10201
[BellMachover] p. 490Definition of alephalephval3 10189
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40377
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32955
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32997  chirredi 32996
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32985
[Beran] p. 3Definition of joinsshjval3 31956
[Beran] p. 39Theorem 2.3(i)cmcm2 32218  cmcm2i 32195  cmcm2ii 32200  cmt2N 40308
[Beran] p. 40Theorem 2.3(iii)lecm 32219  lecmi 32204  lecmii 32205
[Beran] p. 45Theorem 3.4cmcmlem 32193
[Beran] p. 49Theorem 4.2cm2j 32222  cm2ji 32227  cm2mi 32228
[Beran] p. 95Definitiondf-sh 31809  issh2 31811
[Beran] p. 95Lemma 3.1(S5)his5 31688
[Beran] p. 95Lemma 3.1(S6)his6 31701
[Beran] p. 95Lemma 3.1(S7)his7 31692
[Beran] p. 95Lemma 3.2(S8)ho01i 32430
[Beran] p. 95Lemma 3.2(S9)hoeq1 32432
[Beran] p. 95Lemma 3.2(S10)ho02i 32431
[Beran] p. 95Lemma 3.2(S11)hoeq2 32433
[Beran] p. 95Postulate (S1)ax-his1 31684  his1i 31702
[Beran] p. 95Postulate (S2)ax-his2 31685
[Beran] p. 95Postulate (S3)ax-his3 31686
[Beran] p. 95Postulate (S4)ax-his4 31687
[Beran] p. 96Definition of normdf-hnorm 31570  dfhnorm2 31724  normval 31726
[Beran] p. 96Definition for Cauchy sequencehcau 31786
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31575
[Beran] p. 96Definition of complete subspaceisch3 31843
[Beran] p. 96Definition of convergedf-hlim 31574  hlimi 31790
[Beran] p. 97Theorem 3.3(i)norm-i-i 31735  norm-i 31731
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31739  norm-ii 31740  normlem0 31711  normlem1 31712  normlem2 31713  normlem3 31714  normlem4 31715  normlem5 31716  normlem6 31717  normlem7 31718  normlem7tALT 31721
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31741  norm-iii 31742
[Beran] p. 98Remark 3.4bcs 31783  bcsiALT 31781  bcsiHIL 31782
[Beran] p. 98Remark 3.4(B)normlem9at 31723  normpar 31757  normpari 31756
[Beran] p. 98Remark 3.4(C)normpyc 31748  normpyth 31747  normpythi 31744
[Beran] p. 99Remarklnfn0 32649  lnfn0i 32644  lnop0 32568  lnop0i 32572
[Beran] p. 99Theorem 3.5(i)nmcexi 32628  nmcfnex 32655  nmcfnexi 32653  nmcopex 32631  nmcopexi 32629
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32656  nmcfnlbi 32654  nmcoplb 32632  nmcoplbi 32630
[Beran] p. 99Theorem 3.5(iii)lnfncon 32658  lnfnconi 32657  lnopcon 32637  lnopconi 32636
[Beran] p. 100Lemma 3.6normpar2i 31758
[Beran] p. 101Lemma 3.6norm3adifi 31755  norm3adifii 31750  norm3dif 31752  norm3difi 31749
[Beran] p. 102Theorem 3.7(i)chocunii 31903  pjhth 31995  pjhtheu 31996  pjpjhth 32027  pjpjhthi 32028  pjth 25760
[Beran] p. 102Theorem 3.7(ii)ococ 32008  ococi 32007
[Beran] p. 103Remark 3.8nlelchi 32663
[Beran] p. 104Theorem 3.9riesz3i 32664  riesz4 32666  riesz4i 32665
[Beran] p. 104Theorem 3.10cnlnadj 32681  cnlnadjeu 32680  cnlnadjeui 32679  cnlnadji 32678  cnlnadjlem1 32669  nmopadjlei 32690
[Beran] p. 106Theorem 3.11(i)adjeq0 32693
[Beran] p. 106Theorem 3.11(v)nmopadji 32692
[Beran] p. 106Theorem 3.11(ii)adjmul 32694
[Beran] p. 106Theorem 3.11(iv)adjadj 32538
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32704  nmopcoadji 32703
[Beran] p. 106Theorem 3.11(iii)adjadd 32695
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32705
[Beran] p. 106Theorem 3.11(viii)adjcoi 32702  pjadj2coi 32806  pjadjcoi 32763
[Beran] p. 107Definitiondf-ch 31823  isch2 31825
[Beran] p. 107Remark 3.12choccl 31908  isch3 31843  occl 31906  ocsh 31885  shoccl 31907  shocsh 31886
[Beran] p. 107Remark 3.12(B)ococin 32010
[Beran] p. 108Theorem 3.13chintcl 31934
[Beran] p. 109Property (i)pjadj2 32789  pjadj3 32790  pjadji 32287  pjadjii 32276
[Beran] p. 109Property (ii)pjidmco 32783  pjidmcoi 32779  pjidmi 32275
[Beran] p. 110Definition of projector orderingpjordi 32775
[Beran] p. 111Remarkho0val 32352  pjch1 32272
[Beran] p. 111Definitiondf-hfmul 32336  df-hfsum 32335  df-hodif 32334  df-homul 32333  df-hosum 32332
[Beran] p. 111Lemma 4.4(i)pjo 32273
[Beran] p. 111Lemma 4.4(ii)pjch 32296  pjchi 32034
[Beran] p. 111Lemma 4.4(iii)pjoc2 32041  pjoc2i 32040
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 32282
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32767  pjssmii 32283
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32766
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32765
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32770
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32768  pjssge0ii 32284
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32769  pjdifnormii 32285
[Bobzien] p. 116Statement T3stoic3 1809
[Bobzien] p. 117Statement T2stoic2a 1807
[Bobzien] p. 117Statement T4stoic4a 1810
[Bobzien] p. 117Conclusion the contradictorystoic1a 1805
[Bogachev] p. 16Definition 1.5df-oms 34924
[Bogachev] p. 17Lemma 1.5.4omssubadd 34932
[Bogachev] p. 17Example 1.5.2omsmon 34930
[Bogachev] p. 41Definition 1.11.2df-carsg 34934
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34954
[Bogachev] p. 116Definition 2.3.1df-itgm 34985  df-sitm 34963
[Bogachev] p. 118Chapter 2.4.4df-itgm 34985
[Bogachev] p. 118Definition 2.4.1df-sitg 34962
[Bollobas] p. 1Section I.1df-edg 29626  isuhgrop 29648  isusgrop 29743  isuspgrop 29742
[Bollobas] p. 2Section I.1df-isubgr 48959  df-subgr 29849  uhgrspan1 29884  uhgrspansubgr 29872
[Bollobas] p. 3Definitiondf-gric 48979  gricuspgr 49016  isuspgrim 48994
[Bollobas] p. 3Section I.1cusgrsize 30035  df-clnbgr 48917  df-cusgr 29993  df-nbgr 29914  fusgrmaxsize 30045
[Bollobas] p. 4Definitiondf-upwlks 49232  df-wlks 30180
[Bollobas] p. 4Section I.1finsumvtxdg2size 30131  finsumvtxdgeven 30133  fusgr1th 30132  fusgrvtxdgonume 30135  vtxdgoddnumeven 30134
[Bollobas] p. 5Notationdf-pths 30299
[Bollobas] p. 5Definitiondf-crcts 30373  df-cycls 30374  df-trls 30275  df-wlkson 30181
[Bollobas] p. 7Section I.1df-ushgr 29637
[BourbakiAlg1] p. 1Definition 1df-clintop 49297  df-cllaw 49283  df-mgm 18816  df-mgm2 49316
[BourbakiAlg1] p. 4Definition 5df-assintop 49298  df-asslaw 49285  df-sgrp 18908  df-sgrp2 49318
[BourbakiAlg1] p. 7Definition 8df-cmgm2 49317  df-comlaw 49284
[BourbakiAlg1] p. 12Definition 2df-mnd 18924
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33587  mndlactf1o 33591  mndractf1 33589  mndractf1o 33592
[BourbakiAlg1] p. 92Definition 1df-ring 20461
[BourbakiAlg1] p. 93Section I.8.1df-rng 20375
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 34265
[BourbakiAlg2] p. 113Chapter 5.assafld 34269  assarrginv 34268
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34310  fldextrspunfld 34308  fldextrspunlem1 34307  fldextrspunlem2 34309  fldextrspunlsp 34306  fldextrspunlsplem 34305
[BourbakiCAlg2], p. 228Proposition 21arithidom 34069  dfufd2 34082
[BourbakiEns] p. Proposition 8fcof1 7295  fcofo 7296
[BourbakiTop1] p. Remarkxnegmnf 13340  xnegpnf 13339
[BourbakiTop1] p. Remark rexneg 13341
[BourbakiTop1] p. Remark 3ust0 24539  ustfilxp 24532
[BourbakiTop1] p. Axiom GT'tgpsubcn 24409
[BourbakiTop1] p. Criterionishmeo 24078
[BourbakiTop1] p. Example 1cstucnd 24602  iducn 24601  snfil 24183
[BourbakiTop1] p. Example 2neifil 24199
[BourbakiTop1] p. Theorem 1cnextcn 24386
[BourbakiTop1] p. Theorem 2ucnextcn 24622
[BourbakiTop1] p. Theorem 3df-hcmp 34589
[BourbakiTop1] p. Paragraph 3infil 24182
[BourbakiTop1] p. Definition 1df-ucn 24594  df-ust 24520  filintn0 24180  filn0 24181  istgp 24396  ucnprima 24600
[BourbakiTop1] p. Definition 2df-cfilu 24605
[BourbakiTop1] p. Definition 3df-cusp 24616  df-usp 24576  df-utop 24550  trust 24548
[BourbakiTop1] p. Definition 6df-pcmp 34488
[BourbakiTop1] p. Property V_issnei2 23434
[BourbakiTop1] p. Theorem 1(d)iscncl 23587
[BourbakiTop1] p. Condition F_Iustssel 24525
[BourbakiTop1] p. Condition U_Iustdiag 24528
[BourbakiTop1] p. Property V_iiinnei 23443
[BourbakiTop1] p. Property V_ivneiptopreu 23451  neissex 23445
[BourbakiTop1] p. Proposition 1neips 23431  neiss 23427  ucncn 24603  ustund 24541  ustuqtop 24565
[BourbakiTop1] p. Proposition 2cnpco 23585  neiptopreu 23451  utop2nei 24569  utop3cls 24570
[BourbakiTop1] p. Proposition 3fmucnd 24610  uspreg 24592  utopreg 24571
[BourbakiTop1] p. Proposition 4imasncld 24010  imasncls 24011  imasnopn 24009
[BourbakiTop1] p. Proposition 9cnpflf2 24319
[BourbakiTop1] p. Condition F_IIustincl 24527
[BourbakiTop1] p. Condition U_IIustinvel 24529
[BourbakiTop1] p. Property V_iiielnei 23429
[BourbakiTop1] p. Proposition 11cnextucn 24621
[BourbakiTop1] p. Condition F_IIbustbasel 24526
[BourbakiTop1] p. Condition U_IIIustexhalf 24530
[BourbakiTop1] p. Definition C'''df-cmp 23705
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 24165
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23212
[BourbakiTop2] p. 195Definition 1df-ldlf 34485
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 47072
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 47074  stoweid 47073
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 47011  stoweidlem10 47020  stoweidlem14 47024  stoweidlem15 47025  stoweidlem35 47045  stoweidlem36 47046  stoweidlem37 47047  stoweidlem38 47048  stoweidlem40 47050  stoweidlem41 47051  stoweidlem43 47053  stoweidlem44 47054  stoweidlem46 47056  stoweidlem5 47015  stoweidlem50 47060  stoweidlem52 47062  stoweidlem53 47063  stoweidlem55 47065  stoweidlem56 47066
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 47033  stoweidlem24 47034  stoweidlem27 47037  stoweidlem28 47038  stoweidlem30 47040
[BrosowskiDeutsh] p. 91Proofstoweidlem34 47044  stoweidlem59 47069  stoweidlem60 47070
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 47055  stoweidlem49 47059  stoweidlem7 47017
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 47041  stoweidlem39 47049  stoweidlem42 47052  stoweidlem48 47058  stoweidlem51 47061  stoweidlem54 47064  stoweidlem57 47067  stoweidlem58 47068
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 47035
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 47027
[BrosowskiDeutsh] p. 92Proofstoweidlem11 47021  stoweidlem13 47023  stoweidlem26 47036  stoweidlem61 47071
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 47028
[Bruck] p. 1Section I.1df-clintop 49297  df-mgm 18816  df-mgm2 49316
[Bruck] p. 23Section II.1df-sgrp 18908  df-sgrp2 49318
[Bruck] p. 28Theorem 3.2dfgrp3 19249
[ChoquetDD] p. 2Definition of mappingdf-mpt 5187
[Church] p. 129Section II.24df-ifp 1079  dfifp2 1080
[Clemente] p. 10Definition ITnatded 31004
[Clemente] p. 10Definition I` `m,nnatded 31004
[Clemente] p. 11Definition E=>m,nnatded 31004
[Clemente] p. 11Definition I=>m,nnatded 31004
[Clemente] p. 11Definition E` `(1)natded 31004
[Clemente] p. 11Definition E` `(2)natded 31004
[Clemente] p. 12Definition E` `m,n,pnatded 31004
[Clemente] p. 12Definition I` `n(1)natded 31004
[Clemente] p. 12Definition I` `n(2)natded 31004
[Clemente] p. 13Definition I` `m,n,pnatded 31004
[Clemente] p. 14Proof 5.11natded 31004
[Clemente] p. 14Definition E` `nnatded 31004
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 31006  ex-natded5.2 31005
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 31009  ex-natded5.3 31008
[Clemente] p. 18Theorem 5.5ex-natded5.5 31011
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 31013  ex-natded5.7 31012
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 31015  ex-natded5.8 31014
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 31017  ex-natded5.13 31016
[Clemente] p. 32Definition I` `nnatded 31004
[Clemente] p. 32Definition E` `m,n,p,anatded 31004
[Clemente] p. 32Definition E` `n,tnatded 31004
[Clemente] p. 32Definition I` `n,tnatded 31004
[Clemente] p. 43Theorem 9.20ex-natded9.20 31018
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 31019
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 31021  ex-natded9.26 31020
[Cohen] p. 301Remarkrelogoprlem 26919
[Cohen] p. 301Property 2relogmul 26920  relogmuld 26953
[Cohen] p. 301Property 3relogdiv 26921  relogdivd 26954
[Cohen] p. 301Property 4relogexp 26924
[Cohen] p. 301Property 1alog1 26913
[Cohen] p. 301Property 1bloge 26914
[Cohen4] p. 348Observationrelogbcxpb 27115
[Cohen4] p. 349Propertyrelogbf 27119
[Cohen4] p. 352Definitionelogb 27098
[Cohen4] p. 361Property 2relogbmul 27105
[Cohen4] p. 361Property 3logbrec 27110  relogbdiv 27107
[Cohen4] p. 361Property 4relogbreexp 27103
[Cohen4] p. 361Property 6relogbexp 27108
[Cohen4] p. 361Property 1(a)logbid1 27096
[Cohen4] p. 361Property 1(b)logb1 27097
[Cohen4] p. 367Propertylogbchbase 27099
[Cohen4] p. 377Property 2logblt 27112
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34917  sxbrsigalem4 34919
[Cohn] p. 81Section II.5acsdomd 18731  acsinfd 18730  acsinfdimd 18732  acsmap2d 18729  acsmapd 18728
[Cohn] p. 143Example 5.1.1sxbrsiga 34922
[Connell] p. 57Definitiondf-scmat 22806  df-scmatalt 49511
[Conway] p. 4Definitionlesrec 28185  lesrecd 28186
[Conway] p. 5Definitionaddsval 28348  addsval2 28349  df-adds 28346  df-muls 28493  df-negs 28407
[Conway] p. 7Theorem0lt1s 28198
[Conway] p. 12Theorem 12pw2cut2 28848
[Conway] p. 16Theorem 0(i)sltsright 28247
[Conway] p. 16Theorem 0(ii)sltsleft 28246
[Conway] p. 16Theorem 0(iii)lesid 28124
[Conway] p. 17Theorem 3addsass 28391  addsassd 28392  addscom 28352  addscomd 28353  addsrid 28350  addsridd 28351
[Conway] p. 17Definitiondf-0s 28193
[Conway] p. 17Theorem 4(ii)negnegs 28430
[Conway] p. 17Theorem 4(iii)negsid 28427  negsidd 28428
[Conway] p. 18Theorem 5leadds1 28375  leadds1d 28381
[Conway] p. 18Definitiondf-1s 28194
[Conway] p. 18Theorem 6(ii)negscl 28422  negscld 28423
[Conway] p. 18Theorem 6(iii)addscld 28366
[Conway] p. 19Notemulsunif2 28556
[Conway] p. 19Theorem 7addsdi 28541  addsdid 28542  addsdird 28543  mulnegs1d 28546  mulnegs2d 28547  mulsass 28552  mulsassd 28553  mulscom 28525  mulscomd 28526
[Conway] p. 19Theorem 8(i)mulscl 28520  mulscld 28521
[Conway] p. 19Theorem 8(iii)lemulsd 28524  ltmuls 28522  ltmulsd 28523
[Conway] p. 20Theorem 9mulsgt0 28530  mulsgt0d 28531
[Conway] p. 21Theorem 10(iv)precsex 28604
[Conway] p. 23Theorem 11eqcuts3 28190
[Conway] p. 24Definitiondf-reno 28876
[Conway] p. 24Theorem 13(ii)readdscl 28885  remulscl 28888  renegscl 28884
[Conway] p. 27Definitiondf-ons 28638  elons2 28644
[Conway] p. 27Theorem 14ltonsex 28648
[Conway] p. 28Theorem 15oncutlt 28650  onswe 28658
[Conway] p. 29Remarkmadebday 28286  newbday 28288  oldbday 28287
[Conway] p. 29Definitiondf-made 28213  df-new 28215  df-old 28214
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 14001
[Crawley] p. 1Definition of posetdf-poset 18487
[Crawley] p. 107Theorem 13.2hlsupr 40444
[Crawley] p. 110Theorem 13.3arglem1N 41248  dalaw 40944
[Crawley] p. 111Theorem 13.4hlathil 43019
[Crawley] p. 111Definition of set Wdf-watsN 41048
[Crawley] p. 111Definition of dilationdf-dilN 41164  df-ldil 41162  isldil 41168
[Crawley] p. 111Definition of translationdf-ltrn 41163  df-trnN 41165  isltrn 41177  ltrnu 41179
[Crawley] p. 112Lemma Acdlema1N 40849  cdlema2N 40850  exatleN 40462
[Crawley] p. 112Lemma B1cvrat 40534  cdlemb 40852  cdlemb2 41099  cdlemb3 41664  idltrn 41208  l1cvat 40113  lhpat 41101  lhpat2 41103  lshpat 40114  ltrnel 41197  ltrnmw 41209
[Crawley] p. 112Lemma Ccdlemc1 41249  cdlemc2 41250  ltrnnidn 41232  trlat 41227  trljat1 41224  trljat2 41225  trljat3 41226  trlne 41243  trlnidat 41231  trlnle 41244
[Crawley] p. 112Definition of automorphismdf-pautN 41049
[Crawley] p. 113Lemma Ccdlemc 41255  cdlemc3 41251  cdlemc4 41252
[Crawley] p. 113Lemma Dcdlemd 41265  cdlemd1 41256  cdlemd2 41257  cdlemd3 41258  cdlemd4 41259  cdlemd5 41260  cdlemd6 41261  cdlemd7 41262  cdlemd8 41263  cdlemd9 41264  cdleme31sde 41443  cdleme31se 41440  cdleme31se2 41441  cdleme31snd 41444  cdleme32a 41499  cdleme32b 41500  cdleme32c 41501  cdleme32d 41502  cdleme32e 41503  cdleme32f 41504  cdleme32fva 41495  cdleme32fva1 41496  cdleme32fvcl 41498  cdleme32le 41505  cdleme48fv 41557  cdleme4gfv 41565  cdleme50eq 41599  cdleme50f 41600  cdleme50f1 41601  cdleme50f1o 41604  cdleme50laut 41605  cdleme50ldil 41606  cdleme50lebi 41598  cdleme50rn 41603  cdleme50rnlem 41602  cdlemeg49le 41569  cdlemeg49lebilem 41597
[Crawley] p. 113Lemma Ecdleme 41618  cdleme00a 41267  cdleme01N 41279  cdleme02N 41280  cdleme0a 41269  cdleme0aa 41268  cdleme0b 41270  cdleme0c 41271  cdleme0cp 41272  cdleme0cq 41273  cdleme0dN 41274  cdleme0e 41275  cdleme0ex1N 41281  cdleme0ex2N 41282  cdleme0fN 41276  cdleme0gN 41277  cdleme0moN 41283  cdleme1 41285  cdleme10 41312  cdleme10tN 41316  cdleme11 41328  cdleme11a 41318  cdleme11c 41319  cdleme11dN 41320  cdleme11e 41321  cdleme11fN 41322  cdleme11g 41323  cdleme11h 41324  cdleme11j 41325  cdleme11k 41326  cdleme11l 41327  cdleme12 41329  cdleme13 41330  cdleme14 41331  cdleme15 41336  cdleme15a 41332  cdleme15b 41333  cdleme15c 41334  cdleme15d 41335  cdleme16 41343  cdleme16aN 41317  cdleme16b 41337  cdleme16c 41338  cdleme16d 41339  cdleme16e 41340  cdleme16f 41341  cdleme16g 41342  cdleme19a 41361  cdleme19b 41362  cdleme19c 41363  cdleme19d 41364  cdleme19e 41365  cdleme19f 41366  cdleme1b 41284  cdleme2 41286  cdleme20aN 41367  cdleme20bN 41368  cdleme20c 41369  cdleme20d 41370  cdleme20e 41371  cdleme20f 41372  cdleme20g 41373  cdleme20h 41374  cdleme20i 41375  cdleme20j 41376  cdleme20k 41377  cdleme20l 41380  cdleme20l1 41378  cdleme20l2 41379  cdleme20m 41381  cdleme20y 41360  cdleme20zN 41359  cdleme21 41395  cdleme21d 41388  cdleme21e 41389  cdleme22a 41398  cdleme22aa 41397  cdleme22b 41399  cdleme22cN 41400  cdleme22d 41401  cdleme22e 41402  cdleme22eALTN 41403  cdleme22f 41404  cdleme22f2 41405  cdleme22g 41406  cdleme23a 41407  cdleme23b 41408  cdleme23c 41409  cdleme26e 41417  cdleme26eALTN 41419  cdleme26ee 41418  cdleme26f 41421  cdleme26f2 41423  cdleme26f2ALTN 41422  cdleme26fALTN 41420  cdleme27N 41427  cdleme27a 41425  cdleme27cl 41424  cdleme28c 41430  cdleme3 41295  cdleme30a 41436  cdleme31fv 41448  cdleme31fv1 41449  cdleme31fv1s 41450  cdleme31fv2 41451  cdleme31id 41452  cdleme31sc 41442  cdleme31sdnN 41445  cdleme31sn 41438  cdleme31sn1 41439  cdleme31sn1c 41446  cdleme31sn2 41447  cdleme31so 41437  cdleme35a 41506  cdleme35b 41508  cdleme35c 41509  cdleme35d 41510  cdleme35e 41511  cdleme35f 41512  cdleme35fnpq 41507  cdleme35g 41513  cdleme35h 41514  cdleme35h2 41515  cdleme35sn2aw 41516  cdleme35sn3a 41517  cdleme36a 41518  cdleme36m 41519  cdleme37m 41520  cdleme38m 41521  cdleme38n 41522  cdleme39a 41523  cdleme39n 41524  cdleme3b 41287  cdleme3c 41288  cdleme3d 41289  cdleme3e 41290  cdleme3fN 41291  cdleme3fa 41294  cdleme3g 41292  cdleme3h 41293  cdleme4 41296  cdleme40m 41525  cdleme40n 41526  cdleme40v 41527  cdleme40w 41528  cdleme41fva11 41535  cdleme41sn3aw 41532  cdleme41sn4aw 41533  cdleme41snaw 41534  cdleme42a 41529  cdleme42b 41536  cdleme42c 41530  cdleme42d 41531  cdleme42e 41537  cdleme42f 41538  cdleme42g 41539  cdleme42h 41540  cdleme42i 41541  cdleme42k 41542  cdleme42ke 41543  cdleme42keg 41544  cdleme42mN 41545  cdleme42mgN 41546  cdleme43aN 41547  cdleme43bN 41548  cdleme43cN 41549  cdleme43dN 41550  cdleme5 41298  cdleme50ex 41617  cdleme50ltrn 41615  cdleme51finvN 41614  cdleme51finvfvN 41613  cdleme51finvtrN 41616  cdleme6 41299  cdleme7 41307  cdleme7a 41301  cdleme7aa 41300  cdleme7b 41302  cdleme7c 41303  cdleme7d 41304  cdleme7e 41305  cdleme7ga 41306  cdleme8 41308  cdleme8tN 41313  cdleme9 41311  cdleme9a 41309  cdleme9b 41310  cdleme9tN 41315  cdleme9taN 41314  cdlemeda 41356  cdlemedb 41355  cdlemednpq 41357  cdlemednuN 41358  cdlemefr27cl 41461  cdlemefr32fva1 41468  cdlemefr32fvaN 41467  cdlemefrs32fva 41458  cdlemefrs32fva1 41459  cdlemefs27cl 41471  cdlemefs32fva1 41481  cdlemefs32fvaN 41480  cdlemesner 41354  cdlemeulpq 41278
[Crawley] p. 114Lemma E4atex 41134  4atexlem7 41133  cdleme0nex 41348  cdleme17a 41344  cdleme17c 41346  cdleme17d 41556  cdleme17d1 41347  cdleme17d2 41553  cdleme18a 41349  cdleme18b 41350  cdleme18c 41351  cdleme18d 41353  cdleme4a 41297
[Crawley] p. 115Lemma Ecdleme21a 41383  cdleme21at 41386  cdleme21b 41384  cdleme21c 41385  cdleme21ct 41387  cdleme21f 41390  cdleme21g 41391  cdleme21h 41392  cdleme21i 41393  cdleme22gb 41352
[Crawley] p. 116Lemma Fcdlemf 41621  cdlemf1 41619  cdlemf2 41620
[Crawley] p. 116Lemma Gcdlemftr1 41625  cdlemg16 41715  cdlemg28 41762  cdlemg28a 41751  cdlemg28b 41761  cdlemg3a 41655  cdlemg42 41787  cdlemg43 41788  cdlemg44 41791  cdlemg44a 41789  cdlemg46 41793  cdlemg47 41794  cdlemg9 41692  ltrnco 41777  ltrncom 41796  tgrpabl 41809  trlco 41785
[Crawley] p. 116Definition of Gdf-tgrp 41801
[Crawley] p. 117Lemma Gcdlemg17 41735  cdlemg17b 41720
[Crawley] p. 117Definition of Edf-edring-rN 41814  df-edring 41815
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41818
[Crawley] p. 118Remarktendopltp 41838
[Crawley] p. 118Lemma Hcdlemh 41875  cdlemh1 41873  cdlemh2 41874
[Crawley] p. 118Lemma Icdlemi 41878  cdlemi1 41876  cdlemi2 41877
[Crawley] p. 118Lemma Jcdlemj1 41879  cdlemj2 41880  cdlemj3 41881  tendocan 41882
[Crawley] p. 118Lemma Kcdlemk 42032  cdlemk1 41889  cdlemk10 41901  cdlemk11 41907  cdlemk11t 42004  cdlemk11ta 41987  cdlemk11tb 41989  cdlemk11tc 42003  cdlemk11u-2N 41947  cdlemk11u 41929  cdlemk12 41908  cdlemk12u-2N 41948  cdlemk12u 41930  cdlemk13-2N 41934  cdlemk13 41910  cdlemk14-2N 41936  cdlemk14 41912  cdlemk15-2N 41937  cdlemk15 41913  cdlemk16-2N 41938  cdlemk16 41915  cdlemk16a 41914  cdlemk17-2N 41939  cdlemk17 41916  cdlemk18-2N 41944  cdlemk18-3N 41958  cdlemk18 41926  cdlemk19-2N 41945  cdlemk19 41927  cdlemk19u 42028  cdlemk1u 41917  cdlemk2 41890  cdlemk20-2N 41950  cdlemk20 41932  cdlemk21-2N 41949  cdlemk21N 41931  cdlemk22-3 41959  cdlemk22 41951  cdlemk23-3 41960  cdlemk24-3 41961  cdlemk25-3 41962  cdlemk26-3 41964  cdlemk26b-3 41963  cdlemk27-3 41965  cdlemk28-3 41966  cdlemk29-3 41969  cdlemk3 41891  cdlemk30 41952  cdlemk31 41954  cdlemk32 41955  cdlemk33N 41967  cdlemk34 41968  cdlemk35 41970  cdlemk36 41971  cdlemk37 41972  cdlemk38 41973  cdlemk39 41974  cdlemk39u 42026  cdlemk4 41892  cdlemk41 41978  cdlemk42 41999  cdlemk42yN 42002  cdlemk43N 42021  cdlemk45 42005  cdlemk46 42006  cdlemk47 42007  cdlemk48 42008  cdlemk49 42009  cdlemk5 41894  cdlemk50 42010  cdlemk51 42011  cdlemk52 42012  cdlemk53 42015  cdlemk54 42016  cdlemk55 42019  cdlemk55u 42024  cdlemk56 42029  cdlemk5a 41893  cdlemk5auN 41918  cdlemk5u 41919  cdlemk6 41895  cdlemk6u 41920  cdlemk7 41906  cdlemk7u-2N 41946  cdlemk7u 41928  cdlemk8 41896  cdlemk9 41897  cdlemk9bN 41898  cdlemki 41899  cdlemkid 41994  cdlemkj-2N 41940  cdlemkj 41921  cdlemksat 41904  cdlemksel 41903  cdlemksv 41902  cdlemksv2 41905  cdlemkuat 41924  cdlemkuel-2N 41942  cdlemkuel-3 41956  cdlemkuel 41923  cdlemkuv-2N 41941  cdlemkuv2-2 41943  cdlemkuv2-3N 41957  cdlemkuv2 41925  cdlemkuvN 41922  cdlemkvcl 41900  cdlemky 41984  cdlemkyyN 42020  tendoex 42033
[Crawley] p. 120Remarkdva1dim 42043
[Crawley] p. 120Lemma Lcdleml1N 42034  cdleml2N 42035  cdleml3N 42036  cdleml4N 42037  cdleml5N 42038  cdleml6 42039  cdleml7 42040  cdleml8 42041  cdleml9 42042  dia1dim 42119
[Crawley] p. 120Lemma Mdia11N 42106  diaf11N 42107  dialss 42104  diaord 42105  dibf11N 42219  djajN 42195
[Crawley] p. 120Definition of isomorphism mapdiaval 42090
[Crawley] p. 121Lemma Mcdlemm10N 42176  dia2dimlem1 42122  dia2dimlem2 42123  dia2dimlem3 42124  dia2dimlem4 42125  dia2dimlem5 42126  diaf1oN 42188  diarnN 42187  dvheveccl 42170  dvhopN 42174
[Crawley] p. 121Lemma Ncdlemn 42270  cdlemn10 42264  cdlemn11 42269  cdlemn11a 42265  cdlemn11b 42266  cdlemn11c 42267  cdlemn11pre 42268  cdlemn2 42253  cdlemn2a 42254  cdlemn3 42255  cdlemn4 42256  cdlemn4a 42257  cdlemn5 42259  cdlemn5pre 42258  cdlemn6 42260  cdlemn7 42261  cdlemn8 42262  cdlemn9 42263  diclspsn 42252
[Crawley] p. 121Definition of phi(q)df-dic 42231
[Crawley] p. 122Lemma Ndih11 42323  dihf11 42325  dihjust 42275  dihjustlem 42274  dihord 42322  dihord1 42276  dihord10 42281  dihord11b 42280  dihord11c 42282  dihord2 42285  dihord2a 42277  dihord2b 42278  dihord2cN 42279  dihord2pre 42283  dihord2pre2 42284  dihordlem6 42271  dihordlem7 42272  dihordlem7b 42273
[Crawley] p. 122Definition of isomorphism mapdihffval 42288  dihfval 42289  dihval 42290
[Diestel] p. 3Definitiondf-gric 48979  df-grim 48976  isuspgrim 48994
[Diestel] p. 3Section 1.1df-cusgr 29993  df-nbgr 29914
[Diestel] p. 3Definition by df-grisom 48975
[Diestel] p. 4Section 1.1df-isubgr 48959  df-subgr 29849  uhgrspan1 29884  uhgrspansubgr 29872
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 30135  vtxdgoddnumeven 30134
[Diestel] p. 27Section 1.10df-ushgr 29637
[EGA] p. 80Notation 1.1.1rspecval 34496
[EGA] p. 80Proposition 1.1.2zartop 34508
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34500  zarcls1 34501
[EGA] p. 81Corollary 1.1.8zart0 34511
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34514
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34517
[Eisenberg] p. 67Definition 5.3df-dif 3902
[Eisenberg] p. 82Definition 6.3dfom3 9648
[Eisenberg] p. 125Definition 8.21df-map 8849
[Eisenberg] p. 216Example 13.2(4)omenps 9656
[Eisenberg] p. 310Theorem 19.8cardprc 10061
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10639
[Enderton] p. 18Axiom of Empty Setaxnul 5259
[Enderton] p. 19Definitiondf-tp 4589
[Enderton] p. 26Exercise 5unissb 4901
[Enderton] p. 26Exercise 10pwel 5343
[Enderton] p. 28Exercise 7(b)pwun 5544
[Enderton] p. 30Theorem "Distributive laws"iinin1 5039  iinin2 5038  iinun2 5031  iunin1 5030  iunin1f 33152  iunin2 5029  uniin1 5033  uniin2 5034
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5037  iundif2 5032
[Enderton] p. 32Exercise 20unineq 4234
[Enderton] p. 33Exercise 23iinuni 5058
[Enderton] p. 33Exercise 25iununi 5059
[Enderton] p. 33Exercise 24(a)iinpw 5066
[Enderton] p. 33Exercise 24(b)iunpw 7785  iunpwss 5067
[Enderton] p. 36Definitionopthwiener 5487
[Enderton] p. 38Exercise 6(a)unipw 5418
[Enderton] p. 38Exercise 6(b)pwuni 4906
[Enderton] p. 41Lemma 3Dopeluu 5439  rnex 7922  rnexg 7914
[Enderton] p. 41Exercise 8dmuni 5896  rnuni 6140
[Enderton] p. 42Definition of a functiondffun7 6567  dffun8 6568
[Enderton] p. 43Definition of function valuefunfv2 6973
[Enderton] p. 43Definition of single-rootedfuncnv 6609
[Enderton] p. 44Definition (d)dfima2 6058  dfima3 6059
[Enderton] p. 47Theorem 3Hfvco2 6982
[Enderton] p. 49Axiom of Choice (first form)ac7 10551  ac7g 10552  df-ac 10195  dfac2 10210  dfac2a 10208  dfac2b 10209  dfac3 10200  dfac7 10211
[Enderton] p. 50Theorem 3K(a)imauni 7250
[Enderton] p. 52Definitiondf-map 8849
[Enderton] p. 53Exercise 21coass 6267
[Enderton] p. 53Exercise 27dmco 6256
[Enderton] p. 53Exercise 14(a)funin 6616
[Enderton] p. 53Exercise 22(a)imass2 6055
[Enderton] p. 54Remarkixpf 8948  ixpssmap 8960
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8926
[Enderton] p. 55Axiom of Choice (second form)ac9 10561  ac9s 10571
[Enderton] p. 56Theorem 3Meqvrelref 39627  erref 8738
[Enderton] p. 57Lemma 3Neqvrelthi 39630  erthi 8774
[Enderton] p. 57Definitiondf-ec 8719
[Enderton] p. 58Definitiondf-qs 8723
[Enderton] p. 61Exercise 35df-ec 8719
[Enderton] p. 65Exercise 56(a)dmun 5892
[Enderton] p. 68Definition of successordf-suc 6368
[Enderton] p. 71Definitiondf-tr 5213  dftr4 5218
[Enderton] p. 72Theorem 4Eunisuc 6444  unisucg 6443
[Enderton] p. 73Exercise 6unisuc 6444  unisucg 6443
[Enderton] p. 73Exercise 5(a)truni 5228
[Enderton] p. 73Exercise 5(b)trint 5230  trintALT 45863
[Enderton] p. 79Theorem 4I(A1)nna0 8613
[Enderton] p. 79Theorem 4I(A2)nnasuc 8615  onasuc 8536
[Enderton] p. 79Definition of operation valuedf-ov 7423
[Enderton] p. 80Theorem 4J(A1)nnm0 8614
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8616  onmsuc 8537
[Enderton] p. 81Theorem 4K(1)nnaass 8631
[Enderton] p. 81Theorem 4K(2)nna0r 8618  nnacom 8626
[Enderton] p. 81Theorem 4K(3)nndi 8632
[Enderton] p. 81Theorem 4K(4)nnmass 8633
[Enderton] p. 81Theorem 4K(5)nnmcom 8635
[Enderton] p. 82Exercise 16nnm0r 8619  nnmsucr 8634
[Enderton] p. 88Exercise 23nnaordex 8647
[Enderton] p. 129Definitiondf-en 8974
[Enderton] p. 132Theorem 6B(b)canth 7374
[Enderton] p. 133Exercise 1xpomen 10094
[Enderton] p. 133Exercise 2qnnen 16381
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9222
[Enderton] p. 135Corollary 6Cphp3 9224
[Enderton] p. 136Corollary 6Enneneq 9221
[Enderton] p. 136Corollary 6D(a)pssinf 9253
[Enderton] p. 136Corollary 6D(b)ominf 9255
[Enderton] p. 137Lemma 6Fpssnn 9184
[Enderton] p. 138Corollary 6Gssfi 9188
[Enderton] p. 139Theorem 6H(c)mapen 9160
[Enderton] p. 142Theorem 6I(3)xpdjuen 10258
[Enderton] p. 142Theorem 6I(4)mapdjuen 10259
[Enderton] p. 143Theorem 6Jdju0en 10254  dju1en 10250
[Enderton] p. 144Exercise 13iunfi 9332  unifi 9333  unifi2 9334
[Enderton] p. 144Corollary 6Kundif2 4431  unfi 9186  unfi2 9302
[Enderton] p. 145Figure 38ffoss 7958
[Enderton] p. 145Definitiondf-dom 8975
[Enderton] p. 146Example 1domen 8988  domeng 8989
[Enderton] p. 146Example 3nndomo 9233  nnsdom 9655  nnsdomg 9291
[Enderton] p. 149Theorem 6L(a)djudom2 10262
[Enderton] p. 149Theorem 6L(c)mapdom1 9161  xpdom1 9095  xpdom1g 9093  xpdom2g 9092
[Enderton] p. 149Theorem 6L(d)mapdom2 9167
[Enderton] p. 151Theorem 6Mzorn 10585  zorng 10582
[Enderton] p. 151Theorem 6M(4)ac8 10570  dfac5 10207
[Enderton] p. 159Theorem 6Qunictb 10660
[Enderton] p. 164Exampleinfdif 10286
[Enderton] p. 168Definitiondf-po 5559
[Enderton] p. 192Theorem 7M(a)oneli 6478
[Enderton] p. 192Theorem 7M(b)ontr1 6410
[Enderton] p. 192Theorem 7M(c)onirri 6477
[Enderton] p. 193Corollary 7N(b)0elon 6418
[Enderton] p. 193Corollary 7N(c)onsuci 7850
[Enderton] p. 193Corollary 7N(d)ssonunii 7795
[Enderton] p. 194Remarkonprc 7792
[Enderton] p. 194Exercise 16suc11 6472
[Enderton] p. 197Definitiondf-card 10020
[Enderton] p. 197Theorem 7Pcarden 10635
[Enderton] p. 200Exercise 25tfis 7866
[Enderton] p. 202Lemma 7Tr1tr 9783
[Enderton] p. 202Definitiondf-r1 9768
[Enderton] p. 202Theorem 7Qr1val1 9793
[Enderton] p. 204Theorem 7V(b)rankval4 9884  rankval4b 9880
[Enderton] p. 206Theorem 7X(b)en2lp 9607
[Enderton] p. 207Exercise 30rankpr 9871  rankprb 9865  rankpw 9856  rankpwi 9832  rankuniss 9883
[Enderton] p. 207Exercise 34opthreg 9619
[Enderton] p. 208Exercise 35suc11reg 9620
[Enderton] p. 212Definition of alephalephval3 10189
[Enderton] p. 213Theorem 8A(a)alephord2 10155
[Enderton] p. 213Theorem 8A(b)cardalephex 10169
[Enderton] p. 218Theorem Schema 8Eonfununi 8349
[Enderton] p. 222Definitiondf-kard 35818
[Enderton] p. 222Definition of kardkarden 9959  kardex 9957
[Enderton] p. 238Theorem 8Roeoa 8606
[Enderton] p. 238Theorem 8Soeoe 8608
[Enderton] p. 240Exercise 25oarec 8570
[Enderton] p. 257Definition of cofinalitycflm 10327
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17816
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17758
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18727  mrieqv2d 17813  mrieqvd 17812
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17817
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17822  mreexexlem2d 17819
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18733  mreexfidimd 17824
[Frege1879] p. 11Statementdf3or2 44768
[Frege1879] p. 12Statementdf3an2 44769  dfxor4 44766  dfxor5 44767
[Frege1879] p. 26Axiom 1ax-frege1 44790
[Frege1879] p. 26Axiom 2ax-frege2 44791
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44795
[Frege1879] p. 31Proposition 4frege4 44799
[Frege1879] p. 32Proposition 5frege5 44800
[Frege1879] p. 33Proposition 6frege6 44806
[Frege1879] p. 34Proposition 7frege7 44808
[Frege1879] p. 35Axiom 8ax-frege8 44809  axfrege8 44807
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38369
[Frege1879] p. 35Proposition 9frege9 44812
[Frege1879] p. 36Proposition 10frege10 44820
[Frege1879] p. 36Proposition 11frege11 44814
[Frege1879] p. 37Proposition 12frege12 44813
[Frege1879] p. 37Proposition 13frege13 44822
[Frege1879] p. 37Proposition 14frege14 44823
[Frege1879] p. 38Proposition 15frege15 44826
[Frege1879] p. 38Proposition 16frege16 44816
[Frege1879] p. 39Proposition 17frege17 44821
[Frege1879] p. 39Proposition 18frege18 44818
[Frege1879] p. 39Proposition 19frege19 44824
[Frege1879] p. 40Proposition 20frege20 44828
[Frege1879] p. 40Proposition 21frege21 44827
[Frege1879] p. 41Proposition 22frege22 44819
[Frege1879] p. 42Proposition 23frege23 44825
[Frege1879] p. 42Proposition 24frege24 44815
[Frege1879] p. 42Proposition 25frege25 44817  rp-frege25 44805
[Frege1879] p. 42Proposition 26frege26 44810
[Frege1879] p. 43Axiom 28ax-frege28 44830
[Frege1879] p. 43Proposition 27frege27 44811
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44831
[Frege1879] p. 44Axiom 31ax-frege31 44834  axfrege31 44833
[Frege1879] p. 44Proposition 30frege30 44832
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44835
[Frege1879] p. 44Proposition 33frege33 44836
[Frege1879] p. 45Proposition 34frege34 44837
[Frege1879] p. 45Proposition 35frege35 44838
[Frege1879] p. 45Proposition 36frege36 44839
[Frege1879] p. 46Proposition 37frege37 44840
[Frege1879] p. 46Proposition 38frege38 44841
[Frege1879] p. 46Proposition 39frege39 44842
[Frege1879] p. 46Proposition 40frege40 44843
[Frege1879] p. 47Axiom 41ax-frege41 44845  axfrege41 44844
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44846
[Frege1879] p. 47Proposition 43frege43 44847
[Frege1879] p. 47Proposition 44frege44 44848
[Frege1879] p. 47Proposition 45frege45 44849
[Frege1879] p. 48Proposition 46frege46 44850
[Frege1879] p. 48Proposition 47frege47 44851
[Frege1879] p. 49Proposition 48frege48 44852
[Frege1879] p. 49Proposition 49frege49 44853
[Frege1879] p. 49Proposition 50frege50 44854
[Frege1879] p. 50Axiom 52ax-frege52a 44857  ax-frege52c 44888  frege52aid 44858  frege52b 44889
[Frege1879] p. 50Axiom 54ax-frege54a 44862  ax-frege54c 44892  frege54b 44893
[Frege1879] p. 50Proposition 51frege51 44855
[Frege1879] p. 50Proposition 52dfsbcq 3741
[Frege1879] p. 50Proposition 53frege53a 44860  frege53aid 44859  frege53b 44890  frege53c 44914
[Frege1879] p. 50Proposition 54biid 264  eqid 2761
[Frege1879] p. 50Proposition 55frege55a 44868  frege55aid 44865  frege55b 44897  frege55c 44918  frege55cor1a 44869  frege55lem2a 44867  frege55lem2b 44896  frege55lem2c 44917
[Frege1879] p. 50Proposition 56frege56a 44871  frege56aid 44870  frege56b 44898  frege56c 44919
[Frege1879] p. 51Axiom 58ax-frege58a 44875  ax-frege58b 44901  frege58bid 44902  frege58c 44921
[Frege1879] p. 51Proposition 57frege57a 44873  frege57aid 44872  frege57b 44899  frege57c 44920
[Frege1879] p. 51Proposition 58spsbc 3752
[Frege1879] p. 51Proposition 59frege59a 44877  frege59b 44904  frege59c 44922
[Frege1879] p. 52Proposition 60frege60a 44878  frege60b 44905  frege60c 44923
[Frege1879] p. 52Proposition 61frege61a 44879  frege61b 44906  frege61c 44924
[Frege1879] p. 52Proposition 62frege62a 44880  frege62b 44907  frege62c 44925
[Frege1879] p. 52Proposition 63frege63a 44881  frege63b 44908  frege63c 44926
[Frege1879] p. 53Proposition 64frege64a 44882  frege64b 44909  frege64c 44927
[Frege1879] p. 53Proposition 65frege65a 44883  frege65b 44910  frege65c 44928
[Frege1879] p. 54Proposition 66frege66a 44884  frege66b 44911  frege66c 44929
[Frege1879] p. 54Proposition 67frege67a 44885  frege67b 44912  frege67c 44930
[Frege1879] p. 54Proposition 68frege68a 44886  frege68b 44913  frege68c 44931
[Frege1879] p. 55Definition 69dffrege69 44932
[Frege1879] p. 58Proposition 70frege70 44933
[Frege1879] p. 59Proposition 71frege71 44934
[Frege1879] p. 59Proposition 72frege72 44935
[Frege1879] p. 59Proposition 73frege73 44936
[Frege1879] p. 60Definition 76dffrege76 44939
[Frege1879] p. 60Proposition 74frege74 44937
[Frege1879] p. 60Proposition 75frege75 44938
[Frege1879] p. 62Proposition 77frege77 44940  frege77d 44746
[Frege1879] p. 63Proposition 78frege78 44941
[Frege1879] p. 63Proposition 79frege79 44942
[Frege1879] p. 63Proposition 80frege80 44943
[Frege1879] p. 63Proposition 81frege81 44944  frege81d 44747
[Frege1879] p. 64Proposition 82frege82 44945
[Frege1879] p. 65Proposition 83frege83 44946  frege83d 44748
[Frege1879] p. 65Proposition 84frege84 44947
[Frege1879] p. 66Proposition 85frege85 44948
[Frege1879] p. 66Proposition 86frege86 44949
[Frege1879] p. 66Proposition 87frege87 44950  frege87d 44750
[Frege1879] p. 67Proposition 88frege88 44951
[Frege1879] p. 68Proposition 89frege89 44952
[Frege1879] p. 68Proposition 90frege90 44953
[Frege1879] p. 68Proposition 91frege91 44954  frege91d 44751
[Frege1879] p. 69Proposition 92frege92 44955
[Frege1879] p. 70Proposition 93frege93 44956
[Frege1879] p. 70Proposition 94frege94 44957
[Frege1879] p. 70Proposition 95frege95 44958
[Frege1879] p. 71Definition 99dffrege99 44962
[Frege1879] p. 71Proposition 96frege96 44959  frege96d 44749
[Frege1879] p. 71Proposition 97frege97 44960  frege97d 44752
[Frege1879] p. 71Proposition 98frege98 44961  frege98d 44753
[Frege1879] p. 72Proposition 100frege100 44963
[Frege1879] p. 72Proposition 101frege101 44964
[Frege1879] p. 72Proposition 102frege102 44965  frege102d 44754
[Frege1879] p. 73Proposition 103frege103 44966
[Frege1879] p. 73Proposition 104frege104 44967
[Frege1879] p. 73Proposition 105frege105 44968
[Frege1879] p. 73Proposition 106frege106 44969  frege106d 44755
[Frege1879] p. 74Proposition 107frege107 44970
[Frege1879] p. 74Proposition 108frege108 44971  frege108d 44756
[Frege1879] p. 74Proposition 109frege109 44972  frege109d 44757
[Frege1879] p. 75Proposition 110frege110 44973
[Frege1879] p. 75Proposition 111frege111 44974  frege111d 44759
[Frege1879] p. 76Proposition 112frege112 44975
[Frege1879] p. 76Proposition 113frege113 44976
[Frege1879] p. 76Proposition 114frege114 44977  frege114d 44758
[Frege1879] p. 77Definition 115dffrege115 44978
[Frege1879] p. 77Proposition 116frege116 44979
[Frege1879] p. 78Proposition 117frege117 44980
[Frege1879] p. 78Proposition 118frege118 44981
[Frege1879] p. 78Proposition 119frege119 44982
[Frege1879] p. 78Proposition 120frege120 44983
[Frege1879] p. 79Proposition 121frege121 44984
[Frege1879] p. 79Proposition 122frege122 44985  frege122d 44760
[Frege1879] p. 79Proposition 123frege123 44986
[Frege1879] p. 80Proposition 124frege124 44987  frege124d 44761
[Frege1879] p. 81Proposition 125frege125 44988
[Frege1879] p. 81Proposition 126frege126 44989  frege126d 44762
[Frege1879] p. 82Proposition 127frege127 44990
[Frege1879] p. 83Proposition 128frege128 44991
[Frege1879] p. 83Proposition 129frege129 44992  frege129d 44763
[Frege1879] p. 84Proposition 130frege130 44993
[Frege1879] p. 85Proposition 131frege131 44994  frege131d 44764
[Frege1879] p. 86Proposition 132frege132 44995
[Frege1879] p. 86Proposition 133frege133 44996  frege133d 44765
[Fremlin1] p. 13Definition 111G (b)df-salgen 47323
[Fremlin1] p. 13Definition 111G (d)borelmbl 47646
[Fremlin1] p. 13Proposition 111G (b)salgenss 47346
[Fremlin1] p. 14Definition 112Aismea 47461
[Fremlin1] p. 15Remark 112B (d)psmeasure 47481
[Fremlin1] p. 15Property 112C (a)meadjun 47472  meadjunre 47486
[Fremlin1] p. 15Property 112C (b)meassle 47473
[Fremlin1] p. 15Property 112C (c)meaunle 47474
[Fremlin1] p. 16Property 112C (d)iundjiun 47470  meaiunle 47479  meaiunlelem 47478
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47491  meaiuninc2 47492  meaiuninc3 47495  meaiuninc3v 47494  meaiunincf 47493  meaiuninclem 47490
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47497  meaiininc2 47498  meaiininclem 47496
[Fremlin1] p. 19Theorem 113Ccaragen0 47516  caragendifcl 47524  caratheodory 47538  omelesplit 47528
[Fremlin1] p. 19Definition 113Aisome 47504  isomennd 47541  isomenndlem 47540
[Fremlin1] p. 19Remark 113B (c)omeunle 47526
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47545  voncmpl 47631
[Fremlin1] p. 19Definition 113A (ii)omessle 47508
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47533  carageniuncllem1 47531  carageniuncllem2 47532  caragenuncl 47523  caragenuncllem 47522  caragenunicl 47534
[Fremlin1] p. 21Remark 113Dcaragenel2d 47542
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47536  caratheodorylem2 47537
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47545
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47604  hoidmv1lelem1 47601  hoidmv1lelem2 47602  hoidmv1lelem3 47603
[Fremlin1] p. 25Definition 114Eisvonmbl 47648
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47604  hoidmvle 47610  hoidmvlelem1 47605  hoidmvlelem2 47606  hoidmvlelem3 47607  hoidmvlelem4 47608  hoidmvlelem5 47609  hsphoidmvle2 47595  hsphoif 47586  hsphoival 47589
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47558
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47566
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47593  hoidmvn0val 47594  hoidmvval 47587  hoidmvval0 47597  hoidmvval0b 47600
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47598  hsphoidmvle 47596
[Fremlin1] p. 30Definition 115Cdf-ovoln 47547  df-voln 47549
[Fremlin1] p. 30Proposition 115D (a)dmovn 47614  ovn0 47576  ovn0lem 47575  ovnf 47573  ovnome 47583  ovnssle 47571  ovnsslelem 47570  ovnsupge0 47567
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47613  ovnhoilem1 47611  ovnhoilem2 47612  vonhoi 47677
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47630  hoidifhspf 47628  hoidifhspval 47618  hoidifhspval2 47625  hoidifhspval3 47629  hspmbl 47639  hspmbllem1 47636  hspmbllem2 47637  hspmbllem3 47638
[Fremlin1] p. 31Definition 115Evoncmpl 47631  vonmea 47584
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47582  ovnsubadd2 47656  ovnsubadd2lem 47655  ovnsubaddlem1 47580  ovnsubaddlem2 47581
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47641  hoimbl2 47675  hoimbllem 47640  hspdifhsp 47626  opnvonmbl 47644  opnvonmbllem2 47643
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47646
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47689  iccvonmbllem 47688  ioovonmbl 47687
[Fremlin1] p. 32Proposition 115G (d)vonicc 47695  vonicclem2 47694  vonioo 47692  vonioolem2 47691  vonn0icc 47698  vonn0icc2 47702  vonn0ioo 47697  vonn0ioo2 47700
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47699  snvonmbl 47696  vonct 47703  vonsn 47701
[Fremlin1] p. 35Lemma 121Asubsalsal 47369
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47368  subsaliuncllem 47367
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47735  salpreimalegt 47719  salpreimaltle 47736
[Fremlin1] p. 35Proposition 121B (i)issmf 47738  issmff 47744  issmflem 47737
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47755  issmflelem 47754  smfpreimale 47764
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47766  issmfgtlem 47765
[Fremlin1] p. 36Definition 121Cdf-smblfn 47706  issmf 47738  issmff 47744  issmfge 47780  issmfgelem 47779  issmfgt 47766  issmfgtlem 47765  issmfle 47755  issmflelem 47754  issmflem 47737
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47717  salpreimagtlt 47740  salpreimalelt 47739
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47780  issmfgelem 47779
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47763
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47761  cnfsmf 47750
[Fremlin1] p. 36Proposition 121D (c)decsmf 47777  decsmflem 47776  incsmf 47752  incsmflem 47751
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47711  pimconstlt1 47712  smfconst 47759
[Fremlin1] p. 37Proposition 121E (b)smfadd 47775  smfaddlem1 47773  smfaddlem2 47774
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47806
[Fremlin1] p. 37Proposition 121E (d)smfmul 47805  smfmullem1 47801  smfmullem2 47802  smfmullem3 47803  smfmullem4 47804
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47807
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47810  smfpimbor1lem2 47809
[Fremlin1] p. 37Proposition 121E (g)smfco 47812
[Fremlin1] p. 37Proposition 121E (h)smfres 47800
[Fremlin1] p. 38Proposition 121E (e)smfrec 47799
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47808  smfresal 47798
[Fremlin1] p. 38Proposition 121F (a)smflim 47787  smflim2 47816  smflimlem1 47781  smflimlem2 47782  smflimlem3 47783  smflimlem4 47784  smflimlem5 47785  smflimlem6 47786  smflimmpt 47820
[Fremlin1] p. 38Proposition 121F (b)smfsup 47824  smfsuplem1 47821  smfsuplem2 47822  smfsuplem3 47823  smfsupmpt 47825  smfsupxr 47826
[Fremlin1] p. 38Proposition 121F (c)smfinf 47828  smfinflem 47827  smfinfmpt 47829
[Fremlin1] p. 39Remark 121Gsmflim 47787  smflim2 47816  smflimmpt 47820
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47818
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47848  smfdivdmmbl2 47851  smfinfdmmbl 47859  smfinfdmmbllem 47858  smfsupdmmbl 47855  smfsupdmmbllem 47854
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47838  smflimsuplem2 47831  smflimsuplem6 47835  smflimsuplem7 47836  smflimsuplem8 47837  smflimsupmpt 47839
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47841  smfliminflem 47840  smfliminfmpt 47842
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47706
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47852  fsupdm2 47853
[Fremlin1], p. 39Proposition 121Hadddmmbl 47843  adddmmbl2 47844  finfdm 47856  finfdm2 47857  fsupdm 47852  fsupdm2 47853  muldmmbl 47845  muldmmbl2 47846
[Fremlin1], p. 39Proposition 121F (c)finfdm 47856  finfdm2 47857
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25857
[Fremlin5] p. 213Lemma 565Cauniioovol 25900
[Fremlin5] p. 214Lemma 565Cauniioombl 25910
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38617
[Fremlin5] p. 220Theorem 565Maftc1anc 38620
[FreydScedrov] p. 283Axiom of Infinityax-inf 9639  inf1 9623  inf2 9624
[Gleason] p. 117Proposition 9-2.1df-enq 10996  enqer 11006
[Gleason] p. 117Proposition 9-2.2df-1nq 11001  df-nq 10997
[Gleason] p. 117Proposition 9-2.3df-plpq 10993  df-plq 10999
[Gleason] p. 119Proposition 9-2.4caovmo 7658  df-mpq 10994  df-mq 11000
[Gleason] p. 119Proposition 9-2.5df-rq 11002
[Gleason] p. 119Proposition 9-2.6ltexnq 11060
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11061  ltbtwnnq 11063
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11056
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11057
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11064
[Gleason] p. 121Definition 9-3.1df-np 11066
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11078
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11080
[Gleason] p. 122Definitiondf-1p 11067
[Gleason] p. 122Remark (1)prub 11079
[Gleason] p. 122Lemma 9-3.4prlem934 11118
[Gleason] p. 122Proposition 9-3.2df-ltp 11070
[Gleason] p. 122Proposition 9-3.3ltsopr 11117  psslinpr 11116  supexpr 11139  suplem1pr 11137  suplem2pr 11138
[Gleason] p. 123Proposition 9-3.5addclpr 11103  addclprlem1 11101  addclprlem2 11102  df-plp 11068
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11107
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11106
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11119
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11128  ltexprlem1 11121  ltexprlem2 11122  ltexprlem3 11123  ltexprlem4 11124  ltexprlem5 11125  ltexprlem6 11126  ltexprlem7 11127
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11130  ltaprlem 11129
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11131
[Gleason] p. 124Lemma 9-3.6prlem936 11132
[Gleason] p. 124Proposition 9-3.7df-mp 11069  mulclpr 11105  mulclprlem 11104  reclem2pr 11133
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11114
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11109
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11108
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11113
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11136  reclem3pr 11134  reclem4pr 11135
[Gleason] p. 126Proposition 9-4.1df-enr 11140  enrer 11148
[Gleason] p. 126Proposition 9-4.2df-0r 11145  df-1r 11146  df-nr 11141
[Gleason] p. 126Proposition 9-4.3df-mr 11143  df-plr 11142  negexsr 11187  recexsr 11192  recexsrlem 11188
[Gleason] p. 127Proposition 9-4.4df-ltr 11144
[Gleason] p. 130Proposition 10-1.3creui 12315  creur 12314  cru 12312
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11273  axcnre 11249
[Gleason] p. 132Definition 10-3.1crim 15282  crimd 15399  crimi 15360  crre 15281  crred 15398  crrei 15359
[Gleason] p. 132Definition 10-3.2remim 15284  remimd 15365
[Gleason] p. 133Definition 10.36absval2 15451  absval2d 15615  absval2i 15565
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15308  cjaddd 15387  cjaddi 15355
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15309  cjmuld 15388  cjmuli 15356
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15307  cjcjd 15366  cjcji 15338
[Gleason] p. 133Proposition 10-3.4(f)cjre 15306  cjreb 15290  cjrebd 15369  cjrebi 15341  cjred 15393  rere 15289  rereb 15287  rerebd 15368  rerebi 15340  rered 15391
[Gleason] p. 133Proposition 10-3.4(h)addcj 15315  addcjd 15379  addcji 15350
[Gleason] p. 133Proposition 10-3.7(a)absval 15405
[Gleason] p. 133Proposition 10-3.7(b)abscj 15446  abscjd 15620  abscji 15569
[Gleason] p. 133Proposition 10-3.7(c)abs00 15456  abs00d 15616  abs00i 15566  absne0d 15617
[Gleason] p. 133Proposition 10-3.7(d)releabs 15489  releabsd 15621  releabsi 15570
[Gleason] p. 133Proposition 10-3.7(f)absmul 15461  absmuld 15624  absmuli 15572
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15449  sqabsaddi 15573
[Gleason] p. 133Proposition 10-3.7(h)abstri 15498  abstrid 15626  abstrii 15576
[Gleason] p. 134Definition 10-4.1df-exp 14205  exp0 14208  expp1 14211  expp1d 14290
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 27007  cxpaddd 27045  expadd 14247  expaddd 14291  expaddz 14249
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 27016  cxpmuld 27065  expmul 14250  expmuld 14292  expmulz 14251
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 27013  mulcxpd 27056  mulexp 14244  mulexpd 14304  mulexpz 14245
[Gleason] p. 140Exercise 1znnen 16380
[Gleason] p. 141Definition 11-2.1fzval 13641
[Gleason] p. 168Proposition 12-2.1(a)climadd 15799  rlimadd 15810  rlimdiv 15813
[Gleason] p. 168Proposition 12-2.1(b)climsub 15801  rlimsub 15811
[Gleason] p. 168Proposition 12-2.1(c)climmul 15800  rlimmul 15812
[Gleason] p. 171Corollary 12-2.2climmulc2 15804
[Gleason] p. 172Corollary 12-2.5climrecl 15750
[Gleason] p. 172Proposition 12-2.4(c)climabs 15771  climcj 15772  climim 15774  climre 15773  rlimabs 15776  rlimcj 15777  rlimim 15779  rlimre 15778
[Gleason] p. 173Definition 12-3.1df-ltxr 11348  df-xr 11347  ltxr 13244
[Gleason] p. 175Definition 12-4.1df-limsup 15638  limsupval 15641
[Gleason] p. 180Theorem 12-5.1climsup 15837
[Gleason] p. 180Theorem 12-5.3caucvg 15846  caucvgb 15847  caucvgbf 46499  caucvgr 15843  climcau 15838
[Gleason] p. 182Exercise 3cvgcmp 15983
[Gleason] p. 182Exercise 4cvgrat 16052
[Gleason] p. 195Theorem 13-2.12abs1m 15503
[Gleason] p. 217Lemma 13-4.1btwnzge0 13968
[Gleason] p. 223Definition 14-1.1df-met 21672
[Gleason] p. 223Definition 14-1.1(a)met0 24662  xmet0 24661
[Gleason] p. 223Definition 14-1.1(b)metgt0 24678
[Gleason] p. 223Definition 14-1.1(c)metsym 24669
[Gleason] p. 223Definition 14-1.1(d)mettri 24671  mstri 24788  xmettri 24670  xmstri 24787
[Gleason] p. 225Definition 14-1.5xpsmet 24701
[Gleason] p. 230Proposition 14-2.6txlm 23967
[Gleason] p. 240Theorem 14-4.3metcnp4 25631
[Gleason] p. 240Proposition 14-4.2metcnp3 24859
[Gleason] p. 243Proposition 14-4.16addcn 25185  addcn2 15761  mulcn 25187  mulcn2 15763  subcn 25186  subcn2 15762
[Gleason] p. 295Remarkbcval3 14450  bcval4 14451
[Gleason] p. 295Equation 2bcpasc 14465
[Gleason] p. 295Definition of binomial coefficientbcval 14448  df-bc 14447
[Gleason] p. 296Remarkbcn0 14454  bcnn 14456
[Gleason] p. 296Theorem 15-2.8binom 15999
[Gleason] p. 308Equation 2ef0 16257
[Gleason] p. 308Equation 3efcj 16258
[Gleason] p. 309Corollary 15-4.3efne0 16264
[Gleason] p. 309Corollary 15-4.4efexp 16269
[Gleason] p. 310Equation 14sinadd 16332
[Gleason] p. 310Equation 15cosadd 16333
[Gleason] p. 311Equation 17sincossq 16344
[Gleason] p. 311Equation 18cosbnd 16349  sinbnd 16348
[Gleason] p. 311Lemma 15-4.7sqeqor 14360  sqeqori 14358
[Gleason] p. 311Definition of ` `df-pi 16238
[Godowski] p. 730Equation SFgoeqi 32875
[GodowskiGreechie] p. 249Equation IV3oai 32270
[Golan] p. 1Remarksrgisid 20435
[Golan] p. 1Definitiondf-srg 20413
[Golan] p. 149Definitiondf-slmd 33762
[Gonshor] p. 7Definitiondf-cuts 28146
[Gonshor] p. 9Theorem 2.5lesrec 28185  lesrecd 28186
[Gonshor] p. 10Theorem 2.6cofcut1 28306  cofcut1d 28307
[Gonshor] p. 10Theorem 2.7cofcut2 28308  cofcut2d 28309
[Gonshor] p. 12Theorem 2.9cofcutr 28310  cofcutr1d 28311  cofcutr2d 28312
[Gonshor] p. 13Definitiondf-adds 28346
[Gonshor] p. 14Theorem 3.1addsprop 28362
[Gonshor] p. 15Theorem 3.2addsunif 28388
[Gonshor] p. 17Theorem 3.4mulsprop 28516
[Gonshor] p. 18Theorem 3.5mulsunif 28536
[Gonshor] p. 28Lemma 4.2halfcut 28844
[Gonshor] p. 28Theorem 4.2pw2cut 28846
[Gonshor] p. 30Theorem 4.2addhalfcut 28845
[Gonshor] p. 39Theorem 4.4(b)elreno2 28881
[Gonshor] p. 95Theorem 6.1addbday 28404
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36924
[Gratzer] p. 23Section 0.6df-mre 17756
[Gratzer] p. 27Section 0.6df-mri 17758
[Hall] p. 1Section 1.1df-asslaw 49285  df-cllaw 49283  df-comlaw 49284
[Hall] p. 2Section 1.2df-clintop 49297
[Hall] p. 7Section 1.3df-sgrp2 49318
[Halmos] p. 28Partition ` `df-parts 39801  dfmembpart2 39806
[Halmos] p. 31Theorem 17.3riesz1 32667  riesz2 32668
[Halmos] p. 41Definition of Hermitianhmopadj2 32543
[Halmos] p. 42Definition of projector orderingpjordi 32775
[Halmos] p. 43Theorem 26.1elpjhmop 32787  elpjidm 32786  pjnmopi 32750
[Halmos] p. 44Remarkpjinormi 32289  pjinormii 32278
[Halmos] p. 44Theorem 26.2elpjch 32791  pjrn 32309  pjrni 32304  pjvec 32298
[Halmos] p. 44Theorem 26.3pjnorm2 32329
[Halmos] p. 44Theorem 26.4hmopidmpj 32756  hmopidmpji 32754
[Halmos] p. 45Theorem 27.1pjinvari 32793
[Halmos] p. 45Theorem 27.3pjoci 32782  pjocvec 32299
[Halmos] p. 45Theorem 27.4pjorthcoi 32771
[Halmos] p. 48Theorem 29.2pjssposi 32774
[Halmos] p. 48Theorem 29.3pjssdif1i 32777  pjssdif2i 32776
[Halmos] p. 50Definition of spectrumdf-spec 32457
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 24
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1828
[Hatcher] p. 25Definitiondf-phtpc 25313  df-phtpy 25292
[Hatcher] p. 26Definitiondf-pco 25326  df-pi1 25329
[Hatcher] p. 26Proposition 1.2phtpcer 25316
[Hatcher] p. 26Proposition 1.3pi1grp 25371
[Hefferon] p. 240Definition 3.12df-dmat 22805  df-dmatalt 49510
[Helfgott] p. 2Theoremtgoldbach 48915
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48900
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48912  bgoldbtbnd 48907  bgoldbtbnd 48907  tgblthelfgott 48913
[Helfgott] p. 5Proposition 1.1circlevma 35271
[Helfgott] p. 69Statement 7.49circlemethhgt 35272
[Helfgott] p. 69Statement 7.50hgt750lema 35286  hgt750lemb 35285  hgt750leme 35287  hgt750lemf 35282  hgt750lemg 35283
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48909  tgoldbachgt 35292  tgoldbachgtALTV 48910  tgoldbachgtd 35291
[Helfgott] p. 70Statement 7.49ax-hgt749 35273
[Herstein] p. 54Exercise 28df-grpo 31095
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19155  grpoideu 31111  mndideu 18934
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19185  grpoinveu 31121
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19216  grpo2inv 31133
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19228  grpoinvop 31135
[Herstein] p. 57Exercise 1dfgrp3e 19250
[Hitchcock] p. 5Rule A3mptnan 1801
[Hitchcock] p. 5Rule A4mptxor 1802
[Hitchcock] p. 5Rule A5mtpxor 1804
[Holland] p. 1519Theorem 2sumdmdi 33022
[Holland] p. 1520Lemma 5cdj1i 33035  cdj3i 33043  cdj3lem1 33036  cdjreui 33034
[Holland] p. 1524Lemma 7mddmdin0i 33033
[Holland95] p. 13Theorem 3.6hlathil 43019
[Holland95] p. 14Line 15hgmapvs 42949
[Holland95] p. 14Line 16hdmaplkr 42971
[Holland95] p. 14Line 17hdmapellkr 42972
[Holland95] p. 14Line 19hdmapglnm2 42969
[Holland95] p. 14Line 20hdmapip0com 42975
[Holland95] p. 14Theorem 3.6hdmapevec2 42894
[Holland95] p. 14Lines 24 and 25hdmapoc 42989
[Holland95] p. 204Definition of involutiondf-srng 21097
[Holland95] p. 212Definition of subspacedf-psubsp 40561
[Holland95] p. 214Lemma 3.3lclkrlem2v 42586
[Holland95] p. 214Definition 3.2df-lpolN 42539
[Holland95] p. 214Definition of nonsingularpnonsingN 40991
[Holland95] p. 215Lemma 3.3(1)dihoml4 42435  poml4N 41011
[Holland95] p. 215Lemma 3.3(2)dochexmid 42526  pexmidALTN 41036  pexmidN 41027
[Holland95] p. 218Theorem 3.6lclkr 42591
[Holland95] p. 218Definition of dual vector spacedf-ldual 40182  ldualset 40183
[Holland95] p. 222Item 1df-lines 40559  df-pointsN 40560
[Holland95] p. 222Item 2df-polarityN 40961
[Holland95] p. 223Remarkispsubcl2N 41005  omllaw4 40304  pol1N 40968  polcon3N 40975
[Holland95] p. 223Definitiondf-psubclN 40993
[Holland95] p. 223Equation for polaritypolval2N 40964
[Holmes] p. 40Definitiondf-xrn 39313
[Hughes] p. 44Equation 1.21bax-his3 31686
[Hughes] p. 47Definition of projection operatordfpjop 32784
[Hughes] p. 49Equation 1.30eighmre 32565  eigre 32437  eigrei 32436
[Hughes] p. 49Equation 1.31eighmorth 32566  eigorth 32440  eigorthi 32439
[Hughes] p. 137Remark (ii)eigposi 32438
[Huneke] p. 1Claim 1frgrncvvdeq 30910
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30906
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30907
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30908
[Huneke] p. 2Claim 2frgrregorufr 30926  frgrregorufr0 30925  frgrregorufrg 30927
[Huneke] p. 2Claim 3frgrhash2wsp 30933  frrusgrord 30942  frrusgrord0 30941
[Huneke] p. 2Statementdf-clwwlknon 30679
[Huneke] p. 2Statement 4frgrwopreglem4 30916
[Huneke] p. 2Statement 5frgrwopreg1 30919  frgrwopreg2 30920  frgrwopregasn 30917  frgrwopregbsn 30918
[Huneke] p. 2Statement 6frgrwopreglem5 30922
[Huneke] p. 2Statement 7fusgreghash2wspv 30936
[Huneke] p. 2Statement 8fusgreghash2wsp 30939
[Huneke] p. 2Statement 9clwlksndivn 30677  numclwlk1 30972  numclwlk1lem1 30970  numclwlk1lem2 30971  numclwwlk1 30962  numclwwlk8 30993
[Huneke] p. 2Definition 3frgrwopreglem1 30913
[Huneke] p. 2Definition 4df-clwlks 30358
[Huneke] p. 2Definition 62clwwlk 30948
[Huneke] p. 2Definition 7numclwwlkovh 30974  numclwwlkovh0 30973
[Huneke] p. 2Statement 10numclwwlk2 30982
[Huneke] p. 2Statement 11rusgrnumwlkg 30569
[Huneke] p. 2Statement 12numclwwlk3 30986
[Huneke] p. 2Statement 13numclwwlk5 30989
[Huneke] p. 2Statement 14numclwwlk7 30992
[Indrzejczak] p. 33Definition ` `Enatded 31004  natded 31004
[Indrzejczak] p. 33Definition ` `Inatded 31004
[Indrzejczak] p. 34Definition ` `Enatded 31004  natded 31004
[Indrzejczak] p. 34Definition ` `Inatded 31004
[Jech] p. 4Definition of classcv 1569  cvjust 2755
[Jech] p. 42Lemma 6.1alephexp1 10664
[Jech] p. 42Equation 6.1alephadd 10662  alephmul 10663
[Jech] p. 43Lemma 6.2infmap 10661  infmap2 10295
[Jech] p. 71Lemma 9.3jech9.3 9822
[Jech] p. 72Equation 9.3df-scott 9929
[Jech] p. 72Exercise 9.1rankval4 9884  rankval4b 9880
[Jech] p. 72Scheme "Collection Principle"cp 9954
[Jech] p. 78Noteopthprc 5715
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43922
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 44010
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 44011
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43934
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43938
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43939  rmyp1 43940
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43941  rmym1 43942
[JonesMatijasevic] p. 695Equation 2.11rmx0 43932  rmx1 43933  rmxluc 43943
[JonesMatijasevic] p. 695Equation 2.12rmy0 43936  rmy1 43937  rmyluc 43944
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43946
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43947
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43967  jm2.17b 43968  jm2.17c 43969
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 44000
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 44004
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43995
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43970  jm2.24nn 43966
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 44009
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 44015  rmygeid 43971
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 44027
[Juillerat] p. 11Section *5etransc 47293  etransclem47 47291  etransclem48 47292
[Juillerat] p. 12Equation (7)etransclem44 47288
[Juillerat] p. 12Equation *(7)etransclem46 47290
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 47276
[Juillerat] p. 13Proofetransclem35 47279
[Juillerat] p. 13Part of case 2 proven inetransclem38 47282
[Juillerat] p. 13Part of case 2 provenetransclem24 47268
[Juillerat] p. 13Part of case 2: proven inetransclem41 47285
[Juillerat] p. 14Proofetransclem23 47267
[KalishMontague] p. 81Note 1ax-6 2000
[KalishMontague] p. 85Lemma 2equid 2045
[KalishMontague] p. 85Lemma 3equcomi 2050
[KalishMontague] p. 86Lemma 7cbvalivw 2040  cbvaliw 2039  wl-cbvmotv 38446  wl-motae 38448  wl-moteq 38447
[KalishMontague] p. 87Lemma 8spimvw 2019  spimw 2003
[KalishMontague] p. 87Lemma 9spfw 2066  spw 2067
[Kalmbach] p. 14Definition of latticechabs1 32118  chabs1i 32120  chabs2 32119  chabs2i 32121  chjass 32135  chjassi 32088  latabs1 18649  latabs2 18650
[Kalmbach] p. 15Definition of atomdf-at 32940  ela 32941
[Kalmbach] p. 15Definition of coverscvbr2 32885  cvrval2 40332
[Kalmbach] p. 16Definitiondf-ol 40236  df-oml 40237
[Kalmbach] p. 20Definition of commutescmbr 32186  cmbri 32192  cmtvalN 40269  df-cm 32185  df-cmtN 40235
[Kalmbach] p. 22Remarkomllaw5N 40305  pjoml5 32215  pjoml5i 32190
[Kalmbach] p. 22Definitionpjoml2 32213  pjoml2i 32187
[Kalmbach] p. 22Theorem 2(v)cmcm 32216  cmcmi 32194  cmcmii 32199  cmtcomN 40307
[Kalmbach] p. 22Theorem 2(ii)omllaw3 40303  omlsi 32006  pjoml 32038  pjomli 32037
[Kalmbach] p. 22Definition of OML lawomllaw2N 40302
[Kalmbach] p. 23Remarkcmbr2i 32198  cmcm3 32217  cmcm3i 32196  cmcm3ii 32201  cmcm4i 32197  cmt3N 40309  cmt4N 40310  cmtbr2N 40311
[Kalmbach] p. 23Lemma 3cmbr3 32210  cmbr3i 32202  cmtbr3N 40312
[Kalmbach] p. 25Theorem 5fh1 32220  fh1i 32223  fh2 32221  fh2i 32224  omlfh1N 40316
[Kalmbach] p. 65Remarkchjatom 32959  chslej 32100  chsleji 32060  shslej 31982  shsleji 31972
[Kalmbach] p. 65Proposition 1chocin 32097  chocini 32056  chsupcl 31942  chsupval2 32012  h0elch 31857  helch 31845  hsupval2 32011  ocin 31898  ococss 31895  shococss 31896
[Kalmbach] p. 65Definition of subspace sumshsval 31914
[Kalmbach] p. 66Remarkdf-pjh 31997  pjssmi 32767  pjssmii 32283
[Kalmbach] p. 67Lemma 3osum 32247  osumi 32244
[Kalmbach] p. 67Lemma 4pjci 32802
[Kalmbach] p. 103Exercise 6atmd2 33002
[Kalmbach] p. 103Exercise 12mdsl0 32912
[Kalmbach] p. 140Remarkhatomic 32962  hatomici 32961  hatomistici 32964
[Kalmbach] p. 140Proposition 1atlatmstc 40377
[Kalmbach] p. 140Proposition 1(i)atexch 32983  lsatexch 40101
[Kalmbach] p. 140Proposition 1(ii)chcv1 32957  cvlcvr1 40397  cvr1 40468
[Kalmbach] p. 140Proposition 1(iii)cvexch 32976  cvexchi 32971  cvrexch 40478
[Kalmbach] p. 149Remark 2chrelati 32966  hlrelat 40460  hlrelat5N 40459  lrelat 40072
[Kalmbach] p. 153Exercise 5lsmcv 21419  lsmsatcv 40068  spansncv 32255  spansncvi 32254
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 40087  spansncv2 32895
[Kalmbach] p. 266Definitiondf-st 32813
[Kalmbach2] p. 8Definition of adjointdf-adjh 32451
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10731  fpwwe2 10728
[KanamoriPincus] p. 416Corollary 1.3canth4 10732
[KanamoriPincus] p. 417Corollary 1.6canthp1 10739
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10734
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10736
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10749
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10753  gchxpidm 10754
[KanamoriPincus] p. 419Theorem 2.1gchacg 10765  gchhar 10764
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10293  unxpwdom 9583
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10755
[Kreyszig] p. 3Property M1metcl 24651  xmetcl 24650
[Kreyszig] p. 4Property M2meteq0 24658
[Kreyszig] p. 8Definition 1.1-8dscmet 24891
[Kreyszig] p. 12Equation 5conjmul 12034  muleqadd 11960
[Kreyszig] p. 18Definition 1.3-2mopnval 24757
[Kreyszig] p. 19Remarkmopntopon 24758
[Kreyszig] p. 19Theorem T1mopn0 24817  mopnm 24763
[Kreyszig] p. 19Theorem T2unimopn 24815
[Kreyszig] p. 19Definition of neighborhoodneibl 24820
[Kreyszig] p. 20Definition 1.3-3metcnp2 24861
[Kreyszig] p. 25Definition 1.4-1lmbr 23576  lmmbr 25579  lmmbr2 25580
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23698
[Kreyszig] p. 28Theorem 1.4-5lmcau 25634
[Kreyszig] p. 28Definition 1.4-3iscau 25597  iscmet2 25615
[Kreyszig] p. 30Theorem 1.4-7cmetss 25637
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23780  metelcls 25626
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25627  metcld2 25628
[Kreyszig] p. 51Equation 2clmvneg1 25420  lmodvneg1 21180  nvinv 31241  vcm 31178
[Kreyszig] p. 51Equation 1aclm0vs 25416  lmod0vs 21170  slmd0vs 33785  vc0 31176
[Kreyszig] p. 51Equation 1blmodvs0 21171  slmdvs0 33786  vcz 31177
[Kreyszig] p. 58Definition 2.2-1imsmet 31293  ngpmet 24922  nrmmetd 24893
[Kreyszig] p. 59Equation 1imsdval 31288  imsdval2 31289  ncvspds 25482  ngpds 24923
[Kreyszig] p. 63Problem 1nmval 24908  nvnd 31290
[Kreyszig] p. 64Problem 2nmeq0 24937  nmge0 24936  nvge0 31275  nvz 31271
[Kreyszig] p. 64Problem 3nmrtri 24943  nvabs 31274
[Kreyszig] p. 91Definition 2.7-1isblo3i 31403
[Kreyszig] p. 92Equation 2df-nmoo 31347
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31409  blocni 31407
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31408
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25525  ipeq0 21944  ipz 31321
[Kreyszig] p. 135Problem 2cphpyth 25537  pythi 31452
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31456
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25559
[Kreyszig] p. 144Equation 4supcvg 16025
[Kreyszig] p. 144Theorem 3.3-1minvec 25757  minveco 31486
[Kreyszig] p. 196Definition 3.9-1df-aj 31352
[Kreyszig] p. 247Theorem 4.7-2bcth 25650
[Kreyszig] p. 249Theorem 4.7-3ubth 31475
[Kreyszig] p. 470Definition of positive operator orderingleop 32725  leopg 32724
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32743
[Kreyszig] p. 525Theorem 10.1-1htth 31520
[Kulpa] p. 547Theorempoimir 38572
[Kulpa] p. 547Equation (1)poimirlem32 38571
[Kulpa] p. 547Equation (2)poimirlem31 38570
[Kulpa] p. 548Theorembroucube 38573
[Kulpa] p. 548Equation (6)poimirlem26 38565
[Kulpa] p. 548Equation (7)poimirlem27 38566
[Kunen] p. 10Axiom 0ax6e 2413  axnul 5259
[Kunen] p. 11Axiom 3axnul 5259
[Kunen] p. 12Axiom 6zfrep6 5242
[Kunen] p. 24Definition 10.24mapval 8858  mapvalg 8856
[Kunen] p. 30Lemma 10.20fodomg 10600
[Kunen] p. 31Definition 10.24mapex 7952
[Kunen] p. 95Definition 2.1df-r1 9768
[Kunen] p. 97Lemma 2.10r1elss 9814  r1elssi 9813
[Kunen] p. 107Exercise 4rankop 9872  rankopb 9866  rankuni 9879  rankxplim 9896  rankxpsuc 9899
[Kunen2] p. 47Lemma I.9.9relpfr 45944
[Kunen2] p. 53Lemma I.9.21trfr 45952
[Kunen2] p. 53Lemma I.9.24(2)wffr 45951
[Kunen2] p. 53Definition I.9.20tcfr 45953
[Kunen2] p. 95Lemma I.16.2ralabso 45958  rexabso 45959
[Kunen2] p. 96Example I.16.3disjabso 45965  n0abso 45966  ssabso 45964
[Kunen2] p. 111Lemma II.2.4(1)traxext 45967
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45977
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45972
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45975
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45976
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45971
[Kunen2] p. 112Corollary II.2.5wfaxext 45983  wfaxpr 45988  wfaxreg 45990  wfaxrep 45984  wfaxsep 45985  wfaxun 45989
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45974
[Kunen2] p. 113Corollary II.2.9wfaxpow 45987
[Kunen2] p. 114Theorem II.2.13wfaxext 45983
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45982  omelaxinf2 45979
[Kunen2] p. 114Corollary II.2.12wfac8prim 45992  wfaxinf2 45991
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 46005  permaxext 45995  permaxinf2 46003  permaxnul 45998  permaxpow 45999  permaxpr 46000  permaxrep 45996  permaxsep 45997  permaxun 46001
[Kunen2] p. 148Definition II.9.1brpermmodel 45993
[Kunen2] p. 149Exercise II.9.3permac8prim 46004
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4964
[Lang] , p. 225Corollary 1.3finexttrb 34297
[Lang] p. Definitiondf-rn 5662
[Lang] p. 3Statementlidrideqd 18850  mndbn0 18940
[Lang] p. 3Definitiondf-mnd 18924
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18876
[Lang] p. 4Property of composites. Second formulagsumccat 19037
[Lang] p. 5Equationgsumreidx 20131
[Lang] p. 5Definition of an (infinite) productgsumfsupp 49279
[Lang] p. 6Examplenn0mnd 49276
[Lang] p. 6Equationgsumxp2 20194
[Lang] p. 6Statementcycsubm 19417
[Lang] p. 6Definitionmulgnn0gsum 19290
[Lang] p. 6Observationmndlsmidm 19884
[Lang] p. 7Definitiondfgrp2e 19174
[Lang] p. 30Definitiondf-tocyc 33668
[Lang] p. 32Property (a)cyc3genpm 33713
[Lang] p. 32Property (b)cyc3conja 33718  cycpmconjv 33703
[Lang] p. 53Definitiondf-cat 17842
[Lang] p. 53Axiom CAT 1cat1 18272  cat1lem 18271
[Lang] p. 54Definitiondf-iso 17924
[Lang] p. 57Definitiondf-inito 18159  df-termo 18160
[Lang] p. 58Exampleirinitoringc 21785
[Lang] p. 58Statementinitoeu1 18186  termoeu1 18193
[Lang] p. 62Definitiondf-func 18033
[Lang] p. 65Definitiondf-nat 18121
[Lang] p. 83Definition of "ring with unit"dfring2 20517
[Lang] p. 91Notedf-ringc 20898
[Lang] p. 92Statementmxidlprm 33995
[Lang] p. 92Definitionisprmidlc 21628
[Lang] p. 128Remarkdsmmlmod 22051
[Lang] p. 129Prooflincscm 49542  lincscmcl 49544  lincsum 49541  lincsumcl 49543
[Lang] p. 129Statementlincolss 49546
[Lang] p. 129Observationdsmmfi 22044
[Lang] p. 141Theorem 5.3dimkerim 34259  qusdimsum 34260
[Lang] p. 141Corollary 5.4lssdimle 34240
[Lang] p. 147Definitionsnlindsntor 49583
[Lang] p. 504Statementmat1 22762  matring 22758
[Lang] p. 504Definitiondf-mamu 22706
[Lang] p. 505Statementmamuass 22717  mamutpos 22773  matassa 22759  mattposvs 22770  tposmap 22772
[Lang] p. 513Definitionmdet1 22916  mdetf 22910
[Lang] p. 513Theorem 4.4cramer 23009
[Lang] p. 514Proposition 4.6mdetleib 22902
[Lang] p. 514Proposition 4.8mdettpos 22926
[Lang] p. 515Definitiondf-minmar1 22950  smadiadetr 22990
[Lang] p. 515Corollary 4.9mdetero 22925  mdetralt 22923
[Lang] p. 517Proposition 4.15mdetmul 22938
[Lang] p. 518Definitiondf-madu 22949
[Lang] p. 518Proposition 4.16madulid 22960  madurid 22959  matinv 22992
[Lang] p. 561Theorem 3.1cayleyhamilton 23208
[Lang], p. 190Chapter 6vieta 34212
[Lang], p. 224Proposition 1.1extdgfialg 34326  finextalg 34330
[Lang], p. 224Proposition 1.2extdgmul 34295  fedgmul 34263
[Lang], p. 225Proposition 1.4algextdeg 34357
[Lang], p. 561Remarkchpmatply1 23150
[Lang], p. 561Definitiondf-chpmat 23145
[Lang2] p. 3Notationsdf-ind 12321
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45318
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45313
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45319
[LeBlanc] p. 277Rule R2axnul 5259
[Levy] p. 12Axiom 4.3.1df-clab 2740  wl-df.clab 38431
[Levy] p. 59Definitiondf-ttrcl 9709
[Levy] p. 64Theorem 5.6(ii)frinsg 9755
[Levy] p. 338Axiomdf-clel 2836  df-cleq 2753  wl-df.cleq 38432
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38435
[Levy] p. 357Definition extends to class variables a relation already valid for set variables, and is therefore conservative. This only sketches the conservativity arguement; for details see Appendixwl-df.clel 38435
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2836  df-cleq 2753  wl-df.cleq 38432
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2740  wl-df.clab 38431
[Levy] p. 358Axiomdf-clab 2740  wl-df.clab 38431
[Levy58] p. 2Definition Iisfin1-3 10464
[Levy58] p. 2Definition IIdf-fin2 10364
[Levy58] p. 2Definition Iadf-fin1a 10363
[Levy58] p. 2Definition IIIdf-fin3 10366
[Levy58] p. 3Definition Vdf-fin5 10367
[Levy58] p. 3Definition IVdf-fin4 10365
[Levy58] p. 4Definition VIdf-fin6 10368
[Levy58] p. 4Definition VIIdf-fin7 10369
[Levy58], p. 3Theorem 1fin1a2 10493
[Lipparini] p. 3Lemma 2.1.1nosepssdm 28043
[Lipparini] p. 3Lemma 2.1.4noresle 28054
[Lipparini] p. 6Proposition 4.2noinfbnd1 28086  nosupbnd1 28071
[Lipparini] p. 6Proposition 4.3noinfbnd2 28088  nosupbnd2 28073
[Lipparini] p. 7Theorem 5.1noetasuplem3 28092  noetasuplem4 28093
[Lipparini] p. 7Corollary 4.4nosupinfsep 28089
[Lopez-Astorga] p. 12Rule 1mptnan 1801
[Lopez-Astorga] p. 12Rule 2mptxor 1802
[Lopez-Astorga] p. 12Rule 3mtpxor 1804
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 33010
[Maeda] p. 168Lemma 5mdsym 33014  mdsymi 33013
[Maeda] p. 168Lemma 4(i)mdsymlem4 33008  mdsymlem6 33010  mdsymlem7 33011
[Maeda] p. 168Lemma 4(ii)mdsymlem8 33012
[MaedaMaeda] p. 1Remarkssdmd1 32915  ssdmd2 32916  ssmd1 32913  ssmd2 32914
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32911
[MaedaMaeda] p. 1Definition 1.1df-dmd 32883  df-md 32882  mdbr 32896
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32933  mdslj1i 32921  mdslj2i 32922  mdslle1i 32919  mdslle2i 32920  mdslmd1i 32931  mdslmd2i 32932
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32923  mdsl2bi 32925  mdsl2i 32924
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32937
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32934
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32935
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32912
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32917  mdsl3 32918
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32936
[MaedaMaeda] p. 4Theorem 1.14mdcompli 33031
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40379  hlrelat1 40458
[MaedaMaeda] p. 31Lemma 7.5lcvexch 40097
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32938  cvmdi 32926  cvnbtwn4 32891  cvrnbtwn4 40337
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32939
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40398  cvp 32977  cvrp 40474  lcvp 40098
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 33001
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 33000
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40391  hlexch4N 40450
[MaedaMaeda] p. 34Exercise 7.1atabsi 33003
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40501
[MaedaMaeda] p. 61Definition 15.10psubN 40807  atpsubN 40811  df-pointsN 40560  pointpsubN 40809
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40562  pmap11 40820  pmaple 40819  pmapsub 40826  pmapval 40815
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40823  pmap1N 40825
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40828  pmapglb2N 40829  pmapglb2xN 40830  pmapglbx 40827
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40910
[MaedaMaeda] p. 67Postulate PS1ps-1 40535
[MaedaMaeda] p. 68Lemma 16.2df-padd 40854  paddclN 40900  paddidm 40899
[MaedaMaeda] p. 68Condition PS2ps-2 40536
[MaedaMaeda] p. 68Equation 16.2.1paddass 40896
[MaedaMaeda] p. 69Lemma 16.4ps-1 40535
[MaedaMaeda] p. 69Theorem 16.4ps-2 40536
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19889  lsmmod2 19890  lssats 40070  shatomici 32960  shatomistici 32963  shmodi 31992  shmodsi 31991
[MaedaMaeda] p. 130Remark 29.6dmdmd 32902  mdsymlem7 33011
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 32191
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 32095
[MaedaMaeda] p. 139Remarksumdmdii 33017
[Margaris] p. 40Rule Cexlimiv 1963
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 402  df-ex 1813  df-or 862  dfbi2 480
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 31001
[Margaris] p. 59Section 14notnotrALTVD 45897
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45898
[Margaris] p. 79Rule Cexinst01 45608  exinst11 45609
[Margaris] p. 89Theorem 19.219.2 2009  19.2g 2225  r19.2z 4455
[Margaris] p. 89Theorem 19.319.3 2239  rr19.3v 3621
[Margaris] p. 89Theorem 19.5alcom 2196
[Margaris] p. 89Theorem 19.6alex 1859
[Margaris] p. 89Theorem 19.7alnex 1814
[Margaris] p. 89Theorem 19.819.8a 2218
[Margaris] p. 89Theorem 19.919.9 2242  19.9h 2320  exlimd 2255  exlimdh 2324
[Margaris] p. 89Theorem 19.11excom 2199  excomim 2200
[Margaris] p. 89Theorem 19.1219.12 2358
[Margaris] p. 90Section 19conventions-labels 31002  conventions-labels 31002  conventions-labels 31002  conventions-labels 31002
[Margaris] p. 90Theorem 19.14exnal 1860
[Margaris] p. 90Theorem 19.152albi 45362  albi 1851
[Margaris] p. 90Theorem 19.1619.16 2262
[Margaris] p. 90Theorem 19.1719.17 2263
[Margaris] p. 90Theorem 19.182exbi 45364  exbi 1880
[Margaris] p. 90Theorem 19.1919.19 2266
[Margaris] p. 90Theorem 19.202alim 45361  2alimdv 1951  alimd 2249  alimdh 1850  alimdv 1949  ax-4 1842  ralimdaa 3264  ralimdv 3177  ralimdva 3175  ralimdvva 3210  sbcimdv 3807
[Margaris] p. 90Theorem 19.2119.21 2244  19.21h 2321  19.21t 2243  19.21vv 45360  alrimd 2252  alrimdd 2251  alrimdh 1896  alrimdv 1962  alrimi 2250  alrimih 1857  alrimiv 1960  alrimivv 1961  bj-alrimdh 37494  hbralrimi 3153  r19.21be 3256  r19.21bi 3255  ralrimd 3268  ralrimdv 3161  ralrimdva 3163  ralrimdvv 3207  ralrimdvva 3218  ralrimi 3261  ralrimia 3262  ralrimiv 3154  ralrimiva 3155  ralrimivv 3204  ralrimivva 3206  ralrimivvva 3209  ralrimivw 3159
[Margaris] p. 90Theorem 19.222exim 45363  2eximdv 1952  bj-exim 37509  exim 1867  eximd 2253  eximdh 1897  eximdv 1950  rexim 3104  reximd2a 3273  reximdai 3265  reximdd 46163  reximddv 3179  reximddv2 3222  reximddv3 3180  reximdv 3178  reximdv2 3173  reximdva 3176  reximdvai 3174  reximdvva 3211  reximi2 3096
[Margaris] p. 90Theorem 19.2319.23 2248  19.23bi 2228  19.23h 2322  19.23t 2247  exlimdv 1966  exlimdvv 1967  exlimexi 45507  exlimiv 1963  exlimivv 1965  rexlimd3 46159  rexlimdv 3162  rexlimdv3a 3168  rexlimdva 3164  rexlimdva2 3166  rexlimdvaa 3165  rexlimdvv 3219  rexlimdvva 3220  rexlimdvvva 3221  rexlimdvw 3169  rexlimiv 3157  rexlimiva 3156  rexlimivv 3205
[Margaris] p. 90Theorem 19.2419.24 2024
[Margaris] p. 90Theorem 19.2519.25 1913
[Margaris] p. 90Theorem 19.2619.26 1903
[Margaris] p. 90Theorem 19.2719.27 2264  r19.27z 4466  r19.27zv 4467
[Margaris] p. 90Theorem 19.2819.28 2265  19.28vv 45370  r19.28z 4458  r19.28zf 46174  r19.28zv 4462  rr19.28v 3622
[Margaris] p. 90Theorem 19.2919.29 1906  r19.29d2r 3150  r19.29imd 3128
[Margaris] p. 90Theorem 19.3019.30 1914
[Margaris] p. 90Theorem 19.3119.31 2271  19.31vv 45368
[Margaris] p. 90Theorem 19.3219.32 2270  r19.32 48168
[Margaris] p. 90Theorem 19.3319.33-2 45366  19.33 1917
[Margaris] p. 90Theorem 19.3419.34 2025
[Margaris] p. 90Theorem 19.3519.35 1910
[Margaris] p. 90Theorem 19.3619.36 2267  19.36vv 45367  r19.36zv 4468
[Margaris] p. 90Theorem 19.3719.37 2269  19.37vv 45369  r19.37zv 4463
[Margaris] p. 90Theorem 19.3819.38 1872
[Margaris] p. 90Theorem 19.3919.39 2023
[Margaris] p. 90Theorem 19.4019.40-2 1920  19.40 1919  r19.40 3129
[Margaris] p. 90Theorem 19.4119.41 2272  19.41rg 45533
[Margaris] p. 90Theorem 19.4219.42 2273
[Margaris] p. 90Theorem 19.4319.43 1915
[Margaris] p. 90Theorem 19.4419.44 2274  r19.44zv 4465
[Margaris] p. 90Theorem 19.4519.45 2275  r19.45zv 4464
[Margaris] p. 110Exercise 2(b)eu1 2636
[Mayet] p. 370Remarkjpi 32872  largei 32869  stri 32859
[Mayet3] p. 9Definition of CH-statesdf-hst 32814  ishst 32816
[Mayet3] p. 10Theoremhstrbi 32868  hstri 32867
[Mayet3] p. 1223Theorem 4.1mayete3i 32330
[Mayet3] p. 1240Theorem 7.1mayetes3i 32331
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32880
[MegPav2000] p. 2345Definition 3.4-1chintcl 31934  chsupcl 31942
[MegPav2000] p. 2345Definition 3.4-2hatomic 32962
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32956
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32983
[MegPav2000] p. 2366Figure 7pl42N 41041
[MegPav2002] p. 362Lemma 2.2latj31 18661  latj32 18659  latjass 18657
[Megill] p. 444Axiom C5ax-5 1943  ax5ALT 39965
[Megill] p. 444Section 7conventions 31001
[Megill] p. 445Lemma L12aecom-o 39959  ax-c11n 39946  axc11n 2456
[Megill] p. 446Lemma L17equtrr 2055
[Megill] p. 446Lemma L18ax6fromc10 39954
[Megill] p. 446Lemma L19hbnae-o 39986  hbnae 2462
[Megill] p. 447Remark 9.1dfsb1 2511  sbid 2291  sbidd-misc 50812  sbidd 50811
[Megill] p. 448Remark 9.6axc14 2493
[Megill] p. 448Scheme C4'ax-c4 39942
[Megill] p. 448Scheme C5'ax-c5 39941  sp 2220
[Megill] p. 448Scheme C6'ax-11 2194
[Megill] p. 448Scheme C7'ax-c7 39943
[Megill] p. 448Scheme C8'ax-7 2041
[Megill] p. 448Scheme C9'ax-c9 39948
[Megill] p. 448Scheme C10'ax-6 2000  ax-c10 39944
[Megill] p. 448Scheme C11'ax-c11 39945
[Megill] p. 448Scheme C12'ax-8 2147
[Megill] p. 448Scheme C13'ax-9 2155
[Megill] p. 448Scheme C14'ax-c14 39949
[Megill] p. 448Scheme C15'ax-c15 39947
[Megill] p. 448Scheme C16'ax-c16 39950
[Megill] p. 448Theorem 9.4dral1-o 39962  dral1 2469  dral2-o 39988  dral2 2468  drex1 2471  drex2 2472  drsb1 2525  drsb2 2301
[Megill] p. 449Theorem 9.7sbcom2 2209  sbequ 2120  sbid2v 2539
[Megill] p. 450Example in Appendixhba1-o 39955  hba1 2327
[Mendelson] p. 35Axiom A3hirstL-ax3 47962
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3826  rspsbca 3827  stdpc4 2105
[Mendelson] p. 69Axiom 5ax-c4 39942  ra4 3833  stdpc5 2245
[Mendelson] p. 81Rule Cexlimiv 1963
[Mendelson] p. 95Axiom 6stdpc6 2061
[Mendelson] p. 95Axiom 7stdpc7 2286
[Mendelson] p. 225Axiom system NBGru 3738
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5487
[Mendelson] p. 231Exercise 4.10(k)inv1 4348
[Mendelson] p. 231Exercise 4.10(l)unv 4349
[Mendelson] p. 231Exercise 4.10(n)dfin3 4223
[Mendelson] p. 231Exercise 4.10(o)df-nul 4280
[Mendelson] p. 231Exercise 4.10(q)dfin4 4224
[Mendelson] p. 231Exercise 4.10(s)ddif 4088
[Mendelson] p. 231Definition of uniondfun3 4222
[Mendelson] p. 235Exercise 4.12(c)univ 5419
[Mendelson] p. 235Exercise 4.12(d)pwv 4864
[Mendelson] p. 235Exercise 4.12(j)pwin 5542
[Mendelson] p. 235Exercise 4.12(k)pwunss 4575
[Mendelson] p. 235Exercise 4.12(l)pwssun 5543
[Mendelson] p. 235Exercise 4.12(n)uniin 4891
[Mendelson] p. 235Exercise 4.12(p)reli 5804
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6271
[Mendelson] p. 244Proposition 4.8(g)epweon 7789
[Mendelson] p. 246Definition of successordf-suc 6368
[Mendelson] p. 250Exercise 4.36oelim2 8604
[Mendelson] p. 254Proposition 4.22(b)xpen 9159
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9080  xpsneng 9081
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9087  xpcomeng 9088
[Mendelson] p. 254Proposition 4.22(e)xpassen 9090
[Mendelson] p. 255Definitionbrsdom 9001
[Mendelson] p. 255Exercise 4.39endisj 9083
[Mendelson] p. 255Exercise 4.41mapprc 8851
[Mendelson] p. 255Exercise 4.43mapsnen 9065  mapsnend 9064
[Mendelson] p. 255Exercise 4.45mapunen 9165
[Mendelson] p. 255Exercise 4.47xpmapen 9164
[Mendelson] p. 255Exercise 4.42(a)map0e 8910
[Mendelson] p. 255Exercise 4.42(b)map1 9068
[Mendelson] p. 257Proposition 4.24(a)undom 9084
[Mendelson] p. 258Exercise 4.56(c)djuassen 10257  djucomen 10256
[Mendelson] p. 258Exercise 4.56(f)djudom1 10261
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10255
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8539
[Mendelson] p. 266Proposition 4.34(f)oaordex 8566
[Mendelson] p. 275Proposition 4.42(d)entri3 10643
[Mendelson] p. 281Definitiondf-r1 9768
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9821
[Mendelson] p. 287Axiom system MKru 3738
[MertziosUnger] p. 152Definitiondf-frgr 30860
[MertziosUnger] p. 153Remark 1frgrconngr 30895
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30897  vdgn1frgrv3 30898
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30899
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30892
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30885  2pthfrgrrn 30883  2pthfrgrrn2 30884
[Mittelstaedt] p. 9Definitiondf-oc 31854
[Monk1] p. 22Remarkconventions 31001
[Monk1] p. 22Theorem 3.1conventions 31001
[Monk1] p. 26Theorem 2.8(vii)ssin 4184
[Monk1] p. 33Theorem 3.2(i)ssrel 5759  ssrelf 33209
[Monk1] p. 33Theorem 3.2(ii)eqrel 5760
[Monk1] p. 34Definition 3.3df-opab 5168
[Monk1] p. 36Theorem 3.7(i)coi1 6264  coi2 6265
[Monk1] p. 36Theorem 3.8(v)dm0 5902  rn0 5908
[Monk1] p. 36Theorem 3.7(ii)cnvi 5863
[Monk1] p. 37Theorem 3.13(i)relxp 5669
[Monk1] p. 37Theorem 3.13(x)dmxp 5911  rnxp 6162
[Monk1] p. 37Theorem 3.13(ii)0xp 5750  xp0 5751
[Monk1] p. 38Theorem 3.16(ii)ima0 6075
[Monk1] p. 38Theorem 3.16(viii)imai 6072
[Monk1] p. 39Theorem 3.17imaex 7926  imaexg 7925
[Monk1] p. 39Theorem 3.16(xi)imassrn 6197
[Monk1] p. 41Theorem 4.3(i)fnopfv 7075  funfvop 7049
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6939
[Monk1] p. 42Theorem 4.4(iii)fvelima 6950
[Monk1] p. 43Theorem 4.6funun 6586
[Monk1] p. 43Theorem 4.8(iv)dff13 7258  dff13f 7259
[Monk1] p. 46Theorem 4.15(v)funex 7225  funrnex 7966
[Monk1] p. 50Definition 5.4fniunfv 7251
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6228
[Monk1] p. 52Theorem 5.11(viii)ssint 4924
[Monk1] p. 52Definition 5.13 (i)1stval2 8018  df-1st 8001
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8019  df-2nd 8002
[Monk1] p. 112Theorem 15.17(v)ranksn 9868  ranksnb 9837
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9869
[Monk1] p. 112Theorem 15.17(iii)rankun 9870  rankunb 9864
[Monk1] p. 113Theorem 15.18r1val3 9850
[Monk1] p. 113Definition 15.19df-r1 9768  r1val2 9849
[Monk1] p. 117Lemmazorn2 10584  zorn2g 10581
[Monk1] p. 133Theorem 18.11cardom 10067
[Monk1] p. 133Theorem 18.12canth3 10645
[Monk1] p. 133Theorem 18.14carduni 10062
[Monk2] p. 105Axiom C4ax-4 1842
[Monk2] p. 105Axiom C7ax-7 2041
[Monk2] p. 105Axiom C8ax-12 2213  ax-c15 39947  ax12v2 2215
[Monk2] p. 108Lemma 5ax-c4 39942
[Monk2] p. 109Lemma 12ax-11 2194
[Monk2] p. 109Lemma 15equvini 2485  equvinv 2062  eqvinop 5456
[Monk2] p. 113Axiom C5-1ax-5 1943  ax5ALT 39965
[Monk2] p. 113Axiom C5-2ax-10 2178
[Monk2] p. 113Axiom C5-3ax-11 2194
[Monk2] p. 114Lemma 21sp 2220
[Monk2] p. 114Lemma 22axc4 2352  hba1-o 39955  hba1 2327
[Monk2] p. 114Lemma 23nfia1 2190
[Monk2] p. 114Lemma 24nfa2 2210  nfra2 3362  nfra2w 3299
[Moore] p. 53Part Idf-mre 17756
[Munkres] p. 77Example 2distop 23313  indistop 23320  indistopon 23319
[Munkres] p. 77Example 3fctop 23322  fctop2 23323
[Munkres] p. 77Example 4cctop 23324
[Munkres] p. 78Definition of basisdf-bases 23264  isbasis3g 23267
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17614  tgval2 23274
[Munkres] p. 79Remarktgcl 23287
[Munkres] p. 80Lemma 2.1tgval3 23281
[Munkres] p. 80Lemma 2.2tgss2 23305  tgss3 23304
[Munkres] p. 81Lemma 2.3basgen 23306  basgen2 23307
[Munkres] p. 83Exercise 3topdifinf 38273  topdifinfeq 38274  topdifinffin 38272  topdifinfindis 38270
[Munkres] p. 89Definition of subspace topologyresttop 23478
[Munkres] p. 93Theorem 6.1(1)0cld 23356  topcld 23353
[Munkres] p. 93Theorem 6.1(2)iincld 23357
[Munkres] p. 93Theorem 6.1(3)uncld 23359
[Munkres] p. 94Definition of closureclsval 23355
[Munkres] p. 94Definition of interiorntrval 23354
[Munkres] p. 95Theorem 6.5(a)clsndisj 23393  elcls 23391
[Munkres] p. 95Theorem 6.5(b)elcls3 23401
[Munkres] p. 97Theorem 6.6clslp 23466  neindisj 23435
[Munkres] p. 97Corollary 6.7cldlp 23468
[Munkres] p. 97Definition of limit pointislp2 23463  lpval 23457
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23633
[Munkres] p. 102Definition of continuous functiondf-cn 23545  iscn 23553  iscn2 23556
[Munkres] p. 107Theorem 7.2(g)cncnp 23598  cncnp2 23599  cncnpi 23596  df-cnp 23546  iscnp 23555  iscnp2 23557
[Munkres] p. 127Theorem 10.1metcn 24862
[Munkres] p. 128Theorem 10.3metcn4 25632
[Nathanson] p. 123Remarkreprgt 35250  reprinfz1 35251  reprlt 35248
[Nathanson] p. 123Definitiondf-repr 35238
[Nathanson] p. 123Chapter 5.1circlemethnat 35270
[Nathanson] p. 123Propositionbreprexp 35262  breprexpnat 35263  itgexpif 35235
[NielsenChuang] p. 195Equation 4.73unierri 32706
[OeSilva] p. 2042Section 2ax-bgbltosilva 48908
[Pfenning] p. 17Definition XMnatded 31004
[Pfenning] p. 17Definition NNCnatded 31004  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 31004
[Pfenning] p. 18Rule"natded 31004
[Pfenning] p. 18Definition /\Inatded 31004
[Pfenning] p. 18Definition ` `Enatded 31004  natded 31004  natded 31004  natded 31004  natded 31004
[Pfenning] p. 18Definition ` `Inatded 31004  natded 31004  natded 31004  natded 31004  natded 31004
[Pfenning] p. 18Definition ` `ELnatded 31004
[Pfenning] p. 18Definition ` `ERnatded 31004
[Pfenning] p. 18Definition ` `Ea,unatded 31004
[Pfenning] p. 18Definition ` `IRnatded 31004
[Pfenning] p. 18Definition ` `Ianatded 31004
[Pfenning] p. 127Definition =Enatded 31004
[Pfenning] p. 127Definition =Inatded 31004
[Ponnusamy] p. 361Theorem 6.44cphip0l 25523  df-dip 31303  dip0l 31320  ip0l 21942
[Ponnusamy] p. 361Equation 6.45cphipval 25564  ipval 31305
[Ponnusamy] p. 362Equation I1dipcj 31316  ipcj 21940
[Ponnusamy] p. 362Equation I3cphdir 25526  dipdir 31444  ipdir 21945  ipdiri 31432
[Ponnusamy] p. 362Equation I4ipidsq 31312  nmsq 25515
[Ponnusamy] p. 362Equation 6.46ip0i 31427
[Ponnusamy] p. 362Equation 6.47ip1i 31429
[Ponnusamy] p. 362Equation 6.48ip2i 31430
[Ponnusamy] p. 363Equation I2cphass 25532  dipass 31447  ipass 21951  ipassi 31443
[Prugovecki] p. 186Definition of brabraval 32546  df-bra 32452
[Prugovecki] p. 376Equation 8.1df-kb 32453  kbval 32556
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32984
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40946
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32998  atcvat4i 32999  cvrat3 40500  cvrat4 40501  lsatcvat3 40110
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32884  cvrval 40327  df-cv 32881  df-lcv 40077  lspsncv0 21424
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40958
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40959
[Quine] p. 16Definition 2.1df-clab 2740  rabid 3433  rabidd 46170  wl-df.clab 38431
[Quine] p. 17Definition 2.1''dfsb7 2313
[Quine] p. 18Definition 2.7df-cleq 2753  wl-df.cleq 38432
[Quine] p. 19Definition 2.9conventions 31001  df-v 3453
[Quine] p. 34Theorem 5.1eqabb 2900
[Quine] p. 35Theorem 5.2abid1 2897  abid2f 2953
[Quine] p. 40Theorem 6.1sb5 2310
[Quine] p. 40Theorem 6.2sb6 2122  sbalex 2279
[Quine] p. 41Theorem 6.3df-clel 2836  wl-df.clel 38435
[Quine] p. 41Theorem 6.4eqid 2761  eqid1 31068
[Quine] p. 41Theorem 6.5eqcom 2768
[Quine] p. 42Theorem 6.6df-sbc 3740
[Quine] p. 42Theorem 6.7dfsbcq 3741  dfsbcq2 3742
[Quine] p. 43Theorem 6.8vex 3455
[Quine] p. 43Theorem 6.9isset 3465
[Quine] p. 44Theorem 7.3spcgf 3546  spcgv 3551  spcimgf 3514
[Quine] p. 44Theorem 6.11spsbc 3752  spsbcd 3753
[Quine] p. 44Theorem 6.12elex 3472
[Quine] p. 44Theorem 6.13elab 3633  elabg 3630  elabgf 3628
[Quine] p. 44Theorem 6.14noel 4284
[Quine] p. 48Theorem 7.2snprc 4678
[Quine] p. 48Definition 7.1df-pr 4587  df-sn 4585
[Quine] p. 49Theorem 7.4snss 4745  snssg 4744
[Quine] p. 49Theorem 7.5prss 4781  prssg 4780
[Quine] p. 49Theorem 7.6prid1 4723  prid1g 4721  prid2 4724  prid2g 4722  snid 4623  snidg 4621
[Quine] p. 51Theorem 7.12snex 5397
[Quine] p. 51Theorem 7.13prex 5396
[Quine] p. 53Theorem 8.2unisn 4886  unisnALT 45908  unisng 4885
[Quine] p. 53Theorem 8.3uniun 4890
[Quine] p. 54Theorem 8.6elssuni 4899
[Quine] p. 54Theorem 8.7uni0 4896
[Quine] p. 56Theorem 8.17uniabio 6508
[Quine] p. 56Definition 8.18dfaiota2 48156  dfiota2 6495
[Quine] p. 57Theorem 8.19aiotaval 48165  iotaval 6512
[Quine] p. 57Theorem 8.22iotanul 6518
[Quine] p. 58Theorem 8.23iotaex 6514
[Quine] p. 58Definition 9.1df-op 4591
[Quine] p. 61Theorem 9.5opabid 5499  opabidw 5498  opelopab 5517  opelopaba 5510  opelopabaf 5519  opelopabf 5520  opelopabg 5513  opelopabga 5507  opelopabgf 5515  oprabid 7452  oprabidw 7451
[Quine] p. 64Definition 9.11df-xp 5657
[Quine] p. 64Definition 9.12df-cnv 5659
[Quine] p. 64Definition 9.15df-id 5546
[Quine] p. 65Theorem 10.3fun0 6605
[Quine] p. 65Theorem 10.4funi 6572
[Quine] p. 65Theorem 10.5funsn 6593  funsng 6591
[Quine] p. 65Definition 10.1df-fun 6540
[Quine] p. 65Definition 10.2args 6090  dffv4 6882
[Quine] p. 68Definition 10.11conventions 31001  df-fv 6546  fv2 6880
[Quine] p. 124Theorem 17.3nn0opth2 14416  nn0opth2i 14415  nn0opthi 14414  omopthi 8670
[Quine] p. 177Definition 25.2df-rdg 8418
[Quine] p. 232Equation icarddom 10638
[Quine] p. 284Axiom 39(vi)funimaex 6627  funimaexg 6626
[Quine] p. 331Axiom system NFru 3738
[ReedSimon] p. 36Definition (iii)ax-his3 31686
[ReedSimon] p. 63Exercise 4(a)df-dip 31303  polid 31761  polid2i 31759  polidi 31760
[ReedSimon] p. 63Exercise 4(b)df-ph 31415
[ReedSimon] p. 195Remarklnophm 32621  lnophmi 32620
[Retherford] p. 49Exercise 1(i)leopadd 32734
[Retherford] p. 49Exercise 1(ii)leopmul 32736  leopmuli 32735
[Retherford] p. 49Exercise 1(iv)leoptr 32739
[Retherford] p. 49Definition VI.1df-leop 32454  leoppos 32728
[Retherford] p. 49Exercise 1(iii)leoptri 32738
[Retherford] p. 49Definition of operator orderingleop3 32727
[Ribenboim] p. 181Remarknprmdvdsfacm1 48709
[Ribenboim], p. 181Statementppivalnn 48717
[Roman] p. 4Definitiondf-dmat 22805  df-dmatalt 49510
[Roman] p. 18Part Preliminariesdf-rng 20375
[Roman] p. 19Part Preliminariesdf-ring 20461
[Roman] p. 46Theorem 1.6isldepslvec2 49597
[Roman] p. 112Noteisldepslvec2 49597  ldepsnlinc 49620  zlmodzxznm 49609
[Roman] p. 112Examplezlmodzxzequa 49608  zlmodzxzequap 49611  zlmodzxzldep 49616
[Roman] p. 170Theorem 7.8cayleyhamilton 23208
[Rosenlicht] p. 80Theoremheicant 38574
[Rosser] p. 281Definitiondf-op 4591
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 35274
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 35275
[Rotman] p. 28Remarkpgrpgt2nabl 49478  pmtr3ncom 19689
[Rotman] p. 31Theorem 3.4symggen2 19685
[Rotman] p. 42Theorem 3.15cayley 19628  cayleyth 19629
[Rudin] p. 164Equation 27efcan 16262
[Rudin] p. 164Equation 30efzval 16270
[Rudin] p. 167Equation 48absefi 16364
[Russell1905] p. 482Example of "the fatherdfalseu2 50932
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1804
[Sanford] p. 39Rule 4mptxor 1802
[Sanford] p. 40Rule 1mptnan 1801
[Schechter] p. 51Definition of antisymmetryintasym 6109
[Schechter] p. 51Definition of irreflexivityintirr 6112
[Schechter] p. 51Definition of symmetrycnvsym 6108
[Schechter] p. 51Definition of transitivitycotr 6106
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17756
[Schechter] p. 79Definition of Moore closuredf-mrc 17757
[Schechter] p. 82Section 4.5df-mrc 17757
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17759
[Schechter] p. 139Definition AC3dfac9 10215
[Schechter] p. 141Definition (MC)dfac11 44064
[Schechter] p. 149Axiom DC1ax-dc 10524  axdc3 10532
[Schechter] p. 187Definition of "ring with unit"isring 20463  isrngo 38832
[Schechter] p. 276Remark 11.6.espan0 32144
[Schechter] p. 276Definition of spandf-span 31911  spanval 31935
[Schechter] p. 428Definition 15.35bastop1 23311
[Schloeder] p. 1Lemma 1.3onelon 6387  onelond 36948  onelord 44253  ordelon 6386  ordelord 6384
[Schloeder] p. 1Lemma 1.7onepsuc 44254  sucidg 6446
[Schloeder] p. 1Remark 1.50elon 6418  onsuc 7824  ord0 6417  ordsuci 7822
[Schloeder] p. 1Theorem 1.9epsoon 44255
[Schloeder] p. 1Definition 1.1dftr5 5216
[Schloeder] p. 1Definition 1.2dford3 44035  elon2 6373
[Schloeder] p. 1Definition 1.4df-suc 6368
[Schloeder] p. 1Definition 1.6epel 5554  epelg 5552
[Schloeder] p. 1Theorem 1.9(i)elirr 9594  epirron 44256  ordirr 6380
[Schloeder] p. 1Theorem 1.9(ii)oneltr 44258  oneptr 44257  ontr1 6410
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6406  oneptri 44259  ordtri3or 6395
[Schloeder] p. 2Lemma 1.10ondif1 8509  ord0eln0 6419
[Schloeder] p. 2Lemma 1.13elsuci 6432  onsucss 44268  trsucss 6453
[Schloeder] p. 2Lemma 1.14ordsucss 7829
[Schloeder] p. 2Lemma 1.15onnbtwn 6459  ordnbtwn 6458
[Schloeder] p. 2Lemma 1.16orddif0suc 44270  ordnexbtwnsuc 44269
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10479  onsucf1lem 44271  onsucf1o 44274  onsucf1olem 44272  onsucrn 44273
[Schloeder] p. 2Lemma 1.18dflim7 44275
[Schloeder] p. 2Remark 1.12ordzsl 7856
[Schloeder] p. 2Theorem 1.10ondif1i 44264  ordne0gt0 44263
[Schloeder] p. 2Definition 1.11dflim6 44266  limnsuc 44267  onsucelab 44265
[Schloeder] p. 3Remark 1.21omex 9644
[Schloeder] p. 3Theorem 1.19tfinds 7871
[Schloeder] p. 3Theorem 1.22omelon 9647  ordom 7887
[Schloeder] p. 3Definition 1.20dfom3 9648
[Schloeder] p. 4Lemma 2.21onn 8649
[Schloeder] p. 4Lemma 2.7ssonuni 7794  ssorduni 7793
[Schloeder] p. 4Remark 2.4oa1suc 8539
[Schloeder] p. 4Theorem 1.23dfom5 9651  limom 7893
[Schloeder] p. 4Definition 2.1df-1o 8476  df1o2 8483
[Schloeder] p. 4Definition 2.3oa0 8524  oa0suclim 44277  oalim 8540  oasuc 8532
[Schloeder] p. 4Definition 2.5om0 8525  om0suclim 44278  omlim 8541  omsuc 8534
[Schloeder] p. 4Definition 2.6oe0 8530  oe0m1 8529  oe0suclim 44279  oelim 8542  oesuc 8535
[Schloeder] p. 5Lemma 2.10onsupuni 44231
[Schloeder] p. 5Lemma 2.11onsupsucismax 44281
[Schloeder] p. 5Lemma 2.12onsssupeqcond 44282
[Schloeder] p. 5Lemma 2.13limexissup 44283  limexissupab 44285  limiun 44284  limuni 6425
[Schloeder] p. 5Lemma 2.14oa0r 8546
[Schloeder] p. 5Lemma 2.15om1 8550  om1om1r 44286  om1r 8551
[Schloeder] p. 5Remark 2.8oacl 8543  oaomoecl 44280  oecl 8545  omcl 8544
[Schloeder] p. 5Definition 2.9onsupintrab 44233
[Schloeder] p. 6Lemma 2.16oe1 8552
[Schloeder] p. 6Lemma 2.17oe1m 8553
[Schloeder] p. 6Lemma 2.18oe0rif 44287
[Schloeder] p. 6Theorem 2.19oasubex 44288
[Schloeder] p. 6Theorem 2.20nnacl 8620  nnamecl 44289  nnecl 8622  nnmcl 8621
[Schloeder] p. 7Lemma 3.1onsucwordi 44290
[Schloeder] p. 7Lemma 3.2oaword1 8560
[Schloeder] p. 7Lemma 3.3oaword2 8561
[Schloeder] p. 7Lemma 3.4oalimcl 8568
[Schloeder] p. 7Lemma 3.5oaltublim 44292
[Schloeder] p. 8Lemma 3.6oaordi3 44293
[Schloeder] p. 8Lemma 3.81oaomeqom 44295
[Schloeder] p. 8Lemma 3.10oa00 8567
[Schloeder] p. 8Lemma 3.11omge1 44299  omword1 8581
[Schloeder] p. 8Remark 3.9oaordnr 44298  oaordnrex 44297
[Schloeder] p. 8Theorem 3.7oaord3 44294
[Schloeder] p. 9Lemma 3.12omge2 44300  omword2 8582
[Schloeder] p. 9Lemma 3.13omlim2 44301
[Schloeder] p. 9Lemma 3.14omord2lim 44302
[Schloeder] p. 9Lemma 3.15omord2i 44303  omordi 8574
[Schloeder] p. 9Theorem 3.16omord 8576  omord2com 44304
[Schloeder] p. 10Lemma 3.172omomeqom 44305  df-2o 8477
[Schloeder] p. 10Lemma 3.19oege1 44308  oewordi 8600
[Schloeder] p. 10Lemma 3.20oege2 44309  oeworde 8602
[Schloeder] p. 10Lemma 3.21rp-oelim2 44310
[Schloeder] p. 10Lemma 3.22oeord2lim 44311
[Schloeder] p. 10Remark 3.18omnord1 44307  omnord1ex 44306
[Schloeder] p. 11Lemma 3.23oeord2i 44312
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44314
[Schloeder] p. 11Remark 3.26oenord1 44318  oenord1ex 44317
[Schloeder] p. 11Theorem 4.1oaomoencom 44319
[Schloeder] p. 11Theorem 4.2oaass 8569
[Schloeder] p. 11Theorem 3.24oeord2com 44313
[Schloeder] p. 12Theorem 4.3odi 8587
[Schloeder] p. 13Theorem 4.4omass 8588
[Schloeder] p. 14Remark 4.6oenass 44321
[Schloeder] p. 14Theorem 4.7oeoa 8606
[Schloeder] p. 15Lemma 5.1cantnftermord 44322
[Schloeder] p. 15Lemma 5.2cantnfub 44323  cantnfub2 44324
[Schloeder] p. 16Theorem 5.3cantnf2 44327
[Schwabhauser] p. 10Axiom A1axcgrrflx 29492  axtgcgrrflx 28924
[Schwabhauser] p. 10Axiom A2axcgrtr 29493
[Schwabhauser] p. 10Axiom A3axcgrid 29494  axtgcgrid 28925
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28910
[Schwabhauser] p. 11Axiom A4axsegcon 29505  axtgsegcon 28926  df-trkgcb 28912
[Schwabhauser] p. 11Axiom A5ax5seg 29516  axtg5seg 28927  df-trkgcb 28912
[Schwabhauser] p. 11Axiom A6axbtwnid 29517  axtgbtwnid 28928  df-trkgb 28911
[Schwabhauser] p. 12Axiom A7axpasch 29519  axtgpasch 28929  df-trkgb 28911
[Schwabhauser] p. 12Axiom A8axlowdim2 29538  df-trkg2d 35294
[Schwabhauser] p. 13Axiom A8axtglowdim2 28932
[Schwabhauser] p. 13Axiom A9axtgupdim2 28933  df-trkg2d 35294
[Schwabhauser] p. 13Axiom A10axeuclid 29541  axtgeucl 28934  df-trkge 28913
[Schwabhauser] p. 13Axiom A11axcont 29554  axtgcont 28931  axtgcont1 28930  df-trkgb 28911
[Schwabhauser] p. 24Theorem A10prlngmo 29432
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36752
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36754
[Schwabhauser] p. 27Theorem 2.3cgrtr 36757
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36761
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36762  tgcgrcomimp 28939  tgcgrcoml 28941  tgcgrcomr 28940
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36767  tgcgrtriv 28946
[Schwabhauser] p. 28Theorem 2.105segofs 36771  tg5segofs 35305
[Schwabhauser] p. 28Definition 2.10df-afs 35302  df-ofs 36748
[Schwabhauser] p. 29Theorem 2.11cgrextend 36773  tgcgrextend 28947
[Schwabhauser] p. 29Theorem 2.12segconeq 36775  tgsegconeq 28948
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36787  btwntriv2 36777  tgbtwntriv2 28950
[Schwabhauser] p. 30Theorem 3.2btwncomim 36778  tgbtwncom 28951
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36781  tgbtwntriv1 28954
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36782  tgbtwnswapid 28955
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36788  btwnintr 36784  tgbtwnexch2 28959  tgbtwnintr 28956
[Schwabhauser] p. 30Theorem 3.6btwnexch 36790  btwnexch3 36785  tgbtwnexch 28961  tgbtwnexch3 28957
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36789  tgbtwnouttr 28960  tgbtwnouttr2 28958
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29537
[Schwabhauser] p. 32Theorem 3.14btwndiff 36792  tgbtwndiff 28969
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28962  trisegint 36793
[Schwabhauser] p. 34Theorem 4.2ifscgr 36809  tgifscgr 28971
[Schwabhauser] p. 34Theorem 4.11colcom 29021  colrot1 29022  colrot2 29023  lncom 29090  lnrot1 29091  lnrot2 29092
[Schwabhauser] p. 34Definition 4.1df-ifs 36805
[Schwabhauser] p. 35Theorem 4.3cgrsub 36810  tgcgrsub 28972
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36820  tgcgrxfr 28981
[Schwabhauser] p. 35Statement 4.4ercgrg 28980
[Schwabhauser] p. 35Definition 4.4df-cgr3 36806  df-cgrg 28974
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28974
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36821  tgbtwnxfr 28993
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36827  colinearperm2 36829  colinearperm3 36828  colinearperm4 36830  colinearperm5 36831
[Schwabhauser] p. 36Definition 4.8df-ismt 28996
[Schwabhauser] p. 36Definition 4.10df-colinear 36804  tgellng 29016  tglng 29009
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36832
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36840  lnxfr 29029
[Schwabhauser] p. 37Theorem 4.14lineext 36841  lnext 29030
[Schwabhauser] p. 37Theorem 4.16fscgr 36845  tgfscgr 29031
[Schwabhauser] p. 37Theorem 4.17linecgr 36846  lncgr 29032
[Schwabhauser] p. 37Definition 4.15df-fs 36807
[Schwabhauser] p. 38Theorem 4.18lineid 36848  lnid 29033
[Schwabhauser] p. 38Theorem 4.19idinside 36849  tgidinside 29034
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36866  tgbtwnconn1 29038
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36867  tgbtwnconn2 29039
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36868  tgbtwnconn3 29040
[Schwabhauser] p. 41Theorem 5.5brsegle2 36874
[Schwabhauser] p. 41Definition 5.4df-segle 36872  legov 29048
[Schwabhauser] p. 41Definition 5.5legov2 29049
[Schwabhauser] p. 42Remark 5.13legso 29062
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36875
[Schwabhauser] p. 42Theorem 5.7seglerflx 36877
[Schwabhauser] p. 42Theorem 5.8segletr 36879
[Schwabhauser] p. 42Theorem 5.9segleantisym 36880
[Schwabhauser] p. 42Theorem 5.10seglelin 36881
[Schwabhauser] p. 42Theorem 5.11seglemin 36878
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36883
[Schwabhauser] p. 42Proposition 5.7legid 29050
[Schwabhauser] p. 42Proposition 5.8legtrd 29052
[Schwabhauser] p. 42Proposition 5.9legtri3 29053
[Schwabhauser] p. 42Proposition 5.10legtrid 29054
[Schwabhauser] p. 42Proposition 5.11leg0 29055
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36890
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36891
[Schwabhauser] p. 43Theorem 6.4broutsideof 36886  df-outsideof 36885
[Schwabhauser] p. 43Definition 6.1broutsideof2 36887  ishlg 29068
[Schwabhauser] p. 44Theorem 6.4hlln 29073
[Schwabhauser] p. 44Theorem 6.5hlid 29075  outsideofrflx 36892
[Schwabhauser] p. 44Theorem 6.6hlcomb 29069  hlcomd 29070  outsideofcom 36893
[Schwabhauser] p. 44Theorem 6.7hltr 29076  outsideoftr 36894
[Schwabhauser] p. 44Theorem 6.11hlcgreq 29085  hlcgreu 29084  outsideofeu 36896
[Schwabhauser] p. 44Definition 6.8df-ray 36903
[Schwabhauser] p. 45Part 2df-lines2 36904
[Schwabhauser] p. 45Theorem 6.13outsidele 36897
[Schwabhauser] p. 45Theorem 6.15lineunray 36912
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36913  tglineelsb2 29100
[Schwabhauser] p. 45Theorem 6.17linecom 36915  linerflx1 36914  linerflx2 36916  tglinecom 29103  tglinerflx1 29101  tglinerflx2 29102
[Schwabhauser] p. 45Theorem 6.18linethru 36918  tglinethru 29104
[Schwabhauser] p. 45Definition 6.14df-line2 36902  tglng 29009
[Schwabhauser] p. 45Proposition 6.13legbtwn 29057
[Schwabhauser] p. 46Theorem 6.19linethrueu 36921  tglinethrueu 29107
[Schwabhauser] p. 46Theorem 6.21lineintmo 36922  tglineineq 29111  tglineinsn 29112  tglineinteq 29114  tglineintmo 29110
[Schwabhauser] p. 46Theorem 6.23colline 29118
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 29119
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 29120
[Schwabhauser] p. 49Theorem 7.3mirinv 29138
[Schwabhauser] p. 49Theorem 7.7mirmir 29134
[Schwabhauser] p. 49Theorem 7.8mirreu3 29126
[Schwabhauser] p. 49Definition 7.5df-mir 29125  ismir 29131  mirbtwn 29130  mircgr 29129  mirfv 29128  mirval 29127
[Schwabhauser] p. 50Theorem 7.8mirreu 29136
[Schwabhauser] p. 50Theorem 7.9mireq 29137
[Schwabhauser] p. 50Theorem 7.10mirinv 29138
[Schwabhauser] p. 50Theorem 7.11mirf1o 29141
[Schwabhauser] p. 50Theorem 7.13miriso 29142
[Schwabhauser] p. 51Theorem 7.14mirmot 29147
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 29144  mirbtwni 29143
[Schwabhauser] p. 51Theorem 7.16mircgrs 29145
[Schwabhauser] p. 51Theorem 7.17miduniq 29157
[Schwabhauser] p. 52Lemma 7.21symquadlem 29161  symquadmid 29304
[Schwabhauser] p. 52Theorem 7.18miduniq1 29158
[Schwabhauser] p. 52Theorem 7.19miduniq2 29159
[Schwabhauser] p. 52Theorem 7.20colmid 29160
[Schwabhauser] p. 53Lemma 7.22krippen 29163
[Schwabhauser] p. 55Lemma 7.25midexlem 29164
[Schwabhauser] p. 57Theorem 8.2ragcom 29173
[Schwabhauser] p. 57Definition 8.1df-rag 29169  israg 29172
[Schwabhauser] p. 58Theorem 8.3ragcol 29174
[Schwabhauser] p. 58Theorem 8.4ragmir 29175
[Schwabhauser] p. 58Theorem 8.5ragtrivb 29177
[Schwabhauser] p. 58Theorem 8.6ragflat2 29178
[Schwabhauser] p. 58Theorem 8.7ragflat 29179
[Schwabhauser] p. 58Theorem 8.8ragtriva 29180
[Schwabhauser] p. 58Theorem 8.9ragflat3 29181  ragncol 29184
[Schwabhauser] p. 58Theorem 8.10ragcgr 29182
[Schwabhauser] p. 59Theorem 8.12perpcom 29188
[Schwabhauser] p. 59Theorem 8.13ragperp 29192
[Schwabhauser] p. 59Theorem 8.14perpneq 29189
[Schwabhauser] p. 59Definition 8.11df-perpg 29171  isperp 29187
[Schwabhauser] p. 59Definition 8.13isperp2 29190
[Schwabhauser] p. 60Theorem 8.18foot 29197
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 29206  colperpexlem2 29207
[Schwabhauser] p. 63Theorem 8.21colperpex 29209  colperpexlem3 29208
[Schwabhauser] p. 64Theorem 8.22mideu 29214  midex 29213
[Schwabhauser] p. 66Lemma 8.24opphllem 29211
[Schwabhauser] p. 67Theorem 9.2oppcom 29220
[Schwabhauser] p. 67Definition 9.1islnopp 29215
[Schwabhauser] p. 68Lemma 9.3opphllem2 29224
[Schwabhauser] p. 68Lemma 9.4opphllem5 29227  opphllem6 29228
[Schwabhauser] p. 69Theorem 9.5opphl 29230
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28929
[Schwabhauser] p. 70Theorem 9.6outpasch 29233
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29241
[Schwabhauser] p. 71Definition 9.7df-hpg 29236  hpgbr 29238
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29243
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29242
[Schwabhauser] p. 72Theorem 9.11hpgid 29244
[Schwabhauser] p. 72Theorem 9.12hpgcom 29245
[Schwabhauser] p. 72Theorem 9.13hpgtr 29246
[Schwabhauser] p. 73Theorem 9.18colopp 29247
[Schwabhauser] p. 73Theorem 9.19colhp 29248
[Schwabhauser] p. 74Lemma 9.22lnincplng 29262
[Schwabhauser] p. 74Theorem 9.21plngcp 29264
[Schwabhauser] p. 74Theorem 9.24plngrot 29268
[Schwabhauser] p. 74Definition 9.20df-plng 29252  elplng 29258
[Schwabhauser] p. 75Theorem 9.25lnssplng 29270  lnssplng1 29271
[Schwabhauser] p. 76Theorem 9.26plng3p 29275
[Schwabhauser] p. 88Theorem 10.2lmieu 29289
[Schwabhauser] p. 88Definition 10.1df-mid 29279
[Schwabhauser] p. 89Theorem 10.4lmicom 29293
[Schwabhauser] p. 89Theorem 10.5lmilmi 29294
[Schwabhauser] p. 89Theorem 10.6lmireu 29295
[Schwabhauser] p. 89Theorem 10.7lmieq 29296
[Schwabhauser] p. 89Theorem 10.8lmiinv 29297
[Schwabhauser] p. 89Theorem 10.9lmif1o 29300
[Schwabhauser] p. 89Theorem 10.10lmiiso 29302
[Schwabhauser] p. 89Definition 10.3df-lmi 29280
[Schwabhauser] p. 90Theorem 10.11lmimot 29303
[Schwabhauser] p. 91Theorem 10.12hypcgr 29307
[Schwabhauser] p. 92Theorem 10.14lmiopp 29308
[Schwabhauser] p. 92Theorem 10.15lnperpex 29309  lnperpexs 29310
[Schwabhauser] p. 92Theorem 10.16trgcopy 29311  trgcopyeu 29313
[Schwabhauser] p. 95Definition 11.2dfcgra2 29338
[Schwabhauser] p. 95Definition 11.3iscgra 29316
[Schwabhauser] p. 95Proposition 11.4cgracgr 29325
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29323  cgrahl2 29324
[Schwabhauser] p. 96Theorem 11.6cgraid 29326
[Schwabhauser] p. 96Theorem 11.9cgraswap 29327
[Schwabhauser] p. 97Theorem 11.7cgracom 29329
[Schwabhauser] p. 97Theorem 11.8cgratr 29330
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29334  cgrahl 29335
[Schwabhauser] p. 98Theorem 11.13sacgr 29339
[Schwabhauser] p. 98Theorem 11.14oacgr 29340
[Schwabhauser] p. 98Theorem 11.15acopy 29341  acopyeu 29342
[Schwabhauser] p. 98Theorem 11.16ragcgra 29343
[Schwabhauser] p. 98Theorem 11.17cgrarag 29344
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29345
[Schwabhauser] p. 99Theorem 11.19ragraghl 29346
[Schwabhauser] p. 99Theorem 11.20perpeq 29348
[Schwabhauser] p. 99Theorem 11.22tgaaddcpbl 29352
[Schwabhauser] p. 101Theorem 11.24inagswap 29360
[Schwabhauser] p. 101Theorem 11.25inaghl 29364
[Schwabhauser] p. 101Definition 11.23isinag 29357
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29372
[Schwabhauser] p. 102Definition 11.27df-leag 29365  isleag 29366
[Schwabhauser] p. 107Theorem 11.49tgsas 29400  tgsas1 29399  tgsas2 29401  tgsas3 29402
[Schwabhauser] p. 108Theorem 11.50tgasa 29404  tgasa1 29403
[Schwabhauser] p. 109Theorem 11.51tgsss1 29405  tgsss2 29406  tgsss3 29407
[Schwabhauser] p. 121Definition 12.2df-prlng 29415
[Schwabhauser] p. 122Theorem 12.4prlngref 29418
[Schwabhauser] p. 122Theorem 12.5prlngsym 29419
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29424
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29425  dfprlng3 29426
[Schwabhauser] p. 122Theorem 12.9perpprlng 29428
[Schwabhauser] p. 122Theorem 12.10prlngex 29429
[Schwabhauser] p. 123Theorem 12.11prlngmo 29432  prlngmo2 29434
[Schwabhauser] p. 124Theorem 12.13prlngeu 29433
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29436
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29437
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29438
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29439
[Schwabhauser] p. 126Theorem 12.18symquadprlng 29440
[Schwabhauser] p. 126Theorem 12.19prlngsymquad 29442  prlngsymquadopp 29443
[Schwabhauser] p. 126Theorem 12.20quadcgrprlng 29444
[Schwabhauser] p. 126Theorem 12.21tgaltai 29445
[Shapiro] p. 230Theorem 6.5.1dchrhash 27598  dchrsum 27596  dchrsum2 27595  sumdchr 27599
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27600  sum2dchr 27601
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20282  ablfacrp2 20283
[Shapiro], p. 328Equation 9.2.4vmasum 27543
[Shapiro], p. 329Equation 9.2.7logfac2 27544
[Shapiro], p. 329Equation 9.2.9logfacrlim 27551
[Shapiro], p. 331Equation 9.2.13vmadivsum 27809
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27812
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27866  vmalogdivsum2 27865
[Shapiro], p. 375Theorem 9.4.1dirith 27856  dirith2 27855
[Shapiro], p. 375Equation 9.4.3rplogsum 27854  rpvmasum 27853  rpvmasum2 27839
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27814
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27852
[Shapiro], p. 377Lemma 9.4.1dchrisum 27819  dchrisumlem1 27816  dchrisumlem2 27817  dchrisumlem3 27818  dchrisumlema 27815
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27822
[Shapiro], p. 379Equation 9.4.16dchrmusum 27851  dchrmusumlem 27849  dchrvmasumlem 27850
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27821
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27823
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27847  dchrisum0re 27840  dchrisumn0 27848
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27833
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27837
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27838
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27893  pntrsumbnd2 27894  pntrsumo1 27892
[Shapiro], p. 405Equation 10.2.1mudivsum 27857
[Shapiro], p. 406Equation 10.2.6mulogsum 27859
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27861
[Shapiro], p. 407Equation 10.2.8mulog2sum 27864
[Shapiro], p. 418Equation 10.4.6logsqvma 27869
[Shapiro], p. 418Equation 10.4.8logsqvma2 27870
[Shapiro], p. 419Equation 10.4.10selberg 27875
[Shapiro], p. 420Equation 10.4.12selberg2lem 27877
[Shapiro], p. 420Equation 10.4.14selberg2 27878
[Shapiro], p. 422Equation 10.6.7selberg3 27886
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27887
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27884  selberg3lem2 27885
[Shapiro], p. 422Equation 10.4.23selberg4 27888
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27882
[Shapiro], p. 428Equation 10.6.2selbergr 27895
[Shapiro], p. 429Equation 10.6.8selberg3r 27896
[Shapiro], p. 430Equation 10.6.11selberg4r 27897
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27911
[Shapiro], p. 434Equation 10.6.27pntlema 27923  pntlemb 27924  pntlemc 27922  pntlemd 27921  pntlemg 27925
[Shapiro], p. 435Equation 10.6.29pntlema 27923
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27915
[Shapiro], p. 436Lemma 10.6.2pntibnd 27920
[Shapiro], p. 436Equation 10.6.34pntlema 27923
[Shapiro], p. 436Equation 10.6.35pntlem3 27936  pntleml 27938
[Stewart] p. 91Lemma 7.3constrss 34375
[Stewart] p. 92Definition 7.4.df-constr 34362
[Stewart] p. 96Theorem 7.10constraddcl 34394  constrinvcl 34405  constrmulcl 34403  constrnegcl 34395  constrsqrtcl 34411
[Stewart] p. 97Theorem 7.11constrextdg2 34381
[Stewart] p. 98Theorem 7.12constrext2chn 34391
[Stewart] p. 99Theorem 7.132sqr3nconstr 34413
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34423
[Stoll] p. 13Definition corresponds to dfsymdif3 4252
[Stoll] p. 16Exercise 4.40dif 4356  dif0 4327
[Stoll] p. 16Exercise 4.8difdifdir 4447
[Stoll] p. 17Theorem 5.1(5)unvdif 4429
[Stoll] p. 19Theorem 5.2(13)undm 4243
[Stoll] p. 19Theorem 5.2(13')indm 4244
[Stoll] p. 20Remarkinvdif 4225
[Stoll] p. 25Definition of ordered tripledf-ot 4593
[Stoll] p. 43Definitionuniiun 5017
[Stoll] p. 44Definitionintiin 5018
[Stoll] p. 45Definitiondf-iin 4954
[Stoll] p. 45Definition indexed uniondf-iun 4953
[Stoll] p. 176Theorem 3.4(27)iman 407
[Stoll] p. 262Example 4.1dfsymdif3 4252
[Strang] p. 242Section 6.3expgrowth 45319
[Suppes] p. 22Theorem 2eq0 4297  eq0f 4294
[Suppes] p. 22Theorem 4eqss 3946  eqssd 3948  eqssi 3947
[Suppes] p. 23Theorem 5ss0 4352  ss0b 4351
[Suppes] p. 23Theorem 6sstr 3939  sstrALT2 45817
[Suppes] p. 23Theorem 7pssirr 4051
[Suppes] p. 23Theorem 8pssn2lp 4053
[Suppes] p. 23Theorem 9psstr 4056
[Suppes] p. 23Theorem 10pssss 4046
[Suppes] p. 25Theorem 12elin 3915  elun 4100
[Suppes] p. 26Theorem 15inidm 4172
[Suppes] p. 26Theorem 16in0 4345
[Suppes] p. 27Theorem 23unidm 4104
[Suppes] p. 27Theorem 24un0 4344
[Suppes] p. 27Theorem 25ssun1 4124
[Suppes] p. 27Theorem 26ssequn1 4132
[Suppes] p. 27Theorem 27unss 4136
[Suppes] p. 27Theorem 28indir 4232
[Suppes] p. 27Theorem 29undir 4233
[Suppes] p. 28Theorem 32difid 4325
[Suppes] p. 29Theorem 33difin 4218
[Suppes] p. 29Theorem 34indif 4226
[Suppes] p. 29Theorem 35undif1 4430
[Suppes] p. 29Theorem 36difun2 4437
[Suppes] p. 29Theorem 37difin0 4428
[Suppes] p. 29Theorem 38disjdif 4426
[Suppes] p. 29Theorem 39difundi 4236
[Suppes] p. 29Theorem 40difindi 4238
[Suppes] p. 30Theorem 41nalset 5268
[Suppes] p. 39Theorem 61uniss 4875
[Suppes] p. 39Theorem 65uniop 5488
[Suppes] p. 41Theorem 70intsn 4944
[Suppes] p. 42Theorem 71intpr 4942  intprg 4941
[Suppes] p. 42Theorem 73op1stb 5440
[Suppes] p. 42Theorem 78intun 4940
[Suppes] p. 44Definition 15(a)dfiun2 4990  dfiun2g 4988
[Suppes] p. 44Definition 15(b)dfiin2 4991
[Suppes] p. 47Theorem 86elpw 4561  elpw2 5296  elpw2g 5295  elpwg 4560  elpwgdedVD 45899
[Suppes] p. 47Theorem 87pwid 4580
[Suppes] p. 47Theorem 89pw0 4773
[Suppes] p. 48Theorem 90pwpw0 4774
[Suppes] p. 52Theorem 101xpss12 5666
[Suppes] p. 52Theorem 102xpindi 5810  xpindir 5811
[Suppes] p. 52Theorem 103xpundi 5720  xpundir 5721
[Suppes] p. 54Theorem 105elirrv 9591
[Suppes] p. 58Theorem 2relss 5758
[Suppes] p. 59Theorem 4eldm 5882  eldm2 5883  eldm2g 5881  eldmg 5880
[Suppes] p. 59Definition 3df-dm 5661
[Suppes] p. 60Theorem 6dmin 5893
[Suppes] p. 60Theorem 8rnun 6136
[Suppes] p. 60Theorem 9rnin 6137
[Suppes] p. 60Definition 4dfrn2 5870
[Suppes] p. 61Theorem 11brcnv 5860  brcnvg 5857
[Suppes] p. 62Equation 5elcnv 5854  elcnv2 5855
[Suppes] p. 62Theorem 12relcnv 6100
[Suppes] p. 62Theorem 15cnvin 6135
[Suppes] p. 62Theorem 16cnvun 6133
[Suppes] p. 63Definitiondftrrels2 39592
[Suppes] p. 63Theorem 20co02 6262
[Suppes] p. 63Theorem 21dmcoss 5957
[Suppes] p. 63Definition 7df-co 5660
[Suppes] p. 64Theorem 26cnvco 5867
[Suppes] p. 64Theorem 27coass 6267
[Suppes] p. 65Theorem 31resundi 5984
[Suppes] p. 65Theorem 34elima 6061  elima2 6062  elima3 6063  elimag 6060
[Suppes] p. 65Theorem 35imaundi 6141
[Suppes] p. 66Theorem 40dminss 6143
[Suppes] p. 66Theorem 41imainss 6144
[Suppes] p. 67Exercise 11cnvxp 6147
[Suppes] p. 81Definition 34dfec2 8720
[Suppes] p. 82Theorem 72elec 8764  elecALTV 39204  elecg 8762
[Suppes] p. 82Theorem 73eqvrelth 39628  erth 8772  erth2 8773
[Suppes] p. 83Theorem 74eqvreldisj 39631  erdisj 8775
[Suppes] p. 83Definition 35, df-parts 39801  dfmembpart2 39806
[Suppes] p. 89Theorem 96map0b 8911
[Suppes] p. 89Theorem 97map0 8915  map0g 8912
[Suppes] p. 89Theorem 98mapsn 8916  mapsnd 8914
[Suppes] p. 89Theorem 99mapss 8917
[Suppes] p. 91Definition 12(ii)alephsuc 10147
[Suppes] p. 91Definition 12(iii)alephlim 10146
[Suppes] p. 92Theorem 1enref 9012  enrefg 9011
[Suppes] p. 92Theorem 2ensym 9030  ensymb 9029  ensymi 9031
[Suppes] p. 92Theorem 3entr 9033
[Suppes] p. 92Theorem 4unen 9073
[Suppes] p. 94Theorem 15endom 9006
[Suppes] p. 94Theorem 16ssdomg 9027
[Suppes] p. 94Theorem 17domtr 9034
[Suppes] p. 95Theorem 18sbth 9116
[Suppes] p. 97Theorem 23canth2 9149  canth2g 9150
[Suppes] p. 97Definition 3brsdom2 9120  df-sdom 8976  dfsdom2 9119
[Suppes] p. 97Theorem 21(i)sdomirr 9133
[Suppes] p. 97Theorem 22(i)domnsym 9122
[Suppes] p. 97Theorem 21(ii)sdomnsym 9121
[Suppes] p. 97Theorem 22(ii)domsdomtr 9131
[Suppes] p. 97Theorem 22(iv)brdom2 9009
[Suppes] p. 97Theorem 21(iii)sdomtr 9134
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9129
[Suppes] p. 98Exercise 4fundmen 9059  fundmeng 9060
[Suppes] p. 98Exercise 6xpdom3 9094
[Suppes] p. 98Exercise 11sdomentr 9130
[Suppes] p. 104Theorem 37fofi 9305
[Suppes] p. 104Theorem 38pwfi 9310
[Suppes] p. 105Theorem 40pwfi 9310
[Suppes] p. 111Axiom for cardinal numberscarden 10635
[Suppes] p. 130Definition 3df-tr 5213
[Suppes] p. 132Theorem 9ssonuni 7794
[Suppes] p. 134Definition 6df-suc 6368
[Suppes] p. 136Theorem Schema 22findes 7912  finds 7908  finds1 7911  finds2 7910
[Suppes] p. 151Theorem 42isfinite 9653  isfinite2 9290  isfiniteg 9292  unbnn 9288
[Suppes] p. 162Definition 5df-ltnq 11003  df-ltpq 10995
[Suppes] p. 197Theorem Schema 4tfindes 7874  tfinds 7871  tfinds2 7875
[Suppes] p. 209Theorem 18oaord1 8559
[Suppes] p. 209Theorem 21oaword2 8561
[Suppes] p. 211Theorem 25oaass 8569
[Suppes] p. 225Definition 8iscard2 10057
[Suppes] p. 227Theorem 56ondomon 10647
[Suppes] p. 228Theorem 59harcard 10059
[Suppes] p. 228Definition 12(i)aleph0 10145
[Suppes] p. 228Theorem Schema 61onintss 6415
[Suppes] p. 228Theorem Schema 62onminesb 7807  onminsb 7808
[Suppes] p. 229Theorem 64alephval2 10657
[Suppes] p. 229Theorem 65alephcard 10149
[Suppes] p. 229Theorem 66alephord2i 10156
[Suppes] p. 229Theorem 67alephnbtwn 10150
[Suppes] p. 229Definition 12df-aleph 10021
[Suppes] p. 242Theorem 6weth 10573
[Suppes] p. 242Theorem 8entric 10641
[Suppes] p. 242Theorem 9carden 10635
[Szendrei] p. 11Line 6df-cloneop 36461
[Szendrei] p. 11Paragraph 3df-suppos 36465
[TakeutiZaring] p. 8Axiom 1ax-ext 2733
[TakeutiZaring] p. 13Definition 4.5df-cleq 2753  wl-df.cleq 38432
[TakeutiZaring] p. 13Proposition 4.6df-clel 2836  wl-df.clel 38435
[TakeutiZaring] p. 13Proposition 4.9cvjust 2755
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2781
[TakeutiZaring] p. 14Definition 4.16df-oprab 7424
[TakeutiZaring] p. 14Proposition 4.14ru 3738
[TakeutiZaring] p. 15Axiom 2zfpair 5383
[TakeutiZaring] p. 15Exercise 1elpr 4609  elpr2 4611  elpr2g 4610  elprg 4607
[TakeutiZaring] p. 15Exercise 2elsn 4599  elsn2 4626  elsn2g 4625  elsng 4598  velsn 4600
[TakeutiZaring] p. 15Exercise 3elop 5436
[TakeutiZaring] p. 15Exercise 4sneq 4594  sneqr 4800
[TakeutiZaring] p. 15Definition 5.1dfpr2 4605  dfsn2 4597  dfsn2ALT 4606
[TakeutiZaring] p. 16Axiom 3uniex 7758
[TakeutiZaring] p. 16Exercise 6opth 5445
[TakeutiZaring] p. 16Exercise 7opex 5432
[TakeutiZaring] p. 16Exercise 8rext 5416
[TakeutiZaring] p. 16Corollary 5.8unex 7761  unexg 7760
[TakeutiZaring] p. 16Definition 5.3dftp2 4652
[TakeutiZaring] p. 16Definition 5.5df-uni 4868
[TakeutiZaring] p. 16Definition 5.6df-in 3906  df-un 3904
[TakeutiZaring] p. 16Proposition 5.7unipr 4884  uniprg 4883
[TakeutiZaring] p. 17Axiom 4vpwex 5339
[TakeutiZaring] p. 17Exercise 1eltp 4650
[TakeutiZaring] p. 17Exercise 5elsuc 6435  elsucg 6433  sstr2 3938
[TakeutiZaring] p. 17Exercise 6uncom 4105
[TakeutiZaring] p. 17Exercise 7incom 4155
[TakeutiZaring] p. 17Exercise 8unass 4118
[TakeutiZaring] p. 17Exercise 9inass 4173
[TakeutiZaring] p. 17Exercise 10indi 4230
[TakeutiZaring] p. 17Exercise 11undi 4231
[TakeutiZaring] p. 17Definition 5.9df-pss 3919  df-ss 3916
[TakeutiZaring] p. 17Definition 5.10df-pw 4559
[TakeutiZaring] p. 18Exercise 7unss2 4133
[TakeutiZaring] p. 18Exercise 9dfss2 3917  sseqin2 4169
[TakeutiZaring] p. 18Exercise 10ssid 3953
[TakeutiZaring] p. 18Exercise 12inss1 4182  inss2 4183
[TakeutiZaring] p. 18Exercise 13nss 3995
[TakeutiZaring] p. 18Exercise 15unieq 4878
[TakeutiZaring] p. 18Exercise 18sspwb 5417  sspwimp 45900  sspwimpALT 45907  sspwimpALT2 45910  sspwimpcf 45902
[TakeutiZaring] p. 18Exercise 19pweqb 5424
[TakeutiZaring] p. 19Axiom 5ax-rep 5232
[TakeutiZaring] p. 20Definitiondf-rab 3414
[TakeutiZaring] p. 20Corollary 5.160ex 5261
[TakeutiZaring] p. 20Definition 5.12df-dif 3902
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37440  dfnul2 4282
[TakeutiZaring] p. 20Proposition 5.15difid 4325
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4300  n0f 4296  neq0 4299  neq0f 4295
[TakeutiZaring] p. 21Axiom 6zfreg 9590
[TakeutiZaring] p. 21Axiom 6'zfregs 9733
[TakeutiZaring] p. 21Theorem 5.22setind 9748
[TakeutiZaring] p. 21Definition 5.20df-v 3453
[TakeutiZaring] p. 21Proposition 5.21vprc 5274
[TakeutiZaring] p. 22Exercise 10ss 4350
[TakeutiZaring] p. 22Exercise 3ssex 5282  ssexg 5281
[TakeutiZaring] p. 22Exercise 4inex1 5277
[TakeutiZaring] p. 22Exercise 5ruv 9602
[TakeutiZaring] p. 22Exercise 6elirr 9594
[TakeutiZaring] p. 22Exercise 7ssdif0 4314
[TakeutiZaring] p. 22Exercise 11difdif 4082
[TakeutiZaring] p. 22Exercise 13undif3 4246  undif3VD 45864
[TakeutiZaring] p. 22Exercise 14difss 4083
[TakeutiZaring] p. 22Exercise 15sscon 4090
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3078
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3088
[TakeutiZaring] p. 23Proposition 6.2xpex 7767  xpexg 7764
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5658
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6611
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6789  fun11 6614
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6551  svrelfun 6612
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5869
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5871
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5663
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5664
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5660
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6186  dfrel2 6181
[TakeutiZaring] p. 25Exercise 3xpss 5667
[TakeutiZaring] p. 25Exercise 5relun 5789
[TakeutiZaring] p. 25Exercise 6reluni 5796
[TakeutiZaring] p. 25Exercise 9inxp 5809
[TakeutiZaring] p. 25Exercise 12relres 5996
[TakeutiZaring] p. 25Exercise 13opelres 5976  opelresi 5978
[TakeutiZaring] p. 25Exercise 14dmres 6003
[TakeutiZaring] p. 25Exercise 15resss 5992
[TakeutiZaring] p. 25Exercise 17resabs1 5997
[TakeutiZaring] p. 25Exercise 18funres 6582
[TakeutiZaring] p. 25Exercise 24relco 6104
[TakeutiZaring] p. 25Exercise 29funco 6580
[TakeutiZaring] p. 25Exercise 30f1co 6791
[TakeutiZaring] p. 26Definition 6.10eu2 2635
[TakeutiZaring] p. 26Definition 6.11conventions 31001  df-fv 6546  fv3 6903
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7937  cnvexg 7936
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7921  dmexg 7913
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7922  rnexg 7914
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45436
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7932
[TakeutiZaring] p. 27Corollary 6.13fvex 6898
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 48244  tz6.12-1-afv2 48311  tz6.12-1 6908  tz6.12-afv 48243  tz6.12-afv2 48310  tz6.12 6909  tz6.12c-afv2 48312  tz6.12c 6907
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 48307  tz6.12-2 6872  tz6.12i-afv2 48313  tz6.12i 6911
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6541
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6542
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6544  wfo 6536
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6543  wf1 6535
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6545  wf1o 6537
[TakeutiZaring] p. 28Exercise 4eqfnfv 7029  eqfnfv2 7030  eqfnfv2f 7033
[TakeutiZaring] p. 28Exercise 5fvco 6983
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7223
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7221
[TakeutiZaring] p. 29Exercise 9funimaex 6627  funimaexg 6626
[TakeutiZaring] p. 29Definition 6.18df-br 5104
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5560
[TakeutiZaring] p. 30Definition 6.21dffr2 5612  dffr3 6097  eliniseg 6092  iniseg 6095
[TakeutiZaring] p. 30Definition 6.22df-eprel 5551
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5628  fr3nr 7786  frirr 5627
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5604
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7788
[TakeutiZaring] p. 31Exercise 1frss 5615
[TakeutiZaring] p. 31Exercise 4wess 5637
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6350  tz6.26i 6351  wefrc 5645  wereu2 5648
[TakeutiZaring] p. 32Theorem 6.27wfi 6352  wfii 6353
[TakeutiZaring] p. 32Definition 6.28df-isom 6547
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7337
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7338
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7344
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7345
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7346
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7350
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7357
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7359
[TakeutiZaring] p. 35Notationwtr 5212
[TakeutiZaring] p. 35Theorem 7.2trelpss 45437  tz7.2 5634
[TakeutiZaring] p. 35Definition 7.1dftr3 5217
[TakeutiZaring] p. 36Proposition 7.4ordwe 6375
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6383
[TakeutiZaring] p. 36Proposition 7.6ordelord 6384  ordelordALT 45520  ordelordALTVD 45849
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6390  ordelssne 6389
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6388
[TakeutiZaring] p. 37Proposition 7.9ordin 6393
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7796
[TakeutiZaring] p. 38Corollary 7.15ordsson 7797
[TakeutiZaring] p. 38Definition 7.11df-on 6366
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6395
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45532  ordon 7791
[TakeutiZaring] p. 38Proposition 7.13onprc 7792
[TakeutiZaring] p. 39Theorem 7.17tfi 7864
[TakeutiZaring] p. 40Exercise 3ontr2 6411  ontr2d 36949
[TakeutiZaring] p. 40Exercise 7dftr2 5214
[TakeutiZaring] p. 40Exercise 9onssmin 7806
[TakeutiZaring] p. 40Exercise 11unon 7842
[TakeutiZaring] p. 40Exercise 12ordun 6469
[TakeutiZaring] p. 40Exercise 14ordequn 6468
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7793
[TakeutiZaring] p. 40Proposition 7.20elssuni 4899
[TakeutiZaring] p. 41Definition 7.22df-suc 6368
[TakeutiZaring] p. 41Proposition 7.23sssucid 6445  sucidg 6446
[TakeutiZaring] p. 41Proposition 7.24onsuc 7824
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6459  ordnbtwn 6458
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7839
[TakeutiZaring] p. 42Exercise 1df-lim 6367
[TakeutiZaring] p. 42Exercise 4omssnlim 7892
[TakeutiZaring] p. 42Exercise 7ssnlim 7897
[TakeutiZaring] p. 42Exercise 8onsucssi 7852  ordelsuc 7831
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7833
[TakeutiZaring] p. 42Definition 7.27nlimon 7862
[TakeutiZaring] p. 42Definition 7.28dfom2 7879
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7900
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7901
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7902
[TakeutiZaring] p. 43Remarkomon 7889
[TakeutiZaring] p. 43Axiom 7inf3 9636  omex 9644
[TakeutiZaring] p. 43Theorem 7.32ordom 7887
[TakeutiZaring] p. 43Corollary 7.31find 7907
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7904
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7905
[TakeutiZaring] p. 44Exercise 1limomss 7882
[TakeutiZaring] p. 44Exercise 2int0 4922
[TakeutiZaring] p. 44Exercise 3trintss 5231
[TakeutiZaring] p. 44Exercise 4intss1 4923
[TakeutiZaring] p. 44Exercise 5intex 5305
[TakeutiZaring] p. 44Exercise 6oninton 7809
[TakeutiZaring] p. 44Exercise 11ordintdif 6414
[TakeutiZaring] p. 44Definition 7.35df-int 4908
[TakeutiZaring] p. 44Proposition 7.34noinfep 9661
[TakeutiZaring] p. 45Exercise 4onint 7804
[TakeutiZaring] p. 47Lemma 1tfrlem1 8383
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8405
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8406
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8407
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8414  tz7.44-2 8415  tz7.44-3 8416
[TakeutiZaring] p. 50Exercise 1smogt 8375
[TakeutiZaring] p. 50Exercise 3smoiso 8370
[TakeutiZaring] p. 50Definition 7.46df-smo 8354
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8455  tz7.49c 8456
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8453
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8452
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8454
[TakeutiZaring] p. 53Proposition 7.532eu5 2681
[TakeutiZaring] p. 54Definition 7.55df-lexo 35872
[TakeutiZaring] p. 54Definition 7.57df-r0 35873
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10090
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10091
[TakeutiZaring] p. 55Definition 7.59df-j0 35874
[TakeutiZaring] p. 56Definition 8.1oalim 8540  oasuc 8532
[TakeutiZaring] p. 57Remarktfindsg 7872
[TakeutiZaring] p. 57Proposition 8.2oacl 8543
[TakeutiZaring] p. 57Proposition 8.3oa0 8524  oa0r 8546
[TakeutiZaring] p. 57Proposition 8.16omcl 8544
[TakeutiZaring] p. 58Corollary 8.5oacan 8556
[TakeutiZaring] p. 58Proposition 8.4nnaord 8628  nnaordi 8627  oaord 8555  oaordi 8554
[TakeutiZaring] p. 59Proposition 8.6iunss2 5008  uniss2 4902
[TakeutiZaring] p. 59Proposition 8.7oawordri 8558
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8563  oawordex 8565
[TakeutiZaring] p. 59Proposition 8.9nnacl 8620
[TakeutiZaring] p. 59Proposition 8.10oaabs 8657
[TakeutiZaring] p. 60Remarkoancom 9652
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8568
[TakeutiZaring] p. 62Exercise 1nnarcl 8625
[TakeutiZaring] p. 62Exercise 5oaword1 8560
[TakeutiZaring] p. 62Definition 8.15om0x 8527  omlim 8541  omsuc 8534
[TakeutiZaring] p. 62Definition 8.15(a)om0 8525
[TakeutiZaring] p. 63Proposition 8.17nnecl 8622  nnmcl 8621
[TakeutiZaring] p. 63Proposition 8.19nnmord 8641  nnmordi 8640  omord 8576  omordi 8574
[TakeutiZaring] p. 63Proposition 8.20omcan 8577
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8645  omwordri 8580
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8547
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8550  om1r 8551
[TakeutiZaring] p. 64Proposition 8.22om00 8583
[TakeutiZaring] p. 64Proposition 8.23omordlim 8585
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8586
[TakeutiZaring] p. 64Proposition 8.25odi 8587
[TakeutiZaring] p. 65Theorem 8.26omass 8588
[TakeutiZaring] p. 67Definition 8.30nnesuc 8617  oe0 8530  oelim 8542  oesuc 8535  onesuc 8538
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8528
[TakeutiZaring] p. 67Proposition 8.32oen0 8595
[TakeutiZaring] p. 67Proposition 8.33oeordi 8596
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8529
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8553
[TakeutiZaring] p. 68Corollary 8.34oeord 8597
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8603
[TakeutiZaring] p. 68Proposition 8.35oewordri 8601
[TakeutiZaring] p. 68Proposition 8.37oeworde 8602
[TakeutiZaring] p. 69Proposition 8.41oeoa 8606
[TakeutiZaring] p. 70Proposition 8.42oeoe 8608
[TakeutiZaring] p. 73Theorem 9.1trcl 9729  tz9.1 9730
[TakeutiZaring] p. 76Definition 9.9df-r1 9768  r10 9775  r1lim 9779  r1limg 9778  r1suc 9777  r1sucg 9776
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9787  r1ord2 9788  r1ordg 9785
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9797
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9824  tz9.13 9798  tz9.13g 9799
[TakeutiZaring] p. 79Definition 9.14df-rank 9769  rankval 9825  rankvalb 9805  rankvalg 9826
[TakeutiZaring] p. 79Proposition 9.16rankel 9851  rankelb 9833
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9867  rankval3 9853  rankval3b 9836
[TakeutiZaring] p. 79Proposition 9.18rankonid 9839
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9803
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9846  rankr1c 9830  rankr1g 9844
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9847
[TakeutiZaring] p. 80Exercise 1rankss 9863  rankssb 9862
[TakeutiZaring] p. 80Exercise 2unbndrank 9855
[TakeutiZaring] p. 80Proposition 9.19bndrank 9854
[TakeutiZaring] p. 83Axiom of Choiceac4 10553  dfac3 10200
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10109  numth 10550  numth2 10549
[TakeutiZaring] p. 85Definition 10.4cardval 10630
[TakeutiZaring] p. 85Proposition 10.5cardid 10631  cardid2 10034
[TakeutiZaring] p. 85Proposition 10.9oncard 10041
[TakeutiZaring] p. 85Proposition 10.10carden 10635
[TakeutiZaring] p. 85Proposition 10.11cardidm 10040
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 10025
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10046
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 10038
[TakeutiZaring] p. 87Proposition 10.15pwen 9169
[TakeutiZaring] p. 88Exercise 1en0 9045
[TakeutiZaring] p. 88Exercise 7infensuc 9174
[TakeutiZaring] p. 89Exercise 10omxpen 9098
[TakeutiZaring] p. 90Corollary 10.23cardnn 10044
[TakeutiZaring] p. 90Definition 10.27alephiso 10177
[TakeutiZaring] p. 90Proposition 10.20nneneq 9221
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9229
[TakeutiZaring] p. 90Proposition 10.26alephprc 10178
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9226
[TakeutiZaring] p. 91Exercise 2alephle 10167
[TakeutiZaring] p. 91Exercise 3aleph0 10145
[TakeutiZaring] p. 91Exercise 4cardlim 10053
[TakeutiZaring] p. 91Exercise 7infpss 10294
[TakeutiZaring] p. 91Exercise 8infcntss 9314
[TakeutiZaring] p. 91Definition 10.29df-fin 8977  isfi 9002
[TakeutiZaring] p. 92Proposition 10.32onfin 9230
[TakeutiZaring] p. 92Proposition 10.34imadomg 10613
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9091
[TakeutiZaring] p. 93Proposition 10.35fodomb 10605
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10264  unxpdom 9250
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10055  cardsdomelir 10054
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9252
[TakeutiZaring] p. 94Proposition 10.39infxpen 10093
[TakeutiZaring] p. 95Definition 10.42df-map 8849
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10646  infxpidm2 10096
[TakeutiZaring] p. 95Proposition 10.41infdju 10285  infxp 10292
[TakeutiZaring] p. 96Proposition 10.44pw2en 9103  pw2f1o 9101
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9162
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10565
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10560  ac6s5 10569
[TakeutiZaring] p. 98Theorem 10.47unidom 10627
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10628  uniimadomf 10629
[TakeutiZaring] p. 100Definition 11.1cfcof 10352
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10347
[TakeutiZaring] p. 102Exercise 1cfle 10331
[TakeutiZaring] p. 102Exercise 2cf0 10328
[TakeutiZaring] p. 102Exercise 3cfsuc 10335
[TakeutiZaring] p. 102Exercise 4cfom 10342
[TakeutiZaring] p. 102Proposition 11.9coftr 10351
[TakeutiZaring] p. 103Theorem 11.15alephreg 10667
[TakeutiZaring] p. 103Proposition 11.11cardcf 10329
[TakeutiZaring] p. 103Proposition 11.13alephsing 10354
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10176
[TakeutiZaring] p. 104Proposition 11.16carduniima 10175
[TakeutiZaring] p. 104Proposition 11.18alephfp 10187  alephfp2 10188
[TakeutiZaring] p. 106Theorem 11.20gchina 10784
[TakeutiZaring] p. 106Theorem 11.21mappwen 10191
[TakeutiZaring] p. 107Theorem 11.26konigth 10654
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10668
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10669
[TakeutiZaring] p. 143Definition 14.1(1)df-cnv2 35852
[TakeutiZaring] p. 143Definition 14.1(2)df-cnv3 35853
[TakeutiZaring] p. 144Definition 14.2df-gdlop1 35854  df-gdlop2 35855  df-gdlop3 35856  df-gdlop4 35857  df-gdlop5 35858  df-gdlop6 35859  df-gdlop7 35860  df-gdlop8 35861  df-gdlopc 35862
[TakeutiZaring] p. 155Definition 15.2df-j 35875
[TakeutiZaring] p. 156Definition 15.7df-k1 35876  df-k2 35877  df-k3 35878
[TakeutiZaring] p. 158Definition 15.13df-fnl 35879
[TakeutiZaring] p. 158Definition 15.15df-l 35880
[Tarski] p. 67Axiom B5ax-c5 39941
[Tarski] p. 67Scheme B5sp 2220
[Tarski] p. 68Lemma 6avril1 31064  equid 2045
[Tarski] p. 69Lemma 7equcomi 2050
[Tarski] p. 70Lemma 14spim 2417  spime 2419  spimew 2004
[Tarski] p. 70Lemma 16ax-12 2213  ax-c15 39947  ax12i 1999
[Tarski] p. 70Lemmas 16 and 17sb6 2122
[Tarski] p. 75Axiom B7ax6v 2001
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1943  ax5ALT 39965
[Tarski], p. 75Scheme B8 of system S2ax-7 2041  ax-8 2147  ax-9 2155
[Tarski1999] p. 178Axiom 4axtgsegcon 28926
[Tarski1999] p. 178Axiom 5axtg5seg 28927
[Tarski1999] p. 179Axiom 7axtgpasch 28929
[Tarski1999] p. 180Axiom 7.1axtgpasch 28929
[Tarski1999] p. 185Axiom 11axtgcont1 28930
[Truss] p. 114Theorem 5.18ruc 16411
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38578
[Viaclovsky8] p. 3Proposition 7ismblfin 38580
[Weierstrass] p. 272Definitiondf-mdet 22900  mdetuni 22937
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 917
[WhiteheadRussell] p. 96Axiom *1.3olc 882
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 883
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 933
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 983
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 190
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 136
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 91  wl-luk-pm2.04 38369
[WhiteheadRussell] p. 100Theorem *2.05frege5 44800  imim2 59  wl-luk-imim2 38364
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 48089  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 910
[WhiteheadRussell] p. 101Theorem *2.06barbara 2688  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 916
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38367
[WhiteheadRussell] p. 101Theorem *2.11exmid 908
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 911
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 45909  wl-luk-notnotr 38368
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44830  axfrege28 44829  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 881
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 938
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 38361
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 903
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 954
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 31002  pm2.27 43  wl-luk-pm2.27 38359
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 936
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 39304
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 937
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 985
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 986
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 984
[WhiteheadRussell] p. 105Definition *2.33df-3or 1104
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 920
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 921
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 957
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 895
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 896
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 897
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 898
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 899
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 865
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 866
[WhiteheadRussell] p. 107Theorem *2.55orel1 902
[WhiteheadRussell] p. 107Theorem *2.56orel2 904
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 913
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 955
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 956
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 195
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 905  pm2.67 906
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 912
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 988
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 914
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 989
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 990
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 947
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 945
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 987
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 991
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 85
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 946
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1007
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 475  pm3.2im 161
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1008
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1009
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1010
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1011
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 477
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 465
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 408
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 815
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 454
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 455
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 488  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 490  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 777
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 778
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 820
[WhiteheadRussell] p. 113Fact)pm3.45 634
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 822
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 498
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 499
[WhiteheadRussell] p. 113Theorem *3.44jao 975  pm3.44 974
[WhiteheadRussell] p. 113Theorem *3.47anim12 821
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 479
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 978
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 356
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 819
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 846
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 818  bitr 817
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 574
[WhiteheadRussell] p. 117Theorem *4.25oridm 918  pm4.25 919
[WhiteheadRussell] p. 118Theorem *4.3ancom 466
[WhiteheadRussell] p. 118Theorem *4.4andi 1025
[WhiteheadRussell] p. 118Theorem *4.31orcom 884
[WhiteheadRussell] p. 118Theorem *4.32anass 474
[WhiteheadRussell] p. 118Theorem *4.33orass 935
[WhiteheadRussell] p. 118Theorem *4.36anbi1 645
[WhiteheadRussell] p. 118Theorem *4.37orbi1 931
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 649
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 992
[WhiteheadRussell] p. 118Definition *4.34df-3an 1105
[WhiteheadRussell] p. 119Theorem *4.41ordi 1023
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1069
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1040
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1012
[WhiteheadRussell] p. 119Theorem *4.45orabs 1014  pm4.45 1013  pm4.45im 841
[WhiteheadRussell] p. 120Theorem *4.5anor 998
[WhiteheadRussell] p. 120Theorem *4.6imor 867
[WhiteheadRussell] p. 120Theorem *4.7anclb 555
[WhiteheadRussell] p. 120Theorem *4.51ianor 997
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 1000
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1001
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1002
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1003
[WhiteheadRussell] p. 120Theorem *4.56ioran 999  pm4.56 1004
[WhiteheadRussell] p. 120Theorem *4.57oran 1005  pm4.57 1006
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 410
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 870
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 403
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 863
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 411
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 864
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 404
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 567  pm4.71d 571  pm4.71i 569  pm4.71r 568  pm4.71rd 572  pm4.71ri 570
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 964
[WhiteheadRussell] p. 121Theorem *4.73iba 537
[WhiteheadRussell] p. 121Theorem *4.74biorf 950
[WhiteheadRussell] p. 121Theorem *4.76jcab 527  pm4.76 528
[WhiteheadRussell] p. 121Theorem *4.77jaob 976  pm4.77 977
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 948
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1021
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 398
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 399
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1041
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1042
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 392  impexp 456  pm4.87 857
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 836
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 959  pm5.11g 958
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 960
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 962
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 961
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1030
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1031
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1029
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 391
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 837
[WhiteheadRussell] p. 124Theorem *5.22xor 1032
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1065
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1066
[WhiteheadRussell] p. 124Theorem *5.25dfor2 915
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 583
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 393
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 364
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1017
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 968
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 844
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 584
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 849
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 838
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 847
[WhiteheadRussell] p. 125Theorem *5.41imdi 394  pm5.41 395
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 553
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 552
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1022
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1035
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 963
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1016
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1036
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1037
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1045
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1046
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37491
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45342
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45343
[WhiteheadRussell] p. 147Theorem *10.2219.26 1903
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45344
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45345
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45346
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1926
[WhiteheadRussell] p. 151Theorem *10.301albitr 45347
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45348
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45349
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45350
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45351
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45353
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45354
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45355
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45352
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2127
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45358
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45359
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2107
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2197
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1862
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1863
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45360
[WhiteheadRussell] p. 162Theorem *11.322alim 45361
[WhiteheadRussell] p. 162Theorem *11.332albi 45362
[WhiteheadRussell] p. 162Theorem *11.342exim 45363
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45365
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45364
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1920
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45367
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45368
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45366
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1861
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45369
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45370
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1879
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45371
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2376
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1893
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45376
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45372
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45373
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45374
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45375
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45380
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45377
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45378
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45379
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45381
[WhiteheadRussell] p. 175Definition *14.02df-eu 2595
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45391  pm13.13b 45392
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45393
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3037
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3038
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3620
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45399
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45400
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45394
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45535  pm13.193 45395
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45396
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45397
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45398
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45405
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45404
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45403
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3801
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45406  pm14.122b 45407  pm14.122c 45408
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45409  pm14.123b 45410  pm14.123c 45411
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45413
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45412
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45414
[WhiteheadRussell] p. 190Theorem *14.22iota4 6519
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45415
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6520
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45416
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45418
[WhiteheadRussell] p. 192Theorem *14.26eupick 2659  eupickbi 2662  sbaniota 45419
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45417
[WhiteheadRussell] p. 192Theorem *14.271eubi 2610
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45420
[WhiteheadRussell] p. 235Definition *30.01conventions 31001  df-fv 6546
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10082  pm54.43lem 10081
[Young] p. 141Definition of operator orderingleop2 32726
[Young] p. 142Example 12.2(i)0leop 32732  idleop 32733
[vandenDries] p. 42Lemma 61irrapx1 43835
[vandenDries] p. 43Theorem 62pellex 43842  pellexlem1 43836

This page was last updated on 8-Oct-2026.
Copyright terms: Public domain