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 16931 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 16931 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 17328 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 16951 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 16974 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 17043 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 17031 invisoinvl 17052 |
| [Adamek] p. 28 | Example 3.13 | idinv 17051 idiso 17050 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 17036 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 17010 df-iso 17011 dfiso2 17034 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 17017 |
| [Adamek] p. 29 | Remark 3.16 | cicer 17068 |
| [Adamek] p. 29 | Definition 3.15 | cic 17061 df-cic 17058 |
| [Adamek] p. 29 | Definition 3.17 | df-func 17120 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 17032 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 17033 isoco 17039 |
| [Adamek] p. 30 | Remark 3.19 | df-func 17120 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 17143 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 17136 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 17150 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 17359 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 17409 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 17167 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 17166 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 17409 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 17191 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 17197 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 17196 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 17394 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 17394 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 17137 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 17347 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 17185 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 17184 |
| [Adamek] p. 40 | Remark 3.48 | catccat 17356 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 17347 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 17100 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 17101 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 17112 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 17074 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 17200 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 17205 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 17226 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 17230 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 17206 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 17232 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 17243 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 44693 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 17244 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 17264 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 17268 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 17245 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 44696 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 17271 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 17009 |
| [Adamek] p. 185 | Section 10.67 | updjud 9347 |
| [Adamek] p. 478 | Item Rng | df-ringc 44629 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 44962 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 44984 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 13914 df-pfx 14024 df-substr 13994 df-word 13858 lencl 13876 wrd0 13882 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 23314 df-nmoo 28528 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 29936 hmopidmchi 29934 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 29984 pjcmul2i 29985 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 29701 unoplin 29703 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 29702 unopadj2 29721 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 29796 lnopunii 29795 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 29869 |
| [Apostol] p. 18 | Theorem I.1 | addcan 10813 addcan2d 10833 addcan2i 10823 addcand 10832 addcani 10822 |
| [Apostol] p. 18 | Theorem I.2 | negeu 10865 |
| [Apostol] p. 18 | Theorem I.3 | negsub 10923 negsubd 10992 negsubi 10953 |
| [Apostol] p. 18 | Theorem I.4 | negneg 10925 negnegd 10977 negnegi 10945 |
| [Apostol] p. 18 | Theorem I.5 | subdi 11062 subdid 11085 subdii 11078 subdir 11063 subdird 11086 subdiri 11079 |
| [Apostol] p. 18 | Theorem I.6 | mul01 10808 mul01d 10828 mul01i 10819 mul02 10807 mul02d 10827 mul02i 10818 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 11266 mulcan2d 11263 mulcand 11262 mulcani 11268 |
| [Apostol] p. 18 | Theorem I.8 | receu 11274 xreceu 30624 |
| [Apostol] p. 18 | Theorem I.9 | divrec 11303 divrecd 11408 divreci 11374 divreczi 11367 |
| [Apostol] p. 18 | Theorem I.10 | recrec 11326 recreci 11361 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 11269 mul0ord 11279 mul0ori 11277 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 11068 mul2negd 11084 mul2negi 11077 mulneg1 11065 mulneg1d 11082 mulneg1i 11075 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 11344 divadddivd 11449 divadddivi 11391 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 11329 divmuldivd 11446 divmuldivi 11389 rdivmuldivd 30913 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 11330 divdivdivd 11452 divdivdivi 11392 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 12399 rpaddcld 12434 rpmulcl 12400 rpmulcld 12435 |
| [Apostol] p. 20 | Axiom 8 | rpneg 12409 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 12412 |
| [Apostol] p. 20 | Theorem I.17 | lttri 10755 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 11222 ltadd1dd 11240 ltadd1i 11183 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 11479 ltmul1a 11478 ltmul1i 11547 ltmul1ii 11557 ltmul2 11480 ltmul2d 12461 ltmul2dd 12475 ltmul2i 11550 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 11149 msqgt0d 11196 msqgt0i 11166 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 11151 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 11135 lt0neg1d 11198 ltneg 11129 ltnegd 11207 ltnegi 11173 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 11114 lt2addd 11252 lt2addi 11191 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 12378 |
| [Apostol] p. 21 | Exercise 4 | recgt0 11475 recgt0d 11563 recgt0i 11534 recgt0ii 11535 |
| [Apostol] p. 22 | Definition of integers | df-z 11970 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11639 |
| [Apostol] p. 22 | Definition of rationals | df-q 12337 |
| [Apostol] p. 24 | Theorem I.26 | supeu 8902 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 11881 |
| [Apostol] p. 26 | Theorem I.29 | arch 11882 |
| [Apostol] p. 28 | Exercise 2 | btwnz 12072 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 11883 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 12335 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 12334 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12580 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 15680 zneo 12053 zneoALTV 44187 |
| [Apostol] p. 29 | Theorem I.35 | cxpsqrtth 25320 msqsqrtd 14792 resqrtth 14607 sqrtth 14716 sqrtthi 14722 sqsqrtd 14791 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11628 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 12301 |
| [Apostol] p. 361 | Remark | crreczi 13585 |
| [Apostol] p. 363 | Remark | absgt0i 14751 |
| [Apostol] p. 363 | Example | abssubd 14805 abssubi 14755 |
| [ApostolNT] p. 7 | Remark | fmtno0 44057 fmtno1 44058 fmtno2 44067 fmtno3 44068 fmtno4 44069 fmtno5fac 44099 fmtnofz04prm 44094 |
| [ApostolNT] p. 7 | Definition | df-fmtno 44045 |
| [ApostolNT] p. 8 | Definition | df-ppi 25685 |
| [ApostolNT] p. 14 | Definition | df-dvds 15600 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 15615 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 15638 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15634 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15628 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15630 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 15616 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 15617 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15622 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 15653 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 15655 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 15657 |
| [ApostolNT] p. 15 | Definition | df-gcd 15834 dfgcd2 15884 |
| [ApostolNT] p. 16 | Definition | isprm2 16016 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 15987 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 16241 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 15852 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 15885 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 15887 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 15866 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 15858 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 16045 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 16047 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 16254 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 16248 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 15744 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 15921 |
| [ApostolNT] p. 24 | Definition | df-mu 25686 |
| [ApostolNT] p. 25 | Definition | df-phi 16093 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 25776 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 16117 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 16103 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 16107 |
| [ApostolNT] p. 32 | Definition | df-vma 25683 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 25778 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 25800 |
| [ApostolNT] p. 38 | Remark | df-sgm 25687 |
| [ApostolNT] p. 38 | Definition | df-sgm 25687 |
| [ApostolNT] p. 75 | Definition | df-chp 25684 df-cht 25682 |
| [ApostolNT] p. 104 | Definition | congr 15998 |
| [ApostolNT] p. 106 | Remark | dvdsval3 15603 |
| [ApostolNT] p. 106 | Definition | moddvds 15610 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 15687 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 15688 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 13251 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 13288 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 13595 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15633 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 16001 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 16400 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 16003 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 16110 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 16128 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 16111 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 25657 |
| [ApostolNT] p. 179 | Definition | df-lgs 25879 lgsprme0 25923 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 25924 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 25900 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 25915 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 25972 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 25991 2lgsoddprm 26000 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 25958 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 25967 |
| [ApostolNT] p. 188 | Definition | df-lgs 25879 lgs1 25925 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 25916 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 25918 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 25926 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 25927 |
| [Baer] p. 40 | Property (b) | mapdord 38934 |
| [Baer] p. 40 | Property (c) | mapd11 38935 |
| [Baer] p. 40 | Property (e) | mapdin 38958 mapdlsm 38960 |
| [Baer] p. 40 | Property (f) | mapd0 38961 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 38921 mapd1o 38944 |
| [Baer] p. 41 | Property (g) | mapdat 38963 |
| [Baer] p. 44 | Part (1) | mapdpg 39002 |
| [Baer] p. 45 | Part (2) | hdmap1eq 39097 mapdheq 39024 mapdheq2 39025 mapdheq2biN 39026 |
| [Baer] p. 45 | Part (3) | baerlem3 39009 |
| [Baer] p. 46 | Part (4) | mapdheq4 39028 mapdheq4lem 39027 |
| [Baer] p. 46 | Part (5) | baerlem5a 39010 baerlem5abmN 39014 baerlem5amN 39012 baerlem5b 39011 baerlem5bmN 39013 |
| [Baer] p. 47 | Part (6) | hdmap1l6 39117 hdmap1l6a 39105 hdmap1l6e 39110 hdmap1l6f 39111 hdmap1l6g 39112 hdmap1l6lem1 39103 hdmap1l6lem2 39104 mapdh6N 39043 mapdh6aN 39031 mapdh6eN 39036 mapdh6fN 39037 mapdh6gN 39038 mapdh6lem1N 39029 mapdh6lem2N 39030 |
| [Baer] p. 48 | Part 9 | hdmapval 39124 |
| [Baer] p. 48 | Part 10 | hdmap10 39136 |
| [Baer] p. 48 | Part 11 | hdmapadd 39139 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 39113 mapdh6hN 39039 |
| [Baer] p. 48 | Part (7) | mapdh75cN 39049 mapdh75d 39050 mapdh75e 39048 mapdh75fN 39051 mapdh7cN 39045 mapdh7dN 39046 mapdh7eN 39044 mapdh7fN 39047 |
| [Baer] p. 48 | Part (8) | mapdh8 39084 mapdh8a 39071 mapdh8aa 39072 mapdh8ab 39073 mapdh8ac 39074 mapdh8ad 39075 mapdh8b 39076 mapdh8c 39077 mapdh8d 39079 mapdh8d0N 39078 mapdh8e 39080 mapdh8g 39081 mapdh8i 39082 mapdh8j 39083 |
| [Baer] p. 48 | Part (9) | mapdh9a 39085 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 39065 |
| [Baer] p. 49 | Part 12 | hdmap11 39144 hdmapeq0 39140 hdmapf1oN 39161 hdmapneg 39142 hdmaprnN 39160 hdmaprnlem1N 39145 hdmaprnlem3N 39146 hdmaprnlem3uN 39147 hdmaprnlem4N 39149 hdmaprnlem6N 39150 hdmaprnlem7N 39151 hdmaprnlem8N 39152 hdmaprnlem9N 39153 hdmapsub 39143 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 39164 hdmap14lem10 39173 hdmap14lem1a 39162 hdmap14lem2N 39165 hdmap14lem2a 39163 hdmap14lem3 39166 hdmap14lem8 39171 hdmap14lem9 39172 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 39174 hdmap14lem12 39175 hdmap14lem13 39176 hdmap14lem14 39177 hdmap14lem15 39178 hgmapval 39183 |
| [Baer] p. 50 | Part 15 | hgmapadd 39190 hgmapmul 39191 hgmaprnlem2N 39193 hgmapvs 39187 |
| [Baer] p. 50 | Part 16 | hgmaprnN 39197 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 39213 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 39214 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 39215 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 39216 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 39218 hgmapvv 39222 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 39217 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 39219 |
| [Baer] p. 111 | Line 15 | hdmapg 39226 hdmapglem7 39225 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 25321 2irrexpqALT 25386 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2629 |
| [BellMachover] p. 460 | Notation | df-mo 2598 |
| [BellMachover] p. 460 | Definition | mo3 2623 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2770 |
| [BellMachover] p. 462 | Theorem 1.1 | axextmo 2774 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 5160 |
| [BellMachover] p. 463 | Scheme Sep | ax-sep 5167 |
| [BellMachover] p. 463 | Theorem 1.3(ii) | bj-bm1.3ii 34481 bm1.3ii 5170 |
| [BellMachover] p. 466 | Problem | axpow2 5233 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 5234 |
| [BellMachover] p. 466 | Axiom Union | axun2 7443 |
| [BellMachover] p. 468 | Definition | df-ord 6162 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 6177 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 6184 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 6179 |
| [BellMachover] p. 471 | Definition of N | df-om 7561 |
| [BellMachover] p. 471 | Problem 2.5(ii) | uniordint 7501 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 6164 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 9089 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7575 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 9177 |
| [BellMachover] p. 478 | Definition | rankval2 9231 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 9195 r1ord3g 9192 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 9043 |
| [BellMachover] p. 488 | Axiom AC | ac5 9888 dfac4 9533 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 9521 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 36615 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 30136 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 30178 chirredi 30177 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 30166 |
| [Beran] p. 3 | Definition of join | sshjval3 29137 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 29399 cmcm2i 29376 cmcm2ii 29381 cmt2N 36546 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 29400 lecmi 29385 lecmii 29386 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 29374 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 29403 cm2ji 29408 cm2mi 29409 |
| [Beran] p. 95 | Definition | df-sh 28990 issh2 28992 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 28869 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 28882 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 28873 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 29611 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 29613 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 29612 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 29614 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 28865 his1i 28883 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 28866 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 28867 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 28868 |
| [Beran] p. 96 | Definition of norm | df-hnorm 28751 dfhnorm2 28905 normval 28907 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 28967 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 28756 |
| [Beran] p. 96 | Definition of complete subspace | isch3 29024 |
| [Beran] p. 96 | Definition of converge | df-hlim 28755 hlimi 28971 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 28916 norm-i 28912 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 28920 norm-ii 28921 normlem0 28892 normlem1 28893 normlem2 28894 normlem3 28895 normlem4 28896 normlem5 28897 normlem6 28898 normlem7 28899 normlem7tALT 28902 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 28922 norm-iii 28923 |
| [Beran] p. 98 | Remark 3.4 | bcs 28964 bcsiALT 28962 bcsiHIL 28963 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 28904 normpar 28938 normpari 28937 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 28929 normpyth 28928 normpythi 28925 |
| [Beran] p. 99 | Remark | lnfn0 29830 lnfn0i 29825 lnop0 29749 lnop0i 29753 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 29809 nmcfnex 29836 nmcfnexi 29834 nmcopex 29812 nmcopexi 29810 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 29837 nmcfnlbi 29835 nmcoplb 29813 nmcoplbi 29811 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 29839 lnfnconi 29838 lnopcon 29818 lnopconi 29817 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 28939 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 28936 norm3adifii 28931 norm3dif 28933 norm3difi 28930 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 29084 pjhth 29176 pjhtheu 29177 pjpjhth 29208 pjpjhthi 29209 pjth 24043 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 29189 ococi 29188 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 29844 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 29845 riesz4 29847 riesz4i 29846 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 29862 cnlnadjeu 29861 cnlnadjeui 29860 cnlnadji 29859 cnlnadjlem1 29850 nmopadjlei 29871 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 29874 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 29873 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 29875 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 29719 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 29885 nmopcoadji 29884 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 29876 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 29886 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 29883 pjadj2coi 29987 pjadjcoi 29944 |
| [Beran] p. 107 | Definition | df-ch 29004 isch2 29006 |
| [Beran] p. 107 | Remark 3.12 | choccl 29089 isch3 29024 occl 29087 ocsh 29066 shoccl 29088 shocsh 29067 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 29191 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 29115 |
| [Beran] p. 109 | Property (i) | pjadj2 29970 pjadj3 29971 pjadji 29468 pjadjii 29457 |
| [Beran] p. 109 | Property (ii) | pjidmco 29964 pjidmcoi 29960 pjidmi 29456 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 29956 |
| [Beran] p. 111 | Remark | ho0val 29533 pjch1 29453 |
| [Beran] p. 111 | Definition | df-hfmul 29517 df-hfsum 29516 df-hodif 29515 df-homul 29514 df-hosum 29513 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 29454 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 29477 pjchi 29215 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 29222 pjoc2i 29221 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 29463 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 29948 pjssmii 29464 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 29947 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 29946 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 29951 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 29949 pjssge0ii 29465 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 29950 pjdifnormii 29466 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1778 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1776 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1779 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1774 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 31660 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 31668 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 31666 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 31670 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 31690 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 31721 df-sitm 31699 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 31721 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 31698 |
| [Bollobas] p. 1 | Section I.1 | df-edg 26841 isuhgrop 26863 isusgrop 26955 isuspgrop 26954 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 27058 uhgrspan1 27093 uhgrspansubgr 27081 |
| [Bollobas] p. 3 | Definition | isomuspgr 44352 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 27244 df-cusgr 27202 df-nbgr 27123 fusgrmaxsize 27254 |
| [Bollobas] p. 4 | Definition | df-upwlks 44362 df-wlks 27389 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 27340 finsumvtxdgeven 27342 fusgr1th 27341 fusgrvtxdgonume 27344 vtxdgoddnumeven 27343 |
| [Bollobas] p. 5 | Notation | df-pths 27505 |
| [Bollobas] p. 5 | Definition | df-crcts 27575 df-cycls 27576 df-trls 27482 df-wlkson 27390 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 26852 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 44460 df-cllaw 44446 df-mgm 17844 df-mgm2 44479 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 44461 df-asslaw 44448 df-sgrp 17893 df-sgrp2 44481 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 44480 df-comlaw 44447 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 17904 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 19292 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 44499 |
| [BourbakiEns] p. | Proposition 8 | fcof1 7021 fcofo 7022 |
| [BourbakiTop1] p. | Remark | xnegmnf 12591 xnegpnf 12590 |
| [BourbakiTop1] p. | Remark | rexneg 12592 |
| [BourbakiTop1] p. | Remark 3 | ust0 22825 ustfilxp 22818 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 22695 |
| [BourbakiTop1] p. | Criterion | ishmeo 22364 |
| [BourbakiTop1] p. | Example 1 | cstucnd 22890 iducn 22889 snfil 22469 |
| [BourbakiTop1] p. | Example 2 | neifil 22485 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 22672 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 22910 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 31310 |
| [BourbakiTop1] p. | Paragraph 3 | infil 22468 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 22882 df-ust 22806 filintn0 22466 filn0 22467 istgp 22682 ucnprima 22888 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 22893 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 22904 df-usp 22863 df-utop 22837 trust 22835 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 31209 |
| [BourbakiTop1] p. | Property V_i | ssnei2 21721 |
| [BourbakiTop1] p. | Theorem 1(d) | iscncl 21874 |
| [BourbakiTop1] p. | Condition F_I | ustssel 22811 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 22814 |
| [BourbakiTop1] p. | Property V_ii | innei 21730 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 21738 neissex 21732 |
| [BourbakiTop1] p. | Proposition 1 | neips 21718 neiss 21714 ucncn 22891 ustund 22827 ustuqtop 22852 |
| [BourbakiTop1] p. | Proposition 2 | cnpco 21872 neiptopreu 21738 utop2nei 22856 utop3cls 22857 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 22898 uspreg 22880 utopreg 22858 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 22296 imasncls 22297 imasnopn 22295 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 22605 |
| [BourbakiTop1] p. | Condition F_II | ustincl 22813 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 22815 |
| [BourbakiTop1] p. | Property V_iii | elnei 21716 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 22909 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 22812 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 22816 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 21992 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 22451 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 21499 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 31206 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 42704 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 42706 stoweid 42705 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 42643 stoweidlem10 42652 stoweidlem14 42656 stoweidlem15 42657 stoweidlem35 42677 stoweidlem36 42678 stoweidlem37 42679 stoweidlem38 42680 stoweidlem40 42682 stoweidlem41 42683 stoweidlem43 42685 stoweidlem44 42686 stoweidlem46 42688 stoweidlem5 42647 stoweidlem50 42692 stoweidlem52 42694 stoweidlem53 42695 stoweidlem55 42697 stoweidlem56 42698 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 42665 stoweidlem24 42666 stoweidlem27 42669 stoweidlem28 42670 stoweidlem30 42672 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 42676 stoweidlem59 42701 stoweidlem60 42702 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 42687 stoweidlem49 42691 stoweidlem7 42649 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 42673 stoweidlem39 42681 stoweidlem42 42684 stoweidlem48 42690 stoweidlem51 42693 stoweidlem54 42696 stoweidlem57 42699 stoweidlem58 42700 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 42667 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 42659 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 42653 stoweidlem13 42655 stoweidlem26 42668 stoweidlem61 42703 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 42660 |
| [Bruck] p. 1 | Section I.1 | df-clintop 44460 df-mgm 17844 df-mgm2 44479 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 17893 df-sgrp2 44481 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 18190 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 5111 |
| [Church] p. 129 | Section II.24 | df-ifp 1059 dfifp2 1060 |
| [Clemente] p. 10 | Definition IT | natded 28188 |
| [Clemente] p. 10 | Definition I` `m,n | natded 28188 |
| [Clemente] p. 11 | Definition E=>m,n | natded 28188 |
| [Clemente] p. 11 | Definition I=>m,n | natded 28188 |
| [Clemente] p. 11 | Definition E` `(1) | natded 28188 |
| [Clemente] p. 11 | Definition E` `(2) | natded 28188 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 28188 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 28188 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 28188 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 28188 |
| [Clemente] p. 14 | Proof 5.11 | natded 28188 |
| [Clemente] p. 14 | Definition E` `n | natded 28188 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 28190 ex-natded5.2 28189 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 28193 ex-natded5.3 28192 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 28195 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 28197 ex-natded5.7 28196 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 28199 ex-natded5.8 28198 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 28201 ex-natded5.13 28200 |
| [Clemente] p. 32 | Definition I` `n | natded 28188 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 28188 |
| [Clemente] p. 32 | Definition E` `n,t | natded 28188 |
| [Clemente] p. 32 | Definition I` `n,t | natded 28188 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 28202 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 28203 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 28205 ex-natded9.26 28204 |
| [Cohen] p. 301 | Remark | relogoprlem 25182 |
| [Cohen] p. 301 | Property 2 | relogmul 25183 relogmuld 25216 |
| [Cohen] p. 301 | Property 3 | relogdiv 25184 relogdivd 25217 |
| [Cohen] p. 301 | Property 4 | relogexp 25187 |
| [Cohen] p. 301 | Property 1a | log1 25177 |
| [Cohen] p. 301 | Property 1b | loge 25178 |
| [Cohen4] p. 348 | Observation | relogbcxpb 25373 |
| [Cohen4] p. 349 | Property | relogbf 25377 |
| [Cohen4] p. 352 | Definition | elogb 25356 |
| [Cohen4] p. 361 | Property 2 | relogbmul 25363 |
| [Cohen4] p. 361 | Property 3 | logbrec 25368 relogbdiv 25365 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 25361 |
| [Cohen4] p. 361 | Property 6 | relogbexp 25366 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 25354 |
| [Cohen4] p. 361 | Property 1(b) | logb1 25355 |
| [Cohen4] p. 367 | Property | logbchbase 25357 |
| [Cohen4] p. 377 | Property 2 | logblt 25370 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 31653 sxbrsigalem4 31655 |
| [Cohn] p. 81 | Section II.5 | acsdomd 17783 acsinfd 17782 acsinfdimd 17784 acsmap2d 17781 acsmapd 17780 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 31658 |
| [Connell] p. 57 | Definition | df-scmat 21096 df-scmatalt 44808 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 13224 |
| [Crawley] p. 1 | Definition of poset | df-poset 17548 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 36682 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 37486 dalaw 37182 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 39257 |
| [Crawley] p. 111 | Definition of set W | df-watsN 37286 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 37402 df-ldil 37400 isldil 37406 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 37401 df-trnN 37403 isltrn 37415 ltrnu 37417 |
| [Crawley] p. 112 | Lemma A | cdlema1N 37087 cdlema2N 37088 exatleN 36700 |
| [Crawley] p. 112 | Lemma B | 1cvrat 36772 cdlemb 37090 cdlemb2 37337 cdlemb3 37902 idltrn 37446 l1cvat 36351 lhpat 37339 lhpat2 37341 lshpat 36352 ltrnel 37435 ltrnmw 37447 |
| [Crawley] p. 112 | Lemma C | cdlemc1 37487 cdlemc2 37488 ltrnnidn 37470 trlat 37465 trljat1 37462 trljat2 37463 trljat3 37464 trlne 37481 trlnidat 37469 trlnle 37482 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 37287 |
| [Crawley] p. 113 | Lemma C | cdlemc 37493 cdlemc3 37489 cdlemc4 37490 |
| [Crawley] p. 113 | Lemma D | cdlemd 37503 cdlemd1 37494 cdlemd2 37495 cdlemd3 37496 cdlemd4 37497 cdlemd5 37498 cdlemd6 37499 cdlemd7 37500 cdlemd8 37501 cdlemd9 37502 cdleme31sde 37681 cdleme31se 37678 cdleme31se2 37679 cdleme31snd 37682 cdleme32a 37737 cdleme32b 37738 cdleme32c 37739 cdleme32d 37740 cdleme32e 37741 cdleme32f 37742 cdleme32fva 37733 cdleme32fva1 37734 cdleme32fvcl 37736 cdleme32le 37743 cdleme48fv 37795 cdleme4gfv 37803 cdleme50eq 37837 cdleme50f 37838 cdleme50f1 37839 cdleme50f1o 37842 cdleme50laut 37843 cdleme50ldil 37844 cdleme50lebi 37836 cdleme50rn 37841 cdleme50rnlem 37840 cdlemeg49le 37807 cdlemeg49lebilem 37835 |
| [Crawley] p. 113 | Lemma E | cdleme 37856 cdleme00a 37505 cdleme01N 37517 cdleme02N 37518 cdleme0a 37507 cdleme0aa 37506 cdleme0b 37508 cdleme0c 37509 cdleme0cp 37510 cdleme0cq 37511 cdleme0dN 37512 cdleme0e 37513 cdleme0ex1N 37519 cdleme0ex2N 37520 cdleme0fN 37514 cdleme0gN 37515 cdleme0moN 37521 cdleme1 37523 cdleme10 37550 cdleme10tN 37554 cdleme11 37566 cdleme11a 37556 cdleme11c 37557 cdleme11dN 37558 cdleme11e 37559 cdleme11fN 37560 cdleme11g 37561 cdleme11h 37562 cdleme11j 37563 cdleme11k 37564 cdleme11l 37565 cdleme12 37567 cdleme13 37568 cdleme14 37569 cdleme15 37574 cdleme15a 37570 cdleme15b 37571 cdleme15c 37572 cdleme15d 37573 cdleme16 37581 cdleme16aN 37555 cdleme16b 37575 cdleme16c 37576 cdleme16d 37577 cdleme16e 37578 cdleme16f 37579 cdleme16g 37580 cdleme19a 37599 cdleme19b 37600 cdleme19c 37601 cdleme19d 37602 cdleme19e 37603 cdleme19f 37604 cdleme1b 37522 cdleme2 37524 cdleme20aN 37605 cdleme20bN 37606 cdleme20c 37607 cdleme20d 37608 cdleme20e 37609 cdleme20f 37610 cdleme20g 37611 cdleme20h 37612 cdleme20i 37613 cdleme20j 37614 cdleme20k 37615 cdleme20l 37618 cdleme20l1 37616 cdleme20l2 37617 cdleme20m 37619 cdleme20y 37598 cdleme20zN 37597 cdleme21 37633 cdleme21d 37626 cdleme21e 37627 cdleme22a 37636 cdleme22aa 37635 cdleme22b 37637 cdleme22cN 37638 cdleme22d 37639 cdleme22e 37640 cdleme22eALTN 37641 cdleme22f 37642 cdleme22f2 37643 cdleme22g 37644 cdleme23a 37645 cdleme23b 37646 cdleme23c 37647 cdleme26e 37655 cdleme26eALTN 37657 cdleme26ee 37656 cdleme26f 37659 cdleme26f2 37661 cdleme26f2ALTN 37660 cdleme26fALTN 37658 cdleme27N 37665 cdleme27a 37663 cdleme27cl 37662 cdleme28c 37668 cdleme3 37533 cdleme30a 37674 cdleme31fv 37686 cdleme31fv1 37687 cdleme31fv1s 37688 cdleme31fv2 37689 cdleme31id 37690 cdleme31sc 37680 cdleme31sdnN 37683 cdleme31sn 37676 cdleme31sn1 37677 cdleme31sn1c 37684 cdleme31sn2 37685 cdleme31so 37675 cdleme35a 37744 cdleme35b 37746 cdleme35c 37747 cdleme35d 37748 cdleme35e 37749 cdleme35f 37750 cdleme35fnpq 37745 cdleme35g 37751 cdleme35h 37752 cdleme35h2 37753 cdleme35sn2aw 37754 cdleme35sn3a 37755 cdleme36a 37756 cdleme36m 37757 cdleme37m 37758 cdleme38m 37759 cdleme38n 37760 cdleme39a 37761 cdleme39n 37762 cdleme3b 37525 cdleme3c 37526 cdleme3d 37527 cdleme3e 37528 cdleme3fN 37529 cdleme3fa 37532 cdleme3g 37530 cdleme3h 37531 cdleme4 37534 cdleme40m 37763 cdleme40n 37764 cdleme40v 37765 cdleme40w 37766 cdleme41fva11 37773 cdleme41sn3aw 37770 cdleme41sn4aw 37771 cdleme41snaw 37772 cdleme42a 37767 cdleme42b 37774 cdleme42c 37768 cdleme42d 37769 cdleme42e 37775 cdleme42f 37776 cdleme42g 37777 cdleme42h 37778 cdleme42i 37779 cdleme42k 37780 cdleme42ke 37781 cdleme42keg 37782 cdleme42mN 37783 cdleme42mgN 37784 cdleme43aN 37785 cdleme43bN 37786 cdleme43cN 37787 cdleme43dN 37788 cdleme5 37536 cdleme50ex 37855 cdleme50ltrn 37853 cdleme51finvN 37852 cdleme51finvfvN 37851 cdleme51finvtrN 37854 cdleme6 37537 cdleme7 37545 cdleme7a 37539 cdleme7aa 37538 cdleme7b 37540 cdleme7c 37541 cdleme7d 37542 cdleme7e 37543 cdleme7ga 37544 cdleme8 37546 cdleme8tN 37551 cdleme9 37549 cdleme9a 37547 cdleme9b 37548 cdleme9tN 37553 cdleme9taN 37552 cdlemeda 37594 cdlemedb 37593 cdlemednpq 37595 cdlemednuN 37596 cdlemefr27cl 37699 cdlemefr32fva1 37706 cdlemefr32fvaN 37705 cdlemefrs32fva 37696 cdlemefrs32fva1 37697 cdlemefs27cl 37709 cdlemefs32fva1 37719 cdlemefs32fvaN 37718 cdlemesner 37592 cdlemeulpq 37516 |
| [Crawley] p. 114 | Lemma E | 4atex 37372 4atexlem7 37371 cdleme0nex 37586 cdleme17a 37582 cdleme17c 37584 cdleme17d 37794 cdleme17d1 37585 cdleme17d2 37791 cdleme18a 37587 cdleme18b 37588 cdleme18c 37589 cdleme18d 37591 cdleme4a 37535 |
| [Crawley] p. 115 | Lemma E | cdleme21a 37621 cdleme21at 37624 cdleme21b 37622 cdleme21c 37623 cdleme21ct 37625 cdleme21f 37628 cdleme21g 37629 cdleme21h 37630 cdleme21i 37631 cdleme22gb 37590 |
| [Crawley] p. 116 | Lemma F | cdlemf 37859 cdlemf1 37857 cdlemf2 37858 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 37863 cdlemg16 37953 cdlemg28 38000 cdlemg28a 37989 cdlemg28b 37999 cdlemg3a 37893 cdlemg42 38025 cdlemg43 38026 cdlemg44 38029 cdlemg44a 38027 cdlemg46 38031 cdlemg47 38032 cdlemg9 37930 ltrnco 38015 ltrncom 38034 tgrpabl 38047 trlco 38023 |
| [Crawley] p. 116 | Definition of G | df-tgrp 38039 |
| [Crawley] p. 117 | Lemma G | cdlemg17 37973 cdlemg17b 37958 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 38052 df-edring 38053 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 38056 |
| [Crawley] p. 118 | Remark | tendopltp 38076 |
| [Crawley] p. 118 | Lemma H | cdlemh 38113 cdlemh1 38111 cdlemh2 38112 |
| [Crawley] p. 118 | Lemma I | cdlemi 38116 cdlemi1 38114 cdlemi2 38115 |
| [Crawley] p. 118 | Lemma J | cdlemj1 38117 cdlemj2 38118 cdlemj3 38119 tendocan 38120 |
| [Crawley] p. 118 | Lemma K | cdlemk 38270 cdlemk1 38127 cdlemk10 38139 cdlemk11 38145 cdlemk11t 38242 cdlemk11ta 38225 cdlemk11tb 38227 cdlemk11tc 38241 cdlemk11u-2N 38185 cdlemk11u 38167 cdlemk12 38146 cdlemk12u-2N 38186 cdlemk12u 38168 cdlemk13-2N 38172 cdlemk13 38148 cdlemk14-2N 38174 cdlemk14 38150 cdlemk15-2N 38175 cdlemk15 38151 cdlemk16-2N 38176 cdlemk16 38153 cdlemk16a 38152 cdlemk17-2N 38177 cdlemk17 38154 cdlemk18-2N 38182 cdlemk18-3N 38196 cdlemk18 38164 cdlemk19-2N 38183 cdlemk19 38165 cdlemk19u 38266 cdlemk1u 38155 cdlemk2 38128 cdlemk20-2N 38188 cdlemk20 38170 cdlemk21-2N 38187 cdlemk21N 38169 cdlemk22-3 38197 cdlemk22 38189 cdlemk23-3 38198 cdlemk24-3 38199 cdlemk25-3 38200 cdlemk26-3 38202 cdlemk26b-3 38201 cdlemk27-3 38203 cdlemk28-3 38204 cdlemk29-3 38207 cdlemk3 38129 cdlemk30 38190 cdlemk31 38192 cdlemk32 38193 cdlemk33N 38205 cdlemk34 38206 cdlemk35 38208 cdlemk36 38209 cdlemk37 38210 cdlemk38 38211 cdlemk39 38212 cdlemk39u 38264 cdlemk4 38130 cdlemk41 38216 cdlemk42 38237 cdlemk42yN 38240 cdlemk43N 38259 cdlemk45 38243 cdlemk46 38244 cdlemk47 38245 cdlemk48 38246 cdlemk49 38247 cdlemk5 38132 cdlemk50 38248 cdlemk51 38249 cdlemk52 38250 cdlemk53 38253 cdlemk54 38254 cdlemk55 38257 cdlemk55u 38262 cdlemk56 38267 cdlemk5a 38131 cdlemk5auN 38156 cdlemk5u 38157 cdlemk6 38133 cdlemk6u 38158 cdlemk7 38144 cdlemk7u-2N 38184 cdlemk7u 38166 cdlemk8 38134 cdlemk9 38135 cdlemk9bN 38136 cdlemki 38137 cdlemkid 38232 cdlemkj-2N 38178 cdlemkj 38159 cdlemksat 38142 cdlemksel 38141 cdlemksv 38140 cdlemksv2 38143 cdlemkuat 38162 cdlemkuel-2N 38180 cdlemkuel-3 38194 cdlemkuel 38161 cdlemkuv-2N 38179 cdlemkuv2-2 38181 cdlemkuv2-3N 38195 cdlemkuv2 38163 cdlemkuvN 38160 cdlemkvcl 38138 cdlemky 38222 cdlemkyyN 38258 tendoex 38271 |
| [Crawley] p. 120 | Remark | dva1dim 38281 |
| [Crawley] p. 120 | Lemma L | cdleml1N 38272 cdleml2N 38273 cdleml3N 38274 cdleml4N 38275 cdleml5N 38276 cdleml6 38277 cdleml7 38278 cdleml8 38279 cdleml9 38280 dia1dim 38357 |
| [Crawley] p. 120 | Lemma M | dia11N 38344 diaf11N 38345 dialss 38342 diaord 38343 dibf11N 38457 djajN 38433 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 38328 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 38414 dia2dimlem1 38360 dia2dimlem2 38361 dia2dimlem3 38362 dia2dimlem4 38363 dia2dimlem5 38364 diaf1oN 38426 diarnN 38425 dvheveccl 38408 dvhopN 38412 |
| [Crawley] p. 121 | Lemma N | cdlemn 38508 cdlemn10 38502 cdlemn11 38507 cdlemn11a 38503 cdlemn11b 38504 cdlemn11c 38505 cdlemn11pre 38506 cdlemn2 38491 cdlemn2a 38492 cdlemn3 38493 cdlemn4 38494 cdlemn4a 38495 cdlemn5 38497 cdlemn5pre 38496 cdlemn6 38498 cdlemn7 38499 cdlemn8 38500 cdlemn9 38501 diclspsn 38490 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 38469 |
| [Crawley] p. 122 | Lemma N | dih11 38561 dihf11 38563 dihjust 38513 dihjustlem 38512 dihord 38560 dihord1 38514 dihord10 38519 dihord11b 38518 dihord11c 38520 dihord2 38523 dihord2a 38515 dihord2b 38516 dihord2cN 38517 dihord2pre 38521 dihord2pre2 38522 dihordlem6 38509 dihordlem7 38510 dihordlem7b 38511 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 38526 dihfval 38527 dihval 38528 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 27202 df-nbgr 27123 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 27058 uhgrspan1 27093 uhgrspansubgr 27081 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 27344 vtxdgoddnumeven 27343 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 26852 |
| [EGA] p. 80 | Notation 1.1.1 | rspecval 31217 |
| [EGA] p. 80 | Proposition 1.1.2 | zartop 31229 |
| [EGA] p. 80 | Proposition 1.1.2(i) | zarcls0 31221 zarcls1 31222 |
| [EGA] p. 81 | Corollary 1.1.8 | zart0 31232 |
| [EGA], p. 82 | Proposition 1.1.10(ii) | zarcmp 31235 |
| [EGA], p. 83 | Corollary 1.2.3 | rhmpreimacn 31238 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3884 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 9094 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 8391 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 9102 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 9393 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 9966 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 5173 |
| [Enderton] p. 19 | Definition | df-tp 4530 |
| [Enderton] p. 26 | Exercise 5 | unissb 4832 |
| [Enderton] p. 26 | Exercise 10 | pwel 5247 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5423 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 4964 iinin2 4963 iinun2 4958 iunin1 4957 iunin1f 30321 iunin2 4956 uniin1 30315 uniin2 30316 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 4962 iundif2 4959 |
| [Enderton] p. 32 | Exercise 20 | unineq 4204 |
| [Enderton] p. 33 | Exercise 23 | iinuni 4983 |
| [Enderton] p. 33 | Exercise 25 | iununi 4984 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4991 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 7473 iunpwss 4992 |
| [Enderton] p. 36 | Definition | opthwiener 5369 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 5308 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4837 |
| [Enderton] p. 41 | Lemma 3D | opeluu 5327 rnex 7599 rnexg 7595 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5747 rnuni 5974 |
| [Enderton] p. 42 | Definition of a function | dffun7 6351 dffun8 6352 |
| [Enderton] p. 43 | Definition of function value | funfv2 6726 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 6393 |
| [Enderton] p. 44 | Definition (d) | dfima2 5898 dfima3 5899 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6735 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 9884 ac7g 9885 df-ac 9527 dfac2 9542 dfac2a 9540 dfac2b 9541 dfac3 9532 dfac7 9543 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 6983 |
| [Enderton] p. 52 | Definition | df-map 8391 |
| [Enderton] p. 53 | Exercise 21 | coass 6085 |
| [Enderton] p. 53 | Exercise 27 | dmco 6074 |
| [Enderton] p. 53 | Exercise 14(a) | funin 6400 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5932 |
| [Enderton] p. 54 | Remark | ixpf 8467 ixpssmap 8479 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 8445 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 9894 ac9s 9904 |
| [Enderton] p. 56 | Theorem 3M | eqvrelref 36005 erref 8292 |
| [Enderton] p. 57 | Lemma 3N | eqvrelthi 36008 erthi 8323 |
| [Enderton] p. 57 | Definition | df-ec 8274 |
| [Enderton] p. 58 | Definition | df-qs 8278 |
| [Enderton] p. 61 | Exercise 35 | df-ec 8274 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5743 |
| [Enderton] p. 68 | Definition of successor | df-suc 6165 |
| [Enderton] p. 71 | Definition | df-tr 5137 dftr4 5141 |
| [Enderton] p. 72 | Theorem 4E | unisuc 6235 |
| [Enderton] p. 73 | Exercise 6 | unisuc 6235 |
| [Enderton] p. 73 | Exercise 5(a) | truni 5150 |
| [Enderton] p. 73 | Exercise 5(b) | trint 5152 trintALT 41587 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 8213 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 8215 onasuc 8136 |
| [Enderton] p. 79 | Definition of operation value | df-ov 7138 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 8214 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 8216 onmsuc 8137 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 8231 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 8218 nnacom 8226 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 8232 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 8233 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 8235 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 8219 nnmsucr 8234 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 8247 |
| [Enderton] p. 129 | Definition | df-en 8493 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 7090 |
| [Enderton] p. 133 | Exercise 1 | xpomen 9426 |
| [Enderton] p. 133 | Exercise 2 | qnnen 15558 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8685 |
| [Enderton] p. 135 | Corollary 6C | php3 8687 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8684 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 8712 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 8714 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8720 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8722 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8665 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 9590 |
| [Enderton] p. 142 | Theorem 6I(4) | mapdjuen 9591 |
| [Enderton] p. 143 | Theorem 6J | dju0en 9586 dju1en 9582 |
| [Enderton] p. 144 | Exercise 13 | iunfi 8796 unifi 8797 unifi2 8798 |
| [Enderton] p. 144 | Corollary 6K | undif2 4383 unfi 8769 unfi2 8771 |
| [Enderton] p. 145 | Figure 38 | ffoss 7629 |
| [Enderton] p. 145 | Definition | df-dom 8494 |
| [Enderton] p. 146 | Example 1 | domen 8505 domeng 8506 |
| [Enderton] p. 146 | Example 3 | nndomo 8697 nnsdom 9101 nnsdomg 8761 |
| [Enderton] p. 149 | Theorem 6L(a) | djudom2 9594 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8666 xpdom1 8599 xpdom1g 8597 xpdom2g 8596 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8672 |
| [Enderton] p. 151 | Theorem 6M | zorn 9918 zorng 9915 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 9903 dfac5 9539 |
| [Enderton] p. 159 | Theorem 6Q | unictb 9986 |
| [Enderton] p. 164 | Example | infdif 9620 |
| [Enderton] p. 168 | Definition | df-po 5438 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 6266 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 6205 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 6265 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 6212 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7533 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 7482 |
| [Enderton] p. 194 | Remark | onprc 7479 |
| [Enderton] p. 194 | Exercise 16 | suc11 6262 |
| [Enderton] p. 197 | Definition | df-card 9352 |
| [Enderton] p. 197 | Theorem 7P | carden 9962 |
| [Enderton] p. 200 | Exercise 25 | tfis 7549 |
| [Enderton] p. 202 | Lemma 7T | r1tr 9189 |
| [Enderton] p. 202 | Definition | df-r1 9177 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 9199 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 9280 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 9053 |
| [Enderton] p. 207 | Exercise 30 | rankpr 9270 rankprb 9264 rankpw 9256 rankpwi 9236 rankuniss 9279 |
| [Enderton] p. 207 | Exercise 34 | opthreg 9065 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 9066 |
| [Enderton] p. 212 | Definition of aleph | alephval3 9521 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 9487 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 9501 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 7961 |
| [Enderton] p. 222 | Definition of kard | karden 9308 kardex 9307 |
| [Enderton] p. 238 | Theorem 8R | oeoa 8206 |
| [Enderton] p. 238 | Theorem 8S | oeoe 8208 |
| [Enderton] p. 240 | Exercise 25 | oarec 8171 |
| [Enderton] p. 257 | Definition of cofinality | cflm 9661 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 16905 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 16851 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 17779 mrieqv2d 16902 mrieqvd 16901 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 16906 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 16911 mreexexlem2d 16908 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 17785 mreexfidimd 16913 |
| [Frege1879] p. 11 | Statement | df3or2 40469 |
| [Frege1879] p. 12 | Statement | df3an2 40470 dfxor4 40467 dfxor5 40468 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 40491 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 40492 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 40496 |
| [Frege1879] p. 31 | Proposition 4 | frege4 40500 |
| [Frege1879] p. 32 | Proposition 5 | frege5 40501 |
| [Frege1879] p. 33 | Proposition 6 | frege6 40507 |
| [Frege1879] p. 34 | Proposition 7 | frege7 40509 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 40510 axfrege8 40508 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-luk-pm2.04 34862 |
| [Frege1879] p. 35 | Proposition 9 | frege9 40513 |
| [Frege1879] p. 36 | Proposition 10 | frege10 40521 |
| [Frege1879] p. 36 | Proposition 11 | frege11 40515 |
| [Frege1879] p. 37 | Proposition 12 | frege12 40514 |
| [Frege1879] p. 37 | Proposition 13 | frege13 40523 |
| [Frege1879] p. 37 | Proposition 14 | frege14 40524 |
| [Frege1879] p. 38 | Proposition 15 | frege15 40527 |
| [Frege1879] p. 38 | Proposition 16 | frege16 40517 |
| [Frege1879] p. 39 | Proposition 17 | frege17 40522 |
| [Frege1879] p. 39 | Proposition 18 | frege18 40519 |
| [Frege1879] p. 39 | Proposition 19 | frege19 40525 |
| [Frege1879] p. 40 | Proposition 20 | frege20 40529 |
| [Frege1879] p. 40 | Proposition 21 | frege21 40528 |
| [Frege1879] p. 41 | Proposition 22 | frege22 40520 |
| [Frege1879] p. 42 | Proposition 23 | frege23 40526 |
| [Frege1879] p. 42 | Proposition 24 | frege24 40516 |
| [Frege1879] p. 42 | Proposition 25 | frege25 40518 rp-frege25 40506 |
| [Frege1879] p. 42 | Proposition 26 | frege26 40511 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 40531 |
| [Frege1879] p. 43 | Proposition 27 | frege27 40512 |
| [Frege1879] p. 43 | Proposition 28 | con3 156 |
| [Frege1879] p. 43 | Proposition 29 | frege29 40532 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 40535 axfrege31 40534 |
| [Frege1879] p. 44 | Proposition 30 | frege30 40533 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 132 |
| [Frege1879] p. 44 | Proposition 32 | frege32 40536 |
| [Frege1879] p. 44 | Proposition 33 | frege33 40537 |
| [Frege1879] p. 45 | Proposition 34 | frege34 40538 |
| [Frege1879] p. 45 | Proposition 35 | frege35 40539 |
| [Frege1879] p. 45 | Proposition 36 | frege36 40540 |
| [Frege1879] p. 46 | Proposition 37 | frege37 40541 |
| [Frege1879] p. 46 | Proposition 38 | frege38 40542 |
| [Frege1879] p. 46 | Proposition 39 | frege39 40543 |
| [Frege1879] p. 46 | Proposition 40 | frege40 40544 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 40546 axfrege41 40545 |
| [Frege1879] p. 47 | Proposition 41 | notnot 144 |
| [Frege1879] p. 47 | Proposition 42 | frege42 40547 |
| [Frege1879] p. 47 | Proposition 43 | frege43 40548 |
| [Frege1879] p. 47 | Proposition 44 | frege44 40549 |
| [Frege1879] p. 47 | Proposition 45 | frege45 40550 |
| [Frege1879] p. 48 | Proposition 46 | frege46 40551 |
| [Frege1879] p. 48 | Proposition 47 | frege47 40552 |
| [Frege1879] p. 49 | Proposition 48 | frege48 40553 |
| [Frege1879] p. 49 | Proposition 49 | frege49 40554 |
| [Frege1879] p. 49 | Proposition 50 | frege50 40555 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 40558 ax-frege52c 40589 frege52aid 40559 frege52b 40590 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 40563 ax-frege54c 40593 frege54b 40594 |
| [Frege1879] p. 50 | Proposition 51 | frege51 40556 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3722 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 40561 frege53aid 40560 frege53b 40591 frege53c 40615 |
| [Frege1879] p. 50 | Proposition 54 | biid 264 eqid 2798 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 40569 frege55aid 40566 frege55b 40598 frege55c 40619 frege55cor1a 40570 frege55lem2a 40568 frege55lem2b 40597 frege55lem2c 40618 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 40572 frege56aid 40571 frege56b 40599 frege56c 40620 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 40576 ax-frege58b 40602 frege58bid 40603 frege58c 40622 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 40574 frege57aid 40573 frege57b 40600 frege57c 40621 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3733 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 40578 frege59b 40605 frege59c 40623 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 40579 frege60b 40606 frege60c 40624 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 40580 frege61b 40607 frege61c 40625 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 40581 frege62b 40608 frege62c 40626 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 40582 frege63b 40609 frege63c 40627 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 40583 frege64b 40610 frege64c 40628 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 40584 frege65b 40611 frege65c 40629 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 40585 frege66b 40612 frege66c 40630 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 40586 frege67b 40613 frege67c 40631 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 40587 frege68b 40614 frege68c 40632 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 40633 |
| [Frege1879] p. 58 | Proposition 70 | frege70 40634 |
| [Frege1879] p. 59 | Proposition 71 | frege71 40635 |
| [Frege1879] p. 59 | Proposition 72 | frege72 40636 |
| [Frege1879] p. 59 | Proposition 73 | frege73 40637 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 40640 |
| [Frege1879] p. 60 | Proposition 74 | frege74 40638 |
| [Frege1879] p. 60 | Proposition 75 | frege75 40639 |
| [Frege1879] p. 62 | Proposition 77 | frege77 40641 frege77d 40447 |
| [Frege1879] p. 63 | Proposition 78 | frege78 40642 |
| [Frege1879] p. 63 | Proposition 79 | frege79 40643 |
| [Frege1879] p. 63 | Proposition 80 | frege80 40644 |
| [Frege1879] p. 63 | Proposition 81 | frege81 40645 frege81d 40448 |
| [Frege1879] p. 64 | Proposition 82 | frege82 40646 |
| [Frege1879] p. 65 | Proposition 83 | frege83 40647 frege83d 40449 |
| [Frege1879] p. 65 | Proposition 84 | frege84 40648 |
| [Frege1879] p. 66 | Proposition 85 | frege85 40649 |
| [Frege1879] p. 66 | Proposition 86 | frege86 40650 |
| [Frege1879] p. 66 | Proposition 87 | frege87 40651 frege87d 40451 |
| [Frege1879] p. 67 | Proposition 88 | frege88 40652 |
| [Frege1879] p. 68 | Proposition 89 | frege89 40653 |
| [Frege1879] p. 68 | Proposition 90 | frege90 40654 |
| [Frege1879] p. 68 | Proposition 91 | frege91 40655 frege91d 40452 |
| [Frege1879] p. 69 | Proposition 92 | frege92 40656 |
| [Frege1879] p. 70 | Proposition 93 | frege93 40657 |
| [Frege1879] p. 70 | Proposition 94 | frege94 40658 |
| [Frege1879] p. 70 | Proposition 95 | frege95 40659 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 40663 |
| [Frege1879] p. 71 | Proposition 96 | frege96 40660 frege96d 40450 |
| [Frege1879] p. 71 | Proposition 97 | frege97 40661 frege97d 40453 |
| [Frege1879] p. 71 | Proposition 98 | frege98 40662 frege98d 40454 |
| [Frege1879] p. 72 | Proposition 100 | frege100 40664 |
| [Frege1879] p. 72 | Proposition 101 | frege101 40665 |
| [Frege1879] p. 72 | Proposition 102 | frege102 40666 frege102d 40455 |
| [Frege1879] p. 73 | Proposition 103 | frege103 40667 |
| [Frege1879] p. 73 | Proposition 104 | frege104 40668 |
| [Frege1879] p. 73 | Proposition 105 | frege105 40669 |
| [Frege1879] p. 73 | Proposition 106 | frege106 40670 frege106d 40456 |
| [Frege1879] p. 74 | Proposition 107 | frege107 40671 |
| [Frege1879] p. 74 | Proposition 108 | frege108 40672 frege108d 40457 |
| [Frege1879] p. 74 | Proposition 109 | frege109 40673 frege109d 40458 |
| [Frege1879] p. 75 | Proposition 110 | frege110 40674 |
| [Frege1879] p. 75 | Proposition 111 | frege111 40675 frege111d 40460 |
| [Frege1879] p. 76 | Proposition 112 | frege112 40676 |
| [Frege1879] p. 76 | Proposition 113 | frege113 40677 |
| [Frege1879] p. 76 | Proposition 114 | frege114 40678 frege114d 40459 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 40679 |
| [Frege1879] p. 77 | Proposition 116 | frege116 40680 |
| [Frege1879] p. 78 | Proposition 117 | frege117 40681 |
| [Frege1879] p. 78 | Proposition 118 | frege118 40682 |
| [Frege1879] p. 78 | Proposition 119 | frege119 40683 |
| [Frege1879] p. 78 | Proposition 120 | frege120 40684 |
| [Frege1879] p. 79 | Proposition 121 | frege121 40685 |
| [Frege1879] p. 79 | Proposition 122 | frege122 40686 frege122d 40461 |
| [Frege1879] p. 79 | Proposition 123 | frege123 40687 |
| [Frege1879] p. 80 | Proposition 124 | frege124 40688 frege124d 40462 |
| [Frege1879] p. 81 | Proposition 125 | frege125 40689 |
| [Frege1879] p. 81 | Proposition 126 | frege126 40690 frege126d 40463 |
| [Frege1879] p. 82 | Proposition 127 | frege127 40691 |
| [Frege1879] p. 83 | Proposition 128 | frege128 40692 |
| [Frege1879] p. 83 | Proposition 129 | frege129 40693 frege129d 40464 |
| [Frege1879] p. 84 | Proposition 130 | frege130 40694 |
| [Frege1879] p. 85 | Proposition 131 | frege131 40695 frege131d 40465 |
| [Frege1879] p. 86 | Proposition 132 | frege132 40696 |
| [Frege1879] p. 86 | Proposition 133 | frege133 40697 frege133d 40466 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 42955 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 43275 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 42976 |
| [Fremlin1] p. 14 | Definition 112A | ismea 43090 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 43110 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 43101 meadjunre 43115 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 43102 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 43103 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 43099 meaiunle 43108 meaiunlelem 43107 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 43120 meaiuninc2 43121 meaiuninc3 43124 meaiuninc3v 43123 meaiunincf 43122 meaiuninclem 43119 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 43126 meaiininc2 43127 meaiininclem 43125 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 43145 caragendifcl 43153 caratheodory 43167 omelesplit 43157 |
| [Fremlin1] p. 19 | Definition 113A | isome 43133 isomennd 43170 isomenndlem 43169 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 43155 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 43174 voncmpl 43260 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 43137 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 43162 carageniuncllem1 43160 carageniuncllem2 43161 caragenuncl 43152 caragenuncllem 43151 caragenunicl 43163 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 43171 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 43165 caratheodorylem2 43166 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 43174 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 43233 hoidmv1lelem1 43230 hoidmv1lelem2 43231 hoidmv1lelem3 43232 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 43277 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 43233 hoidmvle 43239 hoidmvlelem1 43234 hoidmvlelem2 43235 hoidmvlelem3 43236 hoidmvlelem4 43237 hoidmvlelem5 43238 hsphoidmvle2 43224 hsphoif 43215 hsphoival 43218 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 43187 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 43195 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 43222 hoidmvn0val 43223 hoidmvval 43216 hoidmvval0 43226 hoidmvval0b 43229 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 43227 hsphoidmvle 43225 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 43176 df-voln 43178 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 43243 ovn0 43205 ovn0lem 43204 ovnf 43202 ovnome 43212 ovnssle 43200 ovnsslelem 43199 ovnsupge0 43196 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 43242 ovnhoilem1 43240 ovnhoilem2 43241 vonhoi 43306 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 43259 hoidifhspf 43257 hoidifhspval 43247 hoidifhspval2 43254 hoidifhspval3 43258 hspmbl 43268 hspmbllem1 43265 hspmbllem2 43266 hspmbllem3 43267 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 43260 vonmea 43213 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 43211 ovnsubadd2 43285 ovnsubadd2lem 43284 ovnsubaddlem1 43209 ovnsubaddlem2 43210 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 43270 hoimbl2 43304 hoimbllem 43269 hspdifhsp 43255 opnvonmbl 43273 opnvonmbllem2 43272 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 43275 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 43318 iccvonmbllem 43317 ioovonmbl 43316 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 43324 vonicclem2 43323 vonioo 43321 vonioolem2 43320 vonn0icc 43327 vonn0icc2 43331 vonn0ioo 43326 vonn0ioo2 43329 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 43328 snvonmbl 43325 vonct 43332 vonsn 43330 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 42999 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 42998 subsaliuncllem 42997 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 43359 salpreimalegt 43345 salpreimaltle 43360 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 43362 issmff 43368 issmflem 43361 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 43379 issmflelem 43378 smfpreimale 43388 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 43390 issmfgtlem 43389 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 43335 issmf 43362 issmff 43368 issmfge 43403 issmfgelem 43402 issmfgt 43390 issmfgtlem 43389 issmfle 43379 issmflelem 43378 issmflem 43361 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 43343 salpreimagtlt 43364 salpreimalelt 43363 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 43403 issmfgelem 43402 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 43387 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 43385 cnfsmf 43374 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 43400 decsmflem 43399 incsmf 43376 incsmflem 43375 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 43339 pimconstlt1 43340 smfconst 43383 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 43398 smfaddlem1 43396 smfaddlem2 43397 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 43428 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 43427 smfmullem1 43423 smfmullem2 43424 smfmullem3 43425 smfmullem4 43426 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 43429 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 43432 smfpimbor1lem2 43431 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 43434 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 43422 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 43421 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 43430 smfresal 43420 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 43410 smflim2 43437 smflimlem1 43404 smflimlem2 43405 smflimlem3 43406 smflimlem4 43407 smflimlem5 43408 smflimlem6 43409 smflimmpt 43441 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 43445 smfsuplem1 43442 smfsuplem2 43443 smfsuplem3 43444 smfsupmpt 43446 smfsupxr 43447 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 43449 smfinflem 43448 smfinfmpt 43450 |
| [Fremlin1] p. 39 | Remark 121G | smflim 43410 smflim2 43437 smflimmpt 43441 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 43439 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 43459 smflimsuplem2 43452 smflimsuplem6 43456 smflimsuplem7 43457 smflimsuplem8 43458 smflimsupmpt 43460 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 43462 smfliminflem 43461 smfliminfmpt 43463 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 43335 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 24140 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 24183 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 24193 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 35135 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 35138 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 9085 inf1 9069 inf2 9070 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 10322 enqer 10332 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 10327 df-nq 10323 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 10319 df-plq 10325 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 7365 df-mpq 10320 df-mq 10326 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 10328 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 10386 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 10387 ltbtwnnq 10389 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 10382 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 10383 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 10390 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 10392 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 10404 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 10406 |
| [Gleason] p. 122 | Definition | df-1p 10393 |
| [Gleason] p. 122 | Remark (1) | prub 10405 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 10444 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 10396 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 10443 psslinpr 10442 supexpr 10465 suplem1pr 10463 suplem2pr 10464 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 10429 addclprlem1 10427 addclprlem2 10428 df-plp 10394 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 10433 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 10432 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 10445 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 10454 ltexprlem1 10447 ltexprlem2 10448 ltexprlem3 10449 ltexprlem4 10450 ltexprlem5 10451 ltexprlem6 10452 ltexprlem7 10453 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 10456 ltaprlem 10455 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 10457 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 10458 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 10395 mulclpr 10431 mulclprlem 10430 reclem2pr 10459 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 10440 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 10435 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 10434 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 10439 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 10462 reclem3pr 10460 reclem4pr 10461 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 10466 enrer 10474 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 10471 df-1r 10472 df-nr 10467 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 10469 df-plr 10468 negexsr 10513 recexsr 10518 recexsrlem 10514 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 10470 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11620 creur 11619 cru 11617 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10599 axcnre 10575 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 14466 crimd 14583 crimi 14544 crre 14465 crred 14582 crrei 14543 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 14468 remimd 14549 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14636 absval2d 14797 absval2i 14749 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 14492 cjaddd 14571 cjaddi 14539 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 14493 cjmuld 14572 cjmuli 14540 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 14491 cjcjd 14550 cjcji 14522 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 14490 cjreb 14474 cjrebd 14553 cjrebi 14525 cjred 14577 rere 14473 rereb 14471 rerebd 14552 rerebi 14524 rered 14575 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 14499 addcjd 14563 addcji 14534 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 14589 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14631 abscjd 14802 abscji 14753 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 14641 abs00d 14798 abs00i 14750 absne0d 14799 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 14673 releabsd 14803 releabsi 14754 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 14646 absmuld 14806 absmuli 14756 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14634 sqabsaddi 14757 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 14682 abstrid 14808 abstrii 14760 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 13430 df-exp 13426 exp0 13429 expp1 13432 expp1d 13507 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 25270 cxpaddd 25308 expadd 13467 expaddd 13508 expaddz 13469 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 25279 cxpmuld 25327 expmul 13470 expmuld 13509 expmulz 13471 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 25276 mulcxpd 25319 mulexp 13464 mulexpd 13521 mulexpz 13465 |
| [Gleason] p. 140 | Exercise 1 | znnen 15557 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 12887 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 14980 rlimadd 14991 rlimdiv 14994 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 14982 rlimsub 14992 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 14981 rlimmul 14993 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 14985 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 14932 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 14952 climcj 14953 climim 14955 climre 14954 rlimabs 14957 rlimcj 14958 rlimim 14960 rlimre 14959 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 10669 df-xr 10668 ltxr 12498 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 14820 limsupval 14823 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 15018 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 15027 caucvgb 15028 caucvgr 15024 climcau 15019 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 15163 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 15231 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 14687 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 13193 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 20085 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 22950 xmet0 22949 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 22966 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 22957 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 22959 mstri 23076 xmettri 22958 xmstri 23075 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 22989 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 22253 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 23914 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 23147 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 23470 addcn2 14942 mulcn 23472 mulcn2 14944 subcn 23471 subcn2 14943 |
| [Gleason] p. 295 | Remark | bcval3 13662 bcval4 13663 |
| [Gleason] p. 295 | Equation 2 | bcpasc 13677 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 13660 df-bc 13659 |
| [Gleason] p. 296 | Remark | bcn0 13666 bcnn 13668 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 15177 |
| [Gleason] p. 308 | Equation 2 | ef0 15436 |
| [Gleason] p. 308 | Equation 3 | efcj 15437 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 15442 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 15446 |
| [Gleason] p. 310 | Equation 14 | sinadd 15509 |
| [Gleason] p. 310 | Equation 15 | cosadd 15510 |
| [Gleason] p. 311 | Equation 17 | sincossq 15521 |
| [Gleason] p. 311 | Equation 18 | cosbnd 15526 sinbnd 15525 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 13574 sqeqori 13572 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 15418 |
| [Godowski] p. 730 | Equation SF | goeqi 30056 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 29451 |
| [Golan] p. 1 | Remark | srgisid 19271 |
| [Golan] p. 1 | Definition | df-srg 19249 |
| [Golan] p. 149 | Definition | df-slmd 30879 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 33733 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 16849 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 16851 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 44448 df-cllaw 44446 df-comlaw 44447 |
| [Hall] p. 2 | Section 1.2 | df-clintop 44460 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 44481 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 29848 riesz2 29849 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 29724 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 29956 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 29968 elpjidm 29967 pjnmopi 29931 |
| [Halmos] p. 44 | Remark | pjinormi 29470 pjinormii 29459 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 29972 pjrn 29490 pjrni 29485 pjvec 29479 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 29510 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 29937 hmopidmpji 29935 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 29974 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 29963 pjocvec 29480 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 29952 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 29955 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 29958 pjssdif2i 29957 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 29638 |
| [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 1797 |
| [Hatcher] p. 25 | Definition | df-phtpc 23597 df-phtpy 23576 |
| [Hatcher] p. 26 | Definition | df-pco 23610 df-pi1 23613 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 23600 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 23655 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 21095 df-dmatalt 44807 |
| [Helfgott] p. 2 | Theorem | tgoldbach 44335 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 44320 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 44332 bgoldbtbnd 44327 bgoldbtbnd 44327 tgblthelfgott 44333 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 32023 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 32024 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 32038 hgt750lemb 32037 hgt750leme 32039 hgt750lemf 32034 hgt750lemg 32035 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 44329 tgoldbachgt 32044 tgoldbachgtALTV 44330 tgoldbachgtd 32043 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 32025 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 28276 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 18106 grpoideu 28292 mndideu 17914 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 18130 grpoinveu 28302 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 18158 grpo2inv 28314 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 18169 grpoinvop 28316 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 18191 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1770 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1771 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1773 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 30203 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 30216 cdj3i 30224 cdj3lem1 30217 cdjreui 30215 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 30214 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 39257 |
| [Holland95] p. 14 | Line 15 | hgmapvs 39187 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 39209 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 39210 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 39207 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 39213 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 39132 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 39227 |
| [Holland95] p. 204 | Definition of involution | df-srng 19610 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 36799 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 38824 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 38777 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 37229 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 38673 poml4N 37249 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 38764 pexmidALTN 37274 pexmidN 37265 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 38829 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 36420 ldualset 36421 |
| [Holland95] p. 222 | Item 1 | df-lines 36797 df-pointsN 36798 |
| [Holland95] p. 222 | Item 2 | df-polarityN 37199 |
| [Holland95] p. 223 | Remark | ispsubcl2N 37243 omllaw4 36542 pol1N 37206 polcon3N 37213 |
| [Holland95] p. 223 | Definition | df-psubclN 37231 |
| [Holland95] p. 223 | Equation for polarity | polval2N 37202 |
| [Holmes] p. 40 | Definition | df-xrn 35783 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 28867 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 29965 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 29746 eigre 29618 eigrei 29617 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 29747 eigorth 29621 eigorthi 29620 |
| [Hughes] p. 137 | Remark (ii) | eigposi 29619 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 28094 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 28090 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 28091 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 28092 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 28110 frgrregorufr0 28109 frgrregorufrg 28111 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 28117 frrusgrord 28126 frrusgrord0 28125 |
| [Huneke] p. 2 | Statement | df-clwwlknon 27873 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 28100 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 28103 frgrwopreg2 28104 frgrwopregasn 28101 frgrwopregbsn 28102 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 28106 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 28120 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 28123 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 27871 numclwlk1 28156 numclwlk1lem1 28154 numclwlk1lem2 28155 numclwwlk1 28146 numclwwlk8 28177 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 28097 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 27560 |
| [Huneke] p. 2 | Definition 6 | 2clwwlk 28132 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 28158 numclwwlkovh0 28157 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 28166 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 27763 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 28170 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 28173 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 28176 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 28188 natded 28188 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 28188 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 28188 natded 28188 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 28188 |
| [Jech] p. 4 | Definition of class | cv 1537 cvjust 2793 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 9990 |
| [Jech] p. 42 | Equation 6.1 | alephadd 9988 alephmul 9989 |
| [Jech] p. 43 | Lemma 6.2 | infmap 9987 infmap2 9629 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 9227 |
| [Jech] p. 72 | Equation 9.3 | scott0 9299 scottex 9298 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 9280 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 9304 |
| [Jech] p. 78 | Note | opthprc 5580 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 39856 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 39944 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 39945 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 39868 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 39872 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 39873 rmyp1 39874 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 39875 rmym1 39876 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 39866 rmx1 39867 rmxluc 39877 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 39870 rmy1 39871 rmyluc 39878 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 39880 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 39881 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 39901 jm2.17b 39902 jm2.17c 39903 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 39934 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 39938 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 39929 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 39904 jm2.24nn 39900 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 39943 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 39949 rmygeid 39905 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 39961 |
| [Juillerat] p. 11 | Section *5 | etransc 42925 etransclem47 42923 etransclem48 42924 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 42920 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 42922 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 42908 |
| [Juillerat] p. 13 | Proof | etransclem35 42911 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 42914 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 42900 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 42917 |
| [Juillerat] p. 14 | Proof | etransclem23 42899 |
| [KalishMontague] p. 81 | Note 1 | ax-6 1970 |
| [KalishMontague] p. 85 | Lemma 2 | equid 2019 |
| [KalishMontague] p. 85 | Lemma 3 | equcomi 2024 |
| [KalishMontague] p. 86 | Lemma 7 | cbvalivw 2014 cbvaliw 2013 wl-cbvmotv 34918 wl-motae 34920 wl-moteq 34919 |
| [KalishMontague] p. 87 | Lemma 8 | spimvw 2002 spimw 1973 |
| [KalishMontague] p. 87 | Lemma 9 | spfw 2040 spw 2041 |
| [Kalmbach] p. 14 | Definition of lattice | chabs1 29299 chabs1i 29301 chabs2 29300 chabs2i 29302 chjass 29316 chjassi 29269 latabs1 17689 latabs2 17690 |
| [Kalmbach] p. 15 | Definition of atom | df-at 30121 ela 30122 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 30066 cvrval2 36570 |
| [Kalmbach] p. 16 | Definition | df-ol 36474 df-oml 36475 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 29367 cmbri 29373 cmtvalN 36507 df-cm 29366 df-cmtN 36473 |
| [Kalmbach] p. 22 | Remark | omllaw5N 36543 pjoml5 29396 pjoml5i 29371 |
| [Kalmbach] p. 22 | Definition | pjoml2 29394 pjoml2i 29368 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 29397 cmcmi 29375 cmcmii 29380 cmtcomN 36545 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 36541 omlsi 29187 pjoml 29219 pjomli 29218 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 36540 |
| [Kalmbach] p. 23 | Remark | cmbr2i 29379 cmcm3 29398 cmcm3i 29377 cmcm3ii 29382 cmcm4i 29378 cmt3N 36547 cmt4N 36548 cmtbr2N 36549 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 29391 cmbr3i 29383 cmtbr3N 36550 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 29401 fh1i 29404 fh2 29402 fh2i 29405 omlfh1N 36554 |
| [Kalmbach] p. 65 | Remark | chjatom 30140 chslej 29281 chsleji 29241 shslej 29163 shsleji 29153 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 29278 chocini 29237 chsupcl 29123 chsupval2 29193 h0elch 29038 helch 29026 hsupval2 29192 ocin 29079 ococss 29076 shococss 29077 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 29095 |
| [Kalmbach] p. 66 | Remark | df-pjh 29178 pjssmi 29948 pjssmii 29464 |
| [Kalmbach] p. 67 | Lemma 3 | osum 29428 osumi 29425 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 29983 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 30183 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 30093 |
| [Kalmbach] p. 140 | Remark | hatomic 30143 hatomici 30142 hatomistici 30145 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 36615 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 30164 lsatexch 36339 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 30138 cvlcvr1 36635 cvr1 36706 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 30157 cvexchi 30152 cvrexch 36716 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 30147 hlrelat 36698 hlrelat5N 36697 lrelat 36310 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 19906 lsmsatcv 36306 spansncv 29436 spansncvi 29435 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 36325 spansncv2 30076 |
| [Kalmbach] p. 266 | Definition | df-st 29994 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 29632 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 10057 fpwwe2 10054 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 10058 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 10065 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 10060 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 10062 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 10075 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchdjuidm 10079 gchxpidm 10080 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 10091 gchhar 10090 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwdjudom 9627 unxpwdom 9037 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 10081 |
| [Kreyszig] p. 3 | Property M1 | metcl 22939 xmetcl 22938 |
| [Kreyszig] p. 4 | Property M2 | meteq0 22946 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 23179 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 11346 muleqadd 11273 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 23045 |
| [Kreyszig] p. 19 | Remark | mopntopon 23046 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 23105 mopnm 23051 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 23103 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 23108 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 23149 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 21863 lmmbr 23862 lmmbr2 23863 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 21985 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 23917 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 23880 iscmet2 23898 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 23920 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 22066 metelcls 23909 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 23910 metcld2 23911 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 23704 lmodvneg1 19670 nvinv 28422 vcm 28359 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 23700 lmod0vs 19660 slmd0vs 30902 vc0 28357 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 19661 slmdvs0 30903 vcz 28358 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 28474 ngpmet 23209 nrmmetd 23181 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 28469 imsdval2 28470 ncvspds 23766 ngpds 23210 |
| [Kreyszig] p. 63 | Problem 1 | nmval 23196 nvnd 28471 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 23224 nmge0 23223 nvge0 28456 nvz 28452 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 23230 nvabs 28455 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 28584 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 28528 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 28590 blocni 28588 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 28589 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 23809 ipeq0 20327 ipz 28502 |
| [Kreyszig] p. 135 | Problem 2 | pythi 28633 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 28637 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 15203 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 24040 minveco 28667 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 28533 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 23933 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 28656 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 29906 leopg 29905 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 29924 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 28701 |
| [Kulpa] p. 547 | Theorem | poimir 35090 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 35089 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 35088 |
| [Kulpa] p. 548 | Theorem | broucube 35091 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 35083 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 35084 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2390 axnul 5173 |
| [Kunen] p. 11 | Axiom 3 | axnul 5173 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7638 |
| [Kunen] p. 24 | Definition 10.24 | mapval 8401 mapvalg 8399 |
| [Kunen] p. 30 | Lemma 10.20 | fodomg 9933 |
| [Kunen] p. 31 | Definition 10.24 | mapex 8395 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 9177 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 9219 r1elssi 9218 |
| [Kunen] p. 107 | Exercise 4 | rankop 9271 rankopb 9265 rankuni 9276 rankxplim 9292 rankxpsuc 9295 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4893 |
| [Lang] , p. 225 | Corollary 1.3 | finexttrb 31140 |
| [Lang] p. | Definition | df-rn 5530 |
| [Lang] p. 3 | Statement | lidrideqd 17871 mndbn0 17919 |
| [Lang] p. 3 | Definition | df-mnd 17904 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 17889 |
| [Lang] p. 4 | Property of composites. Second formula | gsumccat 17998 |
| [Lang] p. 5 | Equation | gsumreidx 19030 |
| [Lang] p. 5 | Definition of an (infinite) product | gsumfsupp 44442 |
| [Lang] p. 6 | Example | nn0mnd 44439 |
| [Lang] p. 6 | Equation | gsumxp2 19093 |
| [Lang] p. 6 | Statement | cycsubm 18337 |
| [Lang] p. 6 | Definition | mulgnn0gsum 18226 |
| [Lang] p. 6 | Observation | mndlsmidm 18788 |
| [Lang] p. 7 | Definition | dfgrp2e 18121 |
| [Lang] p. 30 | Definition | df-tocyc 30799 |
| [Lang] p. 32 | Property (a) | cyc3genpm 30844 |
| [Lang] p. 32 | Property (b) | cyc3conja 30849 cycpmconjv 30834 |
| [Lang] p. 53 | Definition | df-cat 16931 |
| [Lang] p. 54 | Definition | df-iso 17011 |
| [Lang] p. 57 | Definition | df-inito 17243 df-termo 17244 |
| [Lang] p. 58 | Example | irinitoringc 44693 |
| [Lang] p. 58 | Statement | initoeu1 17263 termoeu1 17270 |
| [Lang] p. 62 | Definition | df-func 17120 |
| [Lang] p. 65 | Definition | df-nat 17205 |
| [Lang] p. 91 | Note | df-ringc 44629 |
| [Lang] p. 92 | Statement | mxidlprm 31048 |
| [Lang] p. 92 | Definition | isprmidlc 31031 |
| [Lang] p. 128 | Remark | dsmmlmod 20434 |
| [Lang] p. 129 | Proof | lincscm 44839 lincscmcl 44841 lincsum 44838 lincsumcl 44840 |
| [Lang] p. 129 | Statement | lincolss 44843 |
| [Lang] p. 129 | Observation | dsmmfi 20427 |
| [Lang] p. 141 | Theorem 5.3 | dimkerim 31111 qusdimsum 31112 |
| [Lang] p. 141 | Corollary 5.4 | lssdimle 31094 |
| [Lang] p. 147 | Definition | snlindsntor 44880 |
| [Lang] p. 504 | Statement | mat1 21052 matring 21048 |
| [Lang] p. 504 | Definition | df-mamu 20991 |
| [Lang] p. 505 | Statement | mamuass 21007 mamutpos 21063 matassa 21049 mattposvs 21060 tposmap 21062 |
| [Lang] p. 513 | Definition | mdet1 21206 mdetf 21200 |
| [Lang] p. 513 | Theorem 4.4 | cramer 21296 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 21192 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 21216 |
| [Lang] p. 515 | Definition | df-minmar1 21240 smadiadetr 21280 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 21215 mdetralt 21213 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 21228 |
| [Lang] p. 518 | Definition | df-madu 21239 |
| [Lang] p. 518 | Proposition 4.16 | madulid 21250 madurid 21249 matinv 21282 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 21495 |
| [Lang], p. 224 | Proposition 1.2 | extdgmul 31139 fedgmul 31115 |
| [Lang], p. 561 | Remark | chpmatply1 21437 |
| [Lang], p. 561 | Definition | df-chpmat 21432 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 41038 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 41033 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 41039 |
| [LeBlanc] p. 277 | Rule R2 | axnul 5173 |
| [Levy] p. 12 | Axiom 4.3.1 | df-clab 2777 |
| [Levy] p. 338 | Axiom | df-clel 2870 df-cleq 2791 |
| [Levy] p. 357 | Proof sketch of conservativity; for details see Appendix | df-clel 2870 df-cleq 2791 |
| [Levy] p. 357 | Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendix | df-clab 2777 |
| [Levy] p. 358 | Axiom | df-clab 2777 |
| [Levy58] p. 2 | Definition I | isfin1-3 9797 |
| [Levy58] p. 2 | Definition II | df-fin2 9697 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 9696 |
| [Levy58] p. 2 | Definition III | df-fin3 9699 |
| [Levy58] p. 3 | Definition V | df-fin5 9700 |
| [Levy58] p. 3 | Definition IV | df-fin4 9698 |
| [Levy58] p. 4 | Definition VI | df-fin6 9701 |
| [Levy58] p. 4 | Definition VII | df-fin7 9702 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 9826 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 33303 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 33313 |
| [Lipparini] p. 6 | Proposition 4.2 | nosupbnd1 33327 |
| [Lipparini] p. 6 | Proposition 4.3 | nosupbnd2 33329 |
| [Lipparini] p. 7 | Theorem 5.1 | noetalem2 33331 noetalem3 33332 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1770 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1771 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1773 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 30191 |
| [Maeda] p. 168 | Lemma 5 | mdsym 30195 mdsymi 30194 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 30189 mdsymlem6 30191 mdsymlem7 30192 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 30193 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 30096 ssdmd2 30097 ssmd1 30094 ssmd2 30095 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 30092 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 30064 df-md 30063 mdbr 30077 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 30114 mdslj1i 30102 mdslj2i 30103 mdslle1i 30100 mdslle2i 30101 mdslmd1i 30112 mdslmd2i 30113 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 30104 mdsl2bi 30106 mdsl2i 30105 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 30118 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 30115 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 30116 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 30093 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 30098 mdsl3 30099 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 30117 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 30212 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 36617 hlrelat1 36696 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 36335 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 30119 cvmdi 30107 cvnbtwn4 30072 cvrnbtwn4 36575 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 30120 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 36636 cvp 30158 cvrp 36712 lcvp 36336 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 30182 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 30181 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 36629 hlexch4N 36688 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 30184 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 36739 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 37045 atpsubN 37049 df-pointsN 36798 pointpsubN 37047 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 36800 pmap11 37058 pmaple 37057 pmapsub 37064 pmapval 37053 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 37061 pmap1N 37063 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 37066 pmapglb2N 37067 pmapglb2xN 37068 pmapglbx 37065 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 37148 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 36773 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 37092 paddclN 37138 paddidm 37137 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 36774 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 37134 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 36773 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 36774 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 18793 lsmmod2 18794 lssats 36308 shatomici 30141 shatomistici 30144 shmodi 29173 shmodsi 29172 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 30083 mdsymlem7 30192 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 29372 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 29276 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 30198 |
| [Margaris] p. 40 | Rule C | exlimiv 1931 |
| [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 1782 df-or 845 dfbi2 478 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 28185 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 41621 |
| [Margaris] p. 60 | Theorem 8 | jcn 165 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 41622 |
| [Margaris] p. 79 | Rule C | exinst01 41331 exinst11 41332 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1981 19.2g 2185 r19.2z 4398 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2200 rr19.3v 3607 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2160 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1827 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1783 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2178 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2203 19.9h 2290 exlimd 2216 exlimdh 2294 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2166 excomim 2167 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2335 |
| [Margaris] p. 90 | Section 19 | conventions-labels 28186 conventions-labels 28186 conventions-labels 28186 conventions-labels 28186 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1828 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 41082 albi 1820 |
| [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 41084 exbi 1848 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2229 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 41081 2alimdv 1919 alimd 2210 alimdh 1819 alimdv 1917 ax-4 1811 ralimdaa 3181 ralimdv 3145 ralimdva 3144 ralimdvva 3146 sbcimdv 3789 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2205 19.21h 2291 19.21t 2204 19.21vv 41080 alrimd 2213 alrimdd 2212 alrimdh 1864 alrimdv 1930 alrimi 2211 alrimih 1825 alrimiv 1928 alrimivv 1929 hbralrimi 3147 r19.21be 3174 r19.21bi 3173 ralrimd 3182 ralrimdv 3153 ralrimdva 3154 ralrimdvv 3158 ralrimdvva 3159 ralrimi 3180 ralrimia 41767 ralrimiv 3148 ralrimiva 3149 ralrimivv 3155 ralrimivva 3156 ralrimivvva 3157 ralrimivw 3150 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 41083 2eximdv 1920 exim 1835 eximd 2214 eximdh 1865 eximdv 1918 rexim 3204 reximd2a 3271 reximdai 3270 reximdd 41789 reximddv 3234 reximddv2 3237 reximddv3 41788 reximdv 3232 reximdv2 3230 reximdva 3233 reximdvai 3231 reximdvva 3236 reximi2 3207 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2209 19.23bi 2188 19.23h 2292 19.23t 2208 exlimdv 1934 exlimdvv 1935 exlimexi 41230 exlimiv 1931 exlimivv 1933 rexlimd3 41781 rexlimdv 3242 rexlimdv3a 3245 rexlimdva 3243 rexlimdva2 3246 rexlimdvaa 3244 rexlimdvv 3252 rexlimdvva 3253 rexlimdvw 3249 rexlimiv 3239 rexlimiva 3240 rexlimivv 3251 |
| [Margaris] p. 90 | Theorem 19.24 | 19.24 1992 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1881 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26 1871 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 2227 r19.27z 4408 r19.27zv 4409 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2228 19.28vv 41090 r19.28z 4401 r19.28zv 4404 rr19.28v 3608 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1874 r19.29d2r 3291 r19.29imd 3218 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1882 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2234 19.31vv 41088 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2233 r19.32 43653 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 41086 19.33 1885 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1993 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35 1878 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36 2230 19.36vv 41087 r19.36zv 4410 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2232 19.37vv 41089 r19.37zv 4405 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1840 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 1991 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1888 19.40 1887 r19.40 3299 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2235 19.41rg 41256 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2236 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1883 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2237 r19.44zv 4407 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2238 r19.45zv 4406 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2671 |
| [Mayet] p. 370 | Remark | jpi 30053 largei 30050 stri 30040 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 29995 ishst 29997 |
| [Mayet3] p. 10 | Theorem | hstrbi 30049 hstri 30048 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 29511 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 29512 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 30061 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 29115 chsupcl 29123 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 30143 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 30137 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 30164 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 37279 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 17701 latj32 17699 latjass 17697 |
| [Megill] p. 444 | Axiom C5 | ax-5 1911 ax5ALT 36203 |
| [Megill] p. 444 | Section 7 | conventions 28185 |
| [Megill] p. 445 | Lemma L12 | aecom-o 36197 ax-c11n 36184 axc11n 2437 |
| [Megill] p. 446 | Lemma L17 | equtrr 2029 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 36192 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 36224 hbnae 2443 |
| [Megill] p. 447 | Remark 9.1 | dfsb1 2499 sbid 2254 sbidd-misc 45245 sbidd 45244 |
| [Megill] p. 448 | Remark 9.6 | axc14 2475 |
| [Megill] p. 448 | Scheme C4' | ax-c4 36180 |
| [Megill] p. 448 | Scheme C5' | ax-c5 36179 sp 2180 |
| [Megill] p. 448 | Scheme C6' | ax-11 2158 |
| [Megill] p. 448 | Scheme C7' | ax-c7 36181 |
| [Megill] p. 448 | Scheme C8' | ax-7 2015 |
| [Megill] p. 448 | Scheme C9' | ax-c9 36186 |
| [Megill] p. 448 | Scheme C10' | ax-6 1970 ax-c10 36182 |
| [Megill] p. 448 | Scheme C11' | ax-c11 36183 |
| [Megill] p. 448 | Scheme C12' | ax-8 2113 |
| [Megill] p. 448 | Scheme C13' | ax-9 2121 |
| [Megill] p. 448 | Scheme C14' | ax-c14 36187 |
| [Megill] p. 448 | Scheme C15' | ax-c15 36185 |
| [Megill] p. 448 | Scheme C16' | ax-c16 36188 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 36200 dral1 2450 dral2-o 36226 dral2 2449 drex1 2452 drex2 2453 drsb1 2513 drsb2 2264 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2165 sbequ 2088 sbid2v 2528 |
| [Megill] p. 450 | Example in Appendix | hba1-o 36193 hba1 2297 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 43485 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3808 rspsbca 3809 stdpc4 2073 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 36180 ra4 3815 stdpc5 2206 |
| [Mendelson] p. 81 | Rule C | exlimiv 1931 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 2035 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 2249 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3719 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 5369 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 4302 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 4303 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 4193 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 4244 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 4194 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 4064 |
| [Mendelson] p. 231 | Definition of union | dfun3 4192 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 5309 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4797 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5419 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4517 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5421 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4824 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5662 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 6088 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 7477 |
| [Mendelson] p. 246 | Definition of successor | df-suc 6165 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 8204 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8664 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8584 xpsneng 8585 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8591 xpcomeng 8592 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8594 |
| [Mendelson] p. 255 | Definition | brsdom 8515 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8587 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 8393 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8572 mapsnend 8571 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8670 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8669 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 8429 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8575 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8588 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 9589 djucomen 9588 |
| [Mendelson] p. 258 | Exercise 4.56(f) | djudom1 9593 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 9587 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 8139 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 8167 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 9970 |
| [Mendelson] p. 281 | Definition | df-r1 9177 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 9226 |
| [Mendelson] p. 287 | Axiom system MK | ru 3719 |
| [MertziosUnger] p. 152 | Definition | df-frgr 28044 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 28079 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 28081 vdgn1frgrv3 28082 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 28083 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 28076 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 28069 2pthfrgrrn 28067 2pthfrgrrn2 28068 |
| [Mittelstaedt] p. 9 | Definition | df-oc 29035 |
| [Monk1] p. 22 | Remark | conventions 28185 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 28185 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 4157 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5621 ssrelf 30379 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5622 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 5093 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 6082 coi2 6083 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5754 rn0 5760 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5967 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5537 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5763 rnxp 5994 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5613 xp0 5982 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5912 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5909 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7603 imaexALTV 35747 imaexg 7602 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5907 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6820 funfvop 6797 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6696 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6706 |
| [Monk1] p. 43 | Theorem 4.6 | funun 6370 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 6991 dff13f 6992 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 6959 funrnex 7637 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 6984 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 6051 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4854 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7688 df-1st 7671 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7689 df-2nd 7672 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 9267 ranksnb 9240 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 9268 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 9269 rankunb 9263 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 9251 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 9177 r1val2 9250 |
| [Monk1] p. 117 | Lemma | zorn2 9917 zorn2g 9914 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 9399 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 9972 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 9394 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1811 |
| [Monk2] p. 105 | Axiom C7 | ax-7 2015 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2175 ax-c15 36185 ax12v2 2177 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 36180 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2158 |
| [Monk2] p. 109 | Lemma 15 | equvini 2466 equvinv 2036 eqvinop 5343 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1911 ax5ALT 36203 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2142 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2158 |
| [Monk2] p. 114 | Lemma 21 | sp 2180 |
| [Monk2] p. 114 | Lemma 22 | axc4 2329 hba1-o 36193 hba1 2297 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2154 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2174 nfra2 3192 nfra2w 3191 |
| [Moore] p. 53 | Part I | df-mre 16849 |
| [Munkres] p. 77 | Example 2 | distop 21600 indistop 21607 indistopon 21606 |
| [Munkres] p. 77 | Example 3 | fctop 21609 fctop2 21610 |
| [Munkres] p. 77 | Example 4 | cctop 21611 |
| [Munkres] p. 78 | Definition of basis | df-bases 21551 isbasis3g 21554 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 16709 tgval2 21561 |
| [Munkres] p. 79 | Remark | tgcl 21574 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 21568 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 21592 tgss3 21591 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 21593 basgen2 21594 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 34766 topdifinfeq 34767 topdifinffin 34765 topdifinfindis 34763 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 21765 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 21643 topcld 21640 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 21644 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 21646 |
| [Munkres] p. 94 | Definition of closure | clsval 21642 |
| [Munkres] p. 94 | Definition of interior | ntrval 21641 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 21680 elcls 21678 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 21688 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 21753 neindisj 21722 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 21755 |
| [Munkres] p. 97 | Definition of limit point | islp2 21750 lpval 21744 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 21920 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 21832 iscn 21840 iscn2 21843 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 21885 cncnp2 21886 cncnpi 21883 df-cnp 21833 iscnp 21842 iscnp2 21844 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 23150 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 23915 |
| [Nathanson] p. 123 | Remark | reprgt 32002 reprinfz1 32003 reprlt 32000 |
| [Nathanson] p. 123 | Definition | df-repr 31990 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 32022 |
| [Nathanson] p. 123 | Proposition | breprexp 32014 breprexpnat 32015 itgexpif 31987 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 29887 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 44328 |
| [Pfenning] p. 17 | Definition XM | natded 28188 |
| [Pfenning] p. 17 | Definition NNC | natded 28188 notnotrd 135 |
| [Pfenning] p. 17 | Definition ` `C | natded 28188 |
| [Pfenning] p. 18 | Rule" | natded 28188 |
| [Pfenning] p. 18 | Definition /\I | natded 28188 |
| [Pfenning] p. 18 | Definition ` `E | natded 28188 natded 28188 natded 28188 natded 28188 natded 28188 |
| [Pfenning] p. 18 | Definition ` `I | natded 28188 natded 28188 natded 28188 natded 28188 natded 28188 |
| [Pfenning] p. 18 | Definition ` `EL | natded 28188 |
| [Pfenning] p. 18 | Definition ` `ER | natded 28188 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 28188 |
| [Pfenning] p. 18 | Definition ` `IR | natded 28188 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 28188 |
| [Pfenning] p. 127 | Definition =E | natded 28188 |
| [Pfenning] p. 127 | Definition =I | natded 28188 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 23807 df-dip 28484 dip0l 28501 ip0l 20325 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 23847 ipval 28486 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 28497 ipcj 20323 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 23810 dipdir 28625 ipdir 20328 ipdiri 28613 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 28493 nmsq 23799 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 28608 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 28610 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 28611 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 23816 dipass 28628 ipass 20334 ipassi 28624 |
| [Prugovecki] p. 186 | Definition of bra | braval 29727 df-bra 29633 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 29634 kbval 29737 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 30165 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 37184 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 30179 atcvat4i 30180 cvrat3 36738 cvrat4 36739 lsatcvat3 36348 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 30065 cvrval 36565 df-cv 30062 df-lcv 36315 lspsncv0 19911 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 37196 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 37197 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2777 rabid 3331 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2281 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2791 |
| [Quine] p. 19 | Definition 2.9 | conventions 28185 df-v 3443 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2922 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2931 abid2f 2984 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2273 |
| [Quine] p. 40 | Theorem 6.2 | sb56 2274 sb6 2090 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2870 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2798 eqid1 28252 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2805 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3721 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3722 dfsbcq2 3723 |
| [Quine] p. 43 | Theorem 6.8 | vex 3444 |
| [Quine] p. 43 | Theorem 6.9 | isset 3453 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3538 spcgv 3543 spcimgf 3536 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3733 spsbcd 3734 |
| [Quine] p. 44 | Theorem 6.12 | elex 3459 |
| [Quine] p. 44 | Theorem 6.13 | elab 3615 elabg 3614 elabgf 3610 |
| [Quine] p. 44 | Theorem 6.14 | noel 4247 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4613 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4528 df-sn 4526 |
| [Quine] p. 49 | Theorem 7.4 | snss 4679 snssg 4678 |
| [Quine] p. 49 | Theorem 7.5 | prss 4713 prssg 4712 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4658 prid1g 4656 prid2 4659 prid2g 4657 snid 4561 snidg 4559 |
| [Quine] p. 51 | Theorem 7.12 | snex 5297 |
| [Quine] p. 51 | Theorem 7.13 | prex 5298 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4820 unisnALT 41632 unisng 4819 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4823 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4830 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4828 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 6297 |
| [Quine] p. 56 | Definition 8.18 | dfaiota2 43643 dfiota2 6284 |
| [Quine] p. 57 | Theorem 8.19 | aiotaval 43650 iotaval 6298 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 6302 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 6304 |
| [Quine] p. 58 | Definition 9.1 | df-op 4532 |
| [Quine] p. 61 | Theorem 9.5 | opabid 5378 opabidw 5377 opelopab 5394 opelopaba 5388 opelopabaf 5396 opelopabf 5397 opelopabg 5390 opelopabga 5385 opelopabgf 5392 oprabid 7167 oprabidw 7166 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5525 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5527 |
| [Quine] p. 64 | Definition 9.15 | df-id 5425 |
| [Quine] p. 65 | Theorem 10.3 | fun0 6389 |
| [Quine] p. 65 | Theorem 10.4 | funi 6356 |
| [Quine] p. 65 | Theorem 10.5 | funsn 6377 funsng 6375 |
| [Quine] p. 65 | Definition 10.1 | df-fun 6326 |
| [Quine] p. 65 | Definition 10.2 | args 5924 dffv4 6642 |
| [Quine] p. 68 | Definition 10.11 | conventions 28185 df-fv 6332 fv2 6640 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13628 nn0opth2i 13627 nn0opthi 13626 omopthi 8267 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 8029 |
| [Quine] p. 232 | Equation i | carddom 9965 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 6411 funimaexg 6410 |
| [Quine] p. 331 | Axiom system NF | ru 3719 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 28867 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 28484 polid 28942 polid2i 28940 polidi 28941 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 28596 |
| [ReedSimon] p. 195 | Remark | lnophm 29802 lnophmi 29801 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 29915 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 29917 leopmuli 29916 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 29920 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 29635 leoppos 29909 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 29919 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 29908 |
| [Roman] p. 4 | Definition | df-dmat 21095 df-dmatalt 44807 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 44499 |
| [Roman] p. 19 | Part Preliminaries | df-ring 19292 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 44894 |
| [Roman] p. 112 | Note | isldepslvec2 44894 ldepsnlinc 44917 zlmodzxznm 44906 |
| [Roman] p. 112 | Example | zlmodzxzequa 44905 zlmodzxzequap 44908 zlmodzxzldep 44913 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 21495 |
| [Rosenlicht] p. 80 | Theorem | heicant 35092 |
| [Rosser] p. 281 | Definition | df-op 4532 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 32026 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 32027 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 44768 pmtr3ncom 18595 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 18591 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 18534 cayleyth 18535 |
| [Rudin] p. 164 | Equation 27 | efcan 15441 |
| [Rudin] p. 164 | Equation 30 | efzval 15447 |
| [Rudin] p. 167 | Equation 48 | absefi 15541 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 200 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1773 |
| [Sanford] p. 39 | Rule 4 | mptxor 1771 |
| [Sanford] p. 40 | Rule 1 | mptnan 1770 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5942 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5945 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5941 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5939 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 16849 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 16850 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 16850 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 16852 |
| [Schechter] p. 139 | Definition AC3 | dfac9 9547 |
| [Schechter] p. 141 | Definition (MC) | dfac11 40006 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 9857 axdc3 9865 |
| [Schechter] p. 187 | Definition of ring with unit | isring 19294 isrngo 35335 |
| [Schechter] p. 276 | Remark 11.6.e | span0 29325 |
| [Schechter] p. 276 | Definition of span | df-span 29092 spanval 29116 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 21598 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 26708 axtgcgrrflx 26256 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 26709 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 26710 axtgcgrid 26257 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 26242 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 26721 axtgsegcon 26258 df-trkgcb 26244 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 26732 axtg5seg 26259 df-trkgcb 26244 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 26733 axtgbtwnid 26260 df-trkgb 26243 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 26735 axtgpasch 26261 df-trkgb 26243 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 26754 df-trkg2d 32046 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 26264 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 26265 df-trkg2d 32046 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 26757 axtgeucl 26266 df-trkge 26245 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 26770 axtgcont 26263 axtgcont1 26262 df-trkgb 26243 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 33561 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 33563 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 33566 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 33570 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 33571 tgcgrcomimp 26271 tgcgrcoml 26273 tgcgrcomr 26272 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 33576 tgcgrtriv 26278 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 33580 tg5segofs 32054 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 32051 df-ofs 33557 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 33582 tgcgrextend 26279 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 33584 tgsegconeq 26280 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 33596 btwntriv2 33586 tgbtwntriv2 26281 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 33587 tgbtwncom 26282 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 33590 tgbtwntriv1 26285 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 33591 tgbtwnswapid 26286 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 33597 btwnintr 33593 tgbtwnexch2 26290 tgbtwnintr 26287 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 33599 btwnexch3 33594 tgbtwnexch 26292 tgbtwnexch3 26288 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 33598 tgbtwnouttr 26291 tgbtwnouttr2 26289 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 26753 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 33601 tgbtwndiff 26300 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 26293 trisegint 33602 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 33618 tgifscgr 26302 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 26352 colrot1 26353 colrot2 26354 lncom 26416 lnrot1 26417 lnrot2 26418 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 33614 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 33619 tgcgrsub 26303 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 33629 tgcgrxfr 26312 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 26311 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 33615 df-cgrg 26305 |
| [Schwabhauser] p. 35 | Definition instead (given | df-cgrg 26305 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 33630 tgbtwnxfr 26324 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 33636 colinearperm2 33638 colinearperm3 33637 colinearperm4 33639 colinearperm5 33640 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 26327 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 33613 tgellng 26347 tglng 26340 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 33641 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 33649 lnxfr 26360 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 33650 lnext 26361 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 33654 tgfscgr 26362 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 33655 lncgr 26363 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 33616 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 33657 lnid 26364 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 33658 tgidinside 26365 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 33675 tgbtwnconn1 26369 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 33676 tgbtwnconn2 26370 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 33677 tgbtwnconn3 26371 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 33683 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 33681 legov 26379 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 26380 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 26393 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 33684 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 33686 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 33688 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 33689 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 33690 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 33687 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 33692 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 26381 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 26383 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 26384 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 26385 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 26386 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 33699 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 33700 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 33695 df-outsideof 33694 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 33696 ishlg 26396 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 26401 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 26403 outsideofrflx 33701 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 26397 hlcomd 26398 outsideofcom 33702 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 26404 outsideoftr 33703 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 26412 outsideofeu 33705 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 33712 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 33713 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 33706 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 33721 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 33722 tglineelsb2 26426 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 33724 linerflx1 33723 linerflx2 33725 tglinecom 26429 tglinerflx1 26427 tglinerflx2 26428 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 33727 tglinethru 26430 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 33711 tglng 26340 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 26388 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 33730 tglinethrueu 26433 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 33731 tglineineq 26437 tglineinteq 26439 tglineintmo 26436 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 26443 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 26444 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 26445 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 26460 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 26456 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 26448 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 26447 ismir 26453 mirbtwn 26452 mircgr 26451 mirfv 26450 mirval 26449 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 26458 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 26459 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 26460 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 26463 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 26464 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 26469 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 26466 mirbtwni 26465 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 26467 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 26479 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 26483 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 26480 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 26481 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 26482 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 26485 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 26486 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 26492 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 26488 israg 26491 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 26493 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 26494 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 26496 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 26497 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 26498 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 26499 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 26500 ragncol 26503 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 26501 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 26507 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 26511 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 26508 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 26490 isperp 26506 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 26509 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 26516 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 26524 colperpexlem2 26525 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 26527 colperpexlem3 26526 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 26532 midex 26531 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 26529 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 26538 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 26533 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 26542 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 26545 opphllem6 26546 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 26548 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 26261 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 26549 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 26557 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 26552 hpgbr 26554 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 26559 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 26558 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 26560 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 26561 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 26562 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 26563 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 26564 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 26578 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 26568 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 26582 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 26583 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 26584 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 26585 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 26586 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 26589 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 26591 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 26569 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 26592 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 26595 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 26596 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 26597 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 26598 trgcopyeu 26600 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 26624 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 26603 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 26612 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 26610 cgrahl2 26611 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 26613 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 26614 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 26616 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 26617 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 26620 cgrahl 26621 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 26625 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 26626 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 26627 acopyeu 26628 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 26635 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 26639 |
| [Schwabhauser] p. 101 | Definition 11.23 | isinag 26632 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 26647 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 26640 isleag 26641 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 26649 tgsas1 26648 tgsas2 26650 tgsas3 26651 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 26653 tgasa1 26652 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 26654 tgsss2 26655 tgsss3 26656 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 25855 dchrsum 25853 dchrsum2 25852 sumdchr 25856 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 25857 sum2dchr 25858 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 19181 ablfacrp2 19182 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 25800 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 25801 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 25808 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 26066 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 26069 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 26123 vmalogdivsum2 26122 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 26113 dirith2 26112 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 26111 rpvmasum 26110 rpvmasum2 26096 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 26071 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 26109 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 26076 dchrisumlem1 26073 dchrisumlem2 26074 dchrisumlem3 26075 dchrisumlema 26072 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 26079 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 26108 dchrmusumlem 26106 dchrvmasumlem 26107 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 26078 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 26080 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 26104 dchrisum0re 26097 dchrisumn0 26105 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 26090 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 26094 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 26095 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 26150 pntrsumbnd2 26151 pntrsumo1 26149 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 26114 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 26116 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 26118 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 26121 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 26126 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 26127 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 26132 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 26134 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 26135 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 26143 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 26144 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 26141 selberg3lem2 26142 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 26145 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 26139 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 26152 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 26153 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 26154 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 26168 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 26180 pntlemb 26181 pntlemc 26179 pntlemd 26178 pntlemg 26182 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 26180 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 26172 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 26177 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 26180 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 26193 pntleml 26195 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 4221 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 4309 dif0 4286 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4395 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4381 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 4212 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 4213 |
| [Stoll] p. 20 | Remark | invdif 4195 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4534 |
| [Stoll] p. 43 | Definition | uniiun 4945 |
| [Stoll] p. 44 | Definition | intiin 4946 |
| [Stoll] p. 45 | Definition | df-iin 4884 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4883 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 405 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 4221 |
| [Strang] p. 242 | Section 6.3 | expgrowth 41039 |
| [Suppes] p. 22 | Theorem 2 | eq0 4258 eq0f 4255 |
| [Suppes] p. 22 | Theorem 4 | eqss 3930 eqssd 3932 eqssi 3931 |
| [Suppes] p. 23 | Theorem 5 | ss0 4306 ss0b 4305 |
| [Suppes] p. 23 | Theorem 6 | sstr 3923 sstrALT2 41541 |
| [Suppes] p. 23 | Theorem 7 | pssirr 4028 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 4029 |
| [Suppes] p. 23 | Theorem 9 | psstr 4032 |
| [Suppes] p. 23 | Theorem 10 | pssss 4023 |
| [Suppes] p. 25 | Theorem 12 | elin 3897 elun 4076 |
| [Suppes] p. 26 | Theorem 15 | inidm 4145 |
| [Suppes] p. 26 | Theorem 16 | in0 4299 |
| [Suppes] p. 27 | Theorem 23 | unidm 4079 |
| [Suppes] p. 27 | Theorem 24 | un0 4298 |
| [Suppes] p. 27 | Theorem 25 | ssun1 4099 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 4107 |
| [Suppes] p. 27 | Theorem 27 | unss 4111 |
| [Suppes] p. 27 | Theorem 28 | indir 4202 |
| [Suppes] p. 27 | Theorem 29 | undir 4203 |
| [Suppes] p. 28 | Theorem 32 | difid 4284 |
| [Suppes] p. 29 | Theorem 33 | difin 4188 |
| [Suppes] p. 29 | Theorem 34 | indif 4196 |
| [Suppes] p. 29 | Theorem 35 | undif1 4382 |
| [Suppes] p. 29 | Theorem 36 | difun2 4387 |
| [Suppes] p. 29 | Theorem 37 | difin0 4380 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4379 |
| [Suppes] p. 29 | Theorem 39 | difundi 4206 |
| [Suppes] p. 29 | Theorem 40 | difindi 4208 |
| [Suppes] p. 30 | Theorem 41 | nalset 5181 |
| [Suppes] p. 39 | Theorem 61 | uniss 4808 |
| [Suppes] p. 39 | Theorem 65 | uniop 5370 |
| [Suppes] p. 41 | Theorem 70 | intsn 4874 |
| [Suppes] p. 42 | Theorem 71 | intpr 4871 intprg 4872 |
| [Suppes] p. 42 | Theorem 73 | op1stb 5328 |
| [Suppes] p. 42 | Theorem 78 | intun 4870 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4920 dfiun2g 4917 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4921 |
| [Suppes] p. 47 | Theorem 86 | elpw 4501 elpw2 5212 elpw2g 5211 elpwg 4500 elpwgdedVD 41623 |
| [Suppes] p. 47 | Theorem 87 | pwid 4521 |
| [Suppes] p. 47 | Theorem 89 | pw0 4705 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4706 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5534 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5668 xpindir 5669 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5584 xpundir 5585 |
| [Suppes] p. 54 | Theorem 105 | elirrv 9044 |
| [Suppes] p. 58 | Theorem 2 | relss 5620 |
| [Suppes] p. 59 | Theorem 4 | eldm 5733 eldm2 5734 eldm2g 5732 eldmg 5731 |
| [Suppes] p. 59 | Definition 3 | df-dm 5529 |
| [Suppes] p. 60 | Theorem 6 | dmin 5744 |
| [Suppes] p. 60 | Theorem 8 | rnun 5971 |
| [Suppes] p. 60 | Theorem 9 | rnin 5972 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5723 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5717 brcnvg 5714 |
| [Suppes] p. 62 | Equation 5 | elcnv 5711 elcnv2 5712 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5934 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5970 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5968 |
| [Suppes] p. 63 | Definition | dftrrels2 35971 |
| [Suppes] p. 63 | Theorem 20 | co02 6080 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5807 |
| [Suppes] p. 63 | Definition 7 | df-co 5528 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5720 |
| [Suppes] p. 64 | Theorem 27 | coass 6085 |
| [Suppes] p. 65 | Theorem 31 | resundi 5832 |
| [Suppes] p. 65 | Theorem 34 | elima 5901 elima2 5902 elima3 5903 elimag 5900 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5975 |
| [Suppes] p. 66 | Theorem 40 | dminss 5977 |
| [Suppes] p. 66 | Theorem 41 | imainss 5978 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5981 |
| [Suppes] p. 81 | Definition 34 | dfec2 8275 |
| [Suppes] p. 82 | Theorem 72 | elec 8316 elecALTV 35687 elecg 8315 |
| [Suppes] p. 82 | Theorem 73 | eqvrelth 36006 erth 8321 erth2 8322 |
| [Suppes] p. 83 | Theorem 74 | eqvreldisj 36009 erdisj 8324 |
| [Suppes] p. 89 | Theorem 96 | map0b 8430 |
| [Suppes] p. 89 | Theorem 97 | map0 8434 map0g 8431 |
| [Suppes] p. 89 | Theorem 98 | mapsn 8435 mapsnd 8433 |
| [Suppes] p. 89 | Theorem 99 | mapss 8436 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 9479 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 9478 |
| [Suppes] p. 92 | Theorem 1 | enref 8525 enrefg 8524 |
| [Suppes] p. 92 | Theorem 2 | ensym 8541 ensymb 8540 ensymi 8542 |
| [Suppes] p. 92 | Theorem 3 | entr 8544 |
| [Suppes] p. 92 | Theorem 4 | unen 8579 |
| [Suppes] p. 94 | Theorem 15 | endom 8519 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8538 |
| [Suppes] p. 94 | Theorem 17 | domtr 8545 |
| [Suppes] p. 95 | Theorem 18 | sbth 8621 |
| [Suppes] p. 97 | Theorem 23 | canth2 8654 canth2g 8655 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8625 df-sdom 8495 dfsdom2 8624 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8638 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8627 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8626 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8636 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 8522 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8639 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8634 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8566 fundmeng 8567 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8598 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8635 |
| [Suppes] p. 104 | Theorem 37 | fofi 8794 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8803 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8803 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 9962 |
| [Suppes] p. 130 | Definition 3 | df-tr 5137 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 7481 |
| [Suppes] p. 134 | Definition 6 | df-suc 6165 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7593 finds 7589 finds1 7592 finds2 7591 |
| [Suppes] p. 151 | Theorem 42 | isfinite 9099 isfinite2 8760 isfiniteg 8762 unbnn 8758 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 10329 df-ltpq 10321 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7557 tfinds 7554 tfinds2 7558 |
| [Suppes] p. 209 | Theorem 18 | oaord1 8160 |
| [Suppes] p. 209 | Theorem 21 | oaword2 8162 |
| [Suppes] p. 211 | Theorem 25 | oaass 8170 |
| [Suppes] p. 225 | Definition 8 | iscard2 9389 |
| [Suppes] p. 227 | Theorem 56 | ondomon 9974 |
| [Suppes] p. 228 | Theorem 59 | harcard 9391 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 9477 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 6209 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 7493 onminsb 7494 |
| [Suppes] p. 229 | Theorem 64 | alephval2 9983 |
| [Suppes] p. 229 | Theorem 65 | alephcard 9481 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 9488 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 9482 |
| [Suppes] p. 229 | Definition 12 | df-aleph 9353 |
| [Suppes] p. 242 | Theorem 6 | weth 9906 |
| [Suppes] p. 242 | Theorem 8 | entric 9968 |
| [Suppes] p. 242 | Theorem 9 | carden 9962 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2770 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2791 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2870 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2793 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2818 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 7139 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3719 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 5287 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4548 elpr2 4550 elpr2g 4549 elprg 4546 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4540 elsn2 4564 elsn2g 4563 elsng 4539 velsn 4541 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 5324 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4535 sneqr 4731 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4544 dfsn2 4538 dfsn2ALT 4545 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 7447 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 5333 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 5321 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 5306 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 7449 unexg 7452 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4587 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4801 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3888 df-un 3886 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4817 uniprg 4818 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 5243 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4586 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 6228 elsucg 6226 sstr2 3922 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 4080 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 4128 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 4093 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 4146 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 4200 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 4201 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3900 dfss2 3901 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4499 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 4108 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3898 sseqin2 4142 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3937 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 4155 inss2 4156 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 3977 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4811 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 5307 sspwimp 41624 sspwimpALT 41631 sspwimpALT2 41634 sspwimpcf 41626 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 5314 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 5154 |
| [TakeutiZaring] p. 20 | Definition | df-rab 3115 df-wl-rab 35025 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 5175 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3884 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 4245 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 4284 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 4260 n0f 4257 neq0 4259 neq0f 4256 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 9043 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 9158 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 9160 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3443 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 5183 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 4304 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 5189 ssexg 5191 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 5185 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 9050 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 9045 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 4277 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 4058 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 4215 undif3VD 41588 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 4059 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 4066 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 3111 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 3112 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 7456 xpexg 7453 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5526 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 6395 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6559 fun11 6398 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 6336 svrelfun 6396 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5722 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5724 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5531 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5532 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5528 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 6018 dfrel2 6013 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5535 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5648 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5655 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5667 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5847 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5824 opelresi 5826 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5840 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5843 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5848 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 6366 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 6064 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 6364 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6560 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2670 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 28185 df-fv 6332 fv3 6663 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7612 cnvexg 7611 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7598 dmexg 7594 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7599 rnexg 7595 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 41158 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7607 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6658 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 43730 tz6.12-1-afv2 43797 tz6.12-1 6667 tz6.12-afv 43729 tz6.12-afv2 43796 tz6.12 6668 tz6.12c-afv2 43798 tz6.12c 6670 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2-afv2 43793 tz6.12-2 6635 tz6.12i-afv2 43799 tz6.12i 6671 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 6327 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 6328 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 6330 wfo 6322 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 6329 wf1 6321 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 6331 wf1o 6323 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6779 eqfnfv2 6780 eqfnfv2f 6783 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6736 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 6957 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 6955 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 6411 funimaexg 6410 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 5031 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5439 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5484 dffr3 5929 eliniseg 5925 iniseg 5927 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5430 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5497 fr3nr 7474 frirr 5496 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5478 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 7476 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5486 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5506 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 6147 tz6.26i 6148 wefrc 5513 wereu2 5516 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 6149 wfii 6150 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 6333 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 7061 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 7062 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 7068 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 7069 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 7070 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 7074 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 7081 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 7083 |
| [TakeutiZaring] p. 35 | Notation | wtr 5136 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 41159 tz7.2 5503 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 5140 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 6172 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 6180 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 6181 ordelordALT 41243 ordelordALTVD 41573 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 6187 ordelssne 6186 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 6185 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 6189 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 7483 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 7484 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 6163 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 6191 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 41255 ordon 7478 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 7479 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7548 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 6206 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 5138 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 7492 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7526 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 6260 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 6259 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 7480 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4830 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 6165 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 6236 sucidg 6237 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7508 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 6250 ordnbtwn 6249 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7523 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 6164 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7574 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7579 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7536 ordelsuc 7515 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7517 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7546 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7562 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7581 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7582 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7583 |
| [TakeutiZaring] p. 43 | Remark | omon 7571 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 9082 omex 9090 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7569 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7587 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7584 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7585 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7565 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4852 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 5153 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4853 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 5204 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7495 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 6208 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4839 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 9107 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 7490 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 7995 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 8016 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 8017 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 8018 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 8025 tz7.44-2 8026 tz7.44-3 8027 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 7987 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 7982 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 7966 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 8064 tz7.49c 8065 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 8062 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 8061 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 8063 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2717 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 9422 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 9423 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 8140 oasuc 8132 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7555 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 8143 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 8124 oa0r 8146 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 8144 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 8157 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 8228 nnaordi 8227 oaord 8156 oaordi 8155 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4936 uniss2 4833 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 8159 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 8164 oawordex 8166 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 8220 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 8254 |
| [TakeutiZaring] p. 60 | Remark | oancom 9098 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 8169 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 8225 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 8161 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0x 8127 omlim 8141 omsuc 8134 |
| [TakeutiZaring] p. 62 | Definition 8.15(a) | om0 8125 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 8222 nnmcl 8221 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 8241 nnmordi 8240 omord 8177 omordi 8175 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 8178 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 8245 omwordri 8181 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 8147 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 8151 om1r 8152 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 8184 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 8186 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 8187 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 8188 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 8189 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 8217 oe0 8130 oelim 8142 oesuc 8135 onesuc 8138 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 8128 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 8195 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 8196 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 8129 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 8154 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 8197 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 8203 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 8201 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 8202 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 8206 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 8208 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 9154 tz9.1 9155 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 9177 r10 9181 r1lim 9185 r1limg 9184 r1suc 9183 r1sucg 9182 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 9193 r1ord2 9194 r1ordg 9191 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 9203 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 9228 tz9.13 9204 tz9.13g 9205 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 9178 rankval 9229 rankvalb 9210 rankvalg 9230 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 9252 rankelb 9237 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 9266 rankval3 9253 rankval3b 9239 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 9242 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 9208 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 9247 rankr1c 9234 rankr1g 9245 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 9248 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 9262 rankssb 9261 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 9255 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 9254 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 9886 dfac3 9532 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 9441 numth 9883 numth2 9882 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 9957 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 9958 cardid2 9366 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 9373 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 9962 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 9372 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 9357 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 9378 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 9370 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8674 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8555 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8679 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8602 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 9376 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 9509 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8684 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 8693 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 9510 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8689 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 9499 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 9477 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 9385 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9628 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 8776 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 8496 isfi 8516 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 8694 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 9945 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8595 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 9937 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | djuxpdom 9596 unxpdom 8709 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 9387 cardsdomelir 9386 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 8711 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 9425 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 8391 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 9973 infxpidm2 9428 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infdju 9619 infxp 9626 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8607 pw2f1o 8605 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8667 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 9898 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 9893 ac6s5 9902 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 9954 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 9955 uniimadomf 9956 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 9685 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 9680 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 9665 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 9662 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 9668 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 9675 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 9684 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 9993 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 9663 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 9687 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 9508 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 9507 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 9519 alephfp2 9520 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 10110 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 9523 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 9980 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 9994 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 9995 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 36179 |
| [Tarski] p. 67 | Scheme B5 | sp 2180 |
| [Tarski] p. 68 | Lemma 6 | avril1 28248 equid 2019 |
| [Tarski] p. 69 | Lemma 7 | equcomi 2024 |
| [Tarski] p. 70 | Lemma 14 | spim 2394 spime 2396 spimew 1974 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2175 ax-c15 36185 ax12i 1969 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2090 |
| [Tarski] p. 75 | Axiom B7 | ax6v 1971 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1911 ax5ALT 36203 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 2015 ax-8 2113 ax-9 2121 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 26258 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 26259 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 26261 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 26261 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 26262 |
| [Truss] p. 114 | Theorem 5.18 | ruc 15588 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 35096 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 35098 |
| [Weierstrass] p. 272 | Definition | df-mdet 21190 mdetuni 21227 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 901 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 865 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 866 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 917 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 965 |
| [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 34862 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 40501 imim2 58 wl-luk-imim2 34857 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | adh-minimp-imim1 43612 imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 894 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2725 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 900 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-luk-id 34860 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 892 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 144 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 895 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 132 notnotrALT2 41633 wl-luk-notnotr 34861 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 148 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 40531 axfrege28 40530 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 864 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 922 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 123 wl-luk-pm2.21 34854 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 124 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 887 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 937 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-labels 28186 pm2.27 42 wl-luk-pm2.27 34852 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 920 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 921 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 967 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 968 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 966 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1085 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 904 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 905 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 940 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 879 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 880 |
| [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 881 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 882 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 883 |
| [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 848 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 849 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 886 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 888 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 195 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 897 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 938 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 939 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 196 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 889 pm2.67 890 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 179 pm2.521g 177 pm2.521g2 178 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 896 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 970 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 898 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 206 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 971 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 972 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 931 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 929 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 969 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 973 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 930 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 109 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 989 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 473 pm3.2im 163 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 990 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 991 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 992 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 993 |
| [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 802 |
| [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 764 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 765 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 807 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 624 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 809 |
| [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 958 pm3.44 957 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 808 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 477 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 961 |
| [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 806 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 831 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 225 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 805 bitr 804 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 567 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 902 pm4.25 903 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 464 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 1005 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 867 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 472 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 919 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 634 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 915 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 637 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 974 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1086 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 1003 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1049 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 1020 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 994 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 996 pm4.45 995 pm4.45im 826 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 980 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 850 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 549 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 979 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 982 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 983 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 984 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 985 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 981 pm4.56 986 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 987 pm4.57 988 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 408 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 853 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 401 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 846 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 409 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 847 |
| [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 947 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 531 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 934 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 521 pm4.76 522 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 959 pm4.77 960 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 932 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 1001 |
| [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 1021 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 1022 |
| [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 840 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 822 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 942 pm5.11g 941 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 943 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 945 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 944 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 1010 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 1011 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 1009 |
| [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 823 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 1012 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 1045 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 1046 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 899 |
| [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 999 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 951 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 829 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 577 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 834 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 824 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 832 |
| [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 1002 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 1015 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 946 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 998 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 1016 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 1017 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 1025 |
| [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 1026 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 41062 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 41063 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1871 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 41064 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 41065 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 41066 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1894 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 41067 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 41068 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 41069 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 41070 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 41071 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 41073 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 41074 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 41075 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 41072 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2097 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 41078 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 41079 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2075 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2161 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1830 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1831 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 41080 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 41081 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 41082 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 41083 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 41085 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 41084 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1888 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 41087 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 41088 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 41086 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1829 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 41089 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 41090 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1847 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 41091 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2356 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 1861 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 41096 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 41092 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 41093 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 41094 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 41095 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 41100 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 41097 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 41098 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 41099 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 41101 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2629 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 41111 pm13.13b 41112 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 41113 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 3068 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 3069 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3606 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 41119 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 41120 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 41114 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 41258 pm13.193 41115 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 41116 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 41117 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 41118 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 41125 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 41124 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 41123 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3783 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 41126 pm14.122b 41127 pm14.122c 41128 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 41129 pm14.123b 41130 pm14.123c 41131 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 41133 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 41132 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 41134 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 6305 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 41135 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 6306 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 41136 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 41138 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2695 eupickbi 2698 sbaniota 41139 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 41137 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 2644 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 41141 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 28185 df-fv 6332 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 9414 pm54.43lem 9413 |
| [Young] p. 141 | Definition of operator ordering | leop2 29907 |
| [Young] p. 142 | Example 12.2(i) | 0leop 29913 idleop 29914 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 39769 |
| [vandenDries] p. 43 | Theorem 62 | pellex 39776 pellexlem1 39770 |