Bibliographic Cross-References
|
|
Metamath Proof Explorer Bibliographic Cross-References |
|
| Mirrors > Home > MPE Home > Bibliographic Cross-References | ||
| Color key: |
Metamath Proof Explorer |
Hilbert Space Explorer |
 User Mathboxes |
| Bibliographic Reference | Description | Metamath Proof Explorer Page(s) |
|---|---|---|
| [Adamek] p. 21 | Definition 3.1 | df-cat 17042 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 17042 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 17448 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 17063 |
| [Adamek] p. 24 | Example 3.3(4.d) | df-prstc 45803 prsthinc 45799 |
| [Adamek] p. 24 | Example 3.3(4.e) | df-mndtc 45819 df-mndtc 45819 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 17086 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 17156 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 17144 invisoinvl 17165 |
| [Adamek] p. 28 | Example 3.13 | idinv 17164 idiso 17163 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 17149 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 17123 df-iso 17124 dfiso2 17147 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 17130 |
| [Adamek] p. 29 | Remark 3.16 | cicer 17181 |
| [Adamek] p. 29 | Definition 3.15 | cic 17174 df-cic 17171 |
| [Adamek] p. 29 | Definition 3.17 | df-func 17233 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 17145 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 17146 isoco 17152 |
| [Adamek] p. 30 | Remark 3.19 | df-func 17233 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 17256 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 17249 |
| [Adamek] p. 33 | Example 3.26(2) | df-thinc 45780 prsthinc 45799 |
| [Adamek] p. 33 | Example 3.26(3) | df-mndtc 45819 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 17263 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 17483 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 17533 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 17280 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 17279 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 17533 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 17304 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 17310 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 17309 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 17518 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 17518 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 17250 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 17471 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 17298 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 17297 |
| [Adamek] p. 40 | Remark 3.48 | catccat 17480 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 17471 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 17213 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 17214 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 17225 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 17187 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 17313 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 17318 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 17339 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 17343 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 17319 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 17345 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 17356 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 45161 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 17357 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 17384 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 17388 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 17358 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 45164 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 17391 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 17122 |
| [Adamek] p. 185 | Section 10.67 | updjud 9436 |
| [Adamek] p. 478 | Item Rng | df-ringc 45097 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 45428 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 45450 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 14012 df-pfx 14122 df-substr 14092 df-word 13956 lencl 13974 wrd0 13980 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 23461 df-nmoo 28680 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 30088 hmopidmchi 30086 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 30136 pjcmul2i 30137 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 29853 unoplin 29855 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 29854 unopadj2 29873 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 29948 lnopunii 29947 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 30021 |
| [Alling] p. 184 | Axiom B | bdayfo 33521 |
| [Alling] p. 184 | Axiom O | sltso 33520 |
| [Alling] p. 184 | Axiom SD | nodense 33536 |
| [Alling] p. 185 | Lemma 0 | nocvxmin 33614 |
| [Alling] p. 185 | Theorem | conway 33634 |
| [Alling] p. 185 | Axiom FE | noeta 33587 |
| [Alling] p. 186 | Theorem 4 | slerec 33654 |
| [Apostol] p. 18 | Theorem I.1 | addcan 10902 addcan2d 10922 addcan2i 10912 addcand 10921 addcani 10911 |
| [Apostol] p. 18 | Theorem I.2 | negeu 10954 |
| [Apostol] p. 18 | Theorem I.3 | negsub 11012 negsubd 11081 negsubi 11042 |
| [Apostol] p. 18 | Theorem I.4 | negneg 11014 negnegd 11066 negnegi 11034 |
| [Apostol] p. 18 | Theorem I.5 | subdi 11151 subdid 11174 subdii 11167 subdir 11152 subdird 11175 subdiri 11168 |
| [Apostol] p. 18 | Theorem I.6 | mul01 10897 mul01d 10917 mul01i 10908 mul02 10896 mul02d 10916 mul02i 10907 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 11355 mulcan2d 11352 mulcand 11351 mulcani 11357 |
| [Apostol] p. 18 | Theorem I.8 | receu 11363 xreceu 30771 |
| [Apostol] p. 18 | Theorem I.9 | divrec 11392 divrecd 11497 divreci 11463 divreczi 11456 |
| [Apostol] p. 18 | Theorem I.10 | recrec 11415 recreci 11450 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 11358 mul0ord 11368 mul0ori 11366 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 11157 mul2negd 11173 mul2negi 11166 mulneg1 11154 mulneg1d 11171 mulneg1i 11164 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 11433 divadddivd 11538 divadddivi 11480 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 11418 divmuldivd 11535 divmuldivi 11478 rdivmuldivd 31065 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 11419 divdivdivd 11541 divdivdivi 11481 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 12494 rpaddcld 12529 rpmulcl 12495 rpmulcld 12530 |
| [Apostol] p. 20 | Axiom 8 | rpneg 12504 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 12507 |
| [Apostol] p. 20 | Theorem I.17 | lttri 10844 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 11311 ltadd1dd 11329 ltadd1i 11272 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 11568 ltmul1a 11567 ltmul1i 11636 ltmul1ii 11646 ltmul2 11569 ltmul2d 12556 ltmul2dd 12570 ltmul2i 11639 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 11238 msqgt0d 11285 msqgt0i 11255 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 11240 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 11224 lt0neg1d 11287 ltneg 11218 ltnegd 11296 ltnegi 11262 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 11203 lt2addd 11341 lt2addi 11280 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 12473 |
| [Apostol] p. 21 | Exercise 4 | recgt0 11564 recgt0d 11652 recgt0i 11623 recgt0ii 11624 |
| [Apostol] p. 22 | Definition of integers | df-z 12063 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11730 |
| [Apostol] p. 22 | Definition of rationals | df-q 12431 |
| [Apostol] p. 24 | Theorem I.26 | supeu 8991 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 11972 |
| [Apostol] p. 26 | Theorem I.29 | arch 11973 |
| [Apostol] p. 28 | Exercise 2 | btwnz 12165 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 11974 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 12429 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 12428 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12675 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 15784 zneo 12146 zneoALTV 44655 |
| [Apostol] p. 29 | Theorem I.35 | cxpsqrtth 25472 msqsqrtd 14890 resqrtth 14705 sqrtth 14814 sqrtthi 14820 sqsqrtd 14889 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11719 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 12395 |
| [Apostol] p. 361 | Remark | crreczi 13681 |
| [Apostol] p. 363 | Remark | absgt0i 14849 |
| [Apostol] p. 363 | Example | abssubd 14903 abssubi 14853 |
| [ApostolNT] p. 7 | Remark | fmtno0 44526 fmtno1 44527 fmtno2 44536 fmtno3 44537 fmtno4 44538 fmtno5fac 44568 fmtnofz04prm 44563 |
| [ApostolNT] p. 7 | Definition | df-fmtno 44514 |
| [ApostolNT] p. 8 | Definition | df-ppi 25837 |
| [ApostolNT] p. 14 | Definition | df-dvds 15700 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 15715 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 15739 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15734 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15728 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15730 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 15716 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 15717 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15722 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 15756 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 15758 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 15760 |
| [ApostolNT] p. 15 | Definition | df-gcd 15938 dfgcd2 15990 |
| [ApostolNT] p. 16 | Definition | isprm2 16123 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 16094 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 16351 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 15956 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 15991 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 15993 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 15971 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 15963 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 16152 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 16154 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 16364 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 16358 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 15848 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 16028 |
| [ApostolNT] p. 24 | Definition | df-mu 25838 |
| [ApostolNT] p. 25 | Definition | df-phi 16203 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 25928 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 16227 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 16213 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 16217 |
| [ApostolNT] p. 32 | Definition | df-vma 25835 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 25930 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 25952 |
| [ApostolNT] p. 38 | Remark | df-sgm 25839 |
| [ApostolNT] p. 38 | Definition | df-sgm 25839 |
| [ApostolNT] p. 75 | Definition | df-chp 25836 df-cht 25834 |
| [ApostolNT] p. 104 | Definition | congr 16105 |
| [ApostolNT] p. 106 | Remark | dvdsval3 15703 |
| [ApostolNT] p. 106 | Definition | moddvds 15710 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 15791 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 15792 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 13347 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 13384 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 13691 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15733 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 16108 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 16510 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 16110 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 16220 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 16238 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 16221 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 25809 |
| [ApostolNT] p. 179 | Definition | df-lgs 26031 lgsprme0 26075 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 26076 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 26052 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 26067 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 26124 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 26143 2lgsoddprm 26152 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 26110 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 26119 |
| [ApostolNT] p. 188 | Definition | df-lgs 26031 lgs1 26077 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 26068 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 26070 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 26078 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 26079 |
| [Baer] p. 40 | Property (b) | mapdord 39275 |
| [Baer] p. 40 | Property (c) | mapd11 39276 |
| [Baer] p. 40 | Property (e) | mapdin 39299 mapdlsm 39301 |
| [Baer] p. 40 | Property (f) | mapd0 39302 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 39262 mapd1o 39285 |
| [Baer] p. 41 | Property (g) | mapdat 39304 |
| [Baer] p. 44 | Part (1) | mapdpg 39343 |
| [Baer] p. 45 | Part (2) | hdmap1eq 39438 mapdheq 39365 mapdheq2 39366 mapdheq2biN 39367 |
| [Baer] p. 45 | Part (3) | baerlem3 39350 |
| [Baer] p. 46 | Part (4) | mapdheq4 39369 mapdheq4lem 39368 |
| [Baer] p. 46 | Part (5) | baerlem5a 39351 baerlem5abmN 39355 baerlem5amN 39353 baerlem5b 39352 baerlem5bmN 39354 |
| [Baer] p. 47 | Part (6) | hdmap1l6 39458 hdmap1l6a 39446 hdmap1l6e 39451 hdmap1l6f 39452 hdmap1l6g 39453 hdmap1l6lem1 39444 hdmap1l6lem2 39445 mapdh6N 39384 mapdh6aN 39372 mapdh6eN 39377 mapdh6fN 39378 mapdh6gN 39379 mapdh6lem1N 39370 mapdh6lem2N 39371 |
| [Baer] p. 48 | Part 9 | hdmapval 39465 |
| [Baer] p. 48 | Part 10 | hdmap10 39477 |
| [Baer] p. 48 | Part 11 | hdmapadd 39480 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 39454 mapdh6hN 39380 |
| [Baer] p. 48 | Part (7) | mapdh75cN 39390 mapdh75d 39391 mapdh75e 39389 mapdh75fN 39392 mapdh7cN 39386 mapdh7dN 39387 mapdh7eN 39385 mapdh7fN 39388 |
| [Baer] p. 48 | Part (8) | mapdh8 39425 mapdh8a 39412 mapdh8aa 39413 mapdh8ab 39414 mapdh8ac 39415 mapdh8ad 39416 mapdh8b 39417 mapdh8c 39418 mapdh8d 39420 mapdh8d0N 39419 mapdh8e 39421 mapdh8g 39422 mapdh8i 39423 mapdh8j 39424 |
| [Baer] p. 48 | Part (9) | mapdh9a 39426 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 39406 |
| [Baer] p. 49 | Part 12 | hdmap11 39485 hdmapeq0 39481 hdmapf1oN 39502 hdmapneg 39483 hdmaprnN 39501 hdmaprnlem1N 39486 hdmaprnlem3N 39487 hdmaprnlem3uN 39488 hdmaprnlem4N 39490 hdmaprnlem6N 39491 hdmaprnlem7N 39492 hdmaprnlem8N 39493 hdmaprnlem9N 39494 hdmapsub 39484 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 39505 hdmap14lem10 39514 hdmap14lem1a 39503 hdmap14lem2N 39506 hdmap14lem2a 39504 hdmap14lem3 39507 hdmap14lem8 39512 hdmap14lem9 39513 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 39515 hdmap14lem12 39516 hdmap14lem13 39517 hdmap14lem14 39518 hdmap14lem15 39519 hgmapval 39524 |
| [Baer] p. 50 | Part 15 | hgmapadd 39531 hgmapmul 39532 hgmaprnlem2N 39534 hgmapvs 39528 |
| [Baer] p. 50 | Part 16 | hgmaprnN 39538 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 39554 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 39555 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 39556 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 39557 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 39559 hgmapvv 39563 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 39558 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 39560 |
| [Baer] p. 111 | Line 15 | hdmapg 39567 hdmapglem7 39566 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 25473 2irrexpqALT 25538 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2570 |
| [BellMachover] p. 460 | Notation | df-mo 2540 |
| [BellMachover] p. 460 | Definition | mo3 2564 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2710 |
| [BellMachover] p. 462 | Theorem 1.1 | axextmo 2714 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 5160 |
| [BellMachover] p. 463 | Scheme Sep | ax-sep 5167 |
| [BellMachover] p. 463 | Theorem 1.3(ii) | bj-bm1.3ii 34858 bm1.3ii 5170 |
| [BellMachover] p. 466 | Problem | axpow2 5234 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 5235 |
| [BellMachover] p. 466 | Axiom Union | axun2 7481 |
| [BellMachover] p. 468 | Definition | df-ord 6175 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 6190 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 6197 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 6192 |
| [BellMachover] p. 471 | Definition of N | df-om 7600 |
| [BellMachover] p. 471 | Problem 2.5(ii) | uniordint 7540 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 6177 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 9178 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7614 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 9266 |
| [BellMachover] p. 478 | Definition | rankval2 9320 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 9284 r1ord3g 9281 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 9132 |
| [BellMachover] p. 488 | Axiom AC | ac5 9977 dfac4 9622 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 9610 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 36956 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 30288 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 30330 chirredi 30329 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 30318 |
| [Beran] p. 3 | Definition of join | sshjval3 29289 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 29551 cmcm2i 29528 cmcm2ii 29533 cmt2N 36887 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 29552 lecmi 29537 lecmii 29538 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 29526 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 29555 cm2ji 29560 cm2mi 29561 |
| [Beran] p. 95 | Definition | df-sh 29142 issh2 29144 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 29021 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 29034 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 29025 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 29763 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 29765 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 29764 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 29766 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 29017 his1i 29035 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 29018 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 29019 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 29020 |
| [Beran] p. 96 | Definition of norm | df-hnorm 28903 dfhnorm2 29057 normval 29059 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 29119 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 28908 |
| [Beran] p. 96 | Definition of complete subspace | isch3 29176 |
| [Beran] p. 96 | Definition of converge | df-hlim 28907 hlimi 29123 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 29068 norm-i 29064 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 29072 norm-ii 29073 normlem0 29044 normlem1 29045 normlem2 29046 normlem3 29047 normlem4 29048 normlem5 29049 normlem6 29050 normlem7 29051 normlem7tALT 29054 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 29074 norm-iii 29075 |
| [Beran] p. 98 | Remark 3.4 | bcs 29116 bcsiALT 29114 bcsiHIL 29115 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 29056 normpar 29090 normpari 29089 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 29081 normpyth 29080 normpythi 29077 |
| [Beran] p. 99 | Remark | lnfn0 29982 lnfn0i 29977 lnop0 29901 lnop0i 29905 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 29961 nmcfnex 29988 nmcfnexi 29986 nmcopex 29964 nmcopexi 29962 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 29989 nmcfnlbi 29987 nmcoplb 29965 nmcoplbi 29963 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 29991 lnfnconi 29990 lnopcon 29970 lnopconi 29969 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 29091 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 29088 norm3adifii 29083 norm3dif 29085 norm3difi 29082 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 29236 pjhth 29328 pjhtheu 29329 pjpjhth 29360 pjpjhthi 29361 pjth 24191 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 29341 ococi 29340 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 29996 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 29997 riesz4 29999 riesz4i 29998 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 30014 cnlnadjeu 30013 cnlnadjeui 30012 cnlnadji 30011 cnlnadjlem1 30002 nmopadjlei 30023 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 30026 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 30025 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 30027 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 29871 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 30037 nmopcoadji 30036 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 30028 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 30038 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 30035 pjadj2coi 30139 pjadjcoi 30096 |
| [Beran] p. 107 | Definition | df-ch 29156 isch2 29158 |
| [Beran] p. 107 | Remark 3.12 | choccl 29241 isch3 29176 occl 29239 ocsh 29218 shoccl 29240 shocsh 29219 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 29343 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 29267 |
| [Beran] p. 109 | Property (i) | pjadj2 30122 pjadj3 30123 pjadji 29620 pjadjii 29609 |
| [Beran] p. 109 | Property (ii) | pjidmco 30116 pjidmcoi 30112 pjidmi 29608 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 30108 |
| [Beran] p. 111 | Remark | ho0val 29685 pjch1 29605 |
| [Beran] p. 111 | Definition | df-hfmul 29669 df-hfsum 29668 df-hodif 29667 df-homul 29666 df-hosum 29665 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 29606 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 29629 pjchi 29367 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 29374 pjoc2i 29373 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 29615 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 30100 pjssmii 29616 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 30099 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 30098 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 30103 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 30101 pjssge0ii 29617 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 30102 pjdifnormii 29618 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1783 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1781 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1784 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1779 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 31829 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 31837 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 31835 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 31839 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 31859 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 31890 df-sitm 31868 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 31890 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 31867 |
| [Bollobas] p. 1 | Section I.1 | df-edg 26993 isuhgrop 27015 isusgrop 27107 isuspgrop 27106 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 27210 uhgrspan1 27245 uhgrspansubgr 27233 |
| [Bollobas] p. 3 | Definition | isomuspgr 44820 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 27396 df-cusgr 27354 df-nbgr 27275 fusgrmaxsize 27406 |
| [Bollobas] p. 4 | Definition | df-upwlks 44830 df-wlks 27541 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 27492 finsumvtxdgeven 27494 fusgr1th 27493 fusgrvtxdgonume 27496 vtxdgoddnumeven 27495 |
| [Bollobas] p. 5 | Notation | df-pths 27657 |
| [Bollobas] p. 5 | Definition | df-crcts 27727 df-cycls 27728 df-trls 27634 df-wlkson 27542 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 27004 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 44928 df-cllaw 44914 df-mgm 17968 df-mgm2 44947 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 44929 df-asslaw 44916 df-sgrp 18017 df-sgrp2 44949 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 44948 df-comlaw 44915 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 18028 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 19418 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 44967 |
| [BourbakiEns] p. | Proposition 8 | fcof1 7054 fcofo 7055 |
| [BourbakiTop1] p. | Remark | xnegmnf 12686 xnegpnf 12685 |
| [BourbakiTop1] p. | Remark | rexneg 12687 |
| [BourbakiTop1] p. | Remark 3 | ust0 22971 ustfilxp 22964 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 22841 |
| [BourbakiTop1] p. | Criterion | ishmeo 22510 |
| [BourbakiTop1] p. | Example 1 | cstucnd 23036 iducn 23035 snfil 22615 |
| [BourbakiTop1] p. | Example 2 | neifil 22631 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 22818 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 23056 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 31479 |
| [BourbakiTop1] p. | Paragraph 3 | infil 22614 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 23028 df-ust 22952 filintn0 22612 filn0 22613 istgp 22828 ucnprima 23034 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 23039 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 23050 df-usp 23009 df-utop 22983 trust 22981 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 31378 |
| [BourbakiTop1] p. | Property V_i | ssnei2 21867 |
| [BourbakiTop1] p. | Theorem 1(d) | iscncl 22020 |
| [BourbakiTop1] p. | Condition F_I | ustssel 22957 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 22960 |
| [BourbakiTop1] p. | Property V_ii | innei 21876 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 21884 neissex 21878 |
| [BourbakiTop1] p. | Proposition 1 | neips 21864 neiss 21860 ucncn 23037 ustund 22973 ustuqtop 22998 |
| [BourbakiTop1] p. | Proposition 2 | cnpco 22018 neiptopreu 21884 utop2nei 23002 utop3cls 23003 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 23044 uspreg 23026 utopreg 23004 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 22442 imasncls 22443 imasnopn 22441 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 22751 |
| [BourbakiTop1] p. | Condition F_II | ustincl 22959 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 22961 |
| [BourbakiTop1] p. | Property V_iii | elnei 21862 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 23055 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 22958 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 22962 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 22138 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 22597 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 21645 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 31375 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 43145 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 43147 stoweid 43146 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 43084 stoweidlem10 43093 stoweidlem14 43097 stoweidlem15 43098 stoweidlem35 43118 stoweidlem36 43119 stoweidlem37 43120 stoweidlem38 43121 stoweidlem40 43123 stoweidlem41 43124 stoweidlem43 43126 stoweidlem44 43127 stoweidlem46 43129 stoweidlem5 43088 stoweidlem50 43133 stoweidlem52 43135 stoweidlem53 43136 stoweidlem55 43138 stoweidlem56 43139 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 43106 stoweidlem24 43107 stoweidlem27 43110 stoweidlem28 43111 stoweidlem30 43113 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 43117 stoweidlem59 43142 stoweidlem60 43143 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 43128 stoweidlem49 43132 stoweidlem7 43090 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 43114 stoweidlem39 43122 stoweidlem42 43125 stoweidlem48 43131 stoweidlem51 43134 stoweidlem54 43137 stoweidlem57 43140 stoweidlem58 43141 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 43108 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 43100 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 43094 stoweidlem13 43096 stoweidlem26 43109 stoweidlem61 43144 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 43101 |
| [Bruck] p. 1 | Section I.1 | df-clintop 44928 df-mgm 17968 df-mgm2 44947 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 18017 df-sgrp2 44949 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 18316 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 5111 |
| [Church] p. 129 | Section II.24 | df-ifp 1063 dfifp2 1064 |
| [Clemente] p. 10 | Definition IT | natded 28340 |
| [Clemente] p. 10 | Definition I` `m,n | natded 28340 |
| [Clemente] p. 11 | Definition E=>m,n | natded 28340 |
| [Clemente] p. 11 | Definition I=>m,n | natded 28340 |
| [Clemente] p. 11 | Definition E` `(1) | natded 28340 |
| [Clemente] p. 11 | Definition E` `(2) | natded 28340 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 28340 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 28340 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 28340 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 28340 |
| [Clemente] p. 14 | Proof 5.11 | natded 28340 |
| [Clemente] p. 14 | Definition E` `n | natded 28340 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 28342 ex-natded5.2 28341 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 28345 ex-natded5.3 28344 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 28347 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 28349 ex-natded5.7 28348 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 28351 ex-natded5.8 28350 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 28353 ex-natded5.13 28352 |
| [Clemente] p. 32 | Definition I` `n | natded 28340 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 28340 |
| [Clemente] p. 32 | Definition E` `n,t | natded 28340 |
| [Clemente] p. 32 | Definition I` `n,t | natded 28340 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 28354 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 28355 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 28357 ex-natded9.26 28356 |
| [Cohen] p. 301 | Remark | relogoprlem 25334 |
| [Cohen] p. 301 | Property 2 | relogmul 25335 relogmuld 25368 |
| [Cohen] p. 301 | Property 3 | relogdiv 25336 relogdivd 25369 |
| [Cohen] p. 301 | Property 4 | relogexp 25339 |
| [Cohen] p. 301 | Property 1a | log1 25329 |
| [Cohen] p. 301 | Property 1b | loge 25330 |
| [Cohen4] p. 348 | Observation | relogbcxpb 25525 |
| [Cohen4] p. 349 | Property | relogbf 25529 |
| [Cohen4] p. 352 | Definition | elogb 25508 |
| [Cohen4] p. 361 | Property 2 | relogbmul 25515 |
| [Cohen4] p. 361 | Property 3 | logbrec 25520 relogbdiv 25517 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 25513 |
| [Cohen4] p. 361 | Property 6 | relogbexp 25518 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 25506 |
| [Cohen4] p. 361 | Property 1(b) | logb1 25507 |
| [Cohen4] p. 367 | Property | logbchbase 25509 |
| [Cohen4] p. 377 | Property 2 | logblt 25522 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 31822 sxbrsigalem4 31824 |
| [Cohn] p. 81 | Section II.5 | acsdomd 17907 acsinfd 17906 acsinfdimd 17908 acsmap2d 17905 acsmapd 17904 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 31827 |
| [Connell] p. 57 | Definition | df-scmat 21242 df-scmatalt 45274 |
| [Conway] p. 4 | Definition | slerec 33654 |
| [Conway] p. 5 | Definition | addsov 33764 df-adds 33757 df-negs 33758 |
| [Conway] p. 7 | Theorem | 0slt1s 33664 |
| [Conway] p. 16 | Theorem 0(i) | ssltright 33692 |
| [Conway] p. 16 | Theorem 0(ii) | ssltleft 33691 |
| [Conway] p. 16 | Theorem 0(iii) | slerflex 33607 |
| [Conway] p. 17 | Theorem 3 | addscom 33767 addscomd 33768 addsid1 33765 addsid1d 33766 |
| [Conway] p. 17 | Definition | df-0s 33659 |
| [Conway] p. 18 | Definition | df-1s 33660 |
| [Conway] p. 29 | Remark | madebday 33718 newbday 33720 oldbday 33719 |
| [Conway] p. 29 | Definition | df-made 33672 df-new 33674 df-old 33673 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 13320 |
| [Crawley] p. 1 | Definition of poset | df-poset 17672 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 37023 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 37827 dalaw 37523 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 39598 |
| [Crawley] p. 111 | Definition of set W | df-watsN 37627 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 37743 df-ldil 37741 isldil 37747 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 37742 df-trnN 37744 isltrn 37756 ltrnu 37758 |
| [Crawley] p. 112 | Lemma A | cdlema1N 37428 cdlema2N 37429 exatleN 37041 |
| [Crawley] p. 112 | Lemma B | 1cvrat 37113 cdlemb 37431 cdlemb2 37678 cdlemb3 38243 idltrn 37787 l1cvat 36692 lhpat 37680 lhpat2 37682 lshpat 36693 ltrnel 37776 ltrnmw 37788 |
| [Crawley] p. 112 | Lemma C | cdlemc1 37828 cdlemc2 37829 ltrnnidn 37811 trlat 37806 trljat1 37803 trljat2 37804 trljat3 37805 trlne 37822 trlnidat 37810 trlnle 37823 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 37628 |
| [Crawley] p. 113 | Lemma C | cdlemc 37834 cdlemc3 37830 cdlemc4 37831 |
| [Crawley] p. 113 | Lemma D | cdlemd 37844 cdlemd1 37835 cdlemd2 37836 cdlemd3 37837 cdlemd4 37838 cdlemd5 37839 cdlemd6 37840 cdlemd7 37841 cdlemd8 37842 cdlemd9 37843 cdleme31sde 38022 cdleme31se 38019 cdleme31se2 38020 cdleme31snd 38023 cdleme32a 38078 cdleme32b 38079 cdleme32c 38080 cdleme32d 38081 cdleme32e 38082 cdleme32f 38083 cdleme32fva 38074 cdleme32fva1 38075 cdleme32fvcl 38077 cdleme32le 38084 cdleme48fv 38136 cdleme4gfv 38144 cdleme50eq 38178 cdleme50f 38179 cdleme50f1 38180 cdleme50f1o 38183 cdleme50laut 38184 cdleme50ldil 38185 cdleme50lebi 38177 cdleme50rn 38182 cdleme50rnlem 38181 cdlemeg49le 38148 cdlemeg49lebilem 38176 |
| [Crawley] p. 113 | Lemma E | cdleme 38197 cdleme00a 37846 cdleme01N 37858 cdleme02N 37859 cdleme0a 37848 cdleme0aa 37847 cdleme0b 37849 cdleme0c 37850 cdleme0cp 37851 cdleme0cq 37852 cdleme0dN 37853 cdleme0e 37854 cdleme0ex1N 37860 cdleme0ex2N 37861 cdleme0fN 37855 cdleme0gN 37856 cdleme0moN 37862 cdleme1 37864 cdleme10 37891 cdleme10tN 37895 cdleme11 37907 cdleme11a 37897 cdleme11c 37898 cdleme11dN 37899 cdleme11e 37900 cdleme11fN 37901 cdleme11g 37902 cdleme11h 37903 cdleme11j 37904 cdleme11k 37905 cdleme11l 37906 cdleme12 37908 cdleme13 37909 cdleme14 37910 cdleme15 37915 cdleme15a 37911 cdleme15b 37912 cdleme15c 37913 cdleme15d 37914 cdleme16 37922 cdleme16aN 37896 cdleme16b 37916 cdleme16c 37917 cdleme16d 37918 cdleme16e 37919 cdleme16f 37920 cdleme16g 37921 cdleme19a 37940 cdleme19b 37941 cdleme19c 37942 cdleme19d 37943 cdleme19e 37944 cdleme19f 37945 cdleme1b 37863 cdleme2 37865 cdleme20aN 37946 cdleme20bN 37947 cdleme20c 37948 cdleme20d 37949 cdleme20e 37950 cdleme20f 37951 cdleme20g 37952 cdleme20h 37953 cdleme20i 37954 cdleme20j 37955 cdleme20k 37956 cdleme20l 37959 cdleme20l1 37957 cdleme20l2 37958 cdleme20m 37960 cdleme20y 37939 cdleme20zN 37938 cdleme21 37974 cdleme21d 37967 cdleme21e 37968 cdleme22a 37977 cdleme22aa 37976 cdleme22b 37978 cdleme22cN 37979 cdleme22d 37980 cdleme22e 37981 cdleme22eALTN 37982 cdleme22f 37983 cdleme22f2 37984 cdleme22g 37985 cdleme23a 37986 cdleme23b 37987 cdleme23c 37988 cdleme26e 37996 cdleme26eALTN 37998 cdleme26ee 37997 cdleme26f 38000 cdleme26f2 38002 cdleme26f2ALTN 38001 cdleme26fALTN 37999 cdleme27N 38006 cdleme27a 38004 cdleme27cl 38003 cdleme28c 38009 cdleme3 37874 cdleme30a 38015 cdleme31fv 38027 cdleme31fv1 38028 cdleme31fv1s 38029 cdleme31fv2 38030 cdleme31id 38031 cdleme31sc 38021 cdleme31sdnN 38024 cdleme31sn 38017 cdleme31sn1 38018 cdleme31sn1c 38025 cdleme31sn2 38026 cdleme31so 38016 cdleme35a 38085 cdleme35b 38087 cdleme35c 38088 cdleme35d 38089 cdleme35e 38090 cdleme35f 38091 cdleme35fnpq 38086 cdleme35g 38092 cdleme35h 38093 cdleme35h2 38094 cdleme35sn2aw 38095 cdleme35sn3a 38096 cdleme36a 38097 cdleme36m 38098 cdleme37m 38099 cdleme38m 38100 cdleme38n 38101 cdleme39a 38102 cdleme39n 38103 cdleme3b 37866 cdleme3c 37867 cdleme3d 37868 cdleme3e 37869 cdleme3fN 37870 cdleme3fa 37873 cdleme3g 37871 cdleme3h 37872 cdleme4 37875 cdleme40m 38104 cdleme40n 38105 cdleme40v 38106 cdleme40w 38107 cdleme41fva11 38114 cdleme41sn3aw 38111 cdleme41sn4aw 38112 cdleme41snaw 38113 cdleme42a 38108 cdleme42b 38115 cdleme42c 38109 cdleme42d 38110 cdleme42e 38116 cdleme42f 38117 cdleme42g 38118 cdleme42h 38119 cdleme42i 38120 cdleme42k 38121 cdleme42ke 38122 cdleme42keg 38123 cdleme42mN 38124 cdleme42mgN 38125 cdleme43aN 38126 cdleme43bN 38127 cdleme43cN 38128 cdleme43dN 38129 cdleme5 37877 cdleme50ex 38196 cdleme50ltrn 38194 cdleme51finvN 38193 cdleme51finvfvN 38192 cdleme51finvtrN 38195 cdleme6 37878 cdleme7 37886 cdleme7a 37880 cdleme7aa 37879 cdleme7b 37881 cdleme7c 37882 cdleme7d 37883 cdleme7e 37884 cdleme7ga 37885 cdleme8 37887 cdleme8tN 37892 cdleme9 37890 cdleme9a 37888 cdleme9b 37889 cdleme9tN 37894 cdleme9taN 37893 cdlemeda 37935 cdlemedb 37934 cdlemednpq 37936 cdlemednuN 37937 cdlemefr27cl 38040 cdlemefr32fva1 38047 cdlemefr32fvaN 38046 cdlemefrs32fva 38037 cdlemefrs32fva1 38038 cdlemefs27cl 38050 cdlemefs32fva1 38060 cdlemefs32fvaN 38059 cdlemesner 37933 cdlemeulpq 37857 |
| [Crawley] p. 114 | Lemma E | 4atex 37713 4atexlem7 37712 cdleme0nex 37927 cdleme17a 37923 cdleme17c 37925 cdleme17d 38135 cdleme17d1 37926 cdleme17d2 38132 cdleme18a 37928 cdleme18b 37929 cdleme18c 37930 cdleme18d 37932 cdleme4a 37876 |
| [Crawley] p. 115 | Lemma E | cdleme21a 37962 cdleme21at 37965 cdleme21b 37963 cdleme21c 37964 cdleme21ct 37966 cdleme21f 37969 cdleme21g 37970 cdleme21h 37971 cdleme21i 37972 cdleme22gb 37931 |
| [Crawley] p. 116 | Lemma F | cdlemf 38200 cdlemf1 38198 cdlemf2 38199 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 38204 cdlemg16 38294 cdlemg28 38341 cdlemg28a 38330 cdlemg28b 38340 cdlemg3a 38234 cdlemg42 38366 cdlemg43 38367 cdlemg44 38370 cdlemg44a 38368 cdlemg46 38372 cdlemg47 38373 cdlemg9 38271 ltrnco 38356 ltrncom 38375 tgrpabl 38388 trlco 38364 |
| [Crawley] p. 116 | Definition of G | df-tgrp 38380 |
| [Crawley] p. 117 | Lemma G | cdlemg17 38314 cdlemg17b 38299 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 38393 df-edring 38394 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 38397 |
| [Crawley] p. 118 | Remark | tendopltp 38417 |
| [Crawley] p. 118 | Lemma H | cdlemh 38454 cdlemh1 38452 cdlemh2 38453 |
| [Crawley] p. 118 | Lemma I | cdlemi 38457 cdlemi1 38455 cdlemi2 38456 |
| [Crawley] p. 118 | Lemma J | cdlemj1 38458 cdlemj2 38459 cdlemj3 38460 tendocan 38461 |
| [Crawley] p. 118 | Lemma K | cdlemk 38611 cdlemk1 38468 cdlemk10 38480 cdlemk11 38486 cdlemk11t 38583 cdlemk11ta 38566 cdlemk11tb 38568 cdlemk11tc 38582 cdlemk11u-2N 38526 cdlemk11u 38508 cdlemk12 38487 cdlemk12u-2N 38527 cdlemk12u 38509 cdlemk13-2N 38513 cdlemk13 38489 cdlemk14-2N 38515 cdlemk14 38491 cdlemk15-2N 38516 cdlemk15 38492 cdlemk16-2N 38517 cdlemk16 38494 cdlemk16a 38493 cdlemk17-2N 38518 cdlemk17 38495 cdlemk18-2N 38523 cdlemk18-3N 38537 cdlemk18 38505 cdlemk19-2N 38524 cdlemk19 38506 cdlemk19u 38607 cdlemk1u 38496 cdlemk2 38469 cdlemk20-2N 38529 cdlemk20 38511 cdlemk21-2N 38528 cdlemk21N 38510 cdlemk22-3 38538 cdlemk22 38530 cdlemk23-3 38539 cdlemk24-3 38540 cdlemk25-3 38541 cdlemk26-3 38543 cdlemk26b-3 38542 cdlemk27-3 38544 cdlemk28-3 38545 cdlemk29-3 38548 cdlemk3 38470 cdlemk30 38531 cdlemk31 38533 cdlemk32 38534 cdlemk33N 38546 cdlemk34 38547 cdlemk35 38549 cdlemk36 38550 cdlemk37 38551 cdlemk38 38552 cdlemk39 38553 cdlemk39u 38605 cdlemk4 38471 cdlemk41 38557 cdlemk42 38578 cdlemk42yN 38581 cdlemk43N 38600 cdlemk45 38584 cdlemk46 38585 cdlemk47 38586 cdlemk48 38587 cdlemk49 38588 cdlemk5 38473 cdlemk50 38589 cdlemk51 38590 cdlemk52 38591 cdlemk53 38594 cdlemk54 38595 cdlemk55 38598 cdlemk55u 38603 cdlemk56 38608 cdlemk5a 38472 cdlemk5auN 38497 cdlemk5u 38498 cdlemk6 38474 cdlemk6u 38499 cdlemk7 38485 cdlemk7u-2N 38525 cdlemk7u 38507 cdlemk8 38475 cdlemk9 38476 cdlemk9bN 38477 cdlemki 38478 cdlemkid 38573 cdlemkj-2N 38519 cdlemkj 38500 cdlemksat 38483 cdlemksel 38482 cdlemksv 38481 cdlemksv2 38484 cdlemkuat 38503 cdlemkuel-2N 38521 cdlemkuel-3 38535 cdlemkuel 38502 cdlemkuv-2N 38520 cdlemkuv2-2 38522 cdlemkuv2-3N 38536 cdlemkuv2 38504 cdlemkuvN 38501 cdlemkvcl 38479 cdlemky 38563 cdlemkyyN 38599 tendoex 38612 |
| [Crawley] p. 120 | Remark | dva1dim 38622 |
| [Crawley] p. 120 | Lemma L | cdleml1N 38613 cdleml2N 38614 cdleml3N 38615 cdleml4N 38616 cdleml5N 38617 cdleml6 38618 cdleml7 38619 cdleml8 38620 cdleml9 38621 dia1dim 38698 |
| [Crawley] p. 120 | Lemma M | dia11N 38685 diaf11N 38686 dialss 38683 diaord 38684 dibf11N 38798 djajN 38774 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 38669 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 38755 dia2dimlem1 38701 dia2dimlem2 38702 dia2dimlem3 38703 dia2dimlem4 38704 dia2dimlem5 38705 diaf1oN 38767 diarnN 38766 dvheveccl 38749 dvhopN 38753 |
| [Crawley] p. 121 | Lemma N | cdlemn 38849 cdlemn10 38843 cdlemn11 38848 cdlemn11a 38844 cdlemn11b 38845 cdlemn11c 38846 cdlemn11pre 38847 cdlemn2 38832 cdlemn2a 38833 cdlemn3 38834 cdlemn4 38835 cdlemn4a 38836 cdlemn5 38838 cdlemn5pre 38837 cdlemn6 38839 cdlemn7 38840 cdlemn8 38841 cdlemn9 38842 diclspsn 38831 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 38810 |
| [Crawley] p. 122 | Lemma N | dih11 38902 dihf11 38904 dihjust 38854 dihjustlem 38853 dihord 38901 dihord1 38855 dihord10 38860 dihord11b 38859 dihord11c 38861 dihord2 38864 dihord2a 38856 dihord2b 38857 dihord2cN 38858 dihord2pre 38862 dihord2pre2 38863 dihordlem6 38850 dihordlem7 38851 dihordlem7b 38852 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 38867 dihfval 38868 dihval 38869 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 27354 df-nbgr 27275 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 27210 uhgrspan1 27245 uhgrspansubgr 27233 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 27496 vtxdgoddnumeven 27495 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 27004 |
| [EGA] p. 80 | Notation 1.1.1 | rspecval 31386 |
| [EGA] p. 80 | Proposition 1.1.2 | zartop 31398 |
| [EGA] p. 80 | Proposition 1.1.2(i) | zarcls0 31390 zarcls1 31391 |
| [EGA] p. 81 | Corollary 1.1.8 | zart0 31401 |
| [EGA], p. 82 | Proposition 1.1.10(ii) | zarcmp 31404 |
| [EGA], p. 83 | Corollary 1.2.3 | rhmpreimacn 31407 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3846 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 9183 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 8439 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 9191 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 9482 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 10055 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 5173 |
| [Enderton] p. 19 | Definition | df-tp 4521 |
| [Enderton] p. 26 | Exercise 5 | unissb 4830 |
| [Enderton] p. 26 | Exercise 10 | pwel 5248 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5427 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 4964 iinin2 4963 iinun2 4958 iunin1 4957 iunin1f 30471 iunin2 4956 uniin1 30465 uniin2 30466 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 4962 iundif2 4959 |
| [Enderton] p. 32 | Exercise 20 | unineq 4168 |
| [Enderton] p. 33 | Exercise 23 | iinuni 4983 |
| [Enderton] p. 33 | Exercise 25 | iununi 4984 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4991 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 7512 iunpwss 4992 |
| [Enderton] p. 36 | Definition | opthwiener 5371 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 5309 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4835 |
| [Enderton] p. 41 | Lemma 3D | opeluu 5328 rnex 7643 rnexg 7635 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5757 rnuni 5981 |
| [Enderton] p. 42 | Definition of a function | dffun7 6366 dffun8 6367 |
| [Enderton] p. 43 | Definition of function value | funfv2 6756 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 6408 |
| [Enderton] p. 44 | Definition (d) | dfima2 5905 dfima3 5906 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6765 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 9973 ac7g 9974 df-ac 9616 dfac2 9631 dfac2a 9629 dfac2b 9630 dfac3 9621 dfac7 9632 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 7016 |
| [Enderton] p. 52 | Definition | df-map 8439 |
| [Enderton] p. 53 | Exercise 21 | coass 6098 |
| [Enderton] p. 53 | Exercise 27 | dmco 6087 |
| [Enderton] p. 53 | Exercise 14(a) | funin 6415 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5939 |
| [Enderton] p. 54 | Remark | ixpf 8530 ixpssmap 8542 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 8508 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 9983 ac9s 9993 |
| [Enderton] p. 56 | Theorem 3M | eqvrelref 36346 erref 8340 |
| [Enderton] p. 57 | Lemma 3N | eqvrelthi 36349 erthi 8371 |
| [Enderton] p. 57 | Definition | df-ec 8322 |
| [Enderton] p. 58 | Definition | df-qs 8326 |
| [Enderton] p. 61 | Exercise 35 | df-ec 8322 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5753 |
| [Enderton] p. 68 | Definition of successor | df-suc 6178 |
| [Enderton] p. 71 | Definition | df-tr 5137 dftr4 5141 |
| [Enderton] p. 72 | Theorem 4E | unisuc 6248 |
| [Enderton] p. 73 | Exercise 6 | unisuc 6248 |
| [Enderton] p. 73 | Exercise 5(a) | truni 5150 |
| [Enderton] p. 73 | Exercise 5(b) | trint 5152 trintALT 42039 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 8261 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 8263 onasuc 8184 |
| [Enderton] p. 79 | Definition of operation value | df-ov 7173 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 8262 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 8264 onmsuc 8185 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 8279 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 8266 nnacom 8274 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 8280 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 8281 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 8283 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 8267 nnmsucr 8282 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 8295 |
| [Enderton] p. 129 | Definition | df-en 8556 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 7124 |
| [Enderton] p. 133 | Exercise 1 | xpomen 9515 |
| [Enderton] p. 133 | Exercise 2 | qnnen 15658 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8751 |
| [Enderton] p. 135 | Corollary 6C | php3 8753 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8750 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 8807 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 8809 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8767 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8772 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8731 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 9679 |
| [Enderton] p. 142 | Theorem 6I(4) | mapdjuen 9680 |
| [Enderton] p. 143 | Theorem 6J | dju0en 9675 dju1en 9671 |
| [Enderton] p. 144 | Exercise 13 | iunfi 8885 unifi 8886 unifi2 8887 |
| [Enderton] p. 144 | Corollary 6K | undif2 4366 unfi 8771 unfi2 8861 |
| [Enderton] p. 145 | Figure 38 | ffoss 7672 |
| [Enderton] p. 145 | Definition | df-dom 8557 |
| [Enderton] p. 146 | Example 1 | domen 8568 domeng 8569 |
| [Enderton] p. 146 | Example 3 | nndomo 8792 nnsdom 9190 nnsdomg 8851 |
| [Enderton] p. 149 | Theorem 6L(a) | djudom2 9683 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8732 xpdom1 8665 xpdom1g 8663 xpdom2g 8662 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8738 |
| [Enderton] p. 151 | Theorem 6M | zorn 10007 zorng 10004 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 9992 dfac5 9628 |
| [Enderton] p. 159 | Theorem 6Q | unictb 10075 |
| [Enderton] p. 164 | Example | infdif 9709 |
| [Enderton] p. 168 | Definition | df-po 5442 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 6280 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 6218 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 6279 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 6225 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7572 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 7521 |
| [Enderton] p. 194 | Remark | onprc 7518 |
| [Enderton] p. 194 | Exercise 16 | suc11 6275 |
| [Enderton] p. 197 | Definition | df-card 9441 |
| [Enderton] p. 197 | Theorem 7P | carden 10051 |
| [Enderton] p. 200 | Exercise 25 | tfis 7588 |
| [Enderton] p. 202 | Lemma 7T | r1tr 9278 |
| [Enderton] p. 202 | Definition | df-r1 9266 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 9288 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 9369 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 9142 |
| [Enderton] p. 207 | Exercise 30 | rankpr 9359 rankprb 9353 rankpw 9345 rankpwi 9325 rankuniss 9368 |
| [Enderton] p. 207 | Exercise 34 | opthreg 9154 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 9155 |
| [Enderton] p. 212 | Definition of aleph | alephval3 9610 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 9576 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 9590 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 8007 |
| [Enderton] p. 222 | Definition of kard | karden 9397 kardex 9396 |
| [Enderton] p. 238 | Theorem 8R | oeoa 8254 |
| [Enderton] p. 238 | Theorem 8S | oeoe 8256 |
| [Enderton] p. 240 | Exercise 25 | oarec 8219 |
| [Enderton] p. 257 | Definition of cofinality | cflm 9750 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 17016 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 16962 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 17903 mrieqv2d 17013 mrieqvd 17012 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 17017 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 17022 mreexexlem2d 17019 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 17909 mreexfidimd 17024 |
| [Frege1879] p. 11 | Statement | df3or2 40922 |
| [Frege1879] p. 12 | Statement | df3an2 40923 dfxor4 40920 dfxor5 40921 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 40944 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 40945 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 40949 |
| [Frege1879] p. 31 | Proposition 4 | frege4 40953 |
| [Frege1879] p. 32 | Proposition 5 | frege5 40954 |
| [Frege1879] p. 33 | Proposition 6 | frege6 40960 |
| [Frege1879] p. 34 | Proposition 7 | frege7 40962 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 40963 axfrege8 40961 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-luk-pm2.04 35239 |
| [Frege1879] p. 35 | Proposition 9 | frege9 40966 |
| [Frege1879] p. 36 | Proposition 10 | frege10 40974 |
| [Frege1879] p. 36 | Proposition 11 | frege11 40968 |
| [Frege1879] p. 37 | Proposition 12 | frege12 40967 |
| [Frege1879] p. 37 | Proposition 13 | frege13 40976 |
| [Frege1879] p. 37 | Proposition 14 | frege14 40977 |
| [Frege1879] p. 38 | Proposition 15 | frege15 40980 |
| [Frege1879] p. 38 | Proposition 16 | frege16 40970 |
| [Frege1879] p. 39 | Proposition 17 | frege17 40975 |
| [Frege1879] p. 39 | Proposition 18 | frege18 40972 |
| [Frege1879] p. 39 | Proposition 19 | frege19 40978 |
| [Frege1879] p. 40 | Proposition 20 | frege20 40982 |
| [Frege1879] p. 40 | Proposition 21 | frege21 40981 |
| [Frege1879] p. 41 | Proposition 22 | frege22 40973 |
| [Frege1879] p. 42 | Proposition 23 | frege23 40979 |
| [Frege1879] p. 42 | Proposition 24 | frege24 40969 |
| [Frege1879] p. 42 | Proposition 25 | frege25 40971 rp-frege25 40959 |
| [Frege1879] p. 42 | Proposition 26 | frege26 40964 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 40984 |
| [Frege1879] p. 43 | Proposition 27 | frege27 40965 |
| [Frege1879] p. 43 | Proposition 28 | con3 156 |
| [Frege1879] p. 43 | Proposition 29 | frege29 40985 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 40988 axfrege31 40987 |
| [Frege1879] p. 44 | Proposition 30 | frege30 40986 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 132 |
| [Frege1879] p. 44 | Proposition 32 | frege32 40989 |
| [Frege1879] p. 44 | Proposition 33 | frege33 40990 |
| [Frege1879] p. 45 | Proposition 34 | frege34 40991 |
| [Frege1879] p. 45 | Proposition 35 | frege35 40992 |
| [Frege1879] p. 45 | Proposition 36 | frege36 40993 |
| [Frege1879] p. 46 | Proposition 37 | frege37 40994 |
| [Frege1879] p. 46 | Proposition 38 | frege38 40995 |
| [Frege1879] p. 46 | Proposition 39 | frege39 40996 |
| [Frege1879] p. 46 | Proposition 40 | frege40 40997 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 40999 axfrege41 40998 |
| [Frege1879] p. 47 | Proposition 41 | notnot 144 |
| [Frege1879] p. 47 | Proposition 42 | frege42 41000 |
| [Frege1879] p. 47 | Proposition 43 | frege43 41001 |
| [Frege1879] p. 47 | Proposition 44 | frege44 41002 |
| [Frege1879] p. 47 | Proposition 45 | frege45 41003 |
| [Frege1879] p. 48 | Proposition 46 | frege46 41004 |
| [Frege1879] p. 48 | Proposition 47 | frege47 41005 |
| [Frege1879] p. 49 | Proposition 48 | frege48 41006 |
| [Frege1879] p. 49 | Proposition 49 | frege49 41007 |
| [Frege1879] p. 49 | Proposition 50 | frege50 41008 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 41011 ax-frege52c 41042 frege52aid 41012 frege52b 41043 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 41016 ax-frege54c 41046 frege54b 41047 |
| [Frege1879] p. 50 | Proposition 51 | frege51 41009 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3682 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 41014 frege53aid 41013 frege53b 41044 frege53c 41068 |
| [Frege1879] p. 50 | Proposition 54 | biid 264 eqid 2738 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 41022 frege55aid 41019 frege55b 41051 frege55c 41072 frege55cor1a 41023 frege55lem2a 41021 frege55lem2b 41050 frege55lem2c 41071 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 41025 frege56aid 41024 frege56b 41052 frege56c 41073 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 41029 ax-frege58b 41055 frege58bid 41056 frege58c 41075 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 41027 frege57aid 41026 frege57b 41053 frege57c 41074 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3693 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 41031 frege59b 41058 frege59c 41076 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 41032 frege60b 41059 frege60c 41077 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 41033 frege61b 41060 frege61c 41078 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 41034 frege62b 41061 frege62c 41079 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 41035 frege63b 41062 frege63c 41080 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 41036 frege64b 41063 frege64c 41081 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 41037 frege65b 41064 frege65c 41082 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 41038 frege66b 41065 frege66c 41083 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 41039 frege67b 41066 frege67c 41084 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 41040 frege68b 41067 frege68c 41085 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 41086 |
| [Frege1879] p. 58 | Proposition 70 | frege70 41087 |
| [Frege1879] p. 59 | Proposition 71 | frege71 41088 |
| [Frege1879] p. 59 | Proposition 72 | frege72 41089 |
| [Frege1879] p. 59 | Proposition 73 | frege73 41090 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 41093 |
| [Frege1879] p. 60 | Proposition 74 | frege74 41091 |
| [Frege1879] p. 60 | Proposition 75 | frege75 41092 |
| [Frege1879] p. 62 | Proposition 77 | frege77 41094 frege77d 40900 |
| [Frege1879] p. 63 | Proposition 78 | frege78 41095 |
| [Frege1879] p. 63 | Proposition 79 | frege79 41096 |
| [Frege1879] p. 63 | Proposition 80 | frege80 41097 |
| [Frege1879] p. 63 | Proposition 81 | frege81 41098 frege81d 40901 |
| [Frege1879] p. 64 | Proposition 82 | frege82 41099 |
| [Frege1879] p. 65 | Proposition 83 | frege83 41100 frege83d 40902 |
| [Frege1879] p. 65 | Proposition 84 | frege84 41101 |
| [Frege1879] p. 66 | Proposition 85 | frege85 41102 |
| [Frege1879] p. 66 | Proposition 86 | frege86 41103 |
| [Frege1879] p. 66 | Proposition 87 | frege87 41104 frege87d 40904 |
| [Frege1879] p. 67 | Proposition 88 | frege88 41105 |
| [Frege1879] p. 68 | Proposition 89 | frege89 41106 |
| [Frege1879] p. 68 | Proposition 90 | frege90 41107 |
| [Frege1879] p. 68 | Proposition 91 | frege91 41108 frege91d 40905 |
| [Frege1879] p. 69 | Proposition 92 | frege92 41109 |
| [Frege1879] p. 70 | Proposition 93 | frege93 41110 |
| [Frege1879] p. 70 | Proposition 94 | frege94 41111 |
| [Frege1879] p. 70 | Proposition 95 | frege95 41112 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 41116 |
| [Frege1879] p. 71 | Proposition 96 | frege96 41113 frege96d 40903 |
| [Frege1879] p. 71 | Proposition 97 | frege97 41114 frege97d 40906 |
| [Frege1879] p. 71 | Proposition 98 | frege98 41115 frege98d 40907 |
| [Frege1879] p. 72 | Proposition 100 | frege100 41117 |
| [Frege1879] p. 72 | Proposition 101 | frege101 41118 |
| [Frege1879] p. 72 | Proposition 102 | frege102 41119 frege102d 40908 |
| [Frege1879] p. 73 | Proposition 103 | frege103 41120 |
| [Frege1879] p. 73 | Proposition 104 | frege104 41121 |
| [Frege1879] p. 73 | Proposition 105 | frege105 41122 |
| [Frege1879] p. 73 | Proposition 106 | frege106 41123 frege106d 40909 |
| [Frege1879] p. 74 | Proposition 107 | frege107 41124 |
| [Frege1879] p. 74 | Proposition 108 | frege108 41125 frege108d 40910 |
| [Frege1879] p. 74 | Proposition 109 | frege109 41126 frege109d 40911 |
| [Frege1879] p. 75 | Proposition 110 | frege110 41127 |
| [Frege1879] p. 75 | Proposition 111 | frege111 41128 frege111d 40913 |
| [Frege1879] p. 76 | Proposition 112 | frege112 41129 |
| [Frege1879] p. 76 | Proposition 113 | frege113 41130 |
| [Frege1879] p. 76 | Proposition 114 | frege114 41131 frege114d 40912 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 41132 |
| [Frege1879] p. 77 | Proposition 116 | frege116 41133 |
| [Frege1879] p. 78 | Proposition 117 | frege117 41134 |
| [Frege1879] p. 78 | Proposition 118 | frege118 41135 |
| [Frege1879] p. 78 | Proposition 119 | frege119 41136 |
| [Frege1879] p. 78 | Proposition 120 | frege120 41137 |
| [Frege1879] p. 79 | Proposition 121 | frege121 41138 |
| [Frege1879] p. 79 | Proposition 122 | frege122 41139 frege122d 40914 |
| [Frege1879] p. 79 | Proposition 123 | frege123 41140 |
| [Frege1879] p. 80 | Proposition 124 | frege124 41141 frege124d 40915 |
| [Frege1879] p. 81 | Proposition 125 | frege125 41142 |
| [Frege1879] p. 81 | Proposition 126 | frege126 41143 frege126d 40916 |
| [Frege1879] p. 82 | Proposition 127 | frege127 41144 |
| [Frege1879] p. 83 | Proposition 128 | frege128 41145 |
| [Frege1879] p. 83 | Proposition 129 | frege129 41146 frege129d 40917 |
| [Frege1879] p. 84 | Proposition 130 | frege130 41147 |
| [Frege1879] p. 85 | Proposition 131 | frege131 41148 frege131d 40918 |
| [Frege1879] p. 86 | Proposition 132 | frege132 41149 |
| [Frege1879] p. 86 | Proposition 133 | frege133 41150 frege133d 40919 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 43396 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 43716 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 43417 |
| [Fremlin1] p. 14 | Definition 112A | ismea 43531 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 43551 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 43542 meadjunre 43556 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 43543 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 43544 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 43540 meaiunle 43549 meaiunlelem 43548 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 43561 meaiuninc2 43562 meaiuninc3 43565 meaiuninc3v 43564 meaiunincf 43563 meaiuninclem 43560 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 43567 meaiininc2 43568 meaiininclem 43566 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 43586 caragendifcl 43594 caratheodory 43608 omelesplit 43598 |
| [Fremlin1] p. 19 | Definition 113A | isome 43574 isomennd 43611 isomenndlem 43610 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 43596 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 43615 voncmpl 43701 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 43578 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 43603 carageniuncllem1 43601 carageniuncllem2 43602 caragenuncl 43593 caragenuncllem 43592 caragenunicl 43604 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 43612 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 43606 caratheodorylem2 43607 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 43615 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 43674 hoidmv1lelem1 43671 hoidmv1lelem2 43672 hoidmv1lelem3 43673 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 43718 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 43674 hoidmvle 43680 hoidmvlelem1 43675 hoidmvlelem2 43676 hoidmvlelem3 43677 hoidmvlelem4 43678 hoidmvlelem5 43679 hsphoidmvle2 43665 hsphoif 43656 hsphoival 43659 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 43628 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 43636 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 43663 hoidmvn0val 43664 hoidmvval 43657 hoidmvval0 43667 hoidmvval0b 43670 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 43668 hsphoidmvle 43666 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 43617 df-voln 43619 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 43684 ovn0 43646 ovn0lem 43645 ovnf 43643 ovnome 43653 ovnssle 43641 ovnsslelem 43640 ovnsupge0 43637 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 43683 ovnhoilem1 43681 ovnhoilem2 43682 vonhoi 43747 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 43700 hoidifhspf 43698 hoidifhspval 43688 hoidifhspval2 43695 hoidifhspval3 43699 hspmbl 43709 hspmbllem1 43706 hspmbllem2 43707 hspmbllem3 43708 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 43701 vonmea 43654 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 43652 ovnsubadd2 43726 ovnsubadd2lem 43725 ovnsubaddlem1 43650 ovnsubaddlem2 43651 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 43711 hoimbl2 43745 hoimbllem 43710 hspdifhsp 43696 opnvonmbl 43714 opnvonmbllem2 43713 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 43716 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 43759 iccvonmbllem 43758 ioovonmbl 43757 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 43765 vonicclem2 43764 vonioo 43762 vonioolem2 43761 vonn0icc 43768 vonn0icc2 43772 vonn0ioo 43767 vonn0ioo2 43770 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 43769 snvonmbl 43766 vonct 43773 vonsn 43771 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 43440 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 43439 subsaliuncllem 43438 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 43800 salpreimalegt 43786 salpreimaltle 43801 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 43803 issmff 43809 issmflem 43802 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 43820 issmflelem 43819 smfpreimale 43829 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 43831 issmfgtlem 43830 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 43776 issmf 43803 issmff 43809 issmfge 43844 issmfgelem 43843 issmfgt 43831 issmfgtlem 43830 issmfle 43820 issmflelem 43819 issmflem 43802 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 43784 salpreimagtlt 43805 salpreimalelt 43804 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 43844 issmfgelem 43843 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 43828 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 43826 cnfsmf 43815 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 43841 decsmflem 43840 incsmf 43817 incsmflem 43816 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 43780 pimconstlt1 43781 smfconst 43824 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 43839 smfaddlem1 43837 smfaddlem2 43838 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 43869 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 43868 smfmullem1 43864 smfmullem2 43865 smfmullem3 43866 smfmullem4 43867 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 43870 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 43873 smfpimbor1lem2 43872 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 43875 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 43863 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 43862 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 43871 smfresal 43861 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 43851 smflim2 43878 smflimlem1 43845 smflimlem2 43846 smflimlem3 43847 smflimlem4 43848 smflimlem5 43849 smflimlem6 43850 smflimmpt 43882 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 43886 smfsuplem1 43883 smfsuplem2 43884 smfsuplem3 43885 smfsupmpt 43887 smfsupxr 43888 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 43890 smfinflem 43889 smfinfmpt 43891 |
| [Fremlin1] p. 39 | Remark 121G | smflim 43851 smflim2 43878 smflimmpt 43882 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 43880 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 43900 smflimsuplem2 43893 smflimsuplem6 43897 smflimsuplem7 43898 smflimsuplem8 43899 smflimsupmpt 43901 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 43903 smfliminflem 43902 smfliminfmpt 43904 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 43776 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 24288 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 24331 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 24341 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 35478 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 35481 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 9174 inf1 9158 inf2 9159 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 10411 enqer 10421 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 10416 df-nq 10412 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 10408 df-plq 10414 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 7401 df-mpq 10409 df-mq 10415 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 10417 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 10475 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 10476 ltbtwnnq 10478 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 10471 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 10472 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 10479 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 10481 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 10493 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 10495 |
| [Gleason] p. 122 | Definition | df-1p 10482 |
| [Gleason] p. 122 | Remark (1) | prub 10494 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 10533 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 10485 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 10532 psslinpr 10531 supexpr 10554 suplem1pr 10552 suplem2pr 10553 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 10518 addclprlem1 10516 addclprlem2 10517 df-plp 10483 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 10522 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 10521 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 10534 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 10543 ltexprlem1 10536 ltexprlem2 10537 ltexprlem3 10538 ltexprlem4 10539 ltexprlem5 10540 ltexprlem6 10541 ltexprlem7 10542 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 10545 ltaprlem 10544 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 10546 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 10547 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 10484 mulclpr 10520 mulclprlem 10519 reclem2pr 10548 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 10529 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 10524 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 10523 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 10528 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 10551 reclem3pr 10549 reclem4pr 10550 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 10555 enrer 10563 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 10560 df-1r 10561 df-nr 10556 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 10558 df-plr 10557 negexsr 10602 recexsr 10607 recexsrlem 10603 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 10559 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11711 creur 11710 cru 11708 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10688 axcnre 10664 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 14564 crimd 14681 crimi 14642 crre 14563 crred 14680 crrei 14641 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 14566 remimd 14647 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14734 absval2d 14895 absval2i 14847 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 14590 cjaddd 14669 cjaddi 14637 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 14591 cjmuld 14670 cjmuli 14638 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 14589 cjcjd 14648 cjcji 14620 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 14588 cjreb 14572 cjrebd 14651 cjrebi 14623 cjred 14675 rere 14571 rereb 14569 rerebd 14650 rerebi 14622 rered 14673 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 14597 addcjd 14661 addcji 14632 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 14687 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14729 abscjd 14900 abscji 14851 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 14739 abs00d 14896 abs00i 14848 absne0d 14897 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 14771 releabsd 14901 releabsi 14852 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 14744 absmuld 14904 absmuli 14854 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14732 sqabsaddi 14855 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 14780 abstrid 14906 abstrii 14858 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 13522 exp0 13525 expp1 13528 expp1d 13603 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 25422 cxpaddd 25460 expadd 13563 expaddd 13604 expaddz 13565 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 25431 cxpmuld 25479 expmul 13566 expmuld 13605 expmulz 13567 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 25428 mulcxpd 25471 mulexp 13560 mulexpd 13617 mulexpz 13561 |
| [Gleason] p. 140 | Exercise 1 | znnen 15657 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 12983 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 15079 rlimadd 15090 rlimdiv 15095 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 15081 rlimsub 15092 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 15080 rlimmul 15093 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 15084 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 15030 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 15051 climcj 15052 climim 15054 climre 15053 rlimabs 15056 rlimcj 15057 rlimim 15059 rlimre 15058 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 10758 df-xr 10757 ltxr 12593 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 14918 limsupval 14921 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 15119 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 15128 caucvgb 15129 caucvgr 15125 climcau 15120 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 15264 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 15331 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 14785 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 13289 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 20211 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 23096 xmet0 23095 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 23112 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 23103 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 23105 mstri 23222 xmettri 23104 xmstri 23221 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 23135 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 22399 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 24062 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 23293 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 23617 addcn2 15041 mulcn 23619 mulcn2 15043 subcn 23618 subcn2 15042 |
| [Gleason] p. 295 | Remark | bcval3 13758 bcval4 13759 |
| [Gleason] p. 295 | Equation 2 | bcpasc 13773 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 13756 df-bc 13755 |
| [Gleason] p. 296 | Remark | bcn0 13762 bcnn 13764 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 15278 |
| [Gleason] p. 308 | Equation 2 | ef0 15536 |
| [Gleason] p. 308 | Equation 3 | efcj 15537 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 15542 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 15546 |
| [Gleason] p. 310 | Equation 14 | sinadd 15609 |
| [Gleason] p. 310 | Equation 15 | cosadd 15610 |
| [Gleason] p. 311 | Equation 17 | sincossq 15621 |
| [Gleason] p. 311 | Equation 18 | cosbnd 15626 sinbnd 15625 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 13670 sqeqori 13668 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 15518 |
| [Godowski] p. 730 | Equation SF | goeqi 30208 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 29603 |
| [Golan] p. 1 | Remark | srgisid 19397 |
| [Golan] p. 1 | Definition | df-srg 19375 |
| [Golan] p. 149 | Definition | df-slmd 31031 |
| [Gonshor] p. 7 | Definition | df-scut 33619 |
| [Gonshor] p. 9 | Theorem 2.5 | slerec 33654 |
| [Gonshor] p. 10 | Theorem 2.6 | cofcut1 33728 |
| [Gonshor] p. 10 | Theorem 2.7 | cofcut2 33729 |
| [Gonshor] p. 12 | Theorem 2.9 | cofcutr 33730 |
| [Gonshor] p. 13 | Definition | df-adds 33757 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 34099 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 16960 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 16962 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 44916 df-cllaw 44914 df-comlaw 44915 |
| [Hall] p. 2 | Section 1.2 | df-clintop 44928 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 44949 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 30000 riesz2 30001 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 29876 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 30108 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 30120 elpjidm 30119 pjnmopi 30083 |
| [Halmos] p. 44 | Remark | pjinormi 29622 pjinormii 29611 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 30124 pjrn 29642 pjrni 29637 pjvec 29631 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 29662 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 30089 hmopidmpji 30087 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 30126 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 30115 pjocvec 29632 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 30104 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 30107 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 30110 pjssdif2i 30109 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 29790 |
| [Hamilton] p. 28 | Definition 2.1 | ax-1 6 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 23 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1802 |
| [Hatcher] p. 25 | Definition | df-phtpc 23744 df-phtpy 23723 |
| [Hatcher] p. 26 | Definition | df-pco 23757 df-pi1 23760 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 23747 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 23802 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 21241 df-dmatalt 45273 |
| [Helfgott] p. 2 | Theorem | tgoldbach 44803 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 44788 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 44800 bgoldbtbnd 44795 bgoldbtbnd 44795 tgblthelfgott 44801 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 32192 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 32193 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 32207 hgt750lemb 32206 hgt750leme 32208 hgt750lemf 32203 hgt750lemg 32204 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 44797 tgoldbachgt 32213 tgoldbachgtALTV 44798 tgoldbachgtd 32212 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 32194 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 28428 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 18230 grpoideu 28444 mndideu 18038 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 18256 grpoinveu 28454 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 18284 grpo2inv 28466 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 18295 grpoinvop 28468 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 18317 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1775 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1776 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1778 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 30355 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 30368 cdj3i 30376 cdj3lem1 30369 cdjreui 30367 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 30366 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 39598 |
| [Holland95] p. 14 | Line 15 | hgmapvs 39528 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 39550 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 39551 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 39548 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 39554 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 39473 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 39568 |
| [Holland95] p. 204 | Definition of involution | df-srng 19736 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 37140 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 39165 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 39118 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 37570 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 39014 poml4N 37590 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 39105 pexmidALTN 37615 pexmidN 37606 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 39170 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 36761 ldualset 36762 |
| [Holland95] p. 222 | Item 1 | df-lines 37138 df-pointsN 37139 |
| [Holland95] p. 222 | Item 2 | df-polarityN 37540 |
| [Holland95] p. 223 | Remark | ispsubcl2N 37584 omllaw4 36883 pol1N 37547 polcon3N 37554 |
| [Holland95] p. 223 | Definition | df-psubclN 37572 |
| [Holland95] p. 223 | Equation for polarity | polval2N 37543 |
| [Holmes] p. 40 | Definition | df-xrn 36124 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 29019 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 30117 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 29898 eigre 29770 eigrei 29769 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 29899 eigorth 29773 eigorthi 29772 |
| [Hughes] p. 137 | Remark (ii) | eigposi 29771 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 28246 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 28242 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 28243 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 28244 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 28262 frgrregorufr0 28261 frgrregorufrg 28263 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 28269 frrusgrord 28278 frrusgrord0 28277 |
| [Huneke] p. 2 | Statement | df-clwwlknon 28025 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 28252 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 28255 frgrwopreg2 28256 frgrwopregasn 28253 frgrwopregbsn 28254 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 28258 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 28272 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 28275 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 28023 numclwlk1 28308 numclwlk1lem1 28306 numclwlk1lem2 28307 numclwwlk1 28298 numclwwlk8 28329 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 28249 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 27712 |
| [Huneke] p. 2 | Definition 6 | 2clwwlk 28284 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 28310 numclwwlkovh0 28309 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 28318 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 27915 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 28322 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 28325 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 28328 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 28340 natded 28340 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 28340 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 28340 natded 28340 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 28340 |
| [Jech] p. 4 | Definition of class | cv 1541 cvjust 2732 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 10079 |
| [Jech] p. 42 | Equation 6.1 | alephadd 10077 alephmul 10078 |
| [Jech] p. 43 | Lemma 6.2 | infmap 10076 infmap2 9718 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 9316 |
| [Jech] p. 72 | Equation 9.3 | scott0 9388 scottex 9387 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 9369 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 9393 |
| [Jech] p. 78 | Note | opthprc 5587 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 40309 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 40397 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 40398 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 40321 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 40325 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 40326 rmyp1 40327 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 40328 rmym1 40329 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 40319 rmx1 40320 rmxluc 40330 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 40323 rmy1 40324 rmyluc 40331 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 40333 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 40334 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 40354 jm2.17b 40355 jm2.17c 40356 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 40387 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 40391 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 40382 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 40357 jm2.24nn 40353 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 40396 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 40402 rmygeid 40358 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 40414 |
| [Juillerat] p. 11 | Section *5 | etransc 43366 etransclem47 43364 etransclem48 43365 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 43361 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 43363 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 43349 |
| [Juillerat] p. 13 | Proof | etransclem35 43352 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 43355 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 43341 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 43358 |
| [Juillerat] p. 14 | Proof | etransclem23 43340 |
| [KalishMontague] p. 81 | Note 1 | ax-6 1975 |
| [KalishMontague] p. 85 | Lemma 2 | equid 2024 |
| [KalishMontague] p. 85 | Lemma 3 | equcomi 2029 |
| [KalishMontague] p. 86 | Lemma 7 | cbvalivw 2019 cbvaliw 2018 wl-cbvmotv 35295 wl-motae 35297 wl-moteq 35296 |
| [KalishMontague] p. 87 | Lemma 8 | spimvw 2007 spimw 1978 |
| [KalishMontague] p. 87 | Lemma 9 | spfw 2045 spw 2046 |
| [Kalmbach] p. 14 | Definition of lattice | chabs1 29451 chabs1i 29453 chabs2 29452 chabs2i 29454 chjass 29468 chjassi 29421 latabs1 17813 latabs2 17814 |
| [Kalmbach] p. 15 | Definition of atom | df-at 30273 ela 30274 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 30218 cvrval2 36911 |
| [Kalmbach] p. 16 | Definition | df-ol 36815 df-oml 36816 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 29519 cmbri 29525 cmtvalN 36848 df-cm 29518 df-cmtN 36814 |
| [Kalmbach] p. 22 | Remark | omllaw5N 36884 pjoml5 29548 pjoml5i 29523 |
| [Kalmbach] p. 22 | Definition | pjoml2 29546 pjoml2i 29520 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 29549 cmcmi 29527 cmcmii 29532 cmtcomN 36886 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 36882 omlsi 29339 pjoml 29371 pjomli 29370 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 36881 |
| [Kalmbach] p. 23 | Remark | cmbr2i 29531 cmcm3 29550 cmcm3i 29529 cmcm3ii 29534 cmcm4i 29530 cmt3N 36888 cmt4N 36889 cmtbr2N 36890 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 29543 cmbr3i 29535 cmtbr3N 36891 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 29553 fh1i 29556 fh2 29554 fh2i 29557 omlfh1N 36895 |
| [Kalmbach] p. 65 | Remark | chjatom 30292 chslej 29433 chsleji 29393 shslej 29315 shsleji 29305 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 29430 chocini 29389 chsupcl 29275 chsupval2 29345 h0elch 29190 helch 29178 hsupval2 29344 ocin 29231 ococss 29228 shococss 29229 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 29247 |
| [Kalmbach] p. 66 | Remark | df-pjh 29330 pjssmi 30100 pjssmii 29616 |
| [Kalmbach] p. 67 | Lemma 3 | osum 29580 osumi 29577 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 30135 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 30335 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 30245 |
| [Kalmbach] p. 140 | Remark | hatomic 30295 hatomici 30294 hatomistici 30297 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 36956 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 30316 lsatexch 36680 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 30290 cvlcvr1 36976 cvr1 37047 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 30309 cvexchi 30304 cvrexch 37057 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 30299 hlrelat 37039 hlrelat5N 37038 lrelat 36651 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 20032 lsmsatcv 36647 spansncv 29588 spansncvi 29587 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 36666 spansncv2 30228 |
| [Kalmbach] p. 266 | Definition | df-st 30146 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 29784 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 10146 fpwwe2 10143 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 10147 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 10154 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 10149 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 10151 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 10164 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchdjuidm 10168 gchxpidm 10169 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 10180 gchhar 10179 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwdjudom 9716 unxpwdom 9126 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 10170 |
| [Kreyszig] p. 3 | Property M1 | metcl 23085 xmetcl 23084 |
| [Kreyszig] p. 4 | Property M2 | meteq0 23092 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 23325 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 11435 muleqadd 11362 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 23191 |
| [Kreyszig] p. 19 | Remark | mopntopon 23192 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 23251 mopnm 23197 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 23249 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 23254 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 23295 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 22009 lmmbr 24010 lmmbr2 24011 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 22131 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 24065 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 24028 iscmet2 24046 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 24068 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 22212 metelcls 24057 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 24058 metcld2 24059 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 23851 lmodvneg1 19796 nvinv 28574 vcm 28511 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 23847 lmod0vs 19786 slmd0vs 31054 vc0 28509 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 19787 slmdvs0 31055 vcz 28510 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 28626 ngpmet 23356 nrmmetd 23327 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 28621 imsdval2 28622 ncvspds 23913 ngpds 23357 |
| [Kreyszig] p. 63 | Problem 1 | nmval 23342 nvnd 28623 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 23371 nmge0 23370 nvge0 28608 nvz 28604 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 23377 nvabs 28607 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 28736 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 28680 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 28742 blocni 28740 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 28741 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 23956 ipeq0 20454 ipz 28654 |
| [Kreyszig] p. 135 | Problem 2 | cphpyth 23968 pythi 28785 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 28789 |
| [Kreyszig] p. 137 | Lemma 3.2-1(a) | ipcau 23990 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 15304 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 24188 minveco 28819 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 28685 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 24081 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 28808 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 30058 leopg 30057 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 30076 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 28853 |
| [Kulpa] p. 547 | Theorem | poimir 35433 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 35432 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 35431 |
| [Kulpa] p. 548 | Theorem | broucube 35434 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 35426 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 35427 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2383 axnul 5173 |
| [Kunen] p. 11 | Axiom 3 | axnul 5173 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7681 |
| [Kunen] p. 24 | Definition 10.24 | mapval 8449 mapvalg 8447 |
| [Kunen] p. 30 | Lemma 10.20 | fodomg 10022 |
| [Kunen] p. 31 | Definition 10.24 | mapex 8443 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 9266 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 9308 r1elssi 9307 |
| [Kunen] p. 107 | Exercise 4 | rankop 9360 rankopb 9354 rankuni 9365 rankxplim 9381 rankxpsuc 9384 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4893 |
| [Lang] , p. 225 | Corollary 1.3 | finexttrb 31309 |
| [Lang] p. | Definition | df-rn 5536 |
| [Lang] p. 3 | Statement | lidrideqd 17995 mndbn0 18043 |
| [Lang] p. 3 | Definition | df-mnd 18028 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 18013 |
| [Lang] p. 4 | Property of composites. Second formula | gsumccat 18122 |
| [Lang] p. 5 | Equation | gsumreidx 19156 |
| [Lang] p. 5 | Definition of an (infinite) product | gsumfsupp 44910 |
| [Lang] p. 6 | Example | nn0mnd 44907 |
| [Lang] p. 6 | Equation | gsumxp2 19219 |
| [Lang] p. 6 | Statement | cycsubm 18463 |
| [Lang] p. 6 | Definition | mulgnn0gsum 18352 |
| [Lang] p. 6 | Observation | mndlsmidm 18914 |
| [Lang] p. 7 | Definition | dfgrp2e 18247 |
| [Lang] p. 30 | Definition | df-tocyc 30951 |
| [Lang] p. 32 | Property (a) | cyc3genpm 30996 |
| [Lang] p. 32 | Property (b) | cyc3conja 31001 cycpmconjv 30986 |
| [Lang] p. 53 | Definition | df-cat 17042 |
| [Lang] p. 53 | Axiom CAT 1 | cat1 17469 cat1lem 17468 |
| [Lang] p. 54 | Definition | df-iso 17124 |
| [Lang] p. 57 | Definition | df-inito 17356 df-termo 17357 |
| [Lang] p. 58 | Example | irinitoringc 45161 |
| [Lang] p. 58 | Statement | initoeu1 17383 termoeu1 17390 |
| [Lang] p. 62 | Definition | df-func 17233 |
| [Lang] p. 65 | Definition | df-nat 17318 |
| [Lang] p. 91 | Note | df-ringc 45097 |
| [Lang] p. 92 | Statement | mxidlprm 31212 |
| [Lang] p. 92 | Definition | isprmidlc 31195 |
| [Lang] p. 128 | Remark | dsmmlmod 20561 |
| [Lang] p. 129 | Proof | lincscm 45305 lincscmcl 45307 lincsum 45304 lincsumcl 45306 |
| [Lang] p. 129 | Statement | lincolss 45309 |
| [Lang] p. 129 | Observation | dsmmfi 20554 |
| [Lang] p. 141 | Theorem 5.3 | dimkerim 31280 qusdimsum 31281 |
| [Lang] p. 141 | Corollary 5.4 | lssdimle 31263 |
| [Lang] p. 147 | Definition | snlindsntor 45346 |
| [Lang] p. 504 | Statement | mat1 21198 matring 21194 |
| [Lang] p. 504 | Definition | df-mamu 21137 |
| [Lang] p. 505 | Statement | mamuass 21153 mamutpos 21209 matassa 21195 mattposvs 21206 tposmap 21208 |
| [Lang] p. 513 | Definition | mdet1 21352 mdetf 21346 |
| [Lang] p. 513 | Theorem 4.4 | cramer 21442 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 21338 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 21362 |
| [Lang] p. 515 | Definition | df-minmar1 21386 smadiadetr 21426 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 21361 mdetralt 21359 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 21374 |
| [Lang] p. 518 | Definition | df-madu 21385 |
| [Lang] p. 518 | Proposition 4.16 | madulid 21396 madurid 21395 matinv 21428 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 21641 |
| [Lang], p. 224 | Proposition 1.2 | extdgmul 31308 fedgmul 31284 |
| [Lang], p. 561 | Remark | chpmatply1 21583 |
| [Lang], p. 561 | Definition | df-chpmat 21578 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 41490 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 41485 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 41491 |
| [LeBlanc] p. 277 | Rule R2 | axnul 5173 |
| [Levy] p. 12 | Axiom 4.3.1 | df-clab 2717 |
| [Levy] p. 338 | Axiom | df-clel 2811 df-cleq 2730 |
| [Levy] p. 357 | Proof sketch of conservativity; for details see Appendix | df-clel 2811 df-cleq 2730 |
| [Levy] p. 357 | Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendix | df-clab 2717 |
| [Levy] p. 358 | Axiom | df-clab 2717 |
| [Levy58] p. 2 | Definition I | isfin1-3 9886 |
| [Levy58] p. 2 | Definition II | df-fin2 9786 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 9785 |
| [Levy58] p. 2 | Definition III | df-fin3 9788 |
| [Levy58] p. 3 | Definition V | df-fin5 9789 |
| [Levy58] p. 3 | Definition IV | df-fin4 9787 |
| [Levy58] p. 4 | Definition VI | df-fin6 9790 |
| [Levy58] p. 4 | Definition VII | df-fin7 9791 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 9915 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 33530 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 33541 |
| [Lipparini] p. 6 | Proposition 4.2 | noinfbnd1 33573 nosupbnd1 33558 |
| [Lipparini] p. 6 | Proposition 4.3 | noinfbnd2 33575 nosupbnd2 33560 |
| [Lipparini] p. 7 | Theorem 5.1 | noetasuplem3 33579 noetasuplem4 33580 |
| [Lipparini] p. 7 | Corollary 4.4 | nosupinfsep 33576 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1775 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1776 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1778 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 30343 |
| [Maeda] p. 168 | Lemma 5 | mdsym 30347 mdsymi 30346 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 30341 mdsymlem6 30343 mdsymlem7 30344 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 30345 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 30248 ssdmd2 30249 ssmd1 30246 ssmd2 30247 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 30244 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 30216 df-md 30215 mdbr 30229 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 30266 mdslj1i 30254 mdslj2i 30255 mdslle1i 30252 mdslle2i 30253 mdslmd1i 30264 mdslmd2i 30265 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 30256 mdsl2bi 30258 mdsl2i 30257 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 30270 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 30267 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 30268 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 30245 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 30250 mdsl3 30251 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 30269 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 30364 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 36958 hlrelat1 37037 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 36676 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 30271 cvmdi 30259 cvnbtwn4 30224 cvrnbtwn4 36916 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 30272 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 36977 cvp 30310 cvrp 37053 lcvp 36677 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 30334 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 30333 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 36970 hlexch4N 37029 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 30336 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 37080 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 37386 atpsubN 37390 df-pointsN 37139 pointpsubN 37388 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 37141 pmap11 37399 pmaple 37398 pmapsub 37405 pmapval 37394 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 37402 pmap1N 37404 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 37407 pmapglb2N 37408 pmapglb2xN 37409 pmapglbx 37406 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 37489 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 37114 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 37433 paddclN 37479 paddidm 37478 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 37115 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 37475 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 37114 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 37115 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 18919 lsmmod2 18920 lssats 36649 shatomici 30293 shatomistici 30296 shmodi 29325 shmodsi 29324 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 30235 mdsymlem7 30344 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 29524 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 29428 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 30350 |
| [Margaris] p. 40 | Rule C | exlimiv 1937 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | ax-3 8 |
| [Margaris] p. 49 | Definition | df-an 400 df-ex 1787 df-or 847 dfbi2 478 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 28337 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 42073 |
| [Margaris] p. 60 | Theorem 8 | jcn 165 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 42074 |
| [Margaris] p. 79 | Rule C | exinst01 41783 exinst11 41784 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1986 19.2g 2189 r19.2z 4381 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2204 rr19.3v 3565 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2164 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1832 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1788 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2182 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2207 19.9h 2290 exlimd 2220 exlimdh 2294 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2170 excomim 2171 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2329 |
| [Margaris] p. 90 | Section 19 | conventions-labels 28338 conventions-labels 28338 conventions-labels 28338 conventions-labels 28338 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1833 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 41534 albi 1825 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 2227 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 2228 |
| [Margaris] p. 90 | Theorem 19.18 | 2exbi 41536 exbi 1853 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2231 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 41533 2alimdv 1925 alimd 2214 alimdh 1824 alimdv 1923 ax-4 1816 ralimdaa 3129 ralimdv 3092 ralimdva 3091 ralimdvva 3093 sbcimdv 3751 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2209 19.21h 2291 19.21t 2208 19.21vv 41532 alrimd 2217 alrimdd 2216 alrimdh 1870 alrimdv 1936 alrimi 2215 alrimih 1830 alrimiv 1934 alrimivv 1935 hbralrimi 3094 r19.21be 3122 r19.21bi 3121 ralrimd 3130 ralrimdv 3100 ralrimdva 3101 ralrimdvv 3105 ralrimdvva 3106 ralrimi 3128 ralrimia 3396 ralrimiv 3095 ralrimiva 3096 ralrimivv 3102 ralrimivva 3103 ralrimivvva 3104 ralrimivw 3097 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 41535 2eximdv 1926 exim 1840 eximd 2218 eximdh 1871 eximdv 1924 rexim 3154 reximd2a 3222 reximdai 3221 reximdd 42239 reximddv 3185 reximddv2 3188 reximddv3 42238 reximdv 3183 reximdv2 3181 reximdva 3184 reximdvai 3182 reximdvva 3187 reximi2 3158 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2213 19.23bi 2192 19.23h 2292 19.23t 2212 exlimdv 1940 exlimdvv 1941 exlimexi 41682 exlimiv 1937 exlimivv 1939 rexlimd3 42231 rexlimdv 3193 rexlimdv3a 3196 rexlimdva 3194 rexlimdva2 3197 rexlimdvaa 3195 rexlimdvv 3203 rexlimdvva 3204 rexlimdvw 3200 rexlimiv 3190 rexlimiva 3191 rexlimivv 3202 |
| [Margaris] p. 90 | Theorem 19.24 | 19.24 1997 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1887 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26 1877 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 2229 r19.27z 4391 r19.27zv 4392 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2230 19.28vv 41542 r19.28z 4384 r19.28zv 4387 rr19.28v 3566 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1880 r19.29d2r 3242 r19.29imd 3169 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1888 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2236 19.31vv 41540 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2235 r19.32 44122 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 41538 19.33 1891 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1998 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35 1884 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36 2232 19.36vv 41539 r19.36zv 4393 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2234 19.37vv 41541 r19.37zv 4388 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1845 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 1996 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1894 19.40 1893 r19.40 3250 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2237 19.41rg 41708 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2238 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1889 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2239 r19.44zv 4390 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2240 r19.45zv 4389 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2613 |
| [Mayet] p. 370 | Remark | jpi 30205 largei 30202 stri 30192 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 30147 ishst 30149 |
| [Mayet3] p. 10 | Theorem | hstrbi 30201 hstri 30200 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 29663 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 29664 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 30213 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 29267 chsupcl 29275 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 30295 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 30289 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 30316 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 37620 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 17825 latj32 17823 latjass 17821 |
| [Megill] p. 444 | Axiom C5 | ax-5 1917 ax5ALT 36544 |
| [Megill] p. 444 | Section 7 | conventions 28337 |
| [Megill] p. 445 | Lemma L12 | aecom-o 36538 ax-c11n 36525 axc11n 2426 |
| [Megill] p. 446 | Lemma L17 | equtrr 2034 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 36533 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 36565 hbnae 2432 |
| [Megill] p. 447 | Remark 9.1 | dfsb1 2485 sbid 2257 sbidd-misc 45874 sbidd 45873 |
| [Megill] p. 448 | Remark 9.6 | axc14 2463 |
| [Megill] p. 448 | Scheme C4' | ax-c4 36521 |
| [Megill] p. 448 | Scheme C5' | ax-c5 36520 sp 2184 |
| [Megill] p. 448 | Scheme C6' | ax-11 2162 |
| [Megill] p. 448 | Scheme C7' | ax-c7 36522 |
| [Megill] p. 448 | Scheme C8' | ax-7 2020 |
| [Megill] p. 448 | Scheme C9' | ax-c9 36527 |
| [Megill] p. 448 | Scheme C10' | ax-6 1975 ax-c10 36523 |
| [Megill] p. 448 | Scheme C11' | ax-c11 36524 |
| [Megill] p. 448 | Scheme C12' | ax-8 2116 |
| [Megill] p. 448 | Scheme C13' | ax-9 2124 |
| [Megill] p. 448 | Scheme C14' | ax-c14 36528 |
| [Megill] p. 448 | Scheme C15' | ax-c15 36526 |
| [Megill] p. 448 | Scheme C16' | ax-c16 36529 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 36541 dral1 2439 dral2-o 36567 dral2 2438 drex1 2441 drex2 2442 drsb1 2499 drsb2 2267 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2169 sbequ 2093 sbid2v 2513 |
| [Megill] p. 450 | Example in Appendix | hba1-o 36534 hba1 2297 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 43926 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3770 rspsbca 3771 stdpc4 2078 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 36521 ra4 3777 stdpc5 2210 |
| [Mendelson] p. 81 | Rule C | exlimiv 1937 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 2040 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 2252 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3679 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 5371 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 4283 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 4284 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 4157 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 4212 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 4158 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 4027 |
| [Mendelson] p. 231 | Definition of union | dfun3 4156 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 5310 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4793 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5423 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4508 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5425 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4822 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5670 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 6101 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 7516 |
| [Mendelson] p. 246 | Definition of successor | df-suc 6178 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 8252 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8730 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8650 xpsneng 8651 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8657 xpcomeng 8658 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8660 |
| [Mendelson] p. 255 | Definition | brsdom 8578 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8653 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 8441 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8636 mapsnend 8635 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8736 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8735 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 8492 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8639 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8654 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 9678 djucomen 9677 |
| [Mendelson] p. 258 | Exercise 4.56(f) | djudom1 9682 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 9676 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 8187 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 8215 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 10059 |
| [Mendelson] p. 281 | Definition | df-r1 9266 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 9315 |
| [Mendelson] p. 287 | Axiom system MK | ru 3679 |
| [MertziosUnger] p. 152 | Definition | df-frgr 28196 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 28231 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 28233 vdgn1frgrv3 28234 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 28235 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 28228 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 28221 2pthfrgrrn 28219 2pthfrgrrn2 28220 |
| [Mittelstaedt] p. 9 | Definition | df-oc 29187 |
| [Monk1] p. 22 | Remark | conventions 28337 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 28337 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 4121 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5628 ssrelf 30529 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5629 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 5093 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 6095 coi2 6096 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5763 rn0 5769 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5974 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5543 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5772 rnxp 6002 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5620 xp0 5990 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5919 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5916 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7647 imaexALTV 36088 imaexg 7646 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5914 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6853 funfvop 6827 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6725 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6735 |
| [Monk1] p. 43 | Theorem 4.6 | funun 6385 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 7024 dff13f 7025 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 6992 funrnex 7680 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 7017 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 6059 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4852 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7731 df-1st 7714 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7732 df-2nd 7715 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 9356 ranksnb 9329 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 9357 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 9358 rankunb 9352 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 9340 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 9266 r1val2 9339 |
| [Monk1] p. 117 | Lemma | zorn2 10006 zorn2g 10003 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 9488 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 10061 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 9483 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1816 |
| [Monk2] p. 105 | Axiom C7 | ax-7 2020 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2179 ax-c15 36526 ax12v2 2181 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 36521 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2162 |
| [Monk2] p. 109 | Lemma 15 | equvini 2455 equvinv 2041 eqvinop 5344 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1917 ax5ALT 36544 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2145 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2162 |
| [Monk2] p. 114 | Lemma 21 | sp 2184 |
| [Monk2] p. 114 | Lemma 22 | axc4 2323 hba1-o 36534 hba1 2297 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2158 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2178 nfra2 3142 nfra2w 3140 |
| [Moore] p. 53 | Part I | df-mre 16960 |
| [Munkres] p. 77 | Example 2 | distop 21746 indistop 21753 indistopon 21752 |
| [Munkres] p. 77 | Example 3 | fctop 21755 fctop2 21756 |
| [Munkres] p. 77 | Example 4 | cctop 21757 |
| [Munkres] p. 78 | Definition of basis | df-bases 21697 isbasis3g 21700 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 16820 tgval2 21707 |
| [Munkres] p. 79 | Remark | tgcl 21720 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 21714 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 21738 tgss3 21737 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 21739 basgen2 21740 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 35143 topdifinfeq 35144 topdifinffin 35142 topdifinfindis 35140 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 21911 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 21789 topcld 21786 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 21790 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 21792 |
| [Munkres] p. 94 | Definition of closure | clsval 21788 |
| [Munkres] p. 94 | Definition of interior | ntrval 21787 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 21826 elcls 21824 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 21834 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 21899 neindisj 21868 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 21901 |
| [Munkres] p. 97 | Definition of limit point | islp2 21896 lpval 21890 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 22066 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 21978 iscn 21986 iscn2 21989 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 22031 cncnp2 22032 cncnpi 22029 df-cnp 21979 iscnp 21988 iscnp2 21990 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 23296 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 24063 |
| [Nathanson] p. 123 | Remark | reprgt 32171 reprinfz1 32172 reprlt 32169 |
| [Nathanson] p. 123 | Definition | df-repr 32159 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 32191 |
| [Nathanson] p. 123 | Proposition | breprexp 32183 breprexpnat 32184 itgexpif 32156 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 30039 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 44796 |
| [Pfenning] p. 17 | Definition XM | natded 28340 |
| [Pfenning] p. 17 | Definition NNC | natded 28340 notnotrd 135 |
| [Pfenning] p. 17 | Definition ` `C | natded 28340 |
| [Pfenning] p. 18 | Rule" | natded 28340 |
| [Pfenning] p. 18 | Definition /\I | natded 28340 |
| [Pfenning] p. 18 | Definition ` `E | natded 28340 natded 28340 natded 28340 natded 28340 natded 28340 |
| [Pfenning] p. 18 | Definition ` `I | natded 28340 natded 28340 natded 28340 natded 28340 natded 28340 |
| [Pfenning] p. 18 | Definition ` `EL | natded 28340 |
| [Pfenning] p. 18 | Definition ` `ER | natded 28340 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 28340 |
| [Pfenning] p. 18 | Definition ` `IR | natded 28340 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 28340 |
| [Pfenning] p. 127 | Definition =E | natded 28340 |
| [Pfenning] p. 127 | Definition =I | natded 28340 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 23954 df-dip 28636 dip0l 28653 ip0l 20452 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 23995 ipval 28638 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 28649 ipcj 20450 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 23957 dipdir 28777 ipdir 20455 ipdiri 28765 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 28645 nmsq 23946 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 28760 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 28762 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 28763 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 23963 dipass 28780 ipass 20461 ipassi 28776 |
| [Prugovecki] p. 186 | Definition of bra | braval 29879 df-bra 29785 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 29786 kbval 29889 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 30317 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 37525 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 30331 atcvat4i 30332 cvrat3 37079 cvrat4 37080 lsatcvat3 36689 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 30217 cvrval 36906 df-cv 30214 df-lcv 36656 lspsncv0 20037 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 37537 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 37538 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2717 rabid 3281 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2283 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2730 |
| [Quine] p. 19 | Definition 2.9 | conventions 28337 df-v 3400 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2864 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2873 abid2f 2931 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2276 |
| [Quine] p. 40 | Theorem 6.2 | sb6 2095 sbalex 2244 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2811 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2738 eqid1 28404 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2745 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3681 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3682 dfsbcq2 3683 |
| [Quine] p. 43 | Theorem 6.8 | vex 3402 |
| [Quine] p. 43 | Theorem 6.9 | isset 3411 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3495 spcgv 3500 spcimgf 3493 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3693 spsbcd 3694 |
| [Quine] p. 44 | Theorem 6.12 | elex 3416 |
| [Quine] p. 44 | Theorem 6.13 | elab 3573 elabg 3571 elabgf 3568 |
| [Quine] p. 44 | Theorem 6.14 | noel 4219 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4608 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4519 df-sn 4517 |
| [Quine] p. 49 | Theorem 7.4 | snss 4674 snssg 4673 |
| [Quine] p. 49 | Theorem 7.5 | prss 4708 prssg 4707 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4653 prid1g 4651 prid2 4654 prid2g 4652 snid 4552 snidg 4550 |
| [Quine] p. 51 | Theorem 7.12 | snex 5298 |
| [Quine] p. 51 | Theorem 7.13 | prex 5299 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4818 unisnALT 42084 unisng 4817 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4821 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4828 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4826 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 6312 |
| [Quine] p. 56 | Definition 8.18 | dfaiota2 44110 dfiota2 6298 |
| [Quine] p. 57 | Theorem 8.19 | aiotaval 44119 iotaval 6313 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 6317 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 6319 |
| [Quine] p. 58 | Definition 9.1 | df-op 4523 |
| [Quine] p. 61 | Theorem 9.5 | opabid 5381 opabidw 5380 opelopab 5397 opelopaba 5391 opelopabaf 5399 opelopabf 5400 opelopabg 5393 opelopabga 5388 opelopabgf 5395 oprabid 7202 oprabidw 7201 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5531 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5533 |
| [Quine] p. 64 | Definition 9.15 | df-id 5429 |
| [Quine] p. 65 | Theorem 10.3 | fun0 6404 |
| [Quine] p. 65 | Theorem 10.4 | funi 6371 |
| [Quine] p. 65 | Theorem 10.5 | funsn 6392 funsng 6390 |
| [Quine] p. 65 | Definition 10.1 | df-fun 6341 |
| [Quine] p. 65 | Definition 10.2 | args 5931 dffv4 6671 |
| [Quine] p. 68 | Definition 10.11 | conventions 28337 df-fv 6347 fv2 6669 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13724 nn0opth2i 13723 nn0opthi 13722 omopthi 8315 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 8075 |
| [Quine] p. 232 | Equation i | carddom 10054 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 6426 funimaexg 6425 |
| [Quine] p. 331 | Axiom system NF | ru 3679 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 29019 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 28636 polid 29094 polid2i 29092 polidi 29093 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 28748 |
| [ReedSimon] p. 195 | Remark | lnophm 29954 lnophmi 29953 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 30067 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 30069 leopmuli 30068 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 30072 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 29787 leoppos 30061 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 30071 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 30060 |
| [Roman] p. 4 | Definition | df-dmat 21241 df-dmatalt 45273 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 44967 |
| [Roman] p. 19 | Part Preliminaries | df-ring 19418 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 45360 |
| [Roman] p. 112 | Note | isldepslvec2 45360 ldepsnlinc 45383 zlmodzxznm 45372 |
| [Roman] p. 112 | Example | zlmodzxzequa 45371 zlmodzxzequap 45374 zlmodzxzldep 45379 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 21641 |
| [Rosenlicht] p. 80 | Theorem | heicant 35435 |
| [Rosser] p. 281 | Definition | df-op 4523 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 32195 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 32196 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 45236 pmtr3ncom 18721 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 18717 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 18660 cayleyth 18661 |
| [Rudin] p. 164 | Equation 27 | efcan 15541 |
| [Rudin] p. 164 | Equation 30 | efzval 15547 |
| [Rudin] p. 167 | Equation 48 | absefi 15641 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 200 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1778 |
| [Sanford] p. 39 | Rule 4 | mptxor 1776 |
| [Sanford] p. 40 | Rule 1 | mptnan 1775 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5949 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5952 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5948 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5946 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 16960 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 16961 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 16961 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 16963 |
| [Schechter] p. 139 | Definition AC3 | dfac9 9636 |
| [Schechter] p. 141 | Definition (MC) | dfac11 40459 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 9946 axdc3 9954 |
| [Schechter] p. 187 | Definition of ring with unit | isring 19420 isrngo 35678 |
| [Schechter] p. 276 | Remark 11.6.e | span0 29477 |
| [Schechter] p. 276 | Definition of span | df-span 29244 spanval 29268 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 21744 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 26860 axtgcgrrflx 26408 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 26861 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 26862 axtgcgrid 26409 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 26394 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 26873 axtgsegcon 26410 df-trkgcb 26396 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 26884 axtg5seg 26411 df-trkgcb 26396 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 26885 axtgbtwnid 26412 df-trkgb 26395 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 26887 axtgpasch 26413 df-trkgb 26395 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 26906 df-trkg2d 32215 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 26416 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 26417 df-trkg2d 32215 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 26909 axtgeucl 26418 df-trkge 26397 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 26922 axtgcont 26415 axtgcont1 26414 df-trkgb 26395 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 33927 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 33929 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 33932 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 33936 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 33937 tgcgrcomimp 26423 tgcgrcoml 26425 tgcgrcomr 26424 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 33942 tgcgrtriv 26430 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 33946 tg5segofs 32223 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 32220 df-ofs 33923 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 33948 tgcgrextend 26431 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 33950 tgsegconeq 26432 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 33962 btwntriv2 33952 tgbtwntriv2 26433 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 33953 tgbtwncom 26434 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 33956 tgbtwntriv1 26437 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 33957 tgbtwnswapid 26438 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 33963 btwnintr 33959 tgbtwnexch2 26442 tgbtwnintr 26439 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 33965 btwnexch3 33960 tgbtwnexch 26444 tgbtwnexch3 26440 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 33964 tgbtwnouttr 26443 tgbtwnouttr2 26441 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 26905 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 33967 tgbtwndiff 26452 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 26445 trisegint 33968 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 33984 tgifscgr 26454 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 26504 colrot1 26505 colrot2 26506 lncom 26568 lnrot1 26569 lnrot2 26570 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 33980 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 33985 tgcgrsub 26455 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 33995 tgcgrxfr 26464 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 26463 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 33981 df-cgrg 26457 |
| [Schwabhauser] p. 35 | Definition instead (given | df-cgrg 26457 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 33996 tgbtwnxfr 26476 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 34002 colinearperm2 34004 colinearperm3 34003 colinearperm4 34005 colinearperm5 34006 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 26479 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 33979 tgellng 26499 tglng 26492 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 34007 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 34015 lnxfr 26512 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 34016 lnext 26513 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 34020 tgfscgr 26514 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 34021 lncgr 26515 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 33982 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 34023 lnid 26516 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 34024 tgidinside 26517 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 34041 tgbtwnconn1 26521 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 34042 tgbtwnconn2 26522 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 34043 tgbtwnconn3 26523 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 34049 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 34047 legov 26531 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 26532 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 26545 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 34050 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 34052 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 34054 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 34055 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 34056 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 34053 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 34058 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 26533 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 26535 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 26536 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 26537 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 26538 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 34065 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 34066 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 34061 df-outsideof 34060 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 34062 ishlg 26548 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 26553 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 26555 outsideofrflx 34067 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 26549 hlcomd 26550 outsideofcom 34068 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 26556 outsideoftr 34069 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 26564 outsideofeu 34071 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 34078 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 34079 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 34072 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 34087 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 34088 tglineelsb2 26578 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 34090 linerflx1 34089 linerflx2 34091 tglinecom 26581 tglinerflx1 26579 tglinerflx2 26580 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 34093 tglinethru 26582 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 34077 tglng 26492 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 26540 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 34096 tglinethrueu 26585 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 34097 tglineineq 26589 tglineinteq 26591 tglineintmo 26588 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 26595 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 26596 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 26597 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 26612 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 26608 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 26600 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 26599 ismir 26605 mirbtwn 26604 mircgr 26603 mirfv 26602 mirval 26601 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 26610 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 26611 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 26612 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 26615 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 26616 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 26621 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 26618 mirbtwni 26617 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 26619 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 26631 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 26635 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 26632 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 26633 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 26634 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 26637 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 26638 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 26644 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 26640 israg 26643 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 26645 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 26646 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 26648 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 26649 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 26650 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 26651 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 26652 ragncol 26655 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 26653 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 26659 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 26663 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 26660 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 26642 isperp 26658 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 26661 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 26668 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 26676 colperpexlem2 26677 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 26679 colperpexlem3 26678 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 26684 midex 26683 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 26681 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 26690 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 26685 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 26694 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 26697 opphllem6 26698 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 26700 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 26413 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 26701 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 26709 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 26704 hpgbr 26706 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 26711 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 26710 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 26712 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 26713 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 26714 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 26715 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 26716 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 26730 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 26720 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 26734 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 26735 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 26736 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 26737 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 26738 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 26741 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 26743 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 26721 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 26744 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 26747 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 26748 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 26749 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 26750 trgcopyeu 26752 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 26776 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 26755 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 26764 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 26762 cgrahl2 26763 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 26765 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 26766 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 26768 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 26769 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 26772 cgrahl 26773 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 26777 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 26778 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 26779 acopyeu 26780 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 26787 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 26791 |
| [Schwabhauser] p. 101 | Definition 11.23 | isinag 26784 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 26799 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 26792 isleag 26793 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 26801 tgsas1 26800 tgsas2 26802 tgsas3 26803 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 26805 tgasa1 26804 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 26806 tgsss2 26807 tgsss3 26808 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 26007 dchrsum 26005 dchrsum2 26004 sumdchr 26008 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 26009 sum2dchr 26010 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 19307 ablfacrp2 19308 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 25952 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 25953 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 25960 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 26218 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 26221 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 26275 vmalogdivsum2 26274 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 26265 dirith2 26264 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 26263 rpvmasum 26262 rpvmasum2 26248 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 26223 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 26261 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 26228 dchrisumlem1 26225 dchrisumlem2 26226 dchrisumlem3 26227 dchrisumlema 26224 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 26231 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 26260 dchrmusumlem 26258 dchrvmasumlem 26259 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 26230 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 26232 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 26256 dchrisum0re 26249 dchrisumn0 26257 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 26242 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 26246 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 26247 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 26302 pntrsumbnd2 26303 pntrsumo1 26301 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 26266 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 26268 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 26270 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 26273 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 26278 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 26279 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 26284 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 26286 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 26287 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 26295 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 26296 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 26293 selberg3lem2 26294 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 26297 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 26291 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 26304 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 26305 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 26306 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 26320 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 26332 pntlemb 26333 pntlemc 26331 pntlemd 26330 pntlemg 26334 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 26332 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 26324 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 26329 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 26332 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 26345 pntleml 26347 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 4187 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 4290 dif0 4261 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4378 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4364 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 4178 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 4179 |
| [Stoll] p. 20 | Remark | invdif 4159 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4525 |
| [Stoll] p. 43 | Definition | uniiun 4944 |
| [Stoll] p. 44 | Definition | intiin 4945 |
| [Stoll] p. 45 | Definition | df-iin 4884 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4883 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 405 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 4187 |
| [Strang] p. 242 | Section 6.3 | expgrowth 41491 |
| [Suppes] p. 22 | Theorem 2 | eq0 4232 eq0f 4229 |
| [Suppes] p. 22 | Theorem 4 | eqss 3892 eqssd 3894 eqssi 3893 |
| [Suppes] p. 23 | Theorem 5 | ss0 4287 ss0b 4286 |
| [Suppes] p. 23 | Theorem 6 | sstr 3885 sstrALT2 41993 |
| [Suppes] p. 23 | Theorem 7 | pssirr 3991 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 3992 |
| [Suppes] p. 23 | Theorem 9 | psstr 3995 |
| [Suppes] p. 23 | Theorem 10 | pssss 3986 |
| [Suppes] p. 25 | Theorem 12 | elin 3859 elun 4039 |
| [Suppes] p. 26 | Theorem 15 | inidm 4109 |
| [Suppes] p. 26 | Theorem 16 | in0 4280 |
| [Suppes] p. 27 | Theorem 23 | unidm 4042 |
| [Suppes] p. 27 | Theorem 24 | un0 4279 |
| [Suppes] p. 27 | Theorem 25 | ssun1 4062 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 4070 |
| [Suppes] p. 27 | Theorem 27 | unss 4074 |
| [Suppes] p. 27 | Theorem 28 | indir 4166 |
| [Suppes] p. 27 | Theorem 29 | undir 4167 |
| [Suppes] p. 28 | Theorem 32 | difid 4259 |
| [Suppes] p. 29 | Theorem 33 | difin 4152 |
| [Suppes] p. 29 | Theorem 34 | indif 4160 |
| [Suppes] p. 29 | Theorem 35 | undif1 4365 |
| [Suppes] p. 29 | Theorem 36 | difun2 4370 |
| [Suppes] p. 29 | Theorem 37 | difin0 4363 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4361 |
| [Suppes] p. 29 | Theorem 39 | difundi 4170 |
| [Suppes] p. 29 | Theorem 40 | difindi 4172 |
| [Suppes] p. 30 | Theorem 41 | nalset 5181 |
| [Suppes] p. 39 | Theorem 61 | uniss 4804 |
| [Suppes] p. 39 | Theorem 65 | uniop 5372 |
| [Suppes] p. 41 | Theorem 70 | intsn 4874 |
| [Suppes] p. 42 | Theorem 71 | intpr 4870 intprg 4869 |
| [Suppes] p. 42 | Theorem 73 | op1stb 5329 |
| [Suppes] p. 42 | Theorem 78 | intun 4868 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4919 dfiun2g 4917 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4920 |
| [Suppes] p. 47 | Theorem 86 | elpw 4492 elpw2 5213 elpw2g 5212 elpwg 4491 elpwgdedVD 42075 |
| [Suppes] p. 47 | Theorem 87 | pwid 4512 |
| [Suppes] p. 47 | Theorem 89 | pw0 4700 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4701 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5540 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5676 xpindir 5677 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5591 xpundir 5592 |
| [Suppes] p. 54 | Theorem 105 | elirrv 9133 |
| [Suppes] p. 58 | Theorem 2 | relss 5627 |
| [Suppes] p. 59 | Theorem 4 | eldm 5743 eldm2 5744 eldm2g 5742 eldmg 5741 |
| [Suppes] p. 59 | Definition 3 | df-dm 5535 |
| [Suppes] p. 60 | Theorem 6 | dmin 5754 |
| [Suppes] p. 60 | Theorem 8 | rnun 5978 |
| [Suppes] p. 60 | Theorem 9 | rnin 5979 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5731 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5725 brcnvg 5722 |
| [Suppes] p. 62 | Equation 5 | elcnv 5719 elcnv2 5720 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5941 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5977 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5975 |
| [Suppes] p. 63 | Definition | dftrrels2 36312 |
| [Suppes] p. 63 | Theorem 20 | co02 6093 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5814 |
| [Suppes] p. 63 | Definition 7 | df-co 5534 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5728 |
| [Suppes] p. 64 | Theorem 27 | coass 6098 |
| [Suppes] p. 65 | Theorem 31 | resundi 5839 |
| [Suppes] p. 65 | Theorem 34 | elima 5908 elima2 5909 elima3 5910 elimag 5907 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5982 |
| [Suppes] p. 66 | Theorem 40 | dminss 5985 |
| [Suppes] p. 66 | Theorem 41 | imainss 5986 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5989 |
| [Suppes] p. 81 | Definition 34 | dfec2 8323 |
| [Suppes] p. 82 | Theorem 72 | elec 8364 elecALTV 36028 elecg 8363 |
| [Suppes] p. 82 | Theorem 73 | eqvrelth 36347 erth 8369 erth2 8370 |
| [Suppes] p. 83 | Theorem 74 | eqvreldisj 36350 erdisj 8372 |
| [Suppes] p. 89 | Theorem 96 | map0b 8493 |
| [Suppes] p. 89 | Theorem 97 | map0 8497 map0g 8494 |
| [Suppes] p. 89 | Theorem 98 | mapsn 8498 mapsnd 8496 |
| [Suppes] p. 89 | Theorem 99 | mapss 8499 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 9568 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 9567 |
| [Suppes] p. 92 | Theorem 1 | enref 8588 enrefg 8587 |
| [Suppes] p. 92 | Theorem 2 | ensym 8604 ensymb 8603 ensymi 8605 |
| [Suppes] p. 92 | Theorem 3 | entr 8607 |
| [Suppes] p. 92 | Theorem 4 | unen 8644 |
| [Suppes] p. 94 | Theorem 15 | endom 8582 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8601 |
| [Suppes] p. 94 | Theorem 17 | domtr 8608 |
| [Suppes] p. 95 | Theorem 18 | sbth 8687 |
| [Suppes] p. 97 | Theorem 23 | canth2 8720 canth2g 8721 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8691 df-sdom 8558 dfsdom2 8690 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8704 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8693 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8692 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8702 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 8585 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8705 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8700 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8630 fundmeng 8631 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8664 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8701 |
| [Suppes] p. 104 | Theorem 37 | fofi 8883 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8776 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8776 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 10051 |
| [Suppes] p. 130 | Definition 3 | df-tr 5137 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 7520 |
| [Suppes] p. 134 | Definition 6 | df-suc 6178 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7633 finds 7629 finds1 7632 finds2 7631 |
| [Suppes] p. 151 | Theorem 42 | isfinite 9188 isfinite2 8850 isfiniteg 8852 unbnn 8848 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 10418 df-ltpq 10410 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7596 tfinds 7593 tfinds2 7597 |
| [Suppes] p. 209 | Theorem 18 | oaord1 8208 |
| [Suppes] p. 209 | Theorem 21 | oaword2 8210 |
| [Suppes] p. 211 | Theorem 25 | oaass 8218 |
| [Suppes] p. 225 | Definition 8 | iscard2 9478 |
| [Suppes] p. 227 | Theorem 56 | ondomon 10063 |
| [Suppes] p. 228 | Theorem 59 | harcard 9480 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 9566 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 6222 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 7532 onminsb 7533 |
| [Suppes] p. 229 | Theorem 64 | alephval2 10072 |
| [Suppes] p. 229 | Theorem 65 | alephcard 9570 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 9577 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 9571 |
| [Suppes] p. 229 | Definition 12 | df-aleph 9442 |
| [Suppes] p. 242 | Theorem 6 | weth 9995 |
| [Suppes] p. 242 | Theorem 8 | entric 10057 |
| [Suppes] p. 242 | Theorem 9 | carden 10051 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2710 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2730 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2811 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2732 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2758 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 7174 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3679 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 5288 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4539 elpr2 4541 elpr2g 4540 elprg 4537 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4531 elsn2 4555 elsn2g 4554 elsng 4530 velsn 4532 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 5325 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4526 sneqr 4726 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4535 dfsn2 4529 dfsn2ALT 4536 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 7485 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 5334 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 5322 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 5307 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 7487 unexg 7490 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4580 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4797 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3850 df-un 3848 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4814 uniprg 4813 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 5244 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4579 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 6241 elsucg 6239 sstr2 3884 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 4043 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 4091 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 4056 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 4110 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 4164 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 4165 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3862 dfss2 3863 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4490 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 4071 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3860 sseqin2 4106 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3899 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 4119 inss2 4120 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 3939 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4807 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 5308 sspwimp 42076 sspwimpALT 42083 sspwimpALT2 42086 sspwimpcf 42078 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 5315 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 5154 |
| [TakeutiZaring] p. 20 | Definition | df-rab 3062 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 5175 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3846 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 4214 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 4259 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 4235 n0f 4231 neq0 4234 neq0f 4230 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 9132 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 9247 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 9249 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3400 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 5183 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 4285 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 5189 ssexg 5191 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 5185 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 9139 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 9134 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 4252 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 4021 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 4181 undif3VD 42040 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 4022 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 4029 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 3058 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 3059 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 7494 xpexg 7491 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5532 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 6410 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6584 fun11 6413 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 6351 svrelfun 6411 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5730 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5732 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5537 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5538 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5534 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 6026 dfrel2 6021 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5541 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5655 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5662 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5675 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5854 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5831 opelresi 5833 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5847 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5850 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5855 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 6381 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 6077 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 6379 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6586 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2612 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 28337 df-fv 6347 fv3 6692 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7656 cnvexg 7655 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7642 dmexg 7634 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7643 rnexg 7635 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 41610 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7651 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6687 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 44199 tz6.12-1-afv2 44266 tz6.12-1 6696 tz6.12-afv 44198 tz6.12-afv2 44265 tz6.12 6697 tz6.12c-afv2 44267 tz6.12c 6699 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2-afv2 44262 tz6.12-2 6663 tz6.12i-afv2 44268 tz6.12i 6700 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 6342 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 6343 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 6345 wfo 6337 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 6344 wf1 6336 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 6346 wf1o 6338 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6809 eqfnfv2 6810 eqfnfv2f 6813 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6766 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 6990 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 6988 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 6426 funimaexg 6425 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 5031 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5443 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5489 dffr3 5936 eliniseg 5932 iniseg 5934 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5434 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5503 fr3nr 7513 frirr 5502 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5483 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 7515 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5492 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5512 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 6160 tz6.26i 6161 wefrc 5519 wereu2 5522 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 6162 wfii 6163 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 6348 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 7095 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 7096 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 7102 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 7103 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 7104 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 7108 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 7115 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 7117 |
| [TakeutiZaring] p. 35 | Notation | wtr 5136 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 41611 tz7.2 5509 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 5140 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 6185 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 6193 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 6194 ordelordALT 41695 ordelordALTVD 42025 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 6200 ordelssne 6199 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 6198 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 6202 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 7522 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 7523 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 6176 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 6204 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 41707 ordon 7517 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 7518 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7587 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 6219 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 5138 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 7531 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7565 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 6273 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 6272 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 7519 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4828 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 6178 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 6249 sucidg 6250 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7547 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 6263 ordnbtwn 6262 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7562 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 6177 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7613 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7618 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7575 ordelsuc 7554 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7556 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7585 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7601 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7620 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7621 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7622 |
| [TakeutiZaring] p. 43 | Remark | omon 7610 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 9171 omex 9179 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7608 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7627 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7623 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7624 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7604 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4850 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 5153 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4851 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 5205 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7534 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 6221 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4837 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 9196 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 7529 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 8041 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 8062 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 8063 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 8064 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 8071 tz7.44-2 8072 tz7.44-3 8073 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 8033 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 8028 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 8012 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 8110 tz7.49c 8111 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 8108 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 8107 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 8109 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2658 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 9511 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 9512 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 8188 oasuc 8180 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7594 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 8191 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 8172 oa0r 8194 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 8192 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 8205 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 8276 nnaordi 8275 oaord 8204 oaordi 8203 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4935 uniss2 4831 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 8207 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 8212 oawordex 8214 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 8268 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 8302 |
| [TakeutiZaring] p. 60 | Remark | oancom 9187 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 8217 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 8273 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 8209 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0x 8175 omlim 8189 omsuc 8182 |
| [TakeutiZaring] p. 62 | Definition 8.15(a) | om0 8173 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 8270 nnmcl 8269 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 8289 nnmordi 8288 omord 8225 omordi 8223 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 8226 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 8293 omwordri 8229 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 8195 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 8199 om1r 8200 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 8232 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 8234 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 8235 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 8236 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 8237 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 8265 oe0 8178 oelim 8190 oesuc 8183 onesuc 8186 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 8176 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 8243 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 8244 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 8177 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 8202 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 8245 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 8251 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 8249 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 8250 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 8254 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 8256 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 9243 tz9.1 9244 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 9266 r10 9270 r1lim 9274 r1limg 9273 r1suc 9272 r1sucg 9271 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 9282 r1ord2 9283 r1ordg 9280 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 9292 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 9317 tz9.13 9293 tz9.13g 9294 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 9267 rankval 9318 rankvalb 9299 rankvalg 9319 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 9341 rankelb 9326 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 9355 rankval3 9342 rankval3b 9328 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 9331 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 9297 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 9336 rankr1c 9323 rankr1g 9334 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 9337 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 9351 rankssb 9350 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 9344 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 9343 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 9975 dfac3 9621 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 9530 numth 9972 numth2 9971 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 10046 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 10047 cardid2 9455 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 9462 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 10051 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 9461 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 9446 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 9467 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 9459 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8740 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8618 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8745 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8668 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 9465 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 9598 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8750 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 8788 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 9599 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8755 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 9588 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 9566 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 9474 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9717 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 8866 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 8559 isfi 8579 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 8789 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 10034 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8661 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 10026 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | djuxpdom 9685 unxpdom 8804 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 9476 cardsdomelir 9475 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 8806 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 9514 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 8439 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 10062 infxpidm2 9517 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infdju 9708 infxp 9715 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8673 pw2f1o 8671 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8733 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 9987 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 9982 ac6s5 9991 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 10043 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 10044 uniimadomf 10045 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 9774 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 9769 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 9754 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 9751 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 9757 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 9764 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 9773 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 10082 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 9752 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 9776 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 9597 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 9596 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 9608 alephfp2 9609 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 10199 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 9612 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 10069 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 10083 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 10084 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 36520 |
| [Tarski] p. 67 | Scheme B5 | sp 2184 |
| [Tarski] p. 68 | Lemma 6 | avril1 28400 equid 2024 |
| [Tarski] p. 69 | Lemma 7 | equcomi 2029 |
| [Tarski] p. 70 | Lemma 14 | spim 2387 spime 2389 spimew 1979 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2179 ax-c15 36526 ax12i 1974 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2095 |
| [Tarski] p. 75 | Axiom B7 | ax6v 1976 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1917 ax5ALT 36544 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 2020 ax-8 2116 ax-9 2124 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 26410 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 26411 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 26413 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 26413 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 26414 |
| [Truss] p. 114 | Theorem 5.18 | ruc 15688 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 35439 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 35441 |
| [Weierstrass] p. 272 | Definition | df-mdet 21336 mdetuni 21373 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 903 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 867 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 868 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 919 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 967 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 192 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 137 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 90 wl-luk-pm2.04 35239 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 40954 imim2 58 wl-luk-imim2 35234 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | adh-minimp-imim1 44053 imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 896 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2665 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 902 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-luk-id 35237 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 894 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 144 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 897 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 132 notnotrALT2 42085 wl-luk-notnotr 35238 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 148 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 40984 axfrege28 40983 con3 156 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | ax-3 8 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18 128 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 866 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 924 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 123 wl-luk-pm2.21 35231 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 124 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 889 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 939 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-labels 28338 pm2.27 42 wl-luk-pm2.27 35229 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 922 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 923 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 969 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 970 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 968 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1089 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 906 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 907 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 942 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 881 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 882 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5 172 pm2.5g 171 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6 194 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 883 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 884 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 885 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 175 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 176 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 850 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 851 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 888 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 890 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 195 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 899 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 940 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 941 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 196 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 891 pm2.67 892 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 179 pm2.521g 177 pm2.521g2 178 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 898 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 972 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 900 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 206 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 973 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 974 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 933 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 931 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 971 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 975 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 932 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 109 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 991 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 473 pm3.2im 163 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 992 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 993 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 994 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 995 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 475 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 463 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 406 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 803 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 452 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 453 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 486 simplim 170 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 488 simprim 169 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 765 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 766 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 808 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 625 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 810 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 496 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 497 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 960 pm3.44 959 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 809 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 477 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 963 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34b 319 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 264 |
| [WhiteheadRussell] p. 117 | Theorem *4.11 | notbi 322 |
| [WhiteheadRussell] p. 117 | Theorem *4.12 | con2bi 357 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotb 318 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14 807 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 832 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 225 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 806 bitr 805 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 567 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 904 pm4.25 905 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 464 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 1007 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 869 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 472 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 921 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 635 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 917 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 638 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 976 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1090 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 1005 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1053 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 1022 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 996 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 998 pm4.45 997 pm4.45im 827 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 982 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 852 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 549 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 981 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 984 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 985 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 986 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 987 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 983 pm4.56 988 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 989 pm4.57 990 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 408 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 855 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 401 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 848 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 409 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 849 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67 402 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 561 pm4.71d 565 pm4.71i 563 pm4.71r 562 pm4.71rd 566 pm4.71ri 564 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 949 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 531 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 936 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 521 pm4.76 522 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 961 pm4.77 962 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 934 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 1003 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 396 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81 397 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 1023 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 1024 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 351 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 352 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 355 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 392 impexp 454 pm4.87 842 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 823 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 944 pm5.11g 943 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 945 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 947 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 946 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 1012 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 1013 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 1011 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbn 388 pm5.18 386 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 391 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 824 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 1014 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 1049 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 1050 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 901 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 576 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 393 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 365 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6 1001 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 953 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 830 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 577 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 835 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 825 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 833 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 394 pm5.41 395 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 547 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 546 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 1004 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 1017 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 948 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 1000 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 1018 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 1019 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 1027 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 370 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 273 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 1028 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 41514 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 41515 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1877 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 41516 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 41517 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 41518 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1900 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 41519 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 41520 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 41521 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 41522 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 41523 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 41525 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 41526 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 41527 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 41524 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2100 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 41530 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 41531 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2080 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2165 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1835 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1836 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 41532 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 41533 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 41534 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 41535 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 41537 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 41536 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1894 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 41539 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 41540 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 41538 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1834 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 41541 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 41542 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1852 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 41543 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2349 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 1867 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 41548 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 41544 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 41545 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 41546 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 41547 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 41552 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 41549 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 41550 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 41551 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 41553 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2570 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 41563 pm13.13b 41564 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 41565 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 3015 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 3016 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3564 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 41571 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 41572 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 41566 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 41710 pm13.193 41567 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 41568 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 41569 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 41570 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 41577 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 41576 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 41575 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3745 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 41578 pm14.122b 41579 pm14.122c 41580 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 41581 pm14.123b 41582 pm14.123c 41583 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 41585 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 41584 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 41586 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 6320 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 41587 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 6321 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 41588 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 41590 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2636 eupickbi 2639 sbaniota 41591 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 41589 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 2585 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 41593 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 28337 df-fv 6347 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 9503 pm54.43lem 9502 |
| [Young] p. 141 | Definition of operator ordering | leop2 30059 |
| [Young] p. 142 | Example 12.2(i) | 0leop 30065 idleop 30066 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 40222 |
| [vandenDries] p. 43 | Theorem 62 | pellex 40229 pellexlem1 40223 |