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 17293 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 17293 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 17706 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 17314 |
| [Adamek] p. 24 | Example 3.3(4.d) | df-prstc 46224 prsthinc 46215 |
| [Adamek] p. 24 | Example 3.3(4.e) | df-mndtc 46243 df-mndtc 46243 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 17337 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 17409 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 17397 invisoinvl 17418 |
| [Adamek] p. 28 | Example 3.13 | idinv 17417 idiso 17416 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 17402 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 17376 df-iso 17377 dfiso2 17400 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 17383 |
| [Adamek] p. 29 | Remark 3.16 | cicer 17434 |
| [Adamek] p. 29 | Definition 3.15 | cic 17427 df-cic 17424 |
| [Adamek] p. 29 | Definition 3.17 | df-func 17488 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 17398 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 17399 isoco 17405 |
| [Adamek] p. 30 | Remark 3.19 | df-func 17488 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 17511 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 17504 |
| [Adamek] p. 33 | Example 3.26(2) | df-thinc 46181 prsthinc 46215 thincciso 46210 |
| [Adamek] p. 33 | Example 3.26(3) | df-mndtc 46243 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 17518 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 17741 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 17799 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 17536 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 17535 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 17799 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 17560 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 17566 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 17565 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 17784 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 17784 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 17505 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 17729 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 17554 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 17553 |
| [Adamek] p. 40 | Remark 3.48 | catccat 17738 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 17729 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 17468 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 17469 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 17480 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 17440 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 17569 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 17574 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 17597 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 17601 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 17575 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 17603 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 17614 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 45507 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 17615 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 17642 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 17646 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 17616 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 45510 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 17649 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 17375 |
| [Adamek] p. 185 | Section 10.67 | updjud 9622 |
| [Adamek] p. 478 | Item Rng | df-ringc 45443 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 45774 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 45796 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 14201 df-pfx 14311 df-substr 14281 df-word 14145 lencl 14163 wrd0 14169 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 23777 df-nmoo 29007 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 30415 hmopidmchi 30413 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 30463 pjcmul2i 30464 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 30180 unoplin 30182 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 30181 unopadj2 30200 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 30275 lnopunii 30274 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 30348 |
| [Alling] p. 125 | Theorem 4.02(12) | cofcutrtime 34019 |
| [Alling] p. 184 | Axiom B | bdayfo 33806 |
| [Alling] p. 184 | Axiom O | sltso 33805 |
| [Alling] p. 184 | Axiom SD | nodense 33821 |
| [Alling] p. 185 | Lemma 0 | nocvxmin 33899 |
| [Alling] p. 185 | Theorem | conway 33919 |
| [Alling] p. 185 | Axiom FE | noeta 33872 |
| [Alling] p. 186 | Theorem 4 | slerec 33939 |
| [Apostol] p. 18 | Theorem I.1 | addcan 11088 addcan2d 11108 addcan2i 11098 addcand 11107 addcani 11097 |
| [Apostol] p. 18 | Theorem I.2 | negeu 11140 |
| [Apostol] p. 18 | Theorem I.3 | negsub 11198 negsubd 11267 negsubi 11228 |
| [Apostol] p. 18 | Theorem I.4 | negneg 11200 negnegd 11252 negnegi 11220 |
| [Apostol] p. 18 | Theorem I.5 | subdi 11337 subdid 11360 subdii 11353 subdir 11338 subdird 11361 subdiri 11354 |
| [Apostol] p. 18 | Theorem I.6 | mul01 11083 mul01d 11103 mul01i 11094 mul02 11082 mul02d 11102 mul02i 11093 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 11541 mulcan2d 11538 mulcand 11537 mulcani 11543 |
| [Apostol] p. 18 | Theorem I.8 | receu 11549 xreceu 31097 |
| [Apostol] p. 18 | Theorem I.9 | divrec 11578 divrecd 11683 divreci 11649 divreczi 11642 |
| [Apostol] p. 18 | Theorem I.10 | recrec 11601 recreci 11636 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 11544 mul0ord 11554 mul0ori 11552 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 11343 mul2negd 11359 mul2negi 11352 mulneg1 11340 mulneg1d 11357 mulneg1i 11350 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 11619 divadddivd 11724 divadddivi 11666 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 11604 divmuldivd 11721 divmuldivi 11664 rdivmuldivd 31389 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 11605 divdivdivd 11727 divdivdivi 11667 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 12680 rpaddcld 12715 rpmulcl 12681 rpmulcld 12716 |
| [Apostol] p. 20 | Axiom 8 | rpneg 12690 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 12693 |
| [Apostol] p. 20 | Theorem I.17 | lttri 11030 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 11497 ltadd1dd 11515 ltadd1i 11458 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 11754 ltmul1a 11753 ltmul1i 11822 ltmul1ii 11832 ltmul2 11755 ltmul2d 12742 ltmul2dd 12756 ltmul2i 11825 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 11424 msqgt0d 11471 msqgt0i 11441 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 11426 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 11410 lt0neg1d 11473 ltneg 11404 ltnegd 11482 ltnegi 11448 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 11389 lt2addd 11527 lt2addi 11466 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 12659 |
| [Apostol] p. 21 | Exercise 4 | recgt0 11750 recgt0d 11838 recgt0i 11809 recgt0ii 11810 |
| [Apostol] p. 22 | Definition of integers | df-z 12249 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11916 |
| [Apostol] p. 22 | Definition of rationals | df-q 12617 |
| [Apostol] p. 24 | Theorem I.26 | supeu 9142 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 12158 |
| [Apostol] p. 26 | Theorem I.29 | arch 12159 |
| [Apostol] p. 28 | Exercise 2 | btwnz 12351 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 12160 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 12615 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 12614 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12861 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 15975 zneo 12332 zneoALTV 45001 |
| [Apostol] p. 29 | Theorem I.35 | cxpsqrtth 25788 msqsqrtd 15079 resqrtth 14894 sqrtth 15003 sqrtthi 15009 sqsqrtd 15078 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11905 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 12581 |
| [Apostol] p. 361 | Remark | crreczi 13870 |
| [Apostol] p. 363 | Remark | absgt0i 15038 |
| [Apostol] p. 363 | Example | abssubd 15092 abssubi 15042 |
| [ApostolNT] p. 7 | Remark | fmtno0 44872 fmtno1 44873 fmtno2 44882 fmtno3 44883 fmtno4 44884 fmtno5fac 44914 fmtnofz04prm 44909 |
| [ApostolNT] p. 7 | Definition | df-fmtno 44860 |
| [ApostolNT] p. 8 | Definition | df-ppi 26153 |
| [ApostolNT] p. 14 | Definition | df-dvds 15891 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 15906 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 15930 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15925 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15919 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15921 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 15907 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 15908 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15913 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 15947 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 15949 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 15951 |
| [ApostolNT] p. 15 | Definition | df-gcd 16129 dfgcd2 16181 |
| [ApostolNT] p. 16 | Definition | isprm2 16314 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 16285 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 16543 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 16147 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 16182 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 16184 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 16162 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 16154 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 16343 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 16345 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 16556 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 16550 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 16039 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 16219 |
| [ApostolNT] p. 24 | Definition | df-mu 26154 |
| [ApostolNT] p. 25 | Definition | df-phi 16394 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 26244 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 16418 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 16404 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 16408 |
| [ApostolNT] p. 32 | Definition | df-vma 26151 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 26246 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 26268 |
| [ApostolNT] p. 38 | Remark | df-sgm 26155 |
| [ApostolNT] p. 38 | Definition | df-sgm 26155 |
| [ApostolNT] p. 75 | Definition | df-chp 26152 df-cht 26150 |
| [ApostolNT] p. 104 | Definition | congr 16296 |
| [ApostolNT] p. 106 | Remark | dvdsval3 15894 |
| [ApostolNT] p. 106 | Definition | moddvds 15901 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 15982 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 15983 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 13535 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 13572 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 13880 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15924 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 16299 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 16702 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 16301 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 16411 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 16429 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 16412 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 26125 |
| [ApostolNT] p. 179 | Definition | df-lgs 26347 lgsprme0 26391 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 26392 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 26368 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 26383 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 26440 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 26459 2lgsoddprm 26468 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 26426 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 26435 |
| [ApostolNT] p. 188 | Definition | df-lgs 26347 lgs1 26393 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 26384 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 26386 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 26394 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 26395 |
| [Baer] p. 40 | Property (b) | mapdord 39578 |
| [Baer] p. 40 | Property (c) | mapd11 39579 |
| [Baer] p. 40 | Property (e) | mapdin 39602 mapdlsm 39604 |
| [Baer] p. 40 | Property (f) | mapd0 39605 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 39565 mapd1o 39588 |
| [Baer] p. 41 | Property (g) | mapdat 39607 |
| [Baer] p. 44 | Part (1) | mapdpg 39646 |
| [Baer] p. 45 | Part (2) | hdmap1eq 39741 mapdheq 39668 mapdheq2 39669 mapdheq2biN 39670 |
| [Baer] p. 45 | Part (3) | baerlem3 39653 |
| [Baer] p. 46 | Part (4) | mapdheq4 39672 mapdheq4lem 39671 |
| [Baer] p. 46 | Part (5) | baerlem5a 39654 baerlem5abmN 39658 baerlem5amN 39656 baerlem5b 39655 baerlem5bmN 39657 |
| [Baer] p. 47 | Part (6) | hdmap1l6 39761 hdmap1l6a 39749 hdmap1l6e 39754 hdmap1l6f 39755 hdmap1l6g 39756 hdmap1l6lem1 39747 hdmap1l6lem2 39748 mapdh6N 39687 mapdh6aN 39675 mapdh6eN 39680 mapdh6fN 39681 mapdh6gN 39682 mapdh6lem1N 39673 mapdh6lem2N 39674 |
| [Baer] p. 48 | Part 9 | hdmapval 39768 |
| [Baer] p. 48 | Part 10 | hdmap10 39780 |
| [Baer] p. 48 | Part 11 | hdmapadd 39783 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 39757 mapdh6hN 39683 |
| [Baer] p. 48 | Part (7) | mapdh75cN 39693 mapdh75d 39694 mapdh75e 39692 mapdh75fN 39695 mapdh7cN 39689 mapdh7dN 39690 mapdh7eN 39688 mapdh7fN 39691 |
| [Baer] p. 48 | Part (8) | mapdh8 39728 mapdh8a 39715 mapdh8aa 39716 mapdh8ab 39717 mapdh8ac 39718 mapdh8ad 39719 mapdh8b 39720 mapdh8c 39721 mapdh8d 39723 mapdh8d0N 39722 mapdh8e 39724 mapdh8g 39725 mapdh8i 39726 mapdh8j 39727 |
| [Baer] p. 48 | Part (9) | mapdh9a 39729 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 39709 |
| [Baer] p. 49 | Part 12 | hdmap11 39788 hdmapeq0 39784 hdmapf1oN 39805 hdmapneg 39786 hdmaprnN 39804 hdmaprnlem1N 39789 hdmaprnlem3N 39790 hdmaprnlem3uN 39791 hdmaprnlem4N 39793 hdmaprnlem6N 39794 hdmaprnlem7N 39795 hdmaprnlem8N 39796 hdmaprnlem9N 39797 hdmapsub 39787 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 39808 hdmap14lem10 39817 hdmap14lem1a 39806 hdmap14lem2N 39809 hdmap14lem2a 39807 hdmap14lem3 39810 hdmap14lem8 39815 hdmap14lem9 39816 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 39818 hdmap14lem12 39819 hdmap14lem13 39820 hdmap14lem14 39821 hdmap14lem15 39822 hgmapval 39827 |
| [Baer] p. 50 | Part 15 | hgmapadd 39834 hgmapmul 39835 hgmaprnlem2N 39837 hgmapvs 39831 |
| [Baer] p. 50 | Part 16 | hgmaprnN 39841 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 39857 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 39858 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 39859 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 39860 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 39862 hgmapvv 39866 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 39861 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 39863 |
| [Baer] p. 111 | Line 15 | hdmapg 39870 hdmapglem7 39869 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 25789 2irrexpqALT 25854 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2570 |
| [BellMachover] p. 460 | Notation | df-mo 2541 |
| [BellMachover] p. 460 | Definition | mo3 2565 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2710 |
| [BellMachover] p. 462 | Theorem 1.1 | axextmo 2714 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 5210 |
| [BellMachover] p. 463 | Scheme Sep | ax-sep 5217 |
| [BellMachover] p. 463 | Theorem 1.3(ii) | bj-bm1.3ii 35161 bm1.3ii 5220 |
| [BellMachover] p. 466 | Problem | axpow2 5285 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 5286 |
| [BellMachover] p. 466 | Axiom Union | axun2 7568 |
| [BellMachover] p. 468 | Definition | df-ord 6254 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 6269 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 6276 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 6271 |
| [BellMachover] p. 471 | Definition of N | df-om 7688 |
| [BellMachover] p. 471 | Problem 2.5(ii) | uniordint 7628 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 6256 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 9329 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7703 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 9452 |
| [BellMachover] p. 478 | Definition | rankval2 9506 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 9470 r1ord3g 9467 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 9283 |
| [BellMachover] p. 488 | Axiom AC | ac5 10163 dfac4 9808 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 9796 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 37259 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 30615 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 30657 chirredi 30656 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 30645 |
| [Beran] p. 3 | Definition of join | sshjval3 29616 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 29878 cmcm2i 29855 cmcm2ii 29860 cmt2N 37190 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 29879 lecmi 29864 lecmii 29865 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 29853 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 29882 cm2ji 29887 cm2mi 29888 |
| [Beran] p. 95 | Definition | df-sh 29469 issh2 29471 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 29348 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 29361 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 29352 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 30090 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 30092 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 30091 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 30093 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 29344 his1i 29362 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 29345 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 29346 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 29347 |
| [Beran] p. 96 | Definition of norm | df-hnorm 29230 dfhnorm2 29384 normval 29386 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 29446 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 29235 |
| [Beran] p. 96 | Definition of complete subspace | isch3 29503 |
| [Beran] p. 96 | Definition of converge | df-hlim 29234 hlimi 29450 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 29395 norm-i 29391 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 29399 norm-ii 29400 normlem0 29371 normlem1 29372 normlem2 29373 normlem3 29374 normlem4 29375 normlem5 29376 normlem6 29377 normlem7 29378 normlem7tALT 29381 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 29401 norm-iii 29402 |
| [Beran] p. 98 | Remark 3.4 | bcs 29443 bcsiALT 29441 bcsiHIL 29442 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 29383 normpar 29417 normpari 29416 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 29408 normpyth 29407 normpythi 29404 |
| [Beran] p. 99 | Remark | lnfn0 30309 lnfn0i 30304 lnop0 30228 lnop0i 30232 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 30288 nmcfnex 30315 nmcfnexi 30313 nmcopex 30291 nmcopexi 30289 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 30316 nmcfnlbi 30314 nmcoplb 30292 nmcoplbi 30290 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 30318 lnfnconi 30317 lnopcon 30297 lnopconi 30296 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 29418 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 29415 norm3adifii 29410 norm3dif 29412 norm3difi 29409 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 29563 pjhth 29655 pjhtheu 29656 pjpjhth 29687 pjpjhthi 29688 pjth 24507 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 29668 ococi 29667 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 30323 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 30324 riesz4 30326 riesz4i 30325 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 30341 cnlnadjeu 30340 cnlnadjeui 30339 cnlnadji 30338 cnlnadjlem1 30329 nmopadjlei 30350 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 30353 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 30352 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 30354 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 30198 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 30364 nmopcoadji 30363 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 30355 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 30365 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 30362 pjadj2coi 30466 pjadjcoi 30423 |
| [Beran] p. 107 | Definition | df-ch 29483 isch2 29485 |
| [Beran] p. 107 | Remark 3.12 | choccl 29568 isch3 29503 occl 29566 ocsh 29545 shoccl 29567 shocsh 29546 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 29670 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 29594 |
| [Beran] p. 109 | Property (i) | pjadj2 30449 pjadj3 30450 pjadji 29947 pjadjii 29936 |
| [Beran] p. 109 | Property (ii) | pjidmco 30443 pjidmcoi 30439 pjidmi 29935 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 30435 |
| [Beran] p. 111 | Remark | ho0val 30012 pjch1 29932 |
| [Beran] p. 111 | Definition | df-hfmul 29996 df-hfsum 29995 df-hodif 29994 df-homul 29993 df-hosum 29992 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 29933 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 29956 pjchi 29694 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 29701 pjoc2i 29700 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 29942 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 30427 pjssmii 29943 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 30426 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 30425 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 30430 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 30428 pjssge0ii 29944 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 30429 pjdifnormii 29945 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1784 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1782 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1785 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1780 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 32158 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 32166 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 32164 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 32168 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 32188 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 32219 df-sitm 32197 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 32219 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 32196 |
| [Bollobas] p. 1 | Section I.1 | df-edg 27320 isuhgrop 27342 isusgrop 27434 isuspgrop 27433 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 27537 uhgrspan1 27572 uhgrspansubgr 27560 |
| [Bollobas] p. 3 | Definition | isomuspgr 45166 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 27723 df-cusgr 27681 df-nbgr 27602 fusgrmaxsize 27733 |
| [Bollobas] p. 4 | Definition | df-upwlks 45176 df-wlks 27868 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 27819 finsumvtxdgeven 27821 fusgr1th 27820 fusgrvtxdgonume 27823 vtxdgoddnumeven 27822 |
| [Bollobas] p. 5 | Notation | df-pths 27984 |
| [Bollobas] p. 5 | Definition | df-crcts 28054 df-cycls 28055 df-trls 27961 df-wlkson 27869 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 27331 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 45274 df-cllaw 45260 df-mgm 18240 df-mgm2 45293 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 45275 df-asslaw 45262 df-sgrp 18289 df-sgrp2 45295 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 45294 df-comlaw 45261 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 18300 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 19699 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 45313 |
| [BourbakiEns] p. | Proposition 8 | fcof1 7139 fcofo 7140 |
| [BourbakiTop1] p. | Remark | xnegmnf 12872 xnegpnf 12871 |
| [BourbakiTop1] p. | Remark | rexneg 12873 |
| [BourbakiTop1] p. | Remark 3 | ust0 23278 ustfilxp 23271 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 23148 |
| [BourbakiTop1] p. | Criterion | ishmeo 22817 |
| [BourbakiTop1] p. | Example 1 | cstucnd 23343 iducn 23342 snfil 22922 |
| [BourbakiTop1] p. | Example 2 | neifil 22938 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 23125 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 23363 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 31808 |
| [BourbakiTop1] p. | Paragraph 3 | infil 22921 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 23335 df-ust 23259 filintn0 22919 filn0 22920 istgp 23135 ucnprima 23341 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 23346 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 23357 df-usp 23316 df-utop 23290 trust 23288 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 31707 |
| [BourbakiTop1] p. | Property V_i | ssnei2 22174 |
| [BourbakiTop1] p. | Theorem 1(d) | iscncl 22327 |
| [BourbakiTop1] p. | Condition F_I | ustssel 23264 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 23267 |
| [BourbakiTop1] p. | Property V_ii | innei 22183 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 22191 neissex 22185 |
| [BourbakiTop1] p. | Proposition 1 | neips 22171 neiss 22167 ucncn 23344 ustund 23280 ustuqtop 23305 |
| [BourbakiTop1] p. | Proposition 2 | cnpco 22325 neiptopreu 22191 utop2nei 23309 utop3cls 23310 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 23351 uspreg 23333 utopreg 23311 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 22749 imasncls 22750 imasnopn 22748 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 23058 |
| [BourbakiTop1] p. | Condition F_II | ustincl 23266 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 23268 |
| [BourbakiTop1] p. | Property V_iii | elnei 22169 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 23362 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 23265 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 23269 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 22445 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 22904 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 21950 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 31704 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 43485 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 43487 stoweid 43486 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 43424 stoweidlem10 43433 stoweidlem14 43437 stoweidlem15 43438 stoweidlem35 43458 stoweidlem36 43459 stoweidlem37 43460 stoweidlem38 43461 stoweidlem40 43463 stoweidlem41 43464 stoweidlem43 43466 stoweidlem44 43467 stoweidlem46 43469 stoweidlem5 43428 stoweidlem50 43473 stoweidlem52 43475 stoweidlem53 43476 stoweidlem55 43478 stoweidlem56 43479 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 43446 stoweidlem24 43447 stoweidlem27 43450 stoweidlem28 43451 stoweidlem30 43453 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 43457 stoweidlem59 43482 stoweidlem60 43483 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 43468 stoweidlem49 43472 stoweidlem7 43430 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 43454 stoweidlem39 43462 stoweidlem42 43465 stoweidlem48 43471 stoweidlem51 43474 stoweidlem54 43477 stoweidlem57 43480 stoweidlem58 43481 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 43448 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 43440 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 43434 stoweidlem13 43436 stoweidlem26 43449 stoweidlem61 43484 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 43441 |
| [Bruck] p. 1 | Section I.1 | df-clintop 45274 df-mgm 18240 df-mgm2 45293 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 18289 df-sgrp2 45295 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 18588 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 5154 |
| [Church] p. 129 | Section II.24 | df-ifp 1064 dfifp2 1065 |
| [Clemente] p. 10 | Definition IT | natded 28667 |
| [Clemente] p. 10 | Definition I` `m,n | natded 28667 |
| [Clemente] p. 11 | Definition E=>m,n | natded 28667 |
| [Clemente] p. 11 | Definition I=>m,n | natded 28667 |
| [Clemente] p. 11 | Definition E` `(1) | natded 28667 |
| [Clemente] p. 11 | Definition E` `(2) | natded 28667 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 28667 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 28667 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 28667 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 28667 |
| [Clemente] p. 14 | Proof 5.11 | natded 28667 |
| [Clemente] p. 14 | Definition E` `n | natded 28667 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 28669 ex-natded5.2 28668 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 28672 ex-natded5.3 28671 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 28674 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 28676 ex-natded5.7 28675 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 28678 ex-natded5.8 28677 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 28680 ex-natded5.13 28679 |
| [Clemente] p. 32 | Definition I` `n | natded 28667 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 28667 |
| [Clemente] p. 32 | Definition E` `n,t | natded 28667 |
| [Clemente] p. 32 | Definition I` `n,t | natded 28667 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 28681 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 28682 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 28684 ex-natded9.26 28683 |
| [Cohen] p. 301 | Remark | relogoprlem 25650 |
| [Cohen] p. 301 | Property 2 | relogmul 25651 relogmuld 25684 |
| [Cohen] p. 301 | Property 3 | relogdiv 25652 relogdivd 25685 |
| [Cohen] p. 301 | Property 4 | relogexp 25655 |
| [Cohen] p. 301 | Property 1a | log1 25645 |
| [Cohen] p. 301 | Property 1b | loge 25646 |
| [Cohen4] p. 348 | Observation | relogbcxpb 25841 |
| [Cohen4] p. 349 | Property | relogbf 25845 |
| [Cohen4] p. 352 | Definition | elogb 25824 |
| [Cohen4] p. 361 | Property 2 | relogbmul 25831 |
| [Cohen4] p. 361 | Property 3 | logbrec 25836 relogbdiv 25833 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 25829 |
| [Cohen4] p. 361 | Property 6 | relogbexp 25834 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 25822 |
| [Cohen4] p. 361 | Property 1(b) | logb1 25823 |
| [Cohen4] p. 367 | Property | logbchbase 25825 |
| [Cohen4] p. 377 | Property 2 | logblt 25838 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 32151 sxbrsigalem4 32153 |
| [Cohn] p. 81 | Section II.5 | acsdomd 18189 acsinfd 18188 acsinfdimd 18190 acsmap2d 18187 acsmapd 18186 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 32156 |
| [Connell] p. 57 | Definition | df-scmat 21547 df-scmatalt 45620 |
| [Conway] p. 4 | Definition | slerec 33939 |
| [Conway] p. 5 | Definition | addsval 34052 df-adds 34045 df-negs 34046 |
| [Conway] p. 7 | Theorem | 0slt1s 33949 |
| [Conway] p. 16 | Theorem 0(i) | ssltright 33981 |
| [Conway] p. 16 | Theorem 0(ii) | ssltleft 33980 |
| [Conway] p. 16 | Theorem 0(iii) | slerflex 33892 |
| [Conway] p. 17 | Theorem 3 | addscom 34055 addscomd 34056 addsid1 34053 addsid1d 34054 |
| [Conway] p. 17 | Definition | df-0s 33944 |
| [Conway] p. 18 | Definition | df-1s 33945 |
| [Conway] p. 29 | Remark | madebday 34006 newbday 34008 oldbday 34007 |
| [Conway] p. 29 | Definition | df-made 33957 df-new 33959 df-old 33958 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 13508 |
| [Crawley] p. 1 | Definition of poset | df-poset 17945 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 37326 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 38130 dalaw 37826 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 39905 |
| [Crawley] p. 111 | Definition of set W | df-watsN 37930 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 38046 df-ldil 38044 isldil 38050 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 38045 df-trnN 38047 isltrn 38059 ltrnu 38061 |
| [Crawley] p. 112 | Lemma A | cdlema1N 37731 cdlema2N 37732 exatleN 37344 |
| [Crawley] p. 112 | Lemma B | 1cvrat 37416 cdlemb 37734 cdlemb2 37981 cdlemb3 38546 idltrn 38090 l1cvat 36995 lhpat 37983 lhpat2 37985 lshpat 36996 ltrnel 38079 ltrnmw 38091 |
| [Crawley] p. 112 | Lemma C | cdlemc1 38131 cdlemc2 38132 ltrnnidn 38114 trlat 38109 trljat1 38106 trljat2 38107 trljat3 38108 trlne 38125 trlnidat 38113 trlnle 38126 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 37931 |
| [Crawley] p. 113 | Lemma C | cdlemc 38137 cdlemc3 38133 cdlemc4 38134 |
| [Crawley] p. 113 | Lemma D | cdlemd 38147 cdlemd1 38138 cdlemd2 38139 cdlemd3 38140 cdlemd4 38141 cdlemd5 38142 cdlemd6 38143 cdlemd7 38144 cdlemd8 38145 cdlemd9 38146 cdleme31sde 38325 cdleme31se 38322 cdleme31se2 38323 cdleme31snd 38326 cdleme32a 38381 cdleme32b 38382 cdleme32c 38383 cdleme32d 38384 cdleme32e 38385 cdleme32f 38386 cdleme32fva 38377 cdleme32fva1 38378 cdleme32fvcl 38380 cdleme32le 38387 cdleme48fv 38439 cdleme4gfv 38447 cdleme50eq 38481 cdleme50f 38482 cdleme50f1 38483 cdleme50f1o 38486 cdleme50laut 38487 cdleme50ldil 38488 cdleme50lebi 38480 cdleme50rn 38485 cdleme50rnlem 38484 cdlemeg49le 38451 cdlemeg49lebilem 38479 |
| [Crawley] p. 113 | Lemma E | cdleme 38500 cdleme00a 38149 cdleme01N 38161 cdleme02N 38162 cdleme0a 38151 cdleme0aa 38150 cdleme0b 38152 cdleme0c 38153 cdleme0cp 38154 cdleme0cq 38155 cdleme0dN 38156 cdleme0e 38157 cdleme0ex1N 38163 cdleme0ex2N 38164 cdleme0fN 38158 cdleme0gN 38159 cdleme0moN 38165 cdleme1 38167 cdleme10 38194 cdleme10tN 38198 cdleme11 38210 cdleme11a 38200 cdleme11c 38201 cdleme11dN 38202 cdleme11e 38203 cdleme11fN 38204 cdleme11g 38205 cdleme11h 38206 cdleme11j 38207 cdleme11k 38208 cdleme11l 38209 cdleme12 38211 cdleme13 38212 cdleme14 38213 cdleme15 38218 cdleme15a 38214 cdleme15b 38215 cdleme15c 38216 cdleme15d 38217 cdleme16 38225 cdleme16aN 38199 cdleme16b 38219 cdleme16c 38220 cdleme16d 38221 cdleme16e 38222 cdleme16f 38223 cdleme16g 38224 cdleme19a 38243 cdleme19b 38244 cdleme19c 38245 cdleme19d 38246 cdleme19e 38247 cdleme19f 38248 cdleme1b 38166 cdleme2 38168 cdleme20aN 38249 cdleme20bN 38250 cdleme20c 38251 cdleme20d 38252 cdleme20e 38253 cdleme20f 38254 cdleme20g 38255 cdleme20h 38256 cdleme20i 38257 cdleme20j 38258 cdleme20k 38259 cdleme20l 38262 cdleme20l1 38260 cdleme20l2 38261 cdleme20m 38263 cdleme20y 38242 cdleme20zN 38241 cdleme21 38277 cdleme21d 38270 cdleme21e 38271 cdleme22a 38280 cdleme22aa 38279 cdleme22b 38281 cdleme22cN 38282 cdleme22d 38283 cdleme22e 38284 cdleme22eALTN 38285 cdleme22f 38286 cdleme22f2 38287 cdleme22g 38288 cdleme23a 38289 cdleme23b 38290 cdleme23c 38291 cdleme26e 38299 cdleme26eALTN 38301 cdleme26ee 38300 cdleme26f 38303 cdleme26f2 38305 cdleme26f2ALTN 38304 cdleme26fALTN 38302 cdleme27N 38309 cdleme27a 38307 cdleme27cl 38306 cdleme28c 38312 cdleme3 38177 cdleme30a 38318 cdleme31fv 38330 cdleme31fv1 38331 cdleme31fv1s 38332 cdleme31fv2 38333 cdleme31id 38334 cdleme31sc 38324 cdleme31sdnN 38327 cdleme31sn 38320 cdleme31sn1 38321 cdleme31sn1c 38328 cdleme31sn2 38329 cdleme31so 38319 cdleme35a 38388 cdleme35b 38390 cdleme35c 38391 cdleme35d 38392 cdleme35e 38393 cdleme35f 38394 cdleme35fnpq 38389 cdleme35g 38395 cdleme35h 38396 cdleme35h2 38397 cdleme35sn2aw 38398 cdleme35sn3a 38399 cdleme36a 38400 cdleme36m 38401 cdleme37m 38402 cdleme38m 38403 cdleme38n 38404 cdleme39a 38405 cdleme39n 38406 cdleme3b 38169 cdleme3c 38170 cdleme3d 38171 cdleme3e 38172 cdleme3fN 38173 cdleme3fa 38176 cdleme3g 38174 cdleme3h 38175 cdleme4 38178 cdleme40m 38407 cdleme40n 38408 cdleme40v 38409 cdleme40w 38410 cdleme41fva11 38417 cdleme41sn3aw 38414 cdleme41sn4aw 38415 cdleme41snaw 38416 cdleme42a 38411 cdleme42b 38418 cdleme42c 38412 cdleme42d 38413 cdleme42e 38419 cdleme42f 38420 cdleme42g 38421 cdleme42h 38422 cdleme42i 38423 cdleme42k 38424 cdleme42ke 38425 cdleme42keg 38426 cdleme42mN 38427 cdleme42mgN 38428 cdleme43aN 38429 cdleme43bN 38430 cdleme43cN 38431 cdleme43dN 38432 cdleme5 38180 cdleme50ex 38499 cdleme50ltrn 38497 cdleme51finvN 38496 cdleme51finvfvN 38495 cdleme51finvtrN 38498 cdleme6 38181 cdleme7 38189 cdleme7a 38183 cdleme7aa 38182 cdleme7b 38184 cdleme7c 38185 cdleme7d 38186 cdleme7e 38187 cdleme7ga 38188 cdleme8 38190 cdleme8tN 38195 cdleme9 38193 cdleme9a 38191 cdleme9b 38192 cdleme9tN 38197 cdleme9taN 38196 cdlemeda 38238 cdlemedb 38237 cdlemednpq 38239 cdlemednuN 38240 cdlemefr27cl 38343 cdlemefr32fva1 38350 cdlemefr32fvaN 38349 cdlemefrs32fva 38340 cdlemefrs32fva1 38341 cdlemefs27cl 38353 cdlemefs32fva1 38363 cdlemefs32fvaN 38362 cdlemesner 38236 cdlemeulpq 38160 |
| [Crawley] p. 114 | Lemma E | 4atex 38016 4atexlem7 38015 cdleme0nex 38230 cdleme17a 38226 cdleme17c 38228 cdleme17d 38438 cdleme17d1 38229 cdleme17d2 38435 cdleme18a 38231 cdleme18b 38232 cdleme18c 38233 cdleme18d 38235 cdleme4a 38179 |
| [Crawley] p. 115 | Lemma E | cdleme21a 38265 cdleme21at 38268 cdleme21b 38266 cdleme21c 38267 cdleme21ct 38269 cdleme21f 38272 cdleme21g 38273 cdleme21h 38274 cdleme21i 38275 cdleme22gb 38234 |
| [Crawley] p. 116 | Lemma F | cdlemf 38503 cdlemf1 38501 cdlemf2 38502 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 38507 cdlemg16 38597 cdlemg28 38644 cdlemg28a 38633 cdlemg28b 38643 cdlemg3a 38537 cdlemg42 38669 cdlemg43 38670 cdlemg44 38673 cdlemg44a 38671 cdlemg46 38675 cdlemg47 38676 cdlemg9 38574 ltrnco 38659 ltrncom 38678 tgrpabl 38691 trlco 38667 |
| [Crawley] p. 116 | Definition of G | df-tgrp 38683 |
| [Crawley] p. 117 | Lemma G | cdlemg17 38617 cdlemg17b 38602 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 38696 df-edring 38697 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 38700 |
| [Crawley] p. 118 | Remark | tendopltp 38720 |
| [Crawley] p. 118 | Lemma H | cdlemh 38757 cdlemh1 38755 cdlemh2 38756 |
| [Crawley] p. 118 | Lemma I | cdlemi 38760 cdlemi1 38758 cdlemi2 38759 |
| [Crawley] p. 118 | Lemma J | cdlemj1 38761 cdlemj2 38762 cdlemj3 38763 tendocan 38764 |
| [Crawley] p. 118 | Lemma K | cdlemk 38914 cdlemk1 38771 cdlemk10 38783 cdlemk11 38789 cdlemk11t 38886 cdlemk11ta 38869 cdlemk11tb 38871 cdlemk11tc 38885 cdlemk11u-2N 38829 cdlemk11u 38811 cdlemk12 38790 cdlemk12u-2N 38830 cdlemk12u 38812 cdlemk13-2N 38816 cdlemk13 38792 cdlemk14-2N 38818 cdlemk14 38794 cdlemk15-2N 38819 cdlemk15 38795 cdlemk16-2N 38820 cdlemk16 38797 cdlemk16a 38796 cdlemk17-2N 38821 cdlemk17 38798 cdlemk18-2N 38826 cdlemk18-3N 38840 cdlemk18 38808 cdlemk19-2N 38827 cdlemk19 38809 cdlemk19u 38910 cdlemk1u 38799 cdlemk2 38772 cdlemk20-2N 38832 cdlemk20 38814 cdlemk21-2N 38831 cdlemk21N 38813 cdlemk22-3 38841 cdlemk22 38833 cdlemk23-3 38842 cdlemk24-3 38843 cdlemk25-3 38844 cdlemk26-3 38846 cdlemk26b-3 38845 cdlemk27-3 38847 cdlemk28-3 38848 cdlemk29-3 38851 cdlemk3 38773 cdlemk30 38834 cdlemk31 38836 cdlemk32 38837 cdlemk33N 38849 cdlemk34 38850 cdlemk35 38852 cdlemk36 38853 cdlemk37 38854 cdlemk38 38855 cdlemk39 38856 cdlemk39u 38908 cdlemk4 38774 cdlemk41 38860 cdlemk42 38881 cdlemk42yN 38884 cdlemk43N 38903 cdlemk45 38887 cdlemk46 38888 cdlemk47 38889 cdlemk48 38890 cdlemk49 38891 cdlemk5 38776 cdlemk50 38892 cdlemk51 38893 cdlemk52 38894 cdlemk53 38897 cdlemk54 38898 cdlemk55 38901 cdlemk55u 38906 cdlemk56 38911 cdlemk5a 38775 cdlemk5auN 38800 cdlemk5u 38801 cdlemk6 38777 cdlemk6u 38802 cdlemk7 38788 cdlemk7u-2N 38828 cdlemk7u 38810 cdlemk8 38778 cdlemk9 38779 cdlemk9bN 38780 cdlemki 38781 cdlemkid 38876 cdlemkj-2N 38822 cdlemkj 38803 cdlemksat 38786 cdlemksel 38785 cdlemksv 38784 cdlemksv2 38787 cdlemkuat 38806 cdlemkuel-2N 38824 cdlemkuel-3 38838 cdlemkuel 38805 cdlemkuv-2N 38823 cdlemkuv2-2 38825 cdlemkuv2-3N 38839 cdlemkuv2 38807 cdlemkuvN 38804 cdlemkvcl 38782 cdlemky 38866 cdlemkyyN 38902 tendoex 38915 |
| [Crawley] p. 120 | Remark | dva1dim 38925 |
| [Crawley] p. 120 | Lemma L | cdleml1N 38916 cdleml2N 38917 cdleml3N 38918 cdleml4N 38919 cdleml5N 38920 cdleml6 38921 cdleml7 38922 cdleml8 38923 cdleml9 38924 dia1dim 39001 |
| [Crawley] p. 120 | Lemma M | dia11N 38988 diaf11N 38989 dialss 38986 diaord 38987 dibf11N 39101 djajN 39077 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 38972 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 39058 dia2dimlem1 39004 dia2dimlem2 39005 dia2dimlem3 39006 dia2dimlem4 39007 dia2dimlem5 39008 diaf1oN 39070 diarnN 39069 dvheveccl 39052 dvhopN 39056 |
| [Crawley] p. 121 | Lemma N | cdlemn 39152 cdlemn10 39146 cdlemn11 39151 cdlemn11a 39147 cdlemn11b 39148 cdlemn11c 39149 cdlemn11pre 39150 cdlemn2 39135 cdlemn2a 39136 cdlemn3 39137 cdlemn4 39138 cdlemn4a 39139 cdlemn5 39141 cdlemn5pre 39140 cdlemn6 39142 cdlemn7 39143 cdlemn8 39144 cdlemn9 39145 diclspsn 39134 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 39113 |
| [Crawley] p. 122 | Lemma N | dih11 39205 dihf11 39207 dihjust 39157 dihjustlem 39156 dihord 39204 dihord1 39158 dihord10 39163 dihord11b 39162 dihord11c 39164 dihord2 39167 dihord2a 39159 dihord2b 39160 dihord2cN 39161 dihord2pre 39165 dihord2pre2 39166 dihordlem6 39153 dihordlem7 39154 dihordlem7b 39155 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 39170 dihfval 39171 dihval 39172 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 27681 df-nbgr 27602 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 27537 uhgrspan1 27572 uhgrspansubgr 27560 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 27823 vtxdgoddnumeven 27822 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 27331 |
| [EGA] p. 80 | Notation 1.1.1 | rspecval 31715 |
| [EGA] p. 80 | Proposition 1.1.2 | zartop 31727 |
| [EGA] p. 80 | Proposition 1.1.2(i) | zarcls0 31719 zarcls1 31720 |
| [EGA] p. 81 | Corollary 1.1.8 | zart0 31730 |
| [EGA], p. 82 | Proposition 1.1.10(ii) | zarcmp 31733 |
| [EGA], p. 83 | Corollary 1.2.3 | rhmpreimacn 31736 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3887 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 9334 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 8576 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 9342 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 9668 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 10241 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 5223 |
| [Enderton] p. 19 | Definition | df-tp 4564 |
| [Enderton] p. 26 | Exercise 5 | unissb 4871 |
| [Enderton] p. 26 | Exercise 10 | pwel 5299 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5478 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 5005 iinin2 5004 iinun2 4999 iunin1 4998 iunin1f 30797 iunin2 4997 uniin1 30791 uniin2 30792 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 5003 iundif2 5000 |
| [Enderton] p. 32 | Exercise 20 | unineq 4209 |
| [Enderton] p. 33 | Exercise 23 | iinuni 5024 |
| [Enderton] p. 33 | Exercise 25 | iununi 5025 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 5032 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 7599 iunpwss 5033 |
| [Enderton] p. 36 | Definition | opthwiener 5422 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 5360 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4876 |
| [Enderton] p. 41 | Lemma 3D | opeluu 5379 rnex 7733 rnexg 7725 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5812 rnuni 6041 |
| [Enderton] p. 42 | Definition of a function | dffun7 6445 dffun8 6446 |
| [Enderton] p. 43 | Definition of function value | funfv2 6838 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 6487 |
| [Enderton] p. 44 | Definition (d) | dfima2 5960 dfima3 5961 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6847 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 10159 ac7g 10160 df-ac 9802 dfac2 9817 dfac2a 9815 dfac2b 9816 dfac3 9807 dfac7 9818 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 7101 |
| [Enderton] p. 52 | Definition | df-map 8576 |
| [Enderton] p. 53 | Exercise 21 | coass 6158 |
| [Enderton] p. 53 | Exercise 27 | dmco 6147 |
| [Enderton] p. 53 | Exercise 14(a) | funin 6494 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5999 |
| [Enderton] p. 54 | Remark | ixpf 8667 ixpssmap 8679 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 8645 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 10169 ac9s 10179 |
| [Enderton] p. 56 | Theorem 3M | eqvrelref 36649 erref 8477 |
| [Enderton] p. 57 | Lemma 3N | eqvrelthi 36652 erthi 8508 |
| [Enderton] p. 57 | Definition | df-ec 8459 |
| [Enderton] p. 58 | Definition | df-qs 8463 |
| [Enderton] p. 61 | Exercise 35 | df-ec 8459 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5808 |
| [Enderton] p. 68 | Definition of successor | df-suc 6257 |
| [Enderton] p. 71 | Definition | df-tr 5187 dftr4 5191 |
| [Enderton] p. 72 | Theorem 4E | unisuc 6327 |
| [Enderton] p. 73 | Exercise 6 | unisuc 6327 |
| [Enderton] p. 73 | Exercise 5(a) | truni 5200 |
| [Enderton] p. 73 | Exercise 5(b) | trint 5202 trintALT 42382 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 8398 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 8400 onasuc 8321 |
| [Enderton] p. 79 | Definition of operation value | df-ov 7258 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 8399 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 8401 onmsuc 8322 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 8416 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 8403 nnacom 8411 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 8417 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 8418 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 8420 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 8404 nnmsucr 8419 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 8432 |
| [Enderton] p. 129 | Definition | df-en 8693 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 7209 |
| [Enderton] p. 133 | Exercise 1 | xpomen 9701 |
| [Enderton] p. 133 | Exercise 2 | qnnen 15849 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8898 |
| [Enderton] p. 135 | Corollary 6C | php3 8900 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8897 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 8960 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 8962 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8914 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8919 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8878 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 9865 |
| [Enderton] p. 142 | Theorem 6I(4) | mapdjuen 9866 |
| [Enderton] p. 143 | Theorem 6J | dju0en 9861 dju1en 9857 |
| [Enderton] p. 144 | Exercise 13 | iunfi 9036 unifi 9037 unifi2 9038 |
| [Enderton] p. 144 | Corollary 6K | undif2 4408 unfi 8918 unfi2 9012 |
| [Enderton] p. 145 | Figure 38 | ffoss 7762 |
| [Enderton] p. 145 | Definition | df-dom 8694 |
| [Enderton] p. 146 | Example 1 | domen 8707 domeng 8708 |
| [Enderton] p. 146 | Example 3 | nndomo 8945 nnsdom 9341 nnsdomg 9002 |
| [Enderton] p. 149 | Theorem 6L(a) | djudom2 9869 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8879 xpdom1 8812 xpdom1g 8810 xpdom2g 8809 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8885 |
| [Enderton] p. 151 | Theorem 6M | zorn 10193 zorng 10190 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 10178 dfac5 9814 |
| [Enderton] p. 159 | Theorem 6Q | unictb 10261 |
| [Enderton] p. 164 | Example | infdif 9895 |
| [Enderton] p. 168 | Definition | df-po 5494 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 6359 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 6297 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 6358 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 6304 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7660 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 7608 |
| [Enderton] p. 194 | Remark | onprc 7605 |
| [Enderton] p. 194 | Exercise 16 | suc11 6354 |
| [Enderton] p. 197 | Definition | df-card 9627 |
| [Enderton] p. 197 | Theorem 7P | carden 10237 |
| [Enderton] p. 200 | Exercise 25 | tfis 7676 |
| [Enderton] p. 202 | Lemma 7T | r1tr 9464 |
| [Enderton] p. 202 | Definition | df-r1 9452 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 9474 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 9555 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 9293 |
| [Enderton] p. 207 | Exercise 30 | rankpr 9545 rankprb 9539 rankpw 9531 rankpwi 9511 rankuniss 9554 |
| [Enderton] p. 207 | Exercise 34 | opthreg 9305 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 9306 |
| [Enderton] p. 212 | Definition of aleph | alephval3 9796 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 9762 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 9776 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 8143 |
| [Enderton] p. 222 | Definition of kard | karden 9583 kardex 9582 |
| [Enderton] p. 238 | Theorem 8R | oeoa 8391 |
| [Enderton] p. 238 | Theorem 8S | oeoe 8393 |
| [Enderton] p. 240 | Exercise 25 | oarec 8356 |
| [Enderton] p. 257 | Definition of cofinality | cflm 9936 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 17267 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 17213 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 18185 mrieqv2d 17264 mrieqvd 17263 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 17268 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 17273 mreexexlem2d 17270 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 18191 mreexfidimd 17275 |
| [Frege1879] p. 11 | Statement | df3or2 41257 |
| [Frege1879] p. 12 | Statement | df3an2 41258 dfxor4 41255 dfxor5 41256 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 41279 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 41280 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 41284 |
| [Frege1879] p. 31 | Proposition 4 | frege4 41288 |
| [Frege1879] p. 32 | Proposition 5 | frege5 41289 |
| [Frege1879] p. 33 | Proposition 6 | frege6 41295 |
| [Frege1879] p. 34 | Proposition 7 | frege7 41297 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 41298 axfrege8 41296 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-luk-pm2.04 35542 |
| [Frege1879] p. 35 | Proposition 9 | frege9 41301 |
| [Frege1879] p. 36 | Proposition 10 | frege10 41309 |
| [Frege1879] p. 36 | Proposition 11 | frege11 41303 |
| [Frege1879] p. 37 | Proposition 12 | frege12 41302 |
| [Frege1879] p. 37 | Proposition 13 | frege13 41311 |
| [Frege1879] p. 37 | Proposition 14 | frege14 41312 |
| [Frege1879] p. 38 | Proposition 15 | frege15 41315 |
| [Frege1879] p. 38 | Proposition 16 | frege16 41305 |
| [Frege1879] p. 39 | Proposition 17 | frege17 41310 |
| [Frege1879] p. 39 | Proposition 18 | frege18 41307 |
| [Frege1879] p. 39 | Proposition 19 | frege19 41313 |
| [Frege1879] p. 40 | Proposition 20 | frege20 41317 |
| [Frege1879] p. 40 | Proposition 21 | frege21 41316 |
| [Frege1879] p. 41 | Proposition 22 | frege22 41308 |
| [Frege1879] p. 42 | Proposition 23 | frege23 41314 |
| [Frege1879] p. 42 | Proposition 24 | frege24 41304 |
| [Frege1879] p. 42 | Proposition 25 | frege25 41306 rp-frege25 41294 |
| [Frege1879] p. 42 | Proposition 26 | frege26 41299 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 41319 |
| [Frege1879] p. 43 | Proposition 27 | frege27 41300 |
| [Frege1879] p. 43 | Proposition 28 | con3 156 |
| [Frege1879] p. 43 | Proposition 29 | frege29 41320 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 41323 axfrege31 41322 |
| [Frege1879] p. 44 | Proposition 30 | frege30 41321 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 132 |
| [Frege1879] p. 44 | Proposition 32 | frege32 41324 |
| [Frege1879] p. 44 | Proposition 33 | frege33 41325 |
| [Frege1879] p. 45 | Proposition 34 | frege34 41326 |
| [Frege1879] p. 45 | Proposition 35 | frege35 41327 |
| [Frege1879] p. 45 | Proposition 36 | frege36 41328 |
| [Frege1879] p. 46 | Proposition 37 | frege37 41329 |
| [Frege1879] p. 46 | Proposition 38 | frege38 41330 |
| [Frege1879] p. 46 | Proposition 39 | frege39 41331 |
| [Frege1879] p. 46 | Proposition 40 | frege40 41332 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 41334 axfrege41 41333 |
| [Frege1879] p. 47 | Proposition 41 | notnot 144 |
| [Frege1879] p. 47 | Proposition 42 | frege42 41335 |
| [Frege1879] p. 47 | Proposition 43 | frege43 41336 |
| [Frege1879] p. 47 | Proposition 44 | frege44 41337 |
| [Frege1879] p. 47 | Proposition 45 | frege45 41338 |
| [Frege1879] p. 48 | Proposition 46 | frege46 41339 |
| [Frege1879] p. 48 | Proposition 47 | frege47 41340 |
| [Frege1879] p. 49 | Proposition 48 | frege48 41341 |
| [Frege1879] p. 49 | Proposition 49 | frege49 41342 |
| [Frege1879] p. 49 | Proposition 50 | frege50 41343 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 41346 ax-frege52c 41377 frege52aid 41347 frege52b 41378 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 41351 ax-frege54c 41381 frege54b 41382 |
| [Frege1879] p. 50 | Proposition 51 | frege51 41344 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3714 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 41349 frege53aid 41348 frege53b 41379 frege53c 41403 |
| [Frege1879] p. 50 | Proposition 54 | biid 264 eqid 2739 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 41357 frege55aid 41354 frege55b 41386 frege55c 41407 frege55cor1a 41358 frege55lem2a 41356 frege55lem2b 41385 frege55lem2c 41406 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 41360 frege56aid 41359 frege56b 41387 frege56c 41408 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 41364 ax-frege58b 41390 frege58bid 41391 frege58c 41410 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 41362 frege57aid 41361 frege57b 41388 frege57c 41409 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3725 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 41366 frege59b 41393 frege59c 41411 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 41367 frege60b 41394 frege60c 41412 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 41368 frege61b 41395 frege61c 41413 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 41369 frege62b 41396 frege62c 41414 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 41370 frege63b 41397 frege63c 41415 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 41371 frege64b 41398 frege64c 41416 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 41372 frege65b 41399 frege65c 41417 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 41373 frege66b 41400 frege66c 41418 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 41374 frege67b 41401 frege67c 41419 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 41375 frege68b 41402 frege68c 41420 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 41421 |
| [Frege1879] p. 58 | Proposition 70 | frege70 41422 |
| [Frege1879] p. 59 | Proposition 71 | frege71 41423 |
| [Frege1879] p. 59 | Proposition 72 | frege72 41424 |
| [Frege1879] p. 59 | Proposition 73 | frege73 41425 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 41428 |
| [Frege1879] p. 60 | Proposition 74 | frege74 41426 |
| [Frege1879] p. 60 | Proposition 75 | frege75 41427 |
| [Frege1879] p. 62 | Proposition 77 | frege77 41429 frege77d 41235 |
| [Frege1879] p. 63 | Proposition 78 | frege78 41430 |
| [Frege1879] p. 63 | Proposition 79 | frege79 41431 |
| [Frege1879] p. 63 | Proposition 80 | frege80 41432 |
| [Frege1879] p. 63 | Proposition 81 | frege81 41433 frege81d 41236 |
| [Frege1879] p. 64 | Proposition 82 | frege82 41434 |
| [Frege1879] p. 65 | Proposition 83 | frege83 41435 frege83d 41237 |
| [Frege1879] p. 65 | Proposition 84 | frege84 41436 |
| [Frege1879] p. 66 | Proposition 85 | frege85 41437 |
| [Frege1879] p. 66 | Proposition 86 | frege86 41438 |
| [Frege1879] p. 66 | Proposition 87 | frege87 41439 frege87d 41239 |
| [Frege1879] p. 67 | Proposition 88 | frege88 41440 |
| [Frege1879] p. 68 | Proposition 89 | frege89 41441 |
| [Frege1879] p. 68 | Proposition 90 | frege90 41442 |
| [Frege1879] p. 68 | Proposition 91 | frege91 41443 frege91d 41240 |
| [Frege1879] p. 69 | Proposition 92 | frege92 41444 |
| [Frege1879] p. 70 | Proposition 93 | frege93 41445 |
| [Frege1879] p. 70 | Proposition 94 | frege94 41446 |
| [Frege1879] p. 70 | Proposition 95 | frege95 41447 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 41451 |
| [Frege1879] p. 71 | Proposition 96 | frege96 41448 frege96d 41238 |
| [Frege1879] p. 71 | Proposition 97 | frege97 41449 frege97d 41241 |
| [Frege1879] p. 71 | Proposition 98 | frege98 41450 frege98d 41242 |
| [Frege1879] p. 72 | Proposition 100 | frege100 41452 |
| [Frege1879] p. 72 | Proposition 101 | frege101 41453 |
| [Frege1879] p. 72 | Proposition 102 | frege102 41454 frege102d 41243 |
| [Frege1879] p. 73 | Proposition 103 | frege103 41455 |
| [Frege1879] p. 73 | Proposition 104 | frege104 41456 |
| [Frege1879] p. 73 | Proposition 105 | frege105 41457 |
| [Frege1879] p. 73 | Proposition 106 | frege106 41458 frege106d 41244 |
| [Frege1879] p. 74 | Proposition 107 | frege107 41459 |
| [Frege1879] p. 74 | Proposition 108 | frege108 41460 frege108d 41245 |
| [Frege1879] p. 74 | Proposition 109 | frege109 41461 frege109d 41246 |
| [Frege1879] p. 75 | Proposition 110 | frege110 41462 |
| [Frege1879] p. 75 | Proposition 111 | frege111 41463 frege111d 41248 |
| [Frege1879] p. 76 | Proposition 112 | frege112 41464 |
| [Frege1879] p. 76 | Proposition 113 | frege113 41465 |
| [Frege1879] p. 76 | Proposition 114 | frege114 41466 frege114d 41247 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 41467 |
| [Frege1879] p. 77 | Proposition 116 | frege116 41468 |
| [Frege1879] p. 78 | Proposition 117 | frege117 41469 |
| [Frege1879] p. 78 | Proposition 118 | frege118 41470 |
| [Frege1879] p. 78 | Proposition 119 | frege119 41471 |
| [Frege1879] p. 78 | Proposition 120 | frege120 41472 |
| [Frege1879] p. 79 | Proposition 121 | frege121 41473 |
| [Frege1879] p. 79 | Proposition 122 | frege122 41474 frege122d 41249 |
| [Frege1879] p. 79 | Proposition 123 | frege123 41475 |
| [Frege1879] p. 80 | Proposition 124 | frege124 41476 frege124d 41250 |
| [Frege1879] p. 81 | Proposition 125 | frege125 41477 |
| [Frege1879] p. 81 | Proposition 126 | frege126 41478 frege126d 41251 |
| [Frege1879] p. 82 | Proposition 127 | frege127 41479 |
| [Frege1879] p. 83 | Proposition 128 | frege128 41480 |
| [Frege1879] p. 83 | Proposition 129 | frege129 41481 frege129d 41252 |
| [Frege1879] p. 84 | Proposition 130 | frege130 41482 |
| [Frege1879] p. 85 | Proposition 131 | frege131 41483 frege131d 41253 |
| [Frege1879] p. 86 | Proposition 132 | frege132 41484 |
| [Frege1879] p. 86 | Proposition 133 | frege133 41485 frege133d 41254 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 43736 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 44056 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 43757 |
| [Fremlin1] p. 14 | Definition 112A | ismea 43871 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 43891 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 43882 meadjunre 43896 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 43883 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 43884 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 43880 meaiunle 43889 meaiunlelem 43888 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 43901 meaiuninc2 43902 meaiuninc3 43905 meaiuninc3v 43904 meaiunincf 43903 meaiuninclem 43900 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 43907 meaiininc2 43908 meaiininclem 43906 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 43926 caragendifcl 43934 caratheodory 43948 omelesplit 43938 |
| [Fremlin1] p. 19 | Definition 113A | isome 43914 isomennd 43951 isomenndlem 43950 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 43936 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 43955 voncmpl 44041 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 43918 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 43943 carageniuncllem1 43941 carageniuncllem2 43942 caragenuncl 43933 caragenuncllem 43932 caragenunicl 43944 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 43952 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 43946 caratheodorylem2 43947 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 43955 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 44014 hoidmv1lelem1 44011 hoidmv1lelem2 44012 hoidmv1lelem3 44013 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 44058 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 44014 hoidmvle 44020 hoidmvlelem1 44015 hoidmvlelem2 44016 hoidmvlelem3 44017 hoidmvlelem4 44018 hoidmvlelem5 44019 hsphoidmvle2 44005 hsphoif 43996 hsphoival 43999 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 43968 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 43976 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 44003 hoidmvn0val 44004 hoidmvval 43997 hoidmvval0 44007 hoidmvval0b 44010 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 44008 hsphoidmvle 44006 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 43957 df-voln 43959 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 44024 ovn0 43986 ovn0lem 43985 ovnf 43983 ovnome 43993 ovnssle 43981 ovnsslelem 43980 ovnsupge0 43977 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 44023 ovnhoilem1 44021 ovnhoilem2 44022 vonhoi 44087 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 44040 hoidifhspf 44038 hoidifhspval 44028 hoidifhspval2 44035 hoidifhspval3 44039 hspmbl 44049 hspmbllem1 44046 hspmbllem2 44047 hspmbllem3 44048 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 44041 vonmea 43994 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 43992 ovnsubadd2 44066 ovnsubadd2lem 44065 ovnsubaddlem1 43990 ovnsubaddlem2 43991 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 44051 hoimbl2 44085 hoimbllem 44050 hspdifhsp 44036 opnvonmbl 44054 opnvonmbllem2 44053 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 44056 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 44099 iccvonmbllem 44098 ioovonmbl 44097 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 44105 vonicclem2 44104 vonioo 44102 vonioolem2 44101 vonn0icc 44108 vonn0icc2 44112 vonn0ioo 44107 vonn0ioo2 44110 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 44109 snvonmbl 44106 vonct 44113 vonsn 44111 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 43780 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 43779 subsaliuncllem 43778 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 44140 salpreimalegt 44126 salpreimaltle 44141 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 44143 issmff 44149 issmflem 44142 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 44160 issmflelem 44159 smfpreimale 44169 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 44171 issmfgtlem 44170 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 44116 issmf 44143 issmff 44149 issmfge 44184 issmfgelem 44183 issmfgt 44171 issmfgtlem 44170 issmfle 44160 issmflelem 44159 issmflem 44142 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 44124 salpreimagtlt 44145 salpreimalelt 44144 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 44184 issmfgelem 44183 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 44168 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 44166 cnfsmf 44155 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 44181 decsmflem 44180 incsmf 44157 incsmflem 44156 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 44120 pimconstlt1 44121 smfconst 44164 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 44179 smfaddlem1 44177 smfaddlem2 44178 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 44209 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 44208 smfmullem1 44204 smfmullem2 44205 smfmullem3 44206 smfmullem4 44207 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 44210 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 44213 smfpimbor1lem2 44212 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 44215 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 44203 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 44202 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 44211 smfresal 44201 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 44191 smflim2 44218 smflimlem1 44185 smflimlem2 44186 smflimlem3 44187 smflimlem4 44188 smflimlem5 44189 smflimlem6 44190 smflimmpt 44222 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 44226 smfsuplem1 44223 smfsuplem2 44224 smfsuplem3 44225 smfsupmpt 44227 smfsupxr 44228 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 44230 smfinflem 44229 smfinfmpt 44231 |
| [Fremlin1] p. 39 | Remark 121G | smflim 44191 smflim2 44218 smflimmpt 44222 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 44220 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 44240 smflimsuplem2 44233 smflimsuplem6 44237 smflimsuplem7 44238 smflimsuplem8 44239 smflimsupmpt 44241 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 44243 smfliminflem 44242 smfliminfmpt 44244 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 44116 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 24604 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 24647 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 24657 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 35781 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 35784 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 9325 inf1 9309 inf2 9310 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 10597 enqer 10607 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 10602 df-nq 10598 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 10594 df-plq 10600 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 7487 df-mpq 10595 df-mq 10601 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 10603 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 10661 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 10662 ltbtwnnq 10664 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 10657 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 10658 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 10665 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 10667 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 10679 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 10681 |
| [Gleason] p. 122 | Definition | df-1p 10668 |
| [Gleason] p. 122 | Remark (1) | prub 10680 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 10719 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 10671 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 10718 psslinpr 10717 supexpr 10740 suplem1pr 10738 suplem2pr 10739 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 10704 addclprlem1 10702 addclprlem2 10703 df-plp 10669 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 10708 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 10707 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 10720 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 10729 ltexprlem1 10722 ltexprlem2 10723 ltexprlem3 10724 ltexprlem4 10725 ltexprlem5 10726 ltexprlem6 10727 ltexprlem7 10728 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 10731 ltaprlem 10730 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 10732 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 10733 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 10670 mulclpr 10706 mulclprlem 10705 reclem2pr 10734 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 10715 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 10710 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 10709 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 10714 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 10737 reclem3pr 10735 reclem4pr 10736 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 10741 enrer 10749 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 10746 df-1r 10747 df-nr 10742 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 10744 df-plr 10743 negexsr 10788 recexsr 10793 recexsrlem 10789 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 10745 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11897 creur 11896 cru 11894 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10874 axcnre 10850 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 14753 crimd 14870 crimi 14831 crre 14752 crred 14869 crrei 14830 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 14755 remimd 14836 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14923 absval2d 15084 absval2i 15036 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 14779 cjaddd 14858 cjaddi 14826 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 14780 cjmuld 14859 cjmuli 14827 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 14778 cjcjd 14837 cjcji 14809 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 14777 cjreb 14761 cjrebd 14840 cjrebi 14812 cjred 14864 rere 14760 rereb 14758 rerebd 14839 rerebi 14811 rered 14862 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 14786 addcjd 14850 addcji 14821 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 14876 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14918 abscjd 15089 abscji 15040 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 14928 abs00d 15085 abs00i 15037 absne0d 15086 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 14960 releabsd 15090 releabsi 15041 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 14933 absmuld 15093 absmuli 15043 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14921 sqabsaddi 15044 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 14969 abstrid 15095 abstrii 15047 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 13710 exp0 13713 expp1 13716 expp1d 13792 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 25738 cxpaddd 25776 expadd 13752 expaddd 13793 expaddz 13754 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 25747 cxpmuld 25795 expmul 13755 expmuld 13794 expmulz 13756 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 25744 mulcxpd 25787 mulexp 13749 mulexpd 13806 mulexpz 13750 |
| [Gleason] p. 140 | Exercise 1 | znnen 15848 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 13169 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 15268 rlimadd 15279 rlimdiv 15284 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 15270 rlimsub 15281 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 15269 rlimmul 15282 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 15273 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 15219 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 15240 climcj 15241 climim 15243 climre 15242 rlimabs 15245 rlimcj 15246 rlimim 15248 rlimre 15247 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 10944 df-xr 10943 ltxr 12779 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 15107 limsupval 15110 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 15308 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 15317 caucvgb 15318 caucvgr 15314 climcau 15309 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 15455 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 15522 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 14974 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 13475 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 20503 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 23403 xmet0 23402 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 23419 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 23410 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 23412 mstri 23529 xmettri 23411 xmstri 23528 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 23442 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 22706 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 24378 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 23601 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 23933 addcn2 15230 mulcn 23935 mulcn2 15232 subcn 23934 subcn2 15231 |
| [Gleason] p. 295 | Remark | bcval3 13947 bcval4 13948 |
| [Gleason] p. 295 | Equation 2 | bcpasc 13962 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 13945 df-bc 13944 |
| [Gleason] p. 296 | Remark | bcn0 13951 bcnn 13953 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 15469 |
| [Gleason] p. 308 | Equation 2 | ef0 15727 |
| [Gleason] p. 308 | Equation 3 | efcj 15728 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 15733 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 15737 |
| [Gleason] p. 310 | Equation 14 | sinadd 15800 |
| [Gleason] p. 310 | Equation 15 | cosadd 15801 |
| [Gleason] p. 311 | Equation 17 | sincossq 15812 |
| [Gleason] p. 311 | Equation 18 | cosbnd 15817 sinbnd 15816 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 13859 sqeqori 13857 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 15709 |
| [Godowski] p. 730 | Equation SF | goeqi 30535 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 29930 |
| [Golan] p. 1 | Remark | srgisid 19678 |
| [Golan] p. 1 | Definition | df-srg 19656 |
| [Golan] p. 149 | Definition | df-slmd 31355 |
| [Gonshor] p. 7 | Definition | df-scut 33904 |
| [Gonshor] p. 9 | Theorem 2.5 | slerec 33939 |
| [Gonshor] p. 10 | Theorem 2.6 | cofcut1 34016 |
| [Gonshor] p. 10 | Theorem 2.7 | cofcut2 34017 |
| [Gonshor] p. 12 | Theorem 2.9 | cofcutr 34018 |
| [Gonshor] p. 13 | Definition | df-adds 34045 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 34387 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 17211 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 17213 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 45262 df-cllaw 45260 df-comlaw 45261 |
| [Hall] p. 2 | Section 1.2 | df-clintop 45274 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 45295 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 30327 riesz2 30328 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 30203 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 30435 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 30447 elpjidm 30446 pjnmopi 30410 |
| [Halmos] p. 44 | Remark | pjinormi 29949 pjinormii 29938 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 30451 pjrn 29969 pjrni 29964 pjvec 29958 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 29989 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 30416 hmopidmpji 30414 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 30453 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 30442 pjocvec 29959 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 30431 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 30434 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 30437 pjssdif2i 30436 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 30117 |
| [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 1803 |
| [Hatcher] p. 25 | Definition | df-phtpc 24060 df-phtpy 24039 |
| [Hatcher] p. 26 | Definition | df-pco 24073 df-pi1 24076 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 24063 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 24118 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 21546 df-dmatalt 45619 |
| [Helfgott] p. 2 | Theorem | tgoldbach 45149 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 45134 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 45146 bgoldbtbnd 45141 bgoldbtbnd 45141 tgblthelfgott 45147 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 32521 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 32522 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 32536 hgt750lemb 32535 hgt750leme 32537 hgt750lemf 32532 hgt750lemg 32533 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 45143 tgoldbachgt 32542 tgoldbachgtALTV 45144 tgoldbachgtd 32541 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 32523 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 28755 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 18502 grpoideu 28771 mndideu 18310 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 18528 grpoinveu 28781 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 18556 grpo2inv 28793 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 18567 grpoinvop 28795 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 18589 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1776 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1777 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1779 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 30682 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 30695 cdj3i 30703 cdj3lem1 30696 cdjreui 30694 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 30693 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 39905 |
| [Holland95] p. 14 | Line 15 | hgmapvs 39831 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 39853 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 39854 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 39851 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 39857 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 39776 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 39871 |
| [Holland95] p. 204 | Definition of involution | df-srng 20020 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 37443 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 39468 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 39421 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 37873 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 39317 poml4N 37893 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 39408 pexmidALTN 37918 pexmidN 37909 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 39473 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 37064 ldualset 37065 |
| [Holland95] p. 222 | Item 1 | df-lines 37441 df-pointsN 37442 |
| [Holland95] p. 222 | Item 2 | df-polarityN 37843 |
| [Holland95] p. 223 | Remark | ispsubcl2N 37887 omllaw4 37186 pol1N 37850 polcon3N 37857 |
| [Holland95] p. 223 | Definition | df-psubclN 37875 |
| [Holland95] p. 223 | Equation for polarity | polval2N 37846 |
| [Holmes] p. 40 | Definition | df-xrn 36427 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 29346 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 30444 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 30225 eigre 30097 eigrei 30096 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 30226 eigorth 30100 eigorthi 30099 |
| [Hughes] p. 137 | Remark (ii) | eigposi 30098 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 28573 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 28569 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 28570 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 28571 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 28589 frgrregorufr0 28588 frgrregorufrg 28590 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 28596 frrusgrord 28605 frrusgrord0 28604 |
| [Huneke] p. 2 | Statement | df-clwwlknon 28352 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 28579 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 28582 frgrwopreg2 28583 frgrwopregasn 28580 frgrwopregbsn 28581 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 28585 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 28599 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 28602 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 28350 numclwlk1 28635 numclwlk1lem1 28633 numclwlk1lem2 28634 numclwwlk1 28625 numclwwlk8 28656 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 28576 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 28039 |
| [Huneke] p. 2 | Definition 6 | 2clwwlk 28611 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 28637 numclwwlkovh0 28636 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 28645 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 28242 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 28649 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 28652 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 28655 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 28667 natded 28667 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 28667 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 28667 natded 28667 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 28667 |
| [Jech] p. 4 | Definition of class | cv 1542 cvjust 2733 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 10265 |
| [Jech] p. 42 | Equation 6.1 | alephadd 10263 alephmul 10264 |
| [Jech] p. 43 | Lemma 6.2 | infmap 10262 infmap2 9904 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 9502 |
| [Jech] p. 72 | Equation 9.3 | scott0 9574 scottex 9573 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 9555 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 9579 |
| [Jech] p. 78 | Note | opthprc 5642 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 40645 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 40733 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 40734 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 40657 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 40661 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 40662 rmyp1 40663 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 40664 rmym1 40665 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 40655 rmx1 40656 rmxluc 40666 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 40659 rmy1 40660 rmyluc 40667 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 40669 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 40670 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 40690 jm2.17b 40691 jm2.17c 40692 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 40723 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 40727 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 40718 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 40693 jm2.24nn 40689 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 40732 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 40738 rmygeid 40694 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 40750 |
| [Juillerat] p. 11 | Section *5 | etransc 43706 etransclem47 43704 etransclem48 43705 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 43701 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 43703 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 43689 |
| [Juillerat] p. 13 | Proof | etransclem35 43692 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 43695 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 43681 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 43698 |
| [Juillerat] p. 14 | Proof | etransclem23 43680 |
| [KalishMontague] p. 81 | Note 1 | ax-6 1976 |
| [KalishMontague] p. 85 | Lemma 2 | equid 2020 |
| [KalishMontague] p. 85 | Lemma 3 | equcomi 2025 |
| [KalishMontague] p. 86 | Lemma 7 | cbvalivw 2015 cbvaliw 2014 wl-cbvmotv 35598 wl-motae 35600 wl-moteq 35599 |
| [KalishMontague] p. 87 | Lemma 8 | spimvw 2004 spimw 1979 |
| [KalishMontague] p. 87 | Lemma 9 | spfw 2041 spw 2042 |
| [Kalmbach] p. 14 | Definition of lattice | chabs1 29778 chabs1i 29780 chabs2 29779 chabs2i 29781 chjass 29795 chjassi 29748 latabs1 18107 latabs2 18108 |
| [Kalmbach] p. 15 | Definition of atom | df-at 30600 ela 30601 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 30545 cvrval2 37214 |
| [Kalmbach] p. 16 | Definition | df-ol 37118 df-oml 37119 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 29846 cmbri 29852 cmtvalN 37151 df-cm 29845 df-cmtN 37117 |
| [Kalmbach] p. 22 | Remark | omllaw5N 37187 pjoml5 29875 pjoml5i 29850 |
| [Kalmbach] p. 22 | Definition | pjoml2 29873 pjoml2i 29847 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 29876 cmcmi 29854 cmcmii 29859 cmtcomN 37189 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 37185 omlsi 29666 pjoml 29698 pjomli 29697 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 37184 |
| [Kalmbach] p. 23 | Remark | cmbr2i 29858 cmcm3 29877 cmcm3i 29856 cmcm3ii 29861 cmcm4i 29857 cmt3N 37191 cmt4N 37192 cmtbr2N 37193 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 29870 cmbr3i 29862 cmtbr3N 37194 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 29880 fh1i 29883 fh2 29881 fh2i 29884 omlfh1N 37198 |
| [Kalmbach] p. 65 | Remark | chjatom 30619 chslej 29760 chsleji 29720 shslej 29642 shsleji 29632 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 29757 chocini 29716 chsupcl 29602 chsupval2 29672 h0elch 29517 helch 29505 hsupval2 29671 ocin 29558 ococss 29555 shococss 29556 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 29574 |
| [Kalmbach] p. 66 | Remark | df-pjh 29657 pjssmi 30427 pjssmii 29943 |
| [Kalmbach] p. 67 | Lemma 3 | osum 29907 osumi 29904 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 30462 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 30662 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 30572 |
| [Kalmbach] p. 140 | Remark | hatomic 30622 hatomici 30621 hatomistici 30624 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 37259 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 30643 lsatexch 36983 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 30617 cvlcvr1 37279 cvr1 37350 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 30636 cvexchi 30631 cvrexch 37360 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 30626 hlrelat 37342 hlrelat5N 37341 lrelat 36954 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 20317 lsmsatcv 36950 spansncv 29915 spansncvi 29914 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 36969 spansncv2 30555 |
| [Kalmbach] p. 266 | Definition | df-st 30473 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 30111 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 10332 fpwwe2 10329 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 10333 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 10340 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 10335 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 10337 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 10350 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchdjuidm 10354 gchxpidm 10355 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 10366 gchhar 10365 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwdjudom 9902 unxpwdom 9277 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 10356 |
| [Kreyszig] p. 3 | Property M1 | metcl 23392 xmetcl 23391 |
| [Kreyszig] p. 4 | Property M2 | meteq0 23399 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 23633 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 11621 muleqadd 11548 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 23498 |
| [Kreyszig] p. 19 | Remark | mopntopon 23499 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 23559 mopnm 23504 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 23557 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 23562 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 23603 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 22316 lmmbr 24326 lmmbr2 24327 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 22438 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 24381 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 24344 iscmet2 24362 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 24384 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 22519 metelcls 24373 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 24374 metcld2 24375 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 24167 lmodvneg1 20080 nvinv 28901 vcm 28838 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 24163 lmod0vs 20070 slmd0vs 31378 vc0 28836 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 20071 slmdvs0 31379 vcz 28837 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 28953 ngpmet 23664 nrmmetd 23635 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 28948 imsdval2 28949 ncvspds 24229 ngpds 23665 |
| [Kreyszig] p. 63 | Problem 1 | nmval 23650 nvnd 28950 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 23679 nmge0 23678 nvge0 28935 nvz 28931 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 23685 nvabs 28934 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 29063 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 29007 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 29069 blocni 29067 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 29068 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 24272 ipeq0 20754 ipz 28981 |
| [Kreyszig] p. 135 | Problem 2 | cphpyth 24284 pythi 29112 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 29116 |
| [Kreyszig] p. 137 | Lemma 3.2-1(a) | ipcau 24306 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 15495 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 24504 minveco 29146 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 29012 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 24397 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 29135 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 30385 leopg 30384 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 30403 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 29180 |
| [Kulpa] p. 547 | Theorem | poimir 35736 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 35735 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 35734 |
| [Kulpa] p. 548 | Theorem | broucube 35737 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 35729 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 35730 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2384 axnul 5223 |
| [Kunen] p. 11 | Axiom 3 | axnul 5223 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7771 |
| [Kunen] p. 24 | Definition 10.24 | mapval 8586 mapvalg 8584 |
| [Kunen] p. 30 | Lemma 10.20 | fodomg 10208 |
| [Kunen] p. 31 | Definition 10.24 | mapex 8580 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 9452 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 9494 r1elssi 9493 |
| [Kunen] p. 107 | Exercise 4 | rankop 9546 rankopb 9540 rankuni 9551 rankxplim 9567 rankxpsuc 9570 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4934 |
| [Lang] , p. 225 | Corollary 1.3 | finexttrb 31638 |
| [Lang] p. | Definition | df-rn 5591 |
| [Lang] p. 3 | Statement | lidrideqd 18267 mndbn0 18315 |
| [Lang] p. 3 | Definition | df-mnd 18300 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 18285 |
| [Lang] p. 4 | Property of composites. Second formula | gsumccat 18394 |
| [Lang] p. 5 | Equation | gsumreidx 19432 |
| [Lang] p. 5 | Definition of an (infinite) product | gsumfsupp 45256 |
| [Lang] p. 6 | Example | nn0mnd 45253 |
| [Lang] p. 6 | Equation | gsumxp2 19495 |
| [Lang] p. 6 | Statement | cycsubm 18735 |
| [Lang] p. 6 | Definition | mulgnn0gsum 18624 |
| [Lang] p. 6 | Observation | mndlsmidm 19190 |
| [Lang] p. 7 | Definition | dfgrp2e 18519 |
| [Lang] p. 30 | Definition | df-tocyc 31275 |
| [Lang] p. 32 | Property (a) | cyc3genpm 31320 |
| [Lang] p. 32 | Property (b) | cyc3conja 31325 cycpmconjv 31310 |
| [Lang] p. 53 | Definition | df-cat 17293 |
| [Lang] p. 53 | Axiom CAT 1 | cat1 17727 cat1lem 17726 |
| [Lang] p. 54 | Definition | df-iso 17377 |
| [Lang] p. 57 | Definition | df-inito 17614 df-termo 17615 |
| [Lang] p. 58 | Example | irinitoringc 45507 |
| [Lang] p. 58 | Statement | initoeu1 17641 termoeu1 17648 |
| [Lang] p. 62 | Definition | df-func 17488 |
| [Lang] p. 65 | Definition | df-nat 17574 |
| [Lang] p. 91 | Note | df-ringc 45443 |
| [Lang] p. 92 | Statement | mxidlprm 31541 |
| [Lang] p. 92 | Definition | isprmidlc 31524 |
| [Lang] p. 128 | Remark | dsmmlmod 20861 |
| [Lang] p. 129 | Proof | lincscm 45651 lincscmcl 45653 lincsum 45650 lincsumcl 45652 |
| [Lang] p. 129 | Statement | lincolss 45655 |
| [Lang] p. 129 | Observation | dsmmfi 20854 |
| [Lang] p. 141 | Theorem 5.3 | dimkerim 31609 qusdimsum 31610 |
| [Lang] p. 141 | Corollary 5.4 | lssdimle 31592 |
| [Lang] p. 147 | Definition | snlindsntor 45692 |
| [Lang] p. 504 | Statement | mat1 21503 matring 21499 |
| [Lang] p. 504 | Definition | df-mamu 21442 |
| [Lang] p. 505 | Statement | mamuass 21458 mamutpos 21514 matassa 21500 mattposvs 21511 tposmap 21513 |
| [Lang] p. 513 | Definition | mdet1 21657 mdetf 21651 |
| [Lang] p. 513 | Theorem 4.4 | cramer 21747 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 21643 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 21667 |
| [Lang] p. 515 | Definition | df-minmar1 21691 smadiadetr 21731 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 21666 mdetralt 21664 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 21679 |
| [Lang] p. 518 | Definition | df-madu 21690 |
| [Lang] p. 518 | Proposition 4.16 | madulid 21701 madurid 21700 matinv 21733 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 21946 |
| [Lang], p. 224 | Proposition 1.2 | extdgmul 31637 fedgmul 31613 |
| [Lang], p. 561 | Remark | chpmatply1 21888 |
| [Lang], p. 561 | Definition | df-chpmat 21883 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 41833 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 41828 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 41834 |
| [LeBlanc] p. 277 | Rule R2 | axnul 5223 |
| [Levy] p. 12 | Axiom 4.3.1 | df-clab 2717 |
| [Levy] p. 59 | Definition | df-ttrcl 33693 |
| [Levy] p. 64 | Theorem 5.6(ii) | frinsg 9439 |
| [Levy] p. 338 | Axiom | df-clel 2818 df-cleq 2731 |
| [Levy] p. 357 | Proof sketch of conservativity; for details see Appendix | df-clel 2818 df-cleq 2731 |
| [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 10072 |
| [Levy58] p. 2 | Definition II | df-fin2 9972 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 9971 |
| [Levy58] p. 2 | Definition III | df-fin3 9974 |
| [Levy58] p. 3 | Definition V | df-fin5 9975 |
| [Levy58] p. 3 | Definition IV | df-fin4 9973 |
| [Levy58] p. 4 | Definition VI | df-fin6 9976 |
| [Levy58] p. 4 | Definition VII | df-fin7 9977 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 10101 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 33815 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 33826 |
| [Lipparini] p. 6 | Proposition 4.2 | noinfbnd1 33858 nosupbnd1 33843 |
| [Lipparini] p. 6 | Proposition 4.3 | noinfbnd2 33860 nosupbnd2 33845 |
| [Lipparini] p. 7 | Theorem 5.1 | noetasuplem3 33864 noetasuplem4 33865 |
| [Lipparini] p. 7 | Corollary 4.4 | nosupinfsep 33861 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1776 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1777 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1779 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 30670 |
| [Maeda] p. 168 | Lemma 5 | mdsym 30674 mdsymi 30673 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 30668 mdsymlem6 30670 mdsymlem7 30671 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 30672 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 30575 ssdmd2 30576 ssmd1 30573 ssmd2 30574 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 30571 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 30543 df-md 30542 mdbr 30556 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 30593 mdslj1i 30581 mdslj2i 30582 mdslle1i 30579 mdslle2i 30580 mdslmd1i 30591 mdslmd2i 30592 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 30583 mdsl2bi 30585 mdsl2i 30584 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 30597 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 30594 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 30595 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 30572 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 30577 mdsl3 30578 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 30596 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 30691 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 37261 hlrelat1 37340 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 36979 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 30598 cvmdi 30586 cvnbtwn4 30551 cvrnbtwn4 37219 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 30599 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 37280 cvp 30637 cvrp 37356 lcvp 36980 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 30661 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 30660 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 37273 hlexch4N 37332 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 30663 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 37383 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 37689 atpsubN 37693 df-pointsN 37442 pointpsubN 37691 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 37444 pmap11 37702 pmaple 37701 pmapsub 37708 pmapval 37697 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 37705 pmap1N 37707 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 37710 pmapglb2N 37711 pmapglb2xN 37712 pmapglbx 37709 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 37792 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 37417 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 37736 paddclN 37782 paddidm 37781 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 37418 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 37778 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 37417 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 37418 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 19195 lsmmod2 19196 lssats 36952 shatomici 30620 shatomistici 30623 shmodi 29652 shmodsi 29651 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 30562 mdsymlem7 30671 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 29851 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 29755 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 30677 |
| [Margaris] p. 40 | Rule C | exlimiv 1938 |
| [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 1788 df-or 848 dfbi2 478 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 28664 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 42416 |
| [Margaris] p. 60 | Theorem 8 | jcn 165 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 42417 |
| [Margaris] p. 79 | Rule C | exinst01 42126 exinst11 42127 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1985 19.2g 2187 r19.2z 4423 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2202 rr19.3v 3592 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2162 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1833 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1789 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2180 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2205 19.9h 2289 exlimd 2218 exlimdh 2293 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2168 excomim 2169 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2328 |
| [Margaris] p. 90 | Section 19 | conventions-labels 28665 conventions-labels 28665 conventions-labels 28665 conventions-labels 28665 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1834 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 41877 albi 1826 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 2225 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 2226 |
| [Margaris] p. 90 | Theorem 19.18 | 2exbi 41879 exbi 1854 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2229 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 41876 2alimdv 1926 alimd 2212 alimdh 1825 alimdv 1924 ax-4 1817 ralimdaa 3141 ralimdv 3104 ralimdva 3103 ralimdvva 3105 sbcimdv 3787 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2207 19.21h 2290 19.21t 2206 19.21vv 41875 alrimd 2215 alrimdd 2214 alrimdh 1871 alrimdv 1937 alrimi 2213 alrimih 1831 alrimiv 1935 alrimivv 1936 hbralrimi 3106 r19.21be 3134 r19.21bi 3133 ralrimd 3142 ralrimdv 3112 ralrimdva 3113 ralrimdvv 3117 ralrimdvva 3118 ralrimi 3140 ralrimia 3421 ralrimiv 3107 ralrimiva 3108 ralrimivv 3114 ralrimivva 3115 ralrimivvva 3116 ralrimivw 3109 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 41878 2eximdv 1927 exim 1841 eximd 2216 eximdh 1872 eximdv 1925 rexim 3169 reximd2a 3241 reximdai 3240 reximdd 42582 reximddv 3204 reximddv2 3207 reximddv3 42581 reximdv 3202 reximdv2 3199 reximdva 3203 reximdvai 3200 reximdvva 3206 reximi2 3172 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2211 19.23bi 2190 19.23h 2291 19.23t 2210 exlimdv 1941 exlimdvv 1942 exlimexi 42025 exlimiv 1938 exlimivv 1940 rexlimd3 42574 rexlimdv 3212 rexlimdv3a 3215 rexlimdva 3213 rexlimdva2 3216 rexlimdvaa 3214 rexlimdvv 3222 rexlimdvva 3223 rexlimdvw 3219 rexlimiv 3209 rexlimiva 3210 rexlimivv 3221 |
| [Margaris] p. 90 | Theorem 19.24 | 19.24 1994 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1888 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26 1878 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 2227 r19.27z 4433 r19.27zv 4434 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2228 19.28vv 41885 r19.28z 4426 r19.28zv 4429 rr19.28v 3593 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1881 r19.29d2r 3263 r19.29imd 3186 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1889 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2234 19.31vv 41883 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2233 r19.32 44469 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 41881 19.33 1892 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1995 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35 1885 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36 2230 19.36vv 41882 r19.36zv 4435 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2232 19.37vv 41884 r19.37zv 4430 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1846 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 1993 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1895 19.40 1894 r19.40 3274 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2235 19.41rg 42051 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2236 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1890 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2237 r19.44zv 4432 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2238 r19.45zv 4431 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2613 |
| [Mayet] p. 370 | Remark | jpi 30532 largei 30529 stri 30519 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 30474 ishst 30476 |
| [Mayet3] p. 10 | Theorem | hstrbi 30528 hstri 30527 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 29990 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 29991 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 30540 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 29594 chsupcl 29602 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 30622 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 30616 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 30643 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 37923 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 18119 latj32 18117 latjass 18115 |
| [Megill] p. 444 | Axiom C5 | ax-5 1918 ax5ALT 36847 |
| [Megill] p. 444 | Section 7 | conventions 28664 |
| [Megill] p. 445 | Lemma L12 | aecom-o 36841 ax-c11n 36828 axc11n 2427 |
| [Megill] p. 446 | Lemma L17 | equtrr 2030 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 36836 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 36868 hbnae 2433 |
| [Megill] p. 447 | Remark 9.1 | dfsb1 2486 sbid 2255 sbidd-misc 46299 sbidd 46298 |
| [Megill] p. 448 | Remark 9.6 | axc14 2464 |
| [Megill] p. 448 | Scheme C4' | ax-c4 36824 |
| [Megill] p. 448 | Scheme C5' | ax-c5 36823 sp 2182 |
| [Megill] p. 448 | Scheme C6' | ax-11 2160 |
| [Megill] p. 448 | Scheme C7' | ax-c7 36825 |
| [Megill] p. 448 | Scheme C8' | ax-7 2016 |
| [Megill] p. 448 | Scheme C9' | ax-c9 36830 |
| [Megill] p. 448 | Scheme C10' | ax-6 1976 ax-c10 36826 |
| [Megill] p. 448 | Scheme C11' | ax-c11 36827 |
| [Megill] p. 448 | Scheme C12' | ax-8 2114 |
| [Megill] p. 448 | Scheme C13' | ax-9 2122 |
| [Megill] p. 448 | Scheme C14' | ax-c14 36831 |
| [Megill] p. 448 | Scheme C15' | ax-c15 36829 |
| [Megill] p. 448 | Scheme C16' | ax-c16 36832 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 36844 dral1 2440 dral2-o 36870 dral2 2439 drex1 2442 drex2 2443 drsb1 2500 drsb2 2265 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2167 sbequ 2091 sbid2v 2514 |
| [Megill] p. 450 | Example in Appendix | hba1-o 36837 hba1 2296 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 44266 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3809 rspsbca 3810 stdpc4 2076 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 36824 ra4 3816 stdpc5 2208 |
| [Mendelson] p. 81 | Rule C | exlimiv 1938 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 2036 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 2250 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3711 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 5422 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 4326 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 4327 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 4198 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 4255 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 4199 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 4068 |
| [Mendelson] p. 231 | Definition of union | dfun3 4197 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 5361 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4834 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5474 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4551 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5476 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4863 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5725 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 6161 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 7603 |
| [Mendelson] p. 246 | Definition of successor | df-suc 6257 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 8389 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8877 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8797 xpsneng 8798 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8804 xpcomeng 8805 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8807 |
| [Mendelson] p. 255 | Definition | brsdom 8719 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8800 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 8578 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8782 mapsnend 8781 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8883 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8882 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 8629 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8785 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8801 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 9864 djucomen 9863 |
| [Mendelson] p. 258 | Exercise 4.56(f) | djudom1 9868 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 9862 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 8324 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 8352 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 10245 |
| [Mendelson] p. 281 | Definition | df-r1 9452 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 9501 |
| [Mendelson] p. 287 | Axiom system MK | ru 3711 |
| [MertziosUnger] p. 152 | Definition | df-frgr 28523 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 28558 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 28560 vdgn1frgrv3 28561 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 28562 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 28555 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 28548 2pthfrgrrn 28546 2pthfrgrrn2 28547 |
| [Mittelstaedt] p. 9 | Definition | df-oc 29514 |
| [Monk1] p. 22 | Remark | conventions 28664 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 28664 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 4162 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5683 ssrelf 30855 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5684 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 5134 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 6155 coi2 6156 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5818 rn0 5824 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 6034 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5598 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5827 rnxp 6062 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5675 xp0 6050 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5974 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5971 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7737 imaexALTV 36391 imaexg 7736 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5969 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6935 funfvop 6909 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6807 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6817 |
| [Monk1] p. 43 | Theorem 4.6 | funun 6464 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 7109 dff13f 7110 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 7077 funrnex 7770 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 7102 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 6119 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4893 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7821 df-1st 7804 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7822 df-2nd 7805 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 9542 ranksnb 9515 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 9543 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 9544 rankunb 9538 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 9526 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 9452 r1val2 9525 |
| [Monk1] p. 117 | Lemma | zorn2 10192 zorn2g 10189 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 9674 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 10247 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 9669 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1817 |
| [Monk2] p. 105 | Axiom C7 | ax-7 2016 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2177 ax-c15 36829 ax12v2 2179 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 36824 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2160 |
| [Monk2] p. 109 | Lemma 15 | equvini 2456 equvinv 2037 eqvinop 5395 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1918 ax5ALT 36847 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2143 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2160 |
| [Monk2] p. 114 | Lemma 21 | sp 2182 |
| [Monk2] p. 114 | Lemma 22 | axc4 2322 hba1-o 36837 hba1 2296 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2156 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2176 nfra2 3155 nfra2w 3152 |
| [Moore] p. 53 | Part I | df-mre 17211 |
| [Munkres] p. 77 | Example 2 | distop 22052 indistop 22059 indistopon 22058 |
| [Munkres] p. 77 | Example 3 | fctop 22061 fctop2 22062 |
| [Munkres] p. 77 | Example 4 | cctop 22063 |
| [Munkres] p. 78 | Definition of basis | df-bases 22003 isbasis3g 22006 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 17070 tgval2 22013 |
| [Munkres] p. 79 | Remark | tgcl 22026 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 22020 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 22044 tgss3 22043 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 22045 basgen2 22046 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 35446 topdifinfeq 35447 topdifinffin 35445 topdifinfindis 35443 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 22218 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 22096 topcld 22093 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 22097 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 22099 |
| [Munkres] p. 94 | Definition of closure | clsval 22095 |
| [Munkres] p. 94 | Definition of interior | ntrval 22094 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 22133 elcls 22131 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 22141 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 22206 neindisj 22175 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 22208 |
| [Munkres] p. 97 | Definition of limit point | islp2 22203 lpval 22197 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 22373 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 22285 iscn 22293 iscn2 22296 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 22338 cncnp2 22339 cncnpi 22336 df-cnp 22286 iscnp 22295 iscnp2 22297 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 23604 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 24379 |
| [Nathanson] p. 123 | Remark | reprgt 32500 reprinfz1 32501 reprlt 32498 |
| [Nathanson] p. 123 | Definition | df-repr 32488 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 32520 |
| [Nathanson] p. 123 | Proposition | breprexp 32512 breprexpnat 32513 itgexpif 32485 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 30366 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 45142 |
| [Pfenning] p. 17 | Definition XM | natded 28667 |
| [Pfenning] p. 17 | Definition NNC | natded 28667 notnotrd 135 |
| [Pfenning] p. 17 | Definition ` `C | natded 28667 |
| [Pfenning] p. 18 | Rule" | natded 28667 |
| [Pfenning] p. 18 | Definition /\I | natded 28667 |
| [Pfenning] p. 18 | Definition ` `E | natded 28667 natded 28667 natded 28667 natded 28667 natded 28667 |
| [Pfenning] p. 18 | Definition ` `I | natded 28667 natded 28667 natded 28667 natded 28667 natded 28667 |
| [Pfenning] p. 18 | Definition ` `EL | natded 28667 |
| [Pfenning] p. 18 | Definition ` `ER | natded 28667 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 28667 |
| [Pfenning] p. 18 | Definition ` `IR | natded 28667 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 28667 |
| [Pfenning] p. 127 | Definition =E | natded 28667 |
| [Pfenning] p. 127 | Definition =I | natded 28667 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 24270 df-dip 28963 dip0l 28980 ip0l 20752 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 24311 ipval 28965 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 28976 ipcj 20750 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 24273 dipdir 29104 ipdir 20755 ipdiri 29092 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 28972 nmsq 24262 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 29087 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 29089 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 29090 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 24279 dipass 29107 ipass 20761 ipassi 29103 |
| [Prugovecki] p. 186 | Definition of bra | braval 30206 df-bra 30112 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 30113 kbval 30216 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 30644 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 37828 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 30658 atcvat4i 30659 cvrat3 37382 cvrat4 37383 lsatcvat3 36992 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 30544 cvrval 37209 df-cv 30541 df-lcv 36959 lspsncv0 20322 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 37840 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 37841 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2717 rabid 3305 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2282 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2731 |
| [Quine] p. 19 | Definition 2.9 | conventions 28664 df-v 3425 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2872 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2881 abid2f 2939 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2274 |
| [Quine] p. 40 | Theorem 6.2 | sb6 2093 sbalex 2242 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2818 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2739 eqid1 28731 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2746 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3713 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3714 dfsbcq2 3715 |
| [Quine] p. 43 | Theorem 6.8 | vex 3427 |
| [Quine] p. 43 | Theorem 6.9 | isset 3436 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3521 spcgv 3526 spcimgf 3519 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3725 spsbcd 3726 |
| [Quine] p. 44 | Theorem 6.12 | elex 3441 |
| [Quine] p. 44 | Theorem 6.13 | elab 3603 elabg 3601 elabgf 3599 |
| [Quine] p. 44 | Theorem 6.14 | noel 4262 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4651 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4562 df-sn 4560 |
| [Quine] p. 49 | Theorem 7.4 | snss 4717 snssg 4716 |
| [Quine] p. 49 | Theorem 7.5 | prss 4751 prssg 4750 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4696 prid1g 4694 prid2 4697 prid2g 4695 snid 4595 snidg 4593 |
| [Quine] p. 51 | Theorem 7.12 | snex 5349 |
| [Quine] p. 51 | Theorem 7.13 | prex 5350 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4859 unisnALT 42427 unisng 4858 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4862 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4869 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4867 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 6391 |
| [Quine] p. 56 | Definition 8.18 | dfaiota2 44457 dfiota2 6377 |
| [Quine] p. 57 | Theorem 8.19 | aiotaval 44466 iotaval 6392 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 6396 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 6398 |
| [Quine] p. 58 | Definition 9.1 | df-op 4566 |
| [Quine] p. 61 | Theorem 9.5 | opabid 5432 opabidw 5431 opelopab 5448 opelopaba 5442 opelopabaf 5450 opelopabf 5451 opelopabg 5444 opelopabga 5439 opelopabgf 5446 oprabid 7287 oprabidw 7286 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5586 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5588 |
| [Quine] p. 64 | Definition 9.15 | df-id 5480 |
| [Quine] p. 65 | Theorem 10.3 | fun0 6483 |
| [Quine] p. 65 | Theorem 10.4 | funi 6450 |
| [Quine] p. 65 | Theorem 10.5 | funsn 6471 funsng 6469 |
| [Quine] p. 65 | Definition 10.1 | df-fun 6420 |
| [Quine] p. 65 | Definition 10.2 | args 5989 dffv4 6753 |
| [Quine] p. 68 | Definition 10.11 | conventions 28664 df-fv 6426 fv2 6751 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13913 nn0opth2i 13912 nn0opthi 13911 omopthi 8452 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 8212 |
| [Quine] p. 232 | Equation i | carddom 10240 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 6505 funimaexg 6504 |
| [Quine] p. 331 | Axiom system NF | ru 3711 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 29346 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 28963 polid 29421 polid2i 29419 polidi 29420 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 29075 |
| [ReedSimon] p. 195 | Remark | lnophm 30281 lnophmi 30280 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 30394 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 30396 leopmuli 30395 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 30399 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 30114 leoppos 30388 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 30398 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 30387 |
| [Roman] p. 4 | Definition | df-dmat 21546 df-dmatalt 45619 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 45313 |
| [Roman] p. 19 | Part Preliminaries | df-ring 19699 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 45706 |
| [Roman] p. 112 | Note | isldepslvec2 45706 ldepsnlinc 45729 zlmodzxznm 45718 |
| [Roman] p. 112 | Example | zlmodzxzequa 45717 zlmodzxzequap 45720 zlmodzxzldep 45725 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 21946 |
| [Rosenlicht] p. 80 | Theorem | heicant 35738 |
| [Rosser] p. 281 | Definition | df-op 4566 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 32524 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 32525 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 45582 pmtr3ncom 18997 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 18993 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 18936 cayleyth 18937 |
| [Rudin] p. 164 | Equation 27 | efcan 15732 |
| [Rudin] p. 164 | Equation 30 | efzval 15738 |
| [Rudin] p. 167 | Equation 48 | absefi 15832 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 200 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1779 |
| [Sanford] p. 39 | Rule 4 | mptxor 1777 |
| [Sanford] p. 40 | Rule 1 | mptnan 1776 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 6009 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 6012 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 6008 |
| [Schechter] p. 51 | Definition of transitivity | cotr 6006 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 17211 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 17212 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 17212 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 17214 |
| [Schechter] p. 139 | Definition AC3 | dfac9 9822 |
| [Schechter] p. 141 | Definition (MC) | dfac11 40795 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 10132 axdc3 10140 |
| [Schechter] p. 187 | Definition of ring with unit | isring 19701 isrngo 35981 |
| [Schechter] p. 276 | Remark 11.6.e | span0 29804 |
| [Schechter] p. 276 | Definition of span | df-span 29571 spanval 29595 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 22050 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 27184 axtgcgrrflx 26726 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 27185 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 27186 axtgcgrid 26727 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 26712 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 27197 axtgsegcon 26728 df-trkgcb 26714 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 27208 axtg5seg 26729 df-trkgcb 26714 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 27209 axtgbtwnid 26730 df-trkgb 26713 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 27211 axtgpasch 26731 df-trkgb 26713 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 27230 df-trkg2d 32544 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 26734 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 26735 df-trkg2d 32544 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 27233 axtgeucl 26736 df-trkge 26715 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 27246 axtgcont 26733 axtgcont1 26732 df-trkgb 26713 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 34215 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 34217 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 34220 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 34224 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 34225 tgcgrcomimp 26741 tgcgrcoml 26743 tgcgrcomr 26742 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 34230 tgcgrtriv 26748 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 34234 tg5segofs 32552 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 32549 df-ofs 34211 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 34236 tgcgrextend 26749 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 34238 tgsegconeq 26750 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 34250 btwntriv2 34240 tgbtwntriv2 26751 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 34241 tgbtwncom 26752 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 34244 tgbtwntriv1 26755 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 34245 tgbtwnswapid 26756 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 34251 btwnintr 34247 tgbtwnexch2 26760 tgbtwnintr 26757 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 34253 btwnexch3 34248 tgbtwnexch 26762 tgbtwnexch3 26758 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 34252 tgbtwnouttr 26761 tgbtwnouttr2 26759 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 27229 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 34255 tgbtwndiff 26770 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 26763 trisegint 34256 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 34272 tgifscgr 26772 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 26822 colrot1 26823 colrot2 26824 lncom 26886 lnrot1 26887 lnrot2 26888 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 34268 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 34273 tgcgrsub 26773 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 34283 tgcgrxfr 26782 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 26781 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 34269 df-cgrg 26775 |
| [Schwabhauser] p. 35 | Definition instead (given | df-cgrg 26775 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 34284 tgbtwnxfr 26794 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 34290 colinearperm2 34292 colinearperm3 34291 colinearperm4 34293 colinearperm5 34294 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 26797 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 34267 tgellng 26817 tglng 26810 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 34295 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 34303 lnxfr 26830 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 34304 lnext 26831 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 34308 tgfscgr 26832 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 34309 lncgr 26833 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 34270 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 34311 lnid 26834 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 34312 tgidinside 26835 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 34329 tgbtwnconn1 26839 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 34330 tgbtwnconn2 26840 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 34331 tgbtwnconn3 26841 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 34337 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 34335 legov 26849 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 26850 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 26863 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 34338 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 34340 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 34342 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 34343 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 34344 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 34341 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 34346 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 26851 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 26853 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 26854 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 26855 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 26856 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 34353 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 34354 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 34349 df-outsideof 34348 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 34350 ishlg 26866 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 26871 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 26873 outsideofrflx 34355 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 26867 hlcomd 26868 outsideofcom 34356 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 26874 outsideoftr 34357 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 26882 outsideofeu 34359 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 34366 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 34367 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 34360 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 34375 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 34376 tglineelsb2 26896 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 34378 linerflx1 34377 linerflx2 34379 tglinecom 26899 tglinerflx1 26897 tglinerflx2 26898 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 34381 tglinethru 26900 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 34365 tglng 26810 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 26858 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 34384 tglinethrueu 26903 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 34385 tglineineq 26907 tglineinteq 26909 tglineintmo 26906 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 26913 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 26914 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 26915 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 26930 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 26926 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 26918 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 26917 ismir 26923 mirbtwn 26922 mircgr 26921 mirfv 26920 mirval 26919 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 26928 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 26929 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 26930 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 26933 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 26934 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 26939 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 26936 mirbtwni 26935 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 26937 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 26949 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 26953 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 26950 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 26951 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 26952 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 26955 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 26956 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 26962 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 26958 israg 26961 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 26963 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 26964 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 26966 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 26967 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 26968 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 26969 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 26970 ragncol 26973 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 26971 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 26977 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 26981 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 26978 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 26960 isperp 26976 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 26979 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 26986 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 26994 colperpexlem2 26995 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 26997 colperpexlem3 26996 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 27002 midex 27001 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 26999 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 27008 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 27003 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 27012 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 27015 opphllem6 27016 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 27018 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 26731 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 27019 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 27027 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 27022 hpgbr 27024 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 27029 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 27028 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 27030 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 27031 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 27032 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 27033 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 27034 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 27048 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 27038 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 27052 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 27053 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 27054 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 27055 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 27056 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 27059 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 27061 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 27039 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 27062 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 27065 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 27066 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 27067 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 27068 trgcopyeu 27070 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 27094 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 27073 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 27082 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 27080 cgrahl2 27081 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 27083 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 27084 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 27086 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 27087 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 27090 cgrahl 27091 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 27095 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 27096 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 27097 acopyeu 27098 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 27105 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 27109 |
| [Schwabhauser] p. 101 | Definition 11.23 | isinag 27102 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 27117 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 27110 isleag 27111 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 27119 tgsas1 27118 tgsas2 27120 tgsas3 27121 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 27123 tgasa1 27122 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 27124 tgsss2 27125 tgsss3 27126 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 26323 dchrsum 26321 dchrsum2 26320 sumdchr 26324 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 26325 sum2dchr 26326 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 19583 ablfacrp2 19584 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 26268 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 26269 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 26276 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 26534 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 26537 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 26591 vmalogdivsum2 26590 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 26581 dirith2 26580 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 26579 rpvmasum 26578 rpvmasum2 26564 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 26539 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 26577 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 26544 dchrisumlem1 26541 dchrisumlem2 26542 dchrisumlem3 26543 dchrisumlema 26540 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 26547 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 26576 dchrmusumlem 26574 dchrvmasumlem 26575 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 26546 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 26548 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 26572 dchrisum0re 26565 dchrisumn0 26573 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 26558 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 26562 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 26563 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 26618 pntrsumbnd2 26619 pntrsumo1 26617 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 26582 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 26584 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 26586 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 26589 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 26594 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 26595 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 26600 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 26602 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 26603 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 26611 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 26612 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 26609 selberg3lem2 26610 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 26613 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 26607 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 26620 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 26621 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 26622 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 26636 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 26648 pntlemb 26649 pntlemc 26647 pntlemd 26646 pntlemg 26650 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 26648 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 26640 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 26645 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 26648 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 26661 pntleml 26663 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 4228 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 4333 dif0 4304 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4420 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4406 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 4219 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 4220 |
| [Stoll] p. 20 | Remark | invdif 4200 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4568 |
| [Stoll] p. 43 | Definition | uniiun 4985 |
| [Stoll] p. 44 | Definition | intiin 4986 |
| [Stoll] p. 45 | Definition | df-iin 4925 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4924 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 405 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 4228 |
| [Strang] p. 242 | Section 6.3 | expgrowth 41834 |
| [Suppes] p. 22 | Theorem 2 | eq0 4275 eq0f 4272 |
| [Suppes] p. 22 | Theorem 4 | eqss 3933 eqssd 3935 eqssi 3934 |
| [Suppes] p. 23 | Theorem 5 | ss0 4330 ss0b 4329 |
| [Suppes] p. 23 | Theorem 6 | sstr 3926 sstrALT2 42336 |
| [Suppes] p. 23 | Theorem 7 | pssirr 4032 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 4033 |
| [Suppes] p. 23 | Theorem 9 | psstr 4036 |
| [Suppes] p. 23 | Theorem 10 | pssss 4027 |
| [Suppes] p. 25 | Theorem 12 | elin 3900 elun 4080 |
| [Suppes] p. 26 | Theorem 15 | inidm 4150 |
| [Suppes] p. 26 | Theorem 16 | in0 4323 |
| [Suppes] p. 27 | Theorem 23 | unidm 4083 |
| [Suppes] p. 27 | Theorem 24 | un0 4322 |
| [Suppes] p. 27 | Theorem 25 | ssun1 4103 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 4111 |
| [Suppes] p. 27 | Theorem 27 | unss 4115 |
| [Suppes] p. 27 | Theorem 28 | indir 4207 |
| [Suppes] p. 27 | Theorem 29 | undir 4208 |
| [Suppes] p. 28 | Theorem 32 | difid 4302 |
| [Suppes] p. 29 | Theorem 33 | difin 4193 |
| [Suppes] p. 29 | Theorem 34 | indif 4201 |
| [Suppes] p. 29 | Theorem 35 | undif1 4407 |
| [Suppes] p. 29 | Theorem 36 | difun2 4412 |
| [Suppes] p. 29 | Theorem 37 | difin0 4405 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4403 |
| [Suppes] p. 29 | Theorem 39 | difundi 4211 |
| [Suppes] p. 29 | Theorem 40 | difindi 4213 |
| [Suppes] p. 30 | Theorem 41 | nalset 5231 |
| [Suppes] p. 39 | Theorem 61 | uniss 4845 |
| [Suppes] p. 39 | Theorem 65 | uniop 5423 |
| [Suppes] p. 41 | Theorem 70 | intsn 4915 |
| [Suppes] p. 42 | Theorem 71 | intpr 4911 intprg 4910 |
| [Suppes] p. 42 | Theorem 73 | op1stb 5380 |
| [Suppes] p. 42 | Theorem 78 | intun 4909 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4960 dfiun2g 4958 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4961 |
| [Suppes] p. 47 | Theorem 86 | elpw 4535 elpw2 5263 elpw2g 5262 elpwg 4534 elpwgdedVD 42418 |
| [Suppes] p. 47 | Theorem 87 | pwid 4555 |
| [Suppes] p. 47 | Theorem 89 | pw0 4743 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4744 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5595 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5731 xpindir 5732 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5646 xpundir 5647 |
| [Suppes] p. 54 | Theorem 105 | elirrv 9284 |
| [Suppes] p. 58 | Theorem 2 | relss 5682 |
| [Suppes] p. 59 | Theorem 4 | eldm 5798 eldm2 5799 eldm2g 5797 eldmg 5796 |
| [Suppes] p. 59 | Definition 3 | df-dm 5590 |
| [Suppes] p. 60 | Theorem 6 | dmin 5809 |
| [Suppes] p. 60 | Theorem 8 | rnun 6038 |
| [Suppes] p. 60 | Theorem 9 | rnin 6039 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5786 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5780 brcnvg 5777 |
| [Suppes] p. 62 | Equation 5 | elcnv 5774 elcnv2 5775 |
| [Suppes] p. 62 | Theorem 12 | relcnv 6001 |
| [Suppes] p. 62 | Theorem 15 | cnvin 6037 |
| [Suppes] p. 62 | Theorem 16 | cnvun 6035 |
| [Suppes] p. 63 | Definition | dftrrels2 36615 |
| [Suppes] p. 63 | Theorem 20 | co02 6153 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5869 |
| [Suppes] p. 63 | Definition 7 | df-co 5589 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5783 |
| [Suppes] p. 64 | Theorem 27 | coass 6158 |
| [Suppes] p. 65 | Theorem 31 | resundi 5894 |
| [Suppes] p. 65 | Theorem 34 | elima 5963 elima2 5964 elima3 5965 elimag 5962 |
| [Suppes] p. 65 | Theorem 35 | imaundi 6042 |
| [Suppes] p. 66 | Theorem 40 | dminss 6045 |
| [Suppes] p. 66 | Theorem 41 | imainss 6046 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 6049 |
| [Suppes] p. 81 | Definition 34 | dfec2 8460 |
| [Suppes] p. 82 | Theorem 72 | elec 8501 elecALTV 36331 elecg 8500 |
| [Suppes] p. 82 | Theorem 73 | eqvrelth 36650 erth 8506 erth2 8507 |
| [Suppes] p. 83 | Theorem 74 | eqvreldisj 36653 erdisj 8509 |
| [Suppes] p. 89 | Theorem 96 | map0b 8630 |
| [Suppes] p. 89 | Theorem 97 | map0 8634 map0g 8631 |
| [Suppes] p. 89 | Theorem 98 | mapsn 8635 mapsnd 8633 |
| [Suppes] p. 89 | Theorem 99 | mapss 8636 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 9754 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 9753 |
| [Suppes] p. 92 | Theorem 1 | enref 8729 enrefg 8728 |
| [Suppes] p. 92 | Theorem 2 | ensym 8745 ensymb 8744 ensymi 8746 |
| [Suppes] p. 92 | Theorem 3 | entr 8748 |
| [Suppes] p. 92 | Theorem 4 | unen 8791 |
| [Suppes] p. 94 | Theorem 15 | endom 8723 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8742 |
| [Suppes] p. 94 | Theorem 17 | domtr 8749 |
| [Suppes] p. 95 | Theorem 18 | sbth 8834 |
| [Suppes] p. 97 | Theorem 23 | canth2 8867 canth2g 8868 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8838 df-sdom 8695 dfsdom2 8837 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8851 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8840 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8839 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8849 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 8726 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8852 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8847 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8776 fundmeng 8777 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8811 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8848 |
| [Suppes] p. 104 | Theorem 37 | fofi 9034 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8924 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8924 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 10237 |
| [Suppes] p. 130 | Definition 3 | df-tr 5187 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 7607 |
| [Suppes] p. 134 | Definition 6 | df-suc 6257 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7723 finds 7719 finds1 7722 finds2 7721 |
| [Suppes] p. 151 | Theorem 42 | isfinite 9339 isfinite2 9001 isfiniteg 9003 unbnn 8999 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 10604 df-ltpq 10596 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7684 tfinds 7681 tfinds2 7685 |
| [Suppes] p. 209 | Theorem 18 | oaord1 8345 |
| [Suppes] p. 209 | Theorem 21 | oaword2 8347 |
| [Suppes] p. 211 | Theorem 25 | oaass 8355 |
| [Suppes] p. 225 | Definition 8 | iscard2 9664 |
| [Suppes] p. 227 | Theorem 56 | ondomon 10249 |
| [Suppes] p. 228 | Theorem 59 | harcard 9666 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 9752 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 6301 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 7620 onminsb 7621 |
| [Suppes] p. 229 | Theorem 64 | alephval2 10258 |
| [Suppes] p. 229 | Theorem 65 | alephcard 9756 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 9763 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 9757 |
| [Suppes] p. 229 | Definition 12 | df-aleph 9628 |
| [Suppes] p. 242 | Theorem 6 | weth 10181 |
| [Suppes] p. 242 | Theorem 8 | entric 10243 |
| [Suppes] p. 242 | Theorem 9 | carden 10237 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2710 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2731 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2818 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2733 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2762 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 7259 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3711 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 5339 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4582 elpr2 4584 elpr2g 4583 elprg 4580 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4574 elsn2 4598 elsn2g 4597 elsng 4573 velsn 4575 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 5376 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4569 sneqr 4769 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4578 dfsn2 4572 dfsn2ALT 4579 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 7572 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 5385 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 5373 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 5358 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 7574 unexg 7577 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4623 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4838 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3891 df-un 3889 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4855 uniprg 4854 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 5295 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4622 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 6320 elsucg 6318 sstr2 3925 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 4084 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 4132 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 4097 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 4151 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 4205 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 4206 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3903 dfss2 3904 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4533 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 4112 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3901 sseqin2 4147 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3940 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 4160 inss2 4161 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 3980 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4848 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 5359 sspwimp 42419 sspwimpALT 42426 sspwimpALT2 42429 sspwimpcf 42421 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 5366 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 5204 |
| [TakeutiZaring] p. 20 | Definition | df-rab 3073 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 5225 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3887 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 4257 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 4302 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 4278 n0f 4274 neq0 4277 neq0f 4273 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 9283 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 9420 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 9422 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3425 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 5233 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 4328 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 5239 ssexg 5241 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 5235 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 9290 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 9285 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 4295 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 4062 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 4222 undif3VD 42383 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 4063 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 4070 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 3069 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 3070 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 7581 xpexg 7578 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5587 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 6489 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6664 fun11 6492 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 6430 svrelfun 6490 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5785 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5787 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5592 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5593 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5589 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 6086 dfrel2 6081 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5596 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5710 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5717 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5730 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5909 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5886 opelresi 5888 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5902 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5905 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5910 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 6460 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 6137 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 6458 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6666 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2612 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 28664 df-fv 6426 fv3 6774 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7746 cnvexg 7745 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7732 dmexg 7724 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7733 rnexg 7725 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 41953 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7741 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6769 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 44545 tz6.12-1-afv2 44612 tz6.12-1 6778 tz6.12-afv 44544 tz6.12-afv2 44611 tz6.12 6779 tz6.12c-afv2 44613 tz6.12c 6781 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2-afv2 44608 tz6.12-2 6745 tz6.12i-afv2 44614 tz6.12i 6782 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 6421 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 6422 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 6424 wfo 6416 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 6423 wf1 6415 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 6425 wf1o 6417 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6891 eqfnfv2 6892 eqfnfv2f 6895 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6848 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 7075 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 7073 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 6505 funimaexg 6504 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 5072 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5495 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5544 dffr3 5996 eliniseg 5991 iniseg 5994 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5486 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5558 fr3nr 7600 frirr 5557 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5535 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 7602 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5547 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5567 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 6235 tz6.26i 6237 wefrc 5574 wereu2 5577 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 6238 wfii 6240 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 6427 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 7180 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 7181 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 7187 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 7188 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 7189 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 7193 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 7200 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 7202 |
| [TakeutiZaring] p. 35 | Notation | wtr 5186 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 41954 tz7.2 5564 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 5190 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 6264 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 6272 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 6273 ordelordALT 42038 ordelordALTVD 42368 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 6279 ordelssne 6278 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 6277 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 6281 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 7609 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 7610 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 6255 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 6283 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 42050 ordon 7604 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 7605 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7675 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 6298 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 5188 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 7619 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7653 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 6352 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 6351 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 7606 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4869 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 6257 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 6328 sucidg 6329 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7635 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 6342 ordnbtwn 6341 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7650 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 6256 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7702 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7707 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7663 ordelsuc 7642 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7644 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7673 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7689 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7710 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7711 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7712 |
| [TakeutiZaring] p. 43 | Remark | omon 7699 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 9322 omex 9330 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7697 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7717 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7713 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7714 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7692 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4891 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 5203 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4892 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 5255 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7622 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 6300 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4878 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 9347 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 7617 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 8178 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 8199 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 8200 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 8201 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 8208 tz7.44-2 8209 tz7.44-3 8210 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 8169 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 8164 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 8148 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 8247 tz7.49c 8248 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 8245 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 8244 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 8246 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2658 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 9697 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 9698 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 8325 oasuc 8317 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7682 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 8328 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 8309 oa0r 8331 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 8329 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 8342 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 8413 nnaordi 8412 oaord 8341 oaordi 8340 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4976 uniss2 4872 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 8344 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 8349 oawordex 8351 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 8405 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 8439 |
| [TakeutiZaring] p. 60 | Remark | oancom 9338 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 8354 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 8410 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 8346 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0x 8312 omlim 8326 omsuc 8319 |
| [TakeutiZaring] p. 62 | Definition 8.15(a) | om0 8310 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 8407 nnmcl 8406 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 8426 nnmordi 8425 omord 8362 omordi 8360 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 8363 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 8430 omwordri 8366 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 8332 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 8336 om1r 8337 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 8369 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 8371 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 8372 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 8373 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 8374 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 8402 oe0 8315 oelim 8327 oesuc 8320 onesuc 8323 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 8313 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 8380 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 8381 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 8314 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 8339 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 8382 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 8388 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 8386 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 8387 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 8391 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 8393 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 9416 tz9.1 9417 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 9452 r10 9456 r1lim 9460 r1limg 9459 r1suc 9458 r1sucg 9457 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 9468 r1ord2 9469 r1ordg 9466 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 9478 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 9503 tz9.13 9479 tz9.13g 9480 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 9453 rankval 9504 rankvalb 9485 rankvalg 9505 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 9527 rankelb 9512 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 9541 rankval3 9528 rankval3b 9514 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 9517 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 9483 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 9522 rankr1c 9509 rankr1g 9520 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 9523 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 9537 rankssb 9536 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 9530 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 9529 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 10161 dfac3 9807 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 9716 numth 10158 numth2 10157 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 10232 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 10233 cardid2 9641 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 9648 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 10237 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 9647 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 9632 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 9653 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 9645 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8887 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8759 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8892 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8815 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 9651 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 9784 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8897 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 8941 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 9785 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8902 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 9774 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 9752 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 9660 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9903 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 9017 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 8696 isfi 8720 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 8942 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 10220 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8808 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 10212 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | djuxpdom 9871 unxpdom 8957 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 9662 cardsdomelir 9661 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 8959 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 9700 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 8576 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 10248 infxpidm2 9703 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infdju 9894 infxp 9901 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8820 pw2f1o 8818 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8880 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 10173 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 10168 ac6s5 10177 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 10229 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 10230 uniimadomf 10231 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 9960 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 9955 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 9940 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 9937 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 9943 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 9950 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 9959 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 10268 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 9938 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 9962 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 9783 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 9782 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 9794 alephfp2 9795 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 10385 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 9798 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 10255 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 10269 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 10270 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 36823 |
| [Tarski] p. 67 | Scheme B5 | sp 2182 |
| [Tarski] p. 68 | Lemma 6 | avril1 28727 equid 2020 |
| [Tarski] p. 69 | Lemma 7 | equcomi 2025 |
| [Tarski] p. 70 | Lemma 14 | spim 2388 spime 2390 spimew 1980 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2177 ax-c15 36829 ax12i 1975 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2093 |
| [Tarski] p. 75 | Axiom B7 | ax6v 1977 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1918 ax5ALT 36847 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 2016 ax-8 2114 ax-9 2122 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 26728 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 26729 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 26731 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 26731 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 26732 |
| [Truss] p. 114 | Theorem 5.18 | ruc 15879 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 35742 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 35744 |
| [Weierstrass] p. 272 | Definition | df-mdet 21641 mdetuni 21678 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 904 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 868 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 869 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 920 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 968 |
| [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 35542 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 41289 imim2 58 wl-luk-imim2 35537 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | adh-minimp-imim1 44393 imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 897 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2665 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 903 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-luk-id 35540 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 895 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 144 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 898 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 132 notnotrALT2 42428 wl-luk-notnotr 35541 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 148 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 41319 axfrege28 41318 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 867 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 925 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 123 wl-luk-pm2.21 35534 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 124 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 890 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 940 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-labels 28665 pm2.27 42 wl-luk-pm2.27 35532 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 923 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 924 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 970 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 971 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 969 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1090 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 907 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 908 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 943 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 882 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 883 |
| [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 884 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 885 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 886 |
| [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 851 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 852 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 889 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 891 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 195 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 900 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 941 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 942 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 196 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 892 pm2.67 893 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 179 pm2.521g 177 pm2.521g2 178 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 899 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 973 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 901 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 206 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 974 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 975 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 934 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 932 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 972 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 976 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 933 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 109 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 992 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 473 pm3.2im 163 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 993 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 994 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 995 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 996 |
| [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 961 pm3.44 960 |
| [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 964 |
| [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 833 |
| [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 905 pm4.25 906 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 464 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 1008 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 870 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 472 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 922 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 635 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 918 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 638 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 977 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1091 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 1006 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1054 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 1023 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 997 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 999 pm4.45 998 pm4.45im 828 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 983 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 853 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 549 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 982 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 985 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 986 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 987 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 988 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 984 pm4.56 989 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 990 pm4.57 991 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 408 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 856 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 401 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 849 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 409 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 850 |
| [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 950 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 531 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 937 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 521 pm4.76 522 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 962 pm4.77 963 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 935 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 1004 |
| [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 1024 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 1025 |
| [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 843 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 824 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 945 pm5.11g 944 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 946 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 948 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 947 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 1013 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 1014 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 1012 |
| [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 825 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 1015 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 1050 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 1051 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 902 |
| [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 1002 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 954 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 831 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 577 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 836 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 826 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 834 |
| [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 1005 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 1018 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 949 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 1001 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 1019 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 1020 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 1028 |
| [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 1029 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 41857 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 41858 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1878 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 41859 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 41860 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 41861 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1901 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 41862 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 41863 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 41864 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 41865 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 41866 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 41868 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 41869 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 41870 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 41867 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2098 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 41873 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 41874 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2078 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2163 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1836 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1837 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 41875 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 41876 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 41877 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 41878 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 41880 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 41879 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1895 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 41882 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 41883 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 41881 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1835 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 41884 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 41885 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1853 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 41886 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2349 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 1868 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 41891 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 41887 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 41888 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 41889 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 41890 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 41895 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 41892 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 41893 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 41894 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 41896 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2570 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 41906 pm13.13b 41907 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 41908 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 3025 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 3026 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3591 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 41914 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 41915 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 41909 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 42053 pm13.193 41910 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 41911 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 41912 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 41913 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 41920 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 41919 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 41918 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3781 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 41921 pm14.122b 41922 pm14.122c 41923 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 41924 pm14.123b 41925 pm14.123c 41926 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 41928 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 41927 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 41929 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 6399 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 41930 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 6400 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 41931 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 41933 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2636 eupickbi 2639 sbaniota 41934 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 41932 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 2585 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 41936 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 28664 df-fv 6426 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 9689 pm54.43lem 9688 |
| [Young] p. 141 | Definition of operator ordering | leop2 30386 |
| [Young] p. 142 | Example 12.2(i) | 0leop 30392 idleop 30393 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 40558 |
| [vandenDries] p. 43 | Theorem 62 | pellex 40565 pellexlem1 40559 |