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 16941 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 16941 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 17338 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 16961 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 16984 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 17053 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 17041 invisoinvl 17062 |
| [Adamek] p. 28 | Example 3.13 | idinv 17061 idiso 17060 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 17046 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 17020 df-iso 17021 dfiso2 17044 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 17027 |
| [Adamek] p. 29 | Remark 3.16 | cicer 17078 |
| [Adamek] p. 29 | Definition 3.15 | cic 17071 df-cic 17068 |
| [Adamek] p. 29 | Definition 3.17 | df-func 17130 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 17042 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 17043 isoco 17049 |
| [Adamek] p. 30 | Remark 3.19 | df-func 17130 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 17153 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 17146 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 17160 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 17369 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 17419 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 17177 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 17176 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 17419 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 17201 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 17207 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 17206 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 17404 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 17404 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 17147 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 17357 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 17195 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 17194 |
| [Adamek] p. 40 | Remark 3.48 | catccat 17366 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 17357 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 17110 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 17111 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 17122 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 17084 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 17210 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 17215 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 17236 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 17240 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 17216 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 17242 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 17253 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 44347 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 17254 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 17274 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 17278 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 17255 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 44350 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 17281 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 17019 |
| [Adamek] p. 185 | Section 10.67 | updjud 9365 |
| [Adamek] p. 478 | Item Rng | df-ringc 44283 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 44615 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 44637 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 13925 df-pfx 14035 df-substr 14005 df-word 13865 lencl 13885 wrd0 13891 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 23319 df-nmoo 28524 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 29932 hmopidmchi 29930 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 29980 pjcmul2i 29981 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 29697 unoplin 29699 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 29698 unopadj2 29717 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 29792 lnopunii 29791 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 29865 |
| [Apostol] p. 18 | Theorem I.1 | addcan 10826 addcan2d 10846 addcan2i 10836 addcand 10845 addcani 10835 |
| [Apostol] p. 18 | Theorem I.2 | negeu 10878 |
| [Apostol] p. 18 | Theorem I.3 | negsub 10936 negsubd 11005 negsubi 10966 |
| [Apostol] p. 18 | Theorem I.4 | negneg 10938 negnegd 10990 negnegi 10958 |
| [Apostol] p. 18 | Theorem I.5 | subdi 11075 subdid 11098 subdii 11091 subdir 11076 subdird 11099 subdiri 11092 |
| [Apostol] p. 18 | Theorem I.6 | mul01 10821 mul01d 10841 mul01i 10832 mul02 10820 mul02d 10840 mul02i 10831 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 11279 mulcan2d 11276 mulcand 11275 mulcani 11281 |
| [Apostol] p. 18 | Theorem I.8 | receu 11287 xreceu 30600 |
| [Apostol] p. 18 | Theorem I.9 | divrec 11316 divrecd 11421 divreci 11387 divreczi 11380 |
| [Apostol] p. 18 | Theorem I.10 | recrec 11339 recreci 11374 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 11282 mul0ord 11292 mul0ori 11290 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 11081 mul2negd 11097 mul2negi 11090 mulneg1 11078 mulneg1d 11095 mulneg1i 11088 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 11357 divadddivd 11462 divadddivi 11404 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 11342 divmuldivd 11459 divmuldivi 11402 rdivmuldivd 30864 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 11343 divdivdivd 11465 divdivdivi 11405 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 12414 rpaddcld 12449 rpmulcl 12415 rpmulcld 12450 |
| [Apostol] p. 20 | Axiom 8 | rpneg 12424 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 12427 |
| [Apostol] p. 20 | Theorem I.17 | lttri 10768 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 11235 ltadd1dd 11253 ltadd1i 11196 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 11492 ltmul1a 11491 ltmul1i 11560 ltmul1ii 11570 ltmul2 11493 ltmul2d 12476 ltmul2dd 12490 ltmul2i 11563 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 11162 msqgt0d 11209 msqgt0i 11179 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 11164 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 11148 lt0neg1d 11211 ltneg 11142 ltnegd 11220 ltnegi 11186 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 11127 lt2addd 11265 lt2addi 11204 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 12393 |
| [Apostol] p. 21 | Exercise 4 | recgt0 11488 recgt0d 11576 recgt0i 11547 recgt0ii 11548 |
| [Apostol] p. 22 | Definition of integers | df-z 11985 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11654 |
| [Apostol] p. 22 | Definition of rationals | df-q 12352 |
| [Apostol] p. 24 | Theorem I.26 | supeu 8920 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 11896 |
| [Apostol] p. 26 | Theorem I.29 | arch 11897 |
| [Apostol] p. 28 | Exercise 2 | btwnz 12087 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 11898 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 12350 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 12349 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12595 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 15690 zneo 12068 zneoALTV 43841 |
| [Apostol] p. 29 | Theorem I.35 | cxpsqrtth 25314 msqsqrtd 14802 resqrtth 14617 sqrtth 14726 sqrtthi 14732 sqsqrtd 14801 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11643 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 12316 |
| [Apostol] p. 361 | Remark | crreczi 13592 |
| [Apostol] p. 363 | Remark | absgt0i 14761 |
| [Apostol] p. 363 | Example | abssubd 14815 abssubi 14765 |
| [ApostolNT] p. 7 | Remark | fmtno0 43709 fmtno1 43710 fmtno2 43719 fmtno3 43720 fmtno4 43721 fmtno5fac 43751 fmtnofz04prm 43746 |
| [ApostolNT] p. 7 | Definition | df-fmtno 43697 |
| [ApostolNT] p. 8 | Definition | df-ppi 25679 |
| [ApostolNT] p. 14 | Definition | df-dvds 15610 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 15625 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 15648 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15644 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15638 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15640 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 15626 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 15627 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15632 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 15663 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 15665 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 15667 |
| [ApostolNT] p. 15 | Definition | df-gcd 15846 dfgcd2 15896 |
| [ApostolNT] p. 16 | Definition | isprm2 16028 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 15999 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 16253 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 15864 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 15897 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 15899 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 15878 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 15870 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 16057 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 16059 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 16266 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 16260 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 15756 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 15933 |
| [ApostolNT] p. 24 | Definition | df-mu 25680 |
| [ApostolNT] p. 25 | Definition | df-phi 16105 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 25770 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 16129 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 16115 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 16119 |
| [ApostolNT] p. 32 | Definition | df-vma 25677 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 25772 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 25794 |
| [ApostolNT] p. 38 | Remark | df-sgm 25681 |
| [ApostolNT] p. 38 | Definition | df-sgm 25681 |
| [ApostolNT] p. 75 | Definition | df-chp 25678 df-cht 25676 |
| [ApostolNT] p. 104 | Definition | congr 16010 |
| [ApostolNT] p. 106 | Remark | dvdsval3 15613 |
| [ApostolNT] p. 106 | Definition | moddvds 15620 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 15697 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 15698 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 13259 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 13296 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 13602 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15643 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 16013 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 16412 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 16015 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 16122 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 16140 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 16123 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 25651 |
| [ApostolNT] p. 179 | Definition | df-lgs 25873 lgsprme0 25917 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 25918 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 25894 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 25909 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 25966 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 25985 2lgsoddprm 25994 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 25952 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 25961 |
| [ApostolNT] p. 188 | Definition | df-lgs 25873 lgs1 25919 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 25910 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 25912 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 25920 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 25921 |
| [Baer] p. 40 | Property (b) | mapdord 38776 |
| [Baer] p. 40 | Property (c) | mapd11 38777 |
| [Baer] p. 40 | Property (e) | mapdin 38800 mapdlsm 38802 |
| [Baer] p. 40 | Property (f) | mapd0 38803 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 38763 mapd1o 38786 |
| [Baer] p. 41 | Property (g) | mapdat 38805 |
| [Baer] p. 44 | Part (1) | mapdpg 38844 |
| [Baer] p. 45 | Part (2) | hdmap1eq 38939 mapdheq 38866 mapdheq2 38867 mapdheq2biN 38868 |
| [Baer] p. 45 | Part (3) | baerlem3 38851 |
| [Baer] p. 46 | Part (4) | mapdheq4 38870 mapdheq4lem 38869 |
| [Baer] p. 46 | Part (5) | baerlem5a 38852 baerlem5abmN 38856 baerlem5amN 38854 baerlem5b 38853 baerlem5bmN 38855 |
| [Baer] p. 47 | Part (6) | hdmap1l6 38959 hdmap1l6a 38947 hdmap1l6e 38952 hdmap1l6f 38953 hdmap1l6g 38954 hdmap1l6lem1 38945 hdmap1l6lem2 38946 mapdh6N 38885 mapdh6aN 38873 mapdh6eN 38878 mapdh6fN 38879 mapdh6gN 38880 mapdh6lem1N 38871 mapdh6lem2N 38872 |
| [Baer] p. 48 | Part 9 | hdmapval 38966 |
| [Baer] p. 48 | Part 10 | hdmap10 38978 |
| [Baer] p. 48 | Part 11 | hdmapadd 38981 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 38955 mapdh6hN 38881 |
| [Baer] p. 48 | Part (7) | mapdh75cN 38891 mapdh75d 38892 mapdh75e 38890 mapdh75fN 38893 mapdh7cN 38887 mapdh7dN 38888 mapdh7eN 38886 mapdh7fN 38889 |
| [Baer] p. 48 | Part (8) | mapdh8 38926 mapdh8a 38913 mapdh8aa 38914 mapdh8ab 38915 mapdh8ac 38916 mapdh8ad 38917 mapdh8b 38918 mapdh8c 38919 mapdh8d 38921 mapdh8d0N 38920 mapdh8e 38922 mapdh8g 38923 mapdh8i 38924 mapdh8j 38925 |
| [Baer] p. 48 | Part (9) | mapdh9a 38927 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 38907 |
| [Baer] p. 49 | Part 12 | hdmap11 38986 hdmapeq0 38982 hdmapf1oN 39003 hdmapneg 38984 hdmaprnN 39002 hdmaprnlem1N 38987 hdmaprnlem3N 38988 hdmaprnlem3uN 38989 hdmaprnlem4N 38991 hdmaprnlem6N 38992 hdmaprnlem7N 38993 hdmaprnlem8N 38994 hdmaprnlem9N 38995 hdmapsub 38985 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 39006 hdmap14lem10 39015 hdmap14lem1a 39004 hdmap14lem2N 39007 hdmap14lem2a 39005 hdmap14lem3 39008 hdmap14lem8 39013 hdmap14lem9 39014 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 39016 hdmap14lem12 39017 hdmap14lem13 39018 hdmap14lem14 39019 hdmap14lem15 39020 hgmapval 39025 |
| [Baer] p. 50 | Part 15 | hgmapadd 39032 hgmapmul 39033 hgmaprnlem2N 39035 hgmapvs 39029 |
| [Baer] p. 50 | Part 16 | hgmaprnN 39039 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 39055 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 39056 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 39057 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 39058 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 39060 hgmapvv 39064 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 39059 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 39061 |
| [Baer] p. 111 | Line 15 | hdmapg 39068 hdmapglem7 39067 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 25315 2irrexpqALT 25380 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2654 |
| [BellMachover] p. 460 | Notation | df-mo 2622 |
| [BellMachover] p. 460 | Definition | mo3 2648 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2795 |
| [BellMachover] p. 462 | Theorem 1.1 | axextmo 2799 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 5198 |
| [BellMachover] p. 463 | Scheme Sep | ax-sep 5205 |
| [BellMachover] p. 463 | Theorem 1.3(ii) | bj-bm1.3ii 34359 bm1.3ii 5208 |
| [BellMachover] p. 466 | Problem | axpow2 5270 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 5271 |
| [BellMachover] p. 466 | Axiom Union | axun2 7465 |
| [BellMachover] p. 468 | Definition | df-ord 6196 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 6211 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 6218 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 6213 |
| [BellMachover] p. 471 | Definition of N | df-om 7583 |
| [BellMachover] p. 471 | Problem 2.5(ii) | uniordint 7523 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 6198 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 9107 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7597 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 9195 |
| [BellMachover] p. 478 | Definition | rankval2 9249 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 9213 r1ord3g 9210 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 9061 |
| [BellMachover] p. 488 | Axiom AC | ac5 9901 dfac4 9550 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 9538 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 36457 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 30132 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 30174 chirredi 30173 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 30162 |
| [Beran] p. 3 | Definition of join | sshjval3 29133 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 29395 cmcm2i 29372 cmcm2ii 29377 cmt2N 36388 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 29396 lecmi 29381 lecmii 29382 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 29370 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 29399 cm2ji 29404 cm2mi 29405 |
| [Beran] p. 95 | Definition | df-sh 28986 issh2 28988 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 28865 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 28878 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 28869 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 29607 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 29609 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 29608 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 29610 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 28861 his1i 28879 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 28862 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 28863 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 28864 |
| [Beran] p. 96 | Definition of norm | df-hnorm 28747 dfhnorm2 28901 normval 28903 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 28963 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 28752 |
| [Beran] p. 96 | Definition of complete subspace | isch3 29020 |
| [Beran] p. 96 | Definition of converge | df-hlim 28751 hlimi 28967 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 28912 norm-i 28908 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 28916 norm-ii 28917 normlem0 28888 normlem1 28889 normlem2 28890 normlem3 28891 normlem4 28892 normlem5 28893 normlem6 28894 normlem7 28895 normlem7tALT 28898 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 28918 norm-iii 28919 |
| [Beran] p. 98 | Remark 3.4 | bcs 28960 bcsiALT 28958 bcsiHIL 28959 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 28900 normpar 28934 normpari 28933 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 28925 normpyth 28924 normpythi 28921 |
| [Beran] p. 99 | Remark | lnfn0 29826 lnfn0i 29821 lnop0 29745 lnop0i 29749 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 29805 nmcfnex 29832 nmcfnexi 29830 nmcopex 29808 nmcopexi 29806 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 29833 nmcfnlbi 29831 nmcoplb 29809 nmcoplbi 29807 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 29835 lnfnconi 29834 lnopcon 29814 lnopconi 29813 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 28935 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 28932 norm3adifii 28927 norm3dif 28929 norm3difi 28926 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 29080 pjhth 29172 pjhtheu 29173 pjpjhth 29204 pjpjhthi 29205 pjth 24044 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 29185 ococi 29184 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 29840 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 29841 riesz4 29843 riesz4i 29842 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 29858 cnlnadjeu 29857 cnlnadjeui 29856 cnlnadji 29855 cnlnadjlem1 29846 nmopadjlei 29867 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 29870 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 29869 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 29871 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 29715 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 29881 nmopcoadji 29880 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 29872 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 29882 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 29879 pjadj2coi 29983 pjadjcoi 29940 |
| [Beran] p. 107 | Definition | df-ch 29000 isch2 29002 |
| [Beran] p. 107 | Remark 3.12 | choccl 29085 isch3 29020 occl 29083 ocsh 29062 shoccl 29084 shocsh 29063 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 29187 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 29111 |
| [Beran] p. 109 | Property (i) | pjadj2 29966 pjadj3 29967 pjadji 29464 pjadjii 29453 |
| [Beran] p. 109 | Property (ii) | pjidmco 29960 pjidmcoi 29956 pjidmi 29452 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 29952 |
| [Beran] p. 111 | Remark | ho0val 29529 pjch1 29449 |
| [Beran] p. 111 | Definition | df-hfmul 29513 df-hfsum 29512 df-hodif 29511 df-homul 29510 df-hosum 29509 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 29450 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 29473 pjchi 29211 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 29218 pjoc2i 29217 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 29459 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 29944 pjssmii 29460 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 29943 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 29942 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 29947 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 29945 pjssge0ii 29461 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 29946 pjdifnormii 29462 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1777 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1775 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1778 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1773 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 31552 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 31560 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 31558 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 31562 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 31582 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 31613 df-sitm 31591 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 31613 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 31590 |
| [Bollobas] p. 1 | Section I.1 | df-edg 26835 isuhgrop 26857 isusgrop 26949 isuspgrop 26948 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 27052 uhgrspan1 27087 uhgrspansubgr 27075 |
| [Bollobas] p. 3 | Definition | isomuspgr 44006 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 27238 df-cusgr 27196 df-nbgr 27117 fusgrmaxsize 27248 |
| [Bollobas] p. 4 | Definition | df-upwlks 44016 df-wlks 27383 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 27334 finsumvtxdgeven 27336 fusgr1th 27335 fusgrvtxdgonume 27338 vtxdgoddnumeven 27337 |
| [Bollobas] p. 5 | Notation | df-pths 27499 |
| [Bollobas] p. 5 | Definition | df-crcts 27569 df-cycls 27570 df-trls 27476 df-wlkson 27384 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 26846 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 44114 df-cllaw 44100 df-mgm 17854 df-mgm2 44133 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 44115 df-asslaw 44102 df-sgrp 17903 df-sgrp2 44135 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 44134 df-comlaw 44101 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 17914 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 19301 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 44153 |
| [BourbakiEns] p. | Proposition 8 | fcof1 7045 fcofo 7046 |
| [BourbakiTop1] p. | Remark | xnegmnf 12606 xnegpnf 12605 |
| [BourbakiTop1] p. | Remark | rexneg 12607 |
| [BourbakiTop1] p. | Remark 3 | ust0 22830 ustfilxp 22823 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 22700 |
| [BourbakiTop1] p. | Criterion | ishmeo 22369 |
| [BourbakiTop1] p. | Example 1 | cstucnd 22895 iducn 22894 snfil 22474 |
| [BourbakiTop1] p. | Example 2 | neifil 22490 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 22677 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 22915 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 31202 |
| [BourbakiTop1] p. | Paragraph 3 | infil 22473 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 22887 df-ust 22811 filintn0 22471 filn0 22472 istgp 22687 ucnprima 22893 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 22898 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 22909 df-usp 22868 df-utop 22842 trust 22840 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 31122 |
| [BourbakiTop1] p. | Property V_i | ssnei2 21726 |
| [BourbakiTop1] p. | Theorem 1(d) | iscncl 21879 |
| [BourbakiTop1] p. | Condition F_I | ustssel 22816 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 22819 |
| [BourbakiTop1] p. | Property V_ii | innei 21735 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 21743 neissex 21737 |
| [BourbakiTop1] p. | Proposition 1 | neips 21723 neiss 21719 ucncn 22896 ustund 22832 ustuqtop 22857 |
| [BourbakiTop1] p. | Proposition 2 | cnpco 21877 neiptopreu 21743 utop2nei 22861 utop3cls 22862 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 22903 uspreg 22885 utopreg 22863 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 22301 imasncls 22302 imasnopn 22300 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 22610 |
| [BourbakiTop1] p. | Condition F_II | ustincl 22818 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 22820 |
| [BourbakiTop1] p. | Property V_iii | elnei 21721 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 22914 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 22817 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 22821 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 21997 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 22456 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 21504 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 31119 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 42354 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 42356 stoweid 42355 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 42293 stoweidlem10 42302 stoweidlem14 42306 stoweidlem15 42307 stoweidlem35 42327 stoweidlem36 42328 stoweidlem37 42329 stoweidlem38 42330 stoweidlem40 42332 stoweidlem41 42333 stoweidlem43 42335 stoweidlem44 42336 stoweidlem46 42338 stoweidlem5 42297 stoweidlem50 42342 stoweidlem52 42344 stoweidlem53 42345 stoweidlem55 42347 stoweidlem56 42348 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 42315 stoweidlem24 42316 stoweidlem27 42319 stoweidlem28 42320 stoweidlem30 42322 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 42326 stoweidlem59 42351 stoweidlem60 42352 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 42337 stoweidlem49 42341 stoweidlem7 42299 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 42323 stoweidlem39 42331 stoweidlem42 42334 stoweidlem48 42340 stoweidlem51 42343 stoweidlem54 42346 stoweidlem57 42349 stoweidlem58 42350 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 42317 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 42309 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 42303 stoweidlem13 42305 stoweidlem26 42318 stoweidlem61 42353 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 42310 |
| [Bruck] p. 1 | Section I.1 | df-clintop 44114 df-mgm 17854 df-mgm2 44133 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 17903 df-sgrp2 44135 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 18200 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 5149 |
| [Church] p. 129 | Section II.24 | df-ifp 1058 dfifp2 1059 |
| [Clemente] p. 10 | Definition IT | natded 28184 |
| [Clemente] p. 10 | Definition I` `m,n | natded 28184 |
| [Clemente] p. 11 | Definition E=>m,n | natded 28184 |
| [Clemente] p. 11 | Definition I=>m,n | natded 28184 |
| [Clemente] p. 11 | Definition E` `(1) | natded 28184 |
| [Clemente] p. 11 | Definition E` `(2) | natded 28184 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 28184 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 28184 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 28184 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 28184 |
| [Clemente] p. 14 | Proof 5.11 | natded 28184 |
| [Clemente] p. 14 | Definition E` `n | natded 28184 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 28186 ex-natded5.2 28185 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 28189 ex-natded5.3 28188 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 28191 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 28193 ex-natded5.7 28192 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 28195 ex-natded5.8 28194 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 28197 ex-natded5.13 28196 |
| [Clemente] p. 32 | Definition I` `n | natded 28184 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 28184 |
| [Clemente] p. 32 | Definition E` `n,t | natded 28184 |
| [Clemente] p. 32 | Definition I` `n,t | natded 28184 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 28198 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 28199 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 28201 ex-natded9.26 28200 |
| [Cohen] p. 301 | Remark | relogoprlem 25176 |
| [Cohen] p. 301 | Property 2 | relogmul 25177 relogmuld 25210 |
| [Cohen] p. 301 | Property 3 | relogdiv 25178 relogdivd 25211 |
| [Cohen] p. 301 | Property 4 | relogexp 25181 |
| [Cohen] p. 301 | Property 1a | log1 25171 |
| [Cohen] p. 301 | Property 1b | loge 25172 |
| [Cohen4] p. 348 | Observation | relogbcxpb 25367 |
| [Cohen4] p. 349 | Property | relogbf 25371 |
| [Cohen4] p. 352 | Definition | elogb 25350 |
| [Cohen4] p. 361 | Property 2 | relogbmul 25357 |
| [Cohen4] p. 361 | Property 3 | logbrec 25362 relogbdiv 25359 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 25355 |
| [Cohen4] p. 361 | Property 6 | relogbexp 25360 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 25348 |
| [Cohen4] p. 361 | Property 1(b) | logb1 25349 |
| [Cohen4] p. 367 | Property | logbchbase 25351 |
| [Cohen4] p. 377 | Property 2 | logblt 25364 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 31545 sxbrsigalem4 31547 |
| [Cohn] p. 81 | Section II.5 | acsdomd 17793 acsinfd 17792 acsinfdimd 17794 acsmap2d 17791 acsmapd 17790 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 31550 |
| [Connell] p. 57 | Definition | df-scmat 21102 df-scmatalt 44461 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 13232 |
| [Crawley] p. 1 | Definition of poset | df-poset 17558 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 36524 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 37328 dalaw 37024 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 39099 |
| [Crawley] p. 111 | Definition of set W | df-watsN 37128 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 37244 df-ldil 37242 isldil 37248 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 37243 df-trnN 37245 isltrn 37257 ltrnu 37259 |
| [Crawley] p. 112 | Lemma A | cdlema1N 36929 cdlema2N 36930 exatleN 36542 |
| [Crawley] p. 112 | Lemma B | 1cvrat 36614 cdlemb 36932 cdlemb2 37179 cdlemb3 37744 idltrn 37288 l1cvat 36193 lhpat 37181 lhpat2 37183 lshpat 36194 ltrnel 37277 ltrnmw 37289 |
| [Crawley] p. 112 | Lemma C | cdlemc1 37329 cdlemc2 37330 ltrnnidn 37312 trlat 37307 trljat1 37304 trljat2 37305 trljat3 37306 trlne 37323 trlnidat 37311 trlnle 37324 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 37129 |
| [Crawley] p. 113 | Lemma C | cdlemc 37335 cdlemc3 37331 cdlemc4 37332 |
| [Crawley] p. 113 | Lemma D | cdlemd 37345 cdlemd1 37336 cdlemd2 37337 cdlemd3 37338 cdlemd4 37339 cdlemd5 37340 cdlemd6 37341 cdlemd7 37342 cdlemd8 37343 cdlemd9 37344 cdleme31sde 37523 cdleme31se 37520 cdleme31se2 37521 cdleme31snd 37524 cdleme32a 37579 cdleme32b 37580 cdleme32c 37581 cdleme32d 37582 cdleme32e 37583 cdleme32f 37584 cdleme32fva 37575 cdleme32fva1 37576 cdleme32fvcl 37578 cdleme32le 37585 cdleme48fv 37637 cdleme4gfv 37645 cdleme50eq 37679 cdleme50f 37680 cdleme50f1 37681 cdleme50f1o 37684 cdleme50laut 37685 cdleme50ldil 37686 cdleme50lebi 37678 cdleme50rn 37683 cdleme50rnlem 37682 cdlemeg49le 37649 cdlemeg49lebilem 37677 |
| [Crawley] p. 113 | Lemma E | cdleme 37698 cdleme00a 37347 cdleme01N 37359 cdleme02N 37360 cdleme0a 37349 cdleme0aa 37348 cdleme0b 37350 cdleme0c 37351 cdleme0cp 37352 cdleme0cq 37353 cdleme0dN 37354 cdleme0e 37355 cdleme0ex1N 37361 cdleme0ex2N 37362 cdleme0fN 37356 cdleme0gN 37357 cdleme0moN 37363 cdleme1 37365 cdleme10 37392 cdleme10tN 37396 cdleme11 37408 cdleme11a 37398 cdleme11c 37399 cdleme11dN 37400 cdleme11e 37401 cdleme11fN 37402 cdleme11g 37403 cdleme11h 37404 cdleme11j 37405 cdleme11k 37406 cdleme11l 37407 cdleme12 37409 cdleme13 37410 cdleme14 37411 cdleme15 37416 cdleme15a 37412 cdleme15b 37413 cdleme15c 37414 cdleme15d 37415 cdleme16 37423 cdleme16aN 37397 cdleme16b 37417 cdleme16c 37418 cdleme16d 37419 cdleme16e 37420 cdleme16f 37421 cdleme16g 37422 cdleme19a 37441 cdleme19b 37442 cdleme19c 37443 cdleme19d 37444 cdleme19e 37445 cdleme19f 37446 cdleme1b 37364 cdleme2 37366 cdleme20aN 37447 cdleme20bN 37448 cdleme20c 37449 cdleme20d 37450 cdleme20e 37451 cdleme20f 37452 cdleme20g 37453 cdleme20h 37454 cdleme20i 37455 cdleme20j 37456 cdleme20k 37457 cdleme20l 37460 cdleme20l1 37458 cdleme20l2 37459 cdleme20m 37461 cdleme20y 37440 cdleme20zN 37439 cdleme21 37475 cdleme21d 37468 cdleme21e 37469 cdleme22a 37478 cdleme22aa 37477 cdleme22b 37479 cdleme22cN 37480 cdleme22d 37481 cdleme22e 37482 cdleme22eALTN 37483 cdleme22f 37484 cdleme22f2 37485 cdleme22g 37486 cdleme23a 37487 cdleme23b 37488 cdleme23c 37489 cdleme26e 37497 cdleme26eALTN 37499 cdleme26ee 37498 cdleme26f 37501 cdleme26f2 37503 cdleme26f2ALTN 37502 cdleme26fALTN 37500 cdleme27N 37507 cdleme27a 37505 cdleme27cl 37504 cdleme28c 37510 cdleme3 37375 cdleme30a 37516 cdleme31fv 37528 cdleme31fv1 37529 cdleme31fv1s 37530 cdleme31fv2 37531 cdleme31id 37532 cdleme31sc 37522 cdleme31sdnN 37525 cdleme31sn 37518 cdleme31sn1 37519 cdleme31sn1c 37526 cdleme31sn2 37527 cdleme31so 37517 cdleme35a 37586 cdleme35b 37588 cdleme35c 37589 cdleme35d 37590 cdleme35e 37591 cdleme35f 37592 cdleme35fnpq 37587 cdleme35g 37593 cdleme35h 37594 cdleme35h2 37595 cdleme35sn2aw 37596 cdleme35sn3a 37597 cdleme36a 37598 cdleme36m 37599 cdleme37m 37600 cdleme38m 37601 cdleme38n 37602 cdleme39a 37603 cdleme39n 37604 cdleme3b 37367 cdleme3c 37368 cdleme3d 37369 cdleme3e 37370 cdleme3fN 37371 cdleme3fa 37374 cdleme3g 37372 cdleme3h 37373 cdleme4 37376 cdleme40m 37605 cdleme40n 37606 cdleme40v 37607 cdleme40w 37608 cdleme41fva11 37615 cdleme41sn3aw 37612 cdleme41sn4aw 37613 cdleme41snaw 37614 cdleme42a 37609 cdleme42b 37616 cdleme42c 37610 cdleme42d 37611 cdleme42e 37617 cdleme42f 37618 cdleme42g 37619 cdleme42h 37620 cdleme42i 37621 cdleme42k 37622 cdleme42ke 37623 cdleme42keg 37624 cdleme42mN 37625 cdleme42mgN 37626 cdleme43aN 37627 cdleme43bN 37628 cdleme43cN 37629 cdleme43dN 37630 cdleme5 37378 cdleme50ex 37697 cdleme50ltrn 37695 cdleme51finvN 37694 cdleme51finvfvN 37693 cdleme51finvtrN 37696 cdleme6 37379 cdleme7 37387 cdleme7a 37381 cdleme7aa 37380 cdleme7b 37382 cdleme7c 37383 cdleme7d 37384 cdleme7e 37385 cdleme7ga 37386 cdleme8 37388 cdleme8tN 37393 cdleme9 37391 cdleme9a 37389 cdleme9b 37390 cdleme9tN 37395 cdleme9taN 37394 cdlemeda 37436 cdlemedb 37435 cdlemednpq 37437 cdlemednuN 37438 cdlemefr27cl 37541 cdlemefr32fva1 37548 cdlemefr32fvaN 37547 cdlemefrs32fva 37538 cdlemefrs32fva1 37539 cdlemefs27cl 37551 cdlemefs32fva1 37561 cdlemefs32fvaN 37560 cdlemesner 37434 cdlemeulpq 37358 |
| [Crawley] p. 114 | Lemma E | 4atex 37214 4atexlem7 37213 cdleme0nex 37428 cdleme17a 37424 cdleme17c 37426 cdleme17d 37636 cdleme17d1 37427 cdleme17d2 37633 cdleme18a 37429 cdleme18b 37430 cdleme18c 37431 cdleme18d 37433 cdleme4a 37377 |
| [Crawley] p. 115 | Lemma E | cdleme21a 37463 cdleme21at 37466 cdleme21b 37464 cdleme21c 37465 cdleme21ct 37467 cdleme21f 37470 cdleme21g 37471 cdleme21h 37472 cdleme21i 37473 cdleme22gb 37432 |
| [Crawley] p. 116 | Lemma F | cdlemf 37701 cdlemf1 37699 cdlemf2 37700 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 37705 cdlemg16 37795 cdlemg28 37842 cdlemg28a 37831 cdlemg28b 37841 cdlemg3a 37735 cdlemg42 37867 cdlemg43 37868 cdlemg44 37871 cdlemg44a 37869 cdlemg46 37873 cdlemg47 37874 cdlemg9 37772 ltrnco 37857 ltrncom 37876 tgrpabl 37889 trlco 37865 |
| [Crawley] p. 116 | Definition of G | df-tgrp 37881 |
| [Crawley] p. 117 | Lemma G | cdlemg17 37815 cdlemg17b 37800 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 37894 df-edring 37895 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 37898 |
| [Crawley] p. 118 | Remark | tendopltp 37918 |
| [Crawley] p. 118 | Lemma H | cdlemh 37955 cdlemh1 37953 cdlemh2 37954 |
| [Crawley] p. 118 | Lemma I | cdlemi 37958 cdlemi1 37956 cdlemi2 37957 |
| [Crawley] p. 118 | Lemma J | cdlemj1 37959 cdlemj2 37960 cdlemj3 37961 tendocan 37962 |
| [Crawley] p. 118 | Lemma K | cdlemk 38112 cdlemk1 37969 cdlemk10 37981 cdlemk11 37987 cdlemk11t 38084 cdlemk11ta 38067 cdlemk11tb 38069 cdlemk11tc 38083 cdlemk11u-2N 38027 cdlemk11u 38009 cdlemk12 37988 cdlemk12u-2N 38028 cdlemk12u 38010 cdlemk13-2N 38014 cdlemk13 37990 cdlemk14-2N 38016 cdlemk14 37992 cdlemk15-2N 38017 cdlemk15 37993 cdlemk16-2N 38018 cdlemk16 37995 cdlemk16a 37994 cdlemk17-2N 38019 cdlemk17 37996 cdlemk18-2N 38024 cdlemk18-3N 38038 cdlemk18 38006 cdlemk19-2N 38025 cdlemk19 38007 cdlemk19u 38108 cdlemk1u 37997 cdlemk2 37970 cdlemk20-2N 38030 cdlemk20 38012 cdlemk21-2N 38029 cdlemk21N 38011 cdlemk22-3 38039 cdlemk22 38031 cdlemk23-3 38040 cdlemk24-3 38041 cdlemk25-3 38042 cdlemk26-3 38044 cdlemk26b-3 38043 cdlemk27-3 38045 cdlemk28-3 38046 cdlemk29-3 38049 cdlemk3 37971 cdlemk30 38032 cdlemk31 38034 cdlemk32 38035 cdlemk33N 38047 cdlemk34 38048 cdlemk35 38050 cdlemk36 38051 cdlemk37 38052 cdlemk38 38053 cdlemk39 38054 cdlemk39u 38106 cdlemk4 37972 cdlemk41 38058 cdlemk42 38079 cdlemk42yN 38082 cdlemk43N 38101 cdlemk45 38085 cdlemk46 38086 cdlemk47 38087 cdlemk48 38088 cdlemk49 38089 cdlemk5 37974 cdlemk50 38090 cdlemk51 38091 cdlemk52 38092 cdlemk53 38095 cdlemk54 38096 cdlemk55 38099 cdlemk55u 38104 cdlemk56 38109 cdlemk5a 37973 cdlemk5auN 37998 cdlemk5u 37999 cdlemk6 37975 cdlemk6u 38000 cdlemk7 37986 cdlemk7u-2N 38026 cdlemk7u 38008 cdlemk8 37976 cdlemk9 37977 cdlemk9bN 37978 cdlemki 37979 cdlemkid 38074 cdlemkj-2N 38020 cdlemkj 38001 cdlemksat 37984 cdlemksel 37983 cdlemksv 37982 cdlemksv2 37985 cdlemkuat 38004 cdlemkuel-2N 38022 cdlemkuel-3 38036 cdlemkuel 38003 cdlemkuv-2N 38021 cdlemkuv2-2 38023 cdlemkuv2-3N 38037 cdlemkuv2 38005 cdlemkuvN 38002 cdlemkvcl 37980 cdlemky 38064 cdlemkyyN 38100 tendoex 38113 |
| [Crawley] p. 120 | Remark | dva1dim 38123 |
| [Crawley] p. 120 | Lemma L | cdleml1N 38114 cdleml2N 38115 cdleml3N 38116 cdleml4N 38117 cdleml5N 38118 cdleml6 38119 cdleml7 38120 cdleml8 38121 cdleml9 38122 dia1dim 38199 |
| [Crawley] p. 120 | Lemma M | dia11N 38186 diaf11N 38187 dialss 38184 diaord 38185 dibf11N 38299 djajN 38275 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 38170 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 38256 dia2dimlem1 38202 dia2dimlem2 38203 dia2dimlem3 38204 dia2dimlem4 38205 dia2dimlem5 38206 diaf1oN 38268 diarnN 38267 dvheveccl 38250 dvhopN 38254 |
| [Crawley] p. 121 | Lemma N | cdlemn 38350 cdlemn10 38344 cdlemn11 38349 cdlemn11a 38345 cdlemn11b 38346 cdlemn11c 38347 cdlemn11pre 38348 cdlemn2 38333 cdlemn2a 38334 cdlemn3 38335 cdlemn4 38336 cdlemn4a 38337 cdlemn5 38339 cdlemn5pre 38338 cdlemn6 38340 cdlemn7 38341 cdlemn8 38342 cdlemn9 38343 diclspsn 38332 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 38311 |
| [Crawley] p. 122 | Lemma N | dih11 38403 dihf11 38405 dihjust 38355 dihjustlem 38354 dihord 38402 dihord1 38356 dihord10 38361 dihord11b 38360 dihord11c 38362 dihord2 38365 dihord2a 38357 dihord2b 38358 dihord2cN 38359 dihord2pre 38363 dihord2pre2 38364 dihordlem6 38351 dihordlem7 38352 dihordlem7b 38353 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 38368 dihfval 38369 dihval 38370 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 27196 df-nbgr 27117 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 27052 uhgrspan1 27087 uhgrspansubgr 27075 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 27338 vtxdgoddnumeven 27337 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 26846 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3941 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 9112 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 8410 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 9120 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 9411 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 9979 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 5211 |
| [Enderton] p. 19 | Definition | df-tp 4574 |
| [Enderton] p. 26 | Exercise 5 | unissb 4872 |
| [Enderton] p. 26 | Exercise 10 | pwel 5284 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5460 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 5003 iinin2 5002 iinun2 4997 iunin1 4996 iunin1f 30311 iunin2 4995 uniin1 30305 uniin2 30306 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 5001 iundif2 4998 |
| [Enderton] p. 32 | Exercise 20 | unineq 4256 |
| [Enderton] p. 33 | Exercise 23 | iinuni 5022 |
| [Enderton] p. 33 | Exercise 25 | iununi 5023 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 5030 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 7495 iunpwss 5031 |
| [Enderton] p. 36 | Definition | opthwiener 5406 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 5345 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4877 |
| [Enderton] p. 41 | Lemma 3D | opeluu 5364 rnex 7619 rnexg 7616 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5785 rnuni 6009 |
| [Enderton] p. 42 | Definition of a function | dffun7 6384 dffun8 6385 |
| [Enderton] p. 43 | Definition of function value | funfv2 6753 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 6425 |
| [Enderton] p. 44 | Definition (d) | dfima2 5933 dfima3 5934 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6760 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 9897 ac7g 9898 df-ac 9544 dfac2 9559 dfac2a 9557 dfac2b 9558 dfac3 9549 dfac7 9560 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 7007 |
| [Enderton] p. 52 | Definition | df-map 8410 |
| [Enderton] p. 53 | Exercise 21 | coass 6120 |
| [Enderton] p. 53 | Exercise 27 | dmco 6109 |
| [Enderton] p. 53 | Exercise 14(a) | funin 6432 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5967 |
| [Enderton] p. 54 | Remark | ixpf 8486 ixpssmap 8498 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 8464 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 9907 ac9s 9917 |
| [Enderton] p. 56 | Theorem 3M | eqvrelref 35847 erref 8311 |
| [Enderton] p. 57 | Lemma 3N | eqvrelthi 35850 erthi 8342 |
| [Enderton] p. 57 | Definition | df-ec 8293 |
| [Enderton] p. 58 | Definition | df-qs 8297 |
| [Enderton] p. 61 | Exercise 35 | df-ec 8293 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5781 |
| [Enderton] p. 68 | Definition of successor | df-suc 6199 |
| [Enderton] p. 71 | Definition | df-tr 5175 dftr4 5179 |
| [Enderton] p. 72 | Theorem 4E | unisuc 6269 |
| [Enderton] p. 73 | Exercise 6 | unisuc 6269 |
| [Enderton] p. 73 | Exercise 5(a) | truni 5188 |
| [Enderton] p. 73 | Exercise 5(b) | trint 5190 trintALT 41222 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 8232 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 8234 onasuc 8155 |
| [Enderton] p. 79 | Definition of operation value | df-ov 7161 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 8233 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 8235 onmsuc 8156 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 8250 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 8237 nnacom 8245 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 8251 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 8252 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 8254 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 8238 nnmsucr 8253 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 8266 |
| [Enderton] p. 129 | Definition | df-en 8512 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 7113 |
| [Enderton] p. 133 | Exercise 1 | xpomen 9443 |
| [Enderton] p. 133 | Exercise 2 | qnnen 15568 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8703 |
| [Enderton] p. 135 | Corollary 6C | php3 8705 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8702 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 8730 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 8732 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8738 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8740 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8683 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 9607 |
| [Enderton] p. 142 | Theorem 6I(4) | mapdjuen 9608 |
| [Enderton] p. 143 | Theorem 6J | dju0en 9603 dju1en 9599 |
| [Enderton] p. 144 | Exercise 13 | iunfi 8814 unifi 8815 unifi2 8816 |
| [Enderton] p. 144 | Corollary 6K | undif2 4427 unfi 8787 unfi2 8789 |
| [Enderton] p. 145 | Figure 38 | ffoss 7649 |
| [Enderton] p. 145 | Definition | df-dom 8513 |
| [Enderton] p. 146 | Example 1 | domen 8524 domeng 8525 |
| [Enderton] p. 146 | Example 3 | nndomo 8714 nnsdom 9119 nnsdomg 8779 |
| [Enderton] p. 149 | Theorem 6L(a) | djudom2 9611 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8684 xpdom1 8618 xpdom1g 8616 xpdom2g 8615 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8690 |
| [Enderton] p. 151 | Theorem 6M | zorn 9931 zorng 9928 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 9916 dfac5 9556 |
| [Enderton] p. 159 | Theorem 6Q | unictb 9999 |
| [Enderton] p. 164 | Example | infdif 9633 |
| [Enderton] p. 168 | Definition | df-po 5476 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 6300 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 6239 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 6299 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 6246 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7555 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 7504 |
| [Enderton] p. 194 | Remark | onprc 7501 |
| [Enderton] p. 194 | Exercise 16 | suc11 6296 |
| [Enderton] p. 197 | Definition | df-card 9370 |
| [Enderton] p. 197 | Theorem 7P | carden 9975 |
| [Enderton] p. 200 | Exercise 25 | tfis 7571 |
| [Enderton] p. 202 | Lemma 7T | r1tr 9207 |
| [Enderton] p. 202 | Definition | df-r1 9195 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 9217 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 9298 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 9071 |
| [Enderton] p. 207 | Exercise 30 | rankpr 9288 rankprb 9282 rankpw 9274 rankpwi 9254 rankuniss 9297 |
| [Enderton] p. 207 | Exercise 34 | opthreg 9083 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 9084 |
| [Enderton] p. 212 | Definition of aleph | alephval3 9538 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 9504 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 9518 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 7980 |
| [Enderton] p. 222 | Definition of kard | karden 9326 kardex 9325 |
| [Enderton] p. 238 | Theorem 8R | oeoa 8225 |
| [Enderton] p. 238 | Theorem 8S | oeoe 8227 |
| [Enderton] p. 240 | Exercise 25 | oarec 8190 |
| [Enderton] p. 257 | Definition of cofinality | cflm 9674 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 16915 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 16861 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 17789 mrieqv2d 16912 mrieqvd 16911 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 16916 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 16921 mreexexlem2d 16918 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 17795 mreexfidimd 16923 |
| [Frege1879] p. 11 | Statement | df3or2 40120 |
| [Frege1879] p. 12 | Statement | df3an2 40121 dfxor4 40118 dfxor5 40119 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 40143 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 40144 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 40148 |
| [Frege1879] p. 31 | Proposition 4 | frege4 40152 |
| [Frege1879] p. 32 | Proposition 5 | frege5 40153 |
| [Frege1879] p. 33 | Proposition 6 | frege6 40159 |
| [Frege1879] p. 34 | Proposition 7 | frege7 40161 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 40162 axfrege8 40160 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-luk-pm2.04 34728 |
| [Frege1879] p. 35 | Proposition 9 | frege9 40165 |
| [Frege1879] p. 36 | Proposition 10 | frege10 40173 |
| [Frege1879] p. 36 | Proposition 11 | frege11 40167 |
| [Frege1879] p. 37 | Proposition 12 | frege12 40166 |
| [Frege1879] p. 37 | Proposition 13 | frege13 40175 |
| [Frege1879] p. 37 | Proposition 14 | frege14 40176 |
| [Frege1879] p. 38 | Proposition 15 | frege15 40179 |
| [Frege1879] p. 38 | Proposition 16 | frege16 40169 |
| [Frege1879] p. 39 | Proposition 17 | frege17 40174 |
| [Frege1879] p. 39 | Proposition 18 | frege18 40171 |
| [Frege1879] p. 39 | Proposition 19 | frege19 40177 |
| [Frege1879] p. 40 | Proposition 20 | frege20 40181 |
| [Frege1879] p. 40 | Proposition 21 | frege21 40180 |
| [Frege1879] p. 41 | Proposition 22 | frege22 40172 |
| [Frege1879] p. 42 | Proposition 23 | frege23 40178 |
| [Frege1879] p. 42 | Proposition 24 | frege24 40168 |
| [Frege1879] p. 42 | Proposition 25 | frege25 40170 rp-frege25 40158 |
| [Frege1879] p. 42 | Proposition 26 | frege26 40163 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 40183 |
| [Frege1879] p. 43 | Proposition 27 | frege27 40164 |
| [Frege1879] p. 43 | Proposition 28 | con3 156 |
| [Frege1879] p. 43 | Proposition 29 | frege29 40184 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 40187 axfrege31 40186 |
| [Frege1879] p. 44 | Proposition 30 | frege30 40185 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 132 |
| [Frege1879] p. 44 | Proposition 32 | frege32 40188 |
| [Frege1879] p. 44 | Proposition 33 | frege33 40189 |
| [Frege1879] p. 45 | Proposition 34 | frege34 40190 |
| [Frege1879] p. 45 | Proposition 35 | frege35 40191 |
| [Frege1879] p. 45 | Proposition 36 | frege36 40192 |
| [Frege1879] p. 46 | Proposition 37 | frege37 40193 |
| [Frege1879] p. 46 | Proposition 38 | frege38 40194 |
| [Frege1879] p. 46 | Proposition 39 | frege39 40195 |
| [Frege1879] p. 46 | Proposition 40 | frege40 40196 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 40198 axfrege41 40197 |
| [Frege1879] p. 47 | Proposition 41 | notnot 144 |
| [Frege1879] p. 47 | Proposition 42 | frege42 40199 |
| [Frege1879] p. 47 | Proposition 43 | frege43 40200 |
| [Frege1879] p. 47 | Proposition 44 | frege44 40201 |
| [Frege1879] p. 47 | Proposition 45 | frege45 40202 |
| [Frege1879] p. 48 | Proposition 46 | frege46 40203 |
| [Frege1879] p. 48 | Proposition 47 | frege47 40204 |
| [Frege1879] p. 49 | Proposition 48 | frege48 40205 |
| [Frege1879] p. 49 | Proposition 49 | frege49 40206 |
| [Frege1879] p. 49 | Proposition 50 | frege50 40207 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 40210 ax-frege52c 40241 frege52aid 40211 frege52b 40242 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 40215 ax-frege54c 40245 frege54b 40246 |
| [Frege1879] p. 50 | Proposition 51 | frege51 40208 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3776 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 40213 frege53aid 40212 frege53b 40243 frege53c 40267 |
| [Frege1879] p. 50 | Proposition 54 | biid 263 eqid 2823 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 40221 frege55aid 40218 frege55b 40250 frege55c 40271 frege55cor1a 40222 frege55lem2a 40220 frege55lem2b 40249 frege55lem2c 40270 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 40224 frege56aid 40223 frege56b 40251 frege56c 40272 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 40228 ax-frege58b 40254 frege58bid 40255 frege58c 40274 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 40226 frege57aid 40225 frege57b 40252 frege57c 40273 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3787 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 40230 frege59b 40257 frege59c 40275 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 40231 frege60b 40258 frege60c 40276 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 40232 frege61b 40259 frege61c 40277 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 40233 frege62b 40260 frege62c 40278 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 40234 frege63b 40261 frege63c 40279 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 40235 frege64b 40262 frege64c 40280 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 40236 frege65b 40263 frege65c 40281 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 40237 frege66b 40264 frege66c 40282 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 40238 frege67b 40265 frege67c 40283 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 40239 frege68b 40266 frege68c 40284 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 40285 |
| [Frege1879] p. 58 | Proposition 70 | frege70 40286 |
| [Frege1879] p. 59 | Proposition 71 | frege71 40287 |
| [Frege1879] p. 59 | Proposition 72 | frege72 40288 |
| [Frege1879] p. 59 | Proposition 73 | frege73 40289 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 40292 |
| [Frege1879] p. 60 | Proposition 74 | frege74 40290 |
| [Frege1879] p. 60 | Proposition 75 | frege75 40291 |
| [Frege1879] p. 62 | Proposition 77 | frege77 40293 frege77d 40098 |
| [Frege1879] p. 63 | Proposition 78 | frege78 40294 |
| [Frege1879] p. 63 | Proposition 79 | frege79 40295 |
| [Frege1879] p. 63 | Proposition 80 | frege80 40296 |
| [Frege1879] p. 63 | Proposition 81 | frege81 40297 frege81d 40099 |
| [Frege1879] p. 64 | Proposition 82 | frege82 40298 |
| [Frege1879] p. 65 | Proposition 83 | frege83 40299 frege83d 40100 |
| [Frege1879] p. 65 | Proposition 84 | frege84 40300 |
| [Frege1879] p. 66 | Proposition 85 | frege85 40301 |
| [Frege1879] p. 66 | Proposition 86 | frege86 40302 |
| [Frege1879] p. 66 | Proposition 87 | frege87 40303 frege87d 40102 |
| [Frege1879] p. 67 | Proposition 88 | frege88 40304 |
| [Frege1879] p. 68 | Proposition 89 | frege89 40305 |
| [Frege1879] p. 68 | Proposition 90 | frege90 40306 |
| [Frege1879] p. 68 | Proposition 91 | frege91 40307 frege91d 40103 |
| [Frege1879] p. 69 | Proposition 92 | frege92 40308 |
| [Frege1879] p. 70 | Proposition 93 | frege93 40309 |
| [Frege1879] p. 70 | Proposition 94 | frege94 40310 |
| [Frege1879] p. 70 | Proposition 95 | frege95 40311 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 40315 |
| [Frege1879] p. 71 | Proposition 96 | frege96 40312 frege96d 40101 |
| [Frege1879] p. 71 | Proposition 97 | frege97 40313 frege97d 40104 |
| [Frege1879] p. 71 | Proposition 98 | frege98 40314 frege98d 40105 |
| [Frege1879] p. 72 | Proposition 100 | frege100 40316 |
| [Frege1879] p. 72 | Proposition 101 | frege101 40317 |
| [Frege1879] p. 72 | Proposition 102 | frege102 40318 frege102d 40106 |
| [Frege1879] p. 73 | Proposition 103 | frege103 40319 |
| [Frege1879] p. 73 | Proposition 104 | frege104 40320 |
| [Frege1879] p. 73 | Proposition 105 | frege105 40321 |
| [Frege1879] p. 73 | Proposition 106 | frege106 40322 frege106d 40107 |
| [Frege1879] p. 74 | Proposition 107 | frege107 40323 |
| [Frege1879] p. 74 | Proposition 108 | frege108 40324 frege108d 40108 |
| [Frege1879] p. 74 | Proposition 109 | frege109 40325 frege109d 40109 |
| [Frege1879] p. 75 | Proposition 110 | frege110 40326 |
| [Frege1879] p. 75 | Proposition 111 | frege111 40327 frege111d 40111 |
| [Frege1879] p. 76 | Proposition 112 | frege112 40328 |
| [Frege1879] p. 76 | Proposition 113 | frege113 40329 |
| [Frege1879] p. 76 | Proposition 114 | frege114 40330 frege114d 40110 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 40331 |
| [Frege1879] p. 77 | Proposition 116 | frege116 40332 |
| [Frege1879] p. 78 | Proposition 117 | frege117 40333 |
| [Frege1879] p. 78 | Proposition 118 | frege118 40334 |
| [Frege1879] p. 78 | Proposition 119 | frege119 40335 |
| [Frege1879] p. 78 | Proposition 120 | frege120 40336 |
| [Frege1879] p. 79 | Proposition 121 | frege121 40337 |
| [Frege1879] p. 79 | Proposition 122 | frege122 40338 frege122d 40112 |
| [Frege1879] p. 79 | Proposition 123 | frege123 40339 |
| [Frege1879] p. 80 | Proposition 124 | frege124 40340 frege124d 40113 |
| [Frege1879] p. 81 | Proposition 125 | frege125 40341 |
| [Frege1879] p. 81 | Proposition 126 | frege126 40342 frege126d 40114 |
| [Frege1879] p. 82 | Proposition 127 | frege127 40343 |
| [Frege1879] p. 83 | Proposition 128 | frege128 40344 |
| [Frege1879] p. 83 | Proposition 129 | frege129 40345 frege129d 40115 |
| [Frege1879] p. 84 | Proposition 130 | frege130 40346 |
| [Frege1879] p. 85 | Proposition 131 | frege131 40347 frege131d 40116 |
| [Frege1879] p. 86 | Proposition 132 | frege132 40348 |
| [Frege1879] p. 86 | Proposition 133 | frege133 40349 frege133d 40117 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 42605 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 42925 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 42626 |
| [Fremlin1] p. 14 | Definition 112A | ismea 42740 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 42760 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 42751 meadjunre 42765 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 42752 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 42753 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 42749 meaiunle 42758 meaiunlelem 42757 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 42770 meaiuninc2 42771 meaiuninc3 42774 meaiuninc3v 42773 meaiunincf 42772 meaiuninclem 42769 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 42776 meaiininc2 42777 meaiininclem 42775 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 42795 caragendifcl 42803 caratheodory 42817 omelesplit 42807 |
| [Fremlin1] p. 19 | Definition 113A | isome 42783 isomennd 42820 isomenndlem 42819 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 42805 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 42824 voncmpl 42910 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 42787 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 42812 carageniuncllem1 42810 carageniuncllem2 42811 caragenuncl 42802 caragenuncllem 42801 caragenunicl 42813 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 42821 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 42815 caratheodorylem2 42816 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 42824 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 42883 hoidmv1lelem1 42880 hoidmv1lelem2 42881 hoidmv1lelem3 42882 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 42927 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 42883 hoidmvle 42889 hoidmvlelem1 42884 hoidmvlelem2 42885 hoidmvlelem3 42886 hoidmvlelem4 42887 hoidmvlelem5 42888 hsphoidmvle2 42874 hsphoif 42865 hsphoival 42868 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 42837 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 42845 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 42872 hoidmvn0val 42873 hoidmvval 42866 hoidmvval0 42876 hoidmvval0b 42879 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 42877 hsphoidmvle 42875 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 42826 df-voln 42828 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 42893 ovn0 42855 ovn0lem 42854 ovnf 42852 ovnome 42862 ovnssle 42850 ovnsslelem 42849 ovnsupge0 42846 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 42892 ovnhoilem1 42890 ovnhoilem2 42891 vonhoi 42956 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 42909 hoidifhspf 42907 hoidifhspval 42897 hoidifhspval2 42904 hoidifhspval3 42908 hspmbl 42918 hspmbllem1 42915 hspmbllem2 42916 hspmbllem3 42917 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 42910 vonmea 42863 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 42861 ovnsubadd2 42935 ovnsubadd2lem 42934 ovnsubaddlem1 42859 ovnsubaddlem2 42860 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 42920 hoimbl2 42954 hoimbllem 42919 hspdifhsp 42905 opnvonmbl 42923 opnvonmbllem2 42922 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 42925 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 42968 iccvonmbllem 42967 ioovonmbl 42966 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 42974 vonicclem2 42973 vonioo 42971 vonioolem2 42970 vonn0icc 42977 vonn0icc2 42981 vonn0ioo 42976 vonn0ioo2 42979 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 42978 snvonmbl 42975 vonct 42982 vonsn 42980 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 42649 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 42648 subsaliuncllem 42647 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 43009 salpreimalegt 42995 salpreimaltle 43010 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 43012 issmff 43018 issmflem 43011 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 43029 issmflelem 43028 smfpreimale 43038 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 43040 issmfgtlem 43039 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 42985 issmf 43012 issmff 43018 issmfge 43053 issmfgelem 43052 issmfgt 43040 issmfgtlem 43039 issmfle 43029 issmflelem 43028 issmflem 43011 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 42993 salpreimagtlt 43014 salpreimalelt 43013 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 43053 issmfgelem 43052 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 43037 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 43035 cnfsmf 43024 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 43050 decsmflem 43049 incsmf 43026 incsmflem 43025 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 42989 pimconstlt1 42990 smfconst 43033 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 43048 smfaddlem1 43046 smfaddlem2 43047 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 43078 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 43077 smfmullem1 43073 smfmullem2 43074 smfmullem3 43075 smfmullem4 43076 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 43079 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 43082 smfpimbor1lem2 43081 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 43084 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 43072 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 43071 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 43080 smfresal 43070 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 43060 smflim2 43087 smflimlem1 43054 smflimlem2 43055 smflimlem3 43056 smflimlem4 43057 smflimlem5 43058 smflimlem6 43059 smflimmpt 43091 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 43095 smfsuplem1 43092 smfsuplem2 43093 smfsuplem3 43094 smfsupmpt 43096 smfsupxr 43097 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 43099 smfinflem 43098 smfinfmpt 43100 |
| [Fremlin1] p. 39 | Remark 121G | smflim 43060 smflim2 43087 smflimmpt 43091 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 43089 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 43109 smflimsuplem2 43102 smflimsuplem6 43106 smflimsuplem7 43107 smflimsuplem8 43108 smflimsupmpt 43110 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 43112 smfliminflem 43111 smfliminfmpt 43113 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 42985 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 24139 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 24182 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 24192 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 34974 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 34977 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 9103 inf1 9087 inf2 9088 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 10335 enqer 10345 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 10340 df-nq 10336 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 10332 df-plq 10338 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 7387 df-mpq 10333 df-mq 10339 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 10341 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 10399 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 10400 ltbtwnnq 10402 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 10395 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 10396 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 10403 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 10405 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 10417 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 10419 |
| [Gleason] p. 122 | Definition | df-1p 10406 |
| [Gleason] p. 122 | Remark (1) | prub 10418 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 10457 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 10409 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 10456 psslinpr 10455 supexpr 10478 suplem1pr 10476 suplem2pr 10477 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 10442 addclprlem1 10440 addclprlem2 10441 df-plp 10407 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 10446 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 10445 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 10458 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 10467 ltexprlem1 10460 ltexprlem2 10461 ltexprlem3 10462 ltexprlem4 10463 ltexprlem5 10464 ltexprlem6 10465 ltexprlem7 10466 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 10469 ltaprlem 10468 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 10470 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 10471 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 10408 mulclpr 10444 mulclprlem 10443 reclem2pr 10472 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 10453 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 10448 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 10447 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 10452 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 10475 reclem3pr 10473 reclem4pr 10474 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 10479 enrer 10487 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 10484 df-1r 10485 df-nr 10480 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 10482 df-plr 10481 negexsr 10526 recexsr 10531 recexsrlem 10527 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 10483 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11635 creur 11634 cru 11632 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10612 axcnre 10588 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 14476 crimd 14593 crimi 14554 crre 14475 crred 14592 crrei 14553 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 14478 remimd 14559 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14646 absval2d 14807 absval2i 14759 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 14502 cjaddd 14581 cjaddi 14549 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 14503 cjmuld 14582 cjmuli 14550 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 14501 cjcjd 14560 cjcji 14532 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 14500 cjreb 14484 cjrebd 14563 cjrebi 14535 cjred 14587 rere 14483 rereb 14481 rerebd 14562 rerebi 14534 rered 14585 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 14509 addcjd 14573 addcji 14544 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 14599 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14641 abscjd 14812 abscji 14763 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 14651 abs00d 14808 abs00i 14760 absne0d 14809 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 14683 releabsd 14813 releabsi 14764 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 14656 absmuld 14816 absmuli 14766 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14644 sqabsaddi 14767 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 14692 abstrid 14818 abstrii 14770 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 13437 df-exp 13433 exp0 13436 expp1 13439 expp1d 13514 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 25264 cxpaddd 25302 expadd 13474 expaddd 13515 expaddz 13476 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 25273 cxpmuld 25321 expmul 13477 expmuld 13516 expmulz 13478 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 25270 mulcxpd 25313 mulexp 13471 mulexpd 13528 mulexpz 13472 |
| [Gleason] p. 140 | Exercise 1 | znnen 15567 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 12897 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 14990 rlimadd 15001 rlimdiv 15004 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 14992 rlimsub 15002 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 14991 rlimmul 15003 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 14995 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 14942 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 14962 climcj 14963 climim 14965 climre 14964 rlimabs 14967 rlimcj 14968 rlimim 14970 rlimre 14969 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 10682 df-xr 10681 ltxr 12513 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 14830 limsupval 14833 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 15028 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 15037 caucvgb 15038 caucvgr 15034 climcau 15029 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 15173 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 15241 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 14697 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 13201 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 20541 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 22955 xmet0 22954 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 22971 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 22962 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 22964 mstri 23081 xmettri 22963 xmstri 23080 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 22994 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 22258 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 23915 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 23152 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 23475 addcn2 14952 mulcn 23477 mulcn2 14954 subcn 23476 subcn2 14953 |
| [Gleason] p. 295 | Remark | bcval3 13669 bcval4 13670 |
| [Gleason] p. 295 | Equation 2 | bcpasc 13684 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 13667 df-bc 13666 |
| [Gleason] p. 296 | Remark | bcn0 13673 bcnn 13675 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 15187 |
| [Gleason] p. 308 | Equation 2 | ef0 15446 |
| [Gleason] p. 308 | Equation 3 | efcj 15447 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 15452 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 15456 |
| [Gleason] p. 310 | Equation 14 | sinadd 15519 |
| [Gleason] p. 310 | Equation 15 | cosadd 15520 |
| [Gleason] p. 311 | Equation 17 | sincossq 15531 |
| [Gleason] p. 311 | Equation 18 | cosbnd 15536 sinbnd 15535 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 13581 sqeqori 13579 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 15428 |
| [Godowski] p. 730 | Equation SF | goeqi 30052 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 29447 |
| [Golan] p. 1 | Remark | srgisid 19280 |
| [Golan] p. 1 | Definition | df-srg 19258 |
| [Golan] p. 149 | Definition | df-slmd 30831 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 33622 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 16859 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 16861 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 44102 df-cllaw 44100 df-comlaw 44101 |
| [Hall] p. 2 | Section 1.2 | df-clintop 44114 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 44135 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 29844 riesz2 29845 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 29720 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 29952 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 29964 elpjidm 29963 pjnmopi 29927 |
| [Halmos] p. 44 | Remark | pjinormi 29466 pjinormii 29455 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 29968 pjrn 29486 pjrni 29481 pjvec 29475 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 29506 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 29933 hmopidmpji 29931 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 29970 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 29959 pjocvec 29476 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 29948 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 29951 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 29954 pjssdif2i 29953 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 29634 |
| [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 1796 |
| [Hatcher] p. 25 | Definition | df-phtpc 23598 df-phtpy 23577 |
| [Hatcher] p. 26 | Definition | df-pco 23611 df-pi1 23614 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 23601 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 23656 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 21101 df-dmatalt 44460 |
| [Helfgott] p. 2 | Theorem | tgoldbach 43989 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 43974 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 43986 bgoldbtbnd 43981 bgoldbtbnd 43981 tgblthelfgott 43987 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 31915 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 31916 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 31930 hgt750lemb 31929 hgt750leme 31931 hgt750lemf 31926 hgt750lemg 31927 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 43983 tgoldbachgt 31936 tgoldbachgtALTV 43984 tgoldbachgtd 31935 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 31917 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 28272 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 18116 grpoideu 28288 mndideu 17924 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 18140 grpoinveu 28298 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 18168 grpo2inv 28310 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 18179 grpoinvop 28312 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 18201 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1769 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1770 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1772 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 30199 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 30212 cdj3i 30220 cdj3lem1 30213 cdjreui 30211 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 30210 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 39099 |
| [Holland95] p. 14 | Line 15 | hgmapvs 39029 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 39051 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 39052 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 39049 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 39055 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 38974 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 39069 |
| [Holland95] p. 204 | Definition of involution | df-srng 19619 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 36641 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 38666 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 38619 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 37071 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 38515 poml4N 37091 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 38606 pexmidALTN 37116 pexmidN 37107 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 38671 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 36262 ldualset 36263 |
| [Holland95] p. 222 | Item 1 | df-lines 36639 df-pointsN 36640 |
| [Holland95] p. 222 | Item 2 | df-polarityN 37041 |
| [Holland95] p. 223 | Remark | ispsubcl2N 37085 omllaw4 36384 pol1N 37048 polcon3N 37055 |
| [Holland95] p. 223 | Definition | df-psubclN 37073 |
| [Holland95] p. 223 | Equation for polarity | polval2N 37044 |
| [Holmes] p. 40 | Definition | df-xrn 35625 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 28863 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 29961 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 29742 eigre 29614 eigrei 29613 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 29743 eigorth 29617 eigorthi 29616 |
| [Hughes] p. 137 | Remark (ii) | eigposi 29615 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 28090 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 28086 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 28087 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 28088 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 28106 frgrregorufr0 28105 frgrregorufrg 28107 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 28113 frrusgrord 28122 frrusgrord0 28121 |
| [Huneke] p. 2 | Statement | df-clwwlknon 27869 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 28096 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 28099 frgrwopreg2 28100 frgrwopregasn 28097 frgrwopregbsn 28098 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 28102 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 28116 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 28119 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 27867 numclwlk1 28152 numclwlk1lem1 28150 numclwlk1lem2 28151 numclwwlk1 28142 numclwwlk8 28173 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 28093 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 27554 |
| [Huneke] p. 2 | Definition 6 | 2clwwlk 28128 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 28154 numclwwlkovh0 28153 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 28162 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 27758 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 28166 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 28169 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 28172 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 28184 natded 28184 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 28184 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 28184 natded 28184 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 28184 |
| [Jech] p. 4 | Definition of class | cv 1536 cvjust 2818 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 10003 |
| [Jech] p. 42 | Equation 6.1 | alephadd 10001 alephmul 10002 |
| [Jech] p. 43 | Lemma 6.2 | infmap 10000 infmap2 9642 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 9245 |
| [Jech] p. 72 | Equation 9.3 | scott0 9317 scottex 9316 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 9298 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 9322 |
| [Jech] p. 78 | Note | opthprc 5618 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 39519 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 39607 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 39608 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 39531 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 39535 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 39536 rmyp1 39537 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 39538 rmym1 39539 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 39529 rmx1 39530 rmxluc 39540 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 39533 rmy1 39534 rmyluc 39541 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 39543 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 39544 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 39564 jm2.17b 39565 jm2.17c 39566 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 39597 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 39601 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 39592 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 39567 jm2.24nn 39563 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 39606 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 39612 rmygeid 39568 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 39624 |
| [Juillerat] p. 11 | Section *5 | etransc 42575 etransclem47 42573 etransclem48 42574 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 42570 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 42572 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 42558 |
| [Juillerat] p. 13 | Proof | etransclem35 42561 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 42564 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 42550 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 42567 |
| [Juillerat] p. 14 | Proof | etransclem23 42549 |
| [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 34755 wl-motae 34757 wl-moteq 34756 |
| [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 29295 chabs1i 29297 chabs2 29296 chabs2i 29298 chjass 29312 chjassi 29265 latabs1 17699 latabs2 17700 |
| [Kalmbach] p. 15 | Definition of atom | df-at 30117 ela 30118 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 30062 cvrval2 36412 |
| [Kalmbach] p. 16 | Definition | df-ol 36316 df-oml 36317 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 29363 cmbri 29369 cmtvalN 36349 df-cm 29362 df-cmtN 36315 |
| [Kalmbach] p. 22 | Remark | omllaw5N 36385 pjoml5 29392 pjoml5i 29367 |
| [Kalmbach] p. 22 | Definition | pjoml2 29390 pjoml2i 29364 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 29393 cmcmi 29371 cmcmii 29376 cmtcomN 36387 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 36383 omlsi 29183 pjoml 29215 pjomli 29214 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 36382 |
| [Kalmbach] p. 23 | Remark | cmbr2i 29375 cmcm3 29394 cmcm3i 29373 cmcm3ii 29378 cmcm4i 29374 cmt3N 36389 cmt4N 36390 cmtbr2N 36391 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 29387 cmbr3i 29379 cmtbr3N 36392 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 29397 fh1i 29400 fh2 29398 fh2i 29401 omlfh1N 36396 |
| [Kalmbach] p. 65 | Remark | chjatom 30136 chslej 29277 chsleji 29237 shslej 29159 shsleji 29149 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 29274 chocini 29233 chsupcl 29119 chsupval2 29189 h0elch 29034 helch 29022 hsupval2 29188 ocin 29075 ococss 29072 shococss 29073 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 29091 |
| [Kalmbach] p. 66 | Remark | df-pjh 29174 pjssmi 29944 pjssmii 29460 |
| [Kalmbach] p. 67 | Lemma 3 | osum 29424 osumi 29421 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 29979 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 30179 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 30089 |
| [Kalmbach] p. 140 | Remark | hatomic 30139 hatomici 30138 hatomistici 30141 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 36457 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 30160 lsatexch 36181 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 30134 cvlcvr1 36477 cvr1 36548 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 30153 cvexchi 30148 cvrexch 36558 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 30143 hlrelat 36540 hlrelat5N 36539 lrelat 36152 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 19915 lsmsatcv 36148 spansncv 29432 spansncvi 29431 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 36167 spansncv2 30072 |
| [Kalmbach] p. 266 | Definition | df-st 29990 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 29628 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 10070 fpwwe2 10067 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 10071 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 10078 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 10073 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 10075 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 10088 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchdjuidm 10092 gchxpidm 10093 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 10104 gchhar 10103 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwdjudom 9640 unxpwdom 9055 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 10094 |
| [Kreyszig] p. 3 | Property M1 | metcl 22944 xmetcl 22943 |
| [Kreyszig] p. 4 | Property M2 | meteq0 22951 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 23184 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 11359 muleqadd 11286 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 23050 |
| [Kreyszig] p. 19 | Remark | mopntopon 23051 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 23110 mopnm 23056 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 23108 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 23113 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 23154 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 21868 lmmbr 23863 lmmbr2 23864 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 21990 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 23918 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 23881 iscmet2 23899 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 23921 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 22071 metelcls 23910 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 23911 metcld2 23912 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 23705 lmodvneg1 19679 nvinv 28418 vcm 28355 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 23701 lmod0vs 19669 slmd0vs 30854 vc0 28353 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 19670 slmdvs0 30855 vcz 28354 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 28470 ngpmet 23214 nrmmetd 23186 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 28465 imsdval2 28466 ncvspds 23767 ngpds 23215 |
| [Kreyszig] p. 63 | Problem 1 | nmval 23201 nvnd 28467 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 23229 nmge0 23228 nvge0 28452 nvz 28448 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 23235 nvabs 28451 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 28580 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 28524 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 28586 blocni 28584 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 28585 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 23810 ipeq0 20784 ipz 28498 |
| [Kreyszig] p. 135 | Problem 2 | pythi 28629 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 28633 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 15213 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 24041 minveco 28663 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 28529 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 23934 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 28652 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 29902 leopg 29901 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 29920 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 28697 |
| [Kulpa] p. 547 | Theorem | poimir 34927 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 34926 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 34925 |
| [Kulpa] p. 548 | Theorem | broucube 34928 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 34920 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 34921 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2401 axnul 5211 |
| [Kunen] p. 11 | Axiom 3 | axnul 5211 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7658 |
| [Kunen] p. 24 | Definition 10.24 | mapval 8420 mapvalg 8418 |
| [Kunen] p. 30 | Lemma 10.20 | fodom 9946 |
| [Kunen] p. 31 | Definition 10.24 | mapex 8414 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 9195 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 9237 r1elssi 9236 |
| [Kunen] p. 107 | Exercise 4 | rankop 9289 rankopb 9283 rankuni 9294 rankxplim 9310 rankxpsuc 9313 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4933 |
| [Lang] , p. 225 | Corollary 1.3 | finexttrb 31054 |
| [Lang] p. | Definition | df-rn 5568 |
| [Lang] p. 3 | Statement | lidrideqd 17881 mndbn0 17929 |
| [Lang] p. 3 | Definition | df-mnd 17914 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 17899 |
| [Lang] p. 4 | Property of composites. Second formula | gsumccat 18008 |
| [Lang] p. 5 | Equation | gsumreidx 19039 |
| [Lang] p. 5 | Definition of an (infinite) product | gsumfsupp 44096 |
| [Lang] p. 6 | Example | nn0mnd 44093 |
| [Lang] p. 6 | Equation | gsumxp2 19102 |
| [Lang] p. 6 | Statement | cycsubm 18347 |
| [Lang] p. 6 | Definition | mulgnn0gsum 18236 |
| [Lang] p. 6 | Observation | mndlsmidm 18798 |
| [Lang] p. 7 | Definition | dfgrp2e 18131 |
| [Lang] p. 30 | Definition | df-tocyc 30751 |
| [Lang] p. 32 | Property (a) | cyc3genpm 30796 |
| [Lang] p. 32 | Property (b) | cyc3conja 30801 cycpmconjv 30786 |
| [Lang] p. 53 | Definition | df-cat 16941 |
| [Lang] p. 54 | Definition | df-iso 17021 |
| [Lang] p. 57 | Definition | df-inito 17253 df-termo 17254 |
| [Lang] p. 58 | Example | irinitoringc 44347 |
| [Lang] p. 58 | Statement | initoeu1 17273 termoeu1 17280 |
| [Lang] p. 62 | Definition | df-func 17130 |
| [Lang] p. 65 | Definition | df-nat 17215 |
| [Lang] p. 91 | Note | df-ringc 44283 |
| [Lang] p. 92 | Statement | mxidlprm 30979 |
| [Lang] p. 92 | Definition | isprmidlc 30965 |
| [Lang] p. 128 | Remark | dsmmlmod 20891 |
| [Lang] p. 129 | Proof | lincscm 44492 lincscmcl 44494 lincsum 44491 lincsumcl 44493 |
| [Lang] p. 129 | Statement | lincolss 44496 |
| [Lang] p. 129 | Observation | dsmmfi 20884 |
| [Lang] p. 141 | Theorem 5.3 | dimkerim 31025 qusdimsum 31026 |
| [Lang] p. 141 | Corollary 5.4 | lssdimle 31008 |
| [Lang] p. 147 | Definition | snlindsntor 44533 |
| [Lang] p. 504 | Statement | mat1 21058 matring 21054 |
| [Lang] p. 504 | Definition | df-mamu 20997 |
| [Lang] p. 505 | Statement | mamuass 21013 mamutpos 21069 matassa 21055 mattposvs 21066 tposmap 21068 |
| [Lang] p. 513 | Definition | mdet1 21212 mdetf 21206 |
| [Lang] p. 513 | Theorem 4.4 | cramer 21302 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 21198 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 21222 |
| [Lang] p. 515 | Definition | df-minmar1 21246 smadiadetr 21286 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 21221 mdetralt 21219 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 21234 |
| [Lang] p. 518 | Definition | df-madu 21245 |
| [Lang] p. 518 | Proposition 4.16 | madulid 21256 madurid 21255 matinv 21288 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 21500 |
| [Lang], p. 224 | Proposition 1.2 | extdgmul 31053 fedgmul 31029 |
| [Lang], p. 561 | Remark | chpmatply1 21442 |
| [Lang], p. 561 | Definition | df-chpmat 21437 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 40673 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 40668 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 40674 |
| [LeBlanc] p. 277 | Rule R2 | axnul 5211 |
| [Levy] p. 12 | Axiom 4.3.1 | df-clab 2802 |
| [Levy] p. 338 | Axiom | df-clel 2895 df-cleq 2816 |
| [Levy] p. 357 | Proof sketch of conservativity; for details see Appendix | df-clel 2895 df-cleq 2816 |
| [Levy] p. 357 | Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendix | df-clab 2802 |
| [Levy] p. 358 | Axiom | df-clab 2802 |
| [Levy58] p. 2 | Definition I | isfin1-3 9810 |
| [Levy58] p. 2 | Definition II | df-fin2 9710 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 9709 |
| [Levy58] p. 2 | Definition III | df-fin3 9712 |
| [Levy58] p. 3 | Definition V | df-fin5 9713 |
| [Levy58] p. 3 | Definition IV | df-fin4 9711 |
| [Levy58] p. 4 | Definition VI | df-fin6 9714 |
| [Levy58] p. 4 | Definition VII | df-fin7 9715 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 9839 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 33192 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 33202 |
| [Lipparini] p. 6 | Proposition 4.2 | nosupbnd1 33216 |
| [Lipparini] p. 6 | Proposition 4.3 | nosupbnd2 33218 |
| [Lipparini] p. 7 | Theorem 5.1 | noetalem2 33220 noetalem3 33221 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1769 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1770 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1772 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 30187 |
| [Maeda] p. 168 | Lemma 5 | mdsym 30191 mdsymi 30190 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 30185 mdsymlem6 30187 mdsymlem7 30188 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 30189 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 30092 ssdmd2 30093 ssmd1 30090 ssmd2 30091 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 30088 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 30060 df-md 30059 mdbr 30073 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 30110 mdslj1i 30098 mdslj2i 30099 mdslle1i 30096 mdslle2i 30097 mdslmd1i 30108 mdslmd2i 30109 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 30100 mdsl2bi 30102 mdsl2i 30101 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 30114 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 30111 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 30112 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 30089 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 30094 mdsl3 30095 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 30113 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 30208 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 36459 hlrelat1 36538 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 36177 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 30115 cvmdi 30103 cvnbtwn4 30068 cvrnbtwn4 36417 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 30116 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 36478 cvp 30154 cvrp 36554 lcvp 36178 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 30178 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 30177 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 36471 hlexch4N 36530 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 30180 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 36581 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 36887 atpsubN 36891 df-pointsN 36640 pointpsubN 36889 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 36642 pmap11 36900 pmaple 36899 pmapsub 36906 pmapval 36895 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 36903 pmap1N 36905 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 36908 pmapglb2N 36909 pmapglb2xN 36910 pmapglbx 36907 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 36990 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 36615 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 36934 paddclN 36980 paddidm 36979 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 36616 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 36976 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 36615 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 36616 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 18803 lsmmod2 18804 lssats 36150 shatomici 30137 shatomistici 30140 shmodi 29169 shmodsi 29168 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 30079 mdsymlem7 30188 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 29368 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 29272 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 30194 |
| [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 399 df-ex 1781 df-or 844 dfbi2 477 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 28181 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 41256 |
| [Margaris] p. 60 | Theorem 8 | jcn 164 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 41257 |
| [Margaris] p. 79 | Rule C | exinst01 40966 exinst11 40967 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1981 19.2g 2187 r19.2z 4442 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2202 rr19.3v 3663 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2163 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1826 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1782 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2180 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2205 19.9h 2294 exlimd 2218 exlimdh 2298 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2169 excomim 2170 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2346 |
| [Margaris] p. 90 | Section 19 | conventions-labels 28182 conventions-labels 28182 conventions-labels 28182 conventions-labels 28182 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1827 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 40717 albi 1819 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 2227 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 2228 |
| [Margaris] p. 90 | Theorem 19.18 | 2exbi 40719 exbi 1847 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2231 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 40716 2alimdv 1919 alimd 2212 alimdh 1818 alimdv 1917 ax-4 1810 ralimdaa 3219 ralimdv 3180 ralimdva 3179 ralimdvva 3181 sbcimdv 3845 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2207 19.21h 2295 19.21t 2206 19.21vv 40715 alrimd 2215 alrimdd 2214 alrimdh 1864 alrimdv 1930 alrimi 2213 alrimih 1824 alrimiv 1928 alrimivv 1929 hbralrimi 3182 r19.21be 3212 r19.21bi 3210 ralrimd 3220 ralrimdv 3190 ralrimdva 3191 ralrimdvv 3195 ralrimdvva 3196 ralrimi 3218 ralrimia 41405 ralrimiv 3183 ralrimiva 3184 ralrimivv 3192 ralrimivva 3193 ralrimivvva 3194 ralrimivw 3185 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 40718 2eximdv 1920 exim 1834 eximd 2216 eximdh 1865 eximdv 1918 rexim 3243 reximd2a 3314 reximdai 3313 reximdd 41428 reximddv 3277 reximddv2 3280 reximddv3 41427 reximdv 3275 reximdv2 3273 reximdva 3276 reximdvai 3274 reximdvva 3279 reximi2 3246 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2211 19.23bi 2190 19.23h 2296 19.23t 2210 exlimdv 1934 exlimdvv 1935 exlimexi 40865 exlimiv 1931 exlimivv 1933 rexlimd3 41420 rexlimdv 3285 rexlimdv3a 3288 rexlimdva 3286 rexlimdva2 3289 rexlimdvaa 3287 rexlimdvv 3295 rexlimdvva 3296 rexlimdvw 3292 rexlimiv 3282 rexlimiva 3283 rexlimivv 3294 |
| [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 2229 r19.27z 4452 r19.27zv 4453 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2230 19.28vv 40725 r19.28z 4445 r19.28zv 4448 rr19.28v 3664 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1874 r19.29d2r 3337 r19.29imd 3259 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1882 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2236 19.31vv 40723 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2235 r19.32 43303 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 40721 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 2232 19.36vv 40722 r19.36zv 4454 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2234 19.37vv 40724 r19.37zv 4449 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1839 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 1991 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1888 19.40 1887 r19.40 3348 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2237 19.41rg 40891 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2238 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1883 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2239 r19.44zv 4451 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2240 r19.45zv 4450 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2694 |
| [Mayet] p. 370 | Remark | jpi 30049 largei 30046 stri 30036 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 29991 ishst 29993 |
| [Mayet3] p. 10 | Theorem | hstrbi 30045 hstri 30044 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 29507 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 29508 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 30057 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 29111 chsupcl 29119 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 30139 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 30133 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 30160 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 37121 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 17711 latj32 17709 latjass 17707 |
| [Megill] p. 444 | Axiom C5 | ax-5 1911 ax5ALT 36045 |
| [Megill] p. 444 | Section 7 | conventions 28181 |
| [Megill] p. 445 | Lemma L12 | aecom-o 36039 ax-c11n 36026 axc11n 2448 |
| [Megill] p. 446 | Lemma L17 | equtrr 2029 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 36034 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 36066 hbnae 2454 |
| [Megill] p. 447 | Remark 9.1 | dfsb1 2510 sbid 2257 sbidd-misc 44825 sbidd 44824 |
| [Megill] p. 448 | Remark 9.6 | axc14 2486 |
| [Megill] p. 448 | Scheme C4' | ax-c4 36022 |
| [Megill] p. 448 | Scheme C5' | ax-c5 36021 sp 2182 |
| [Megill] p. 448 | Scheme C6' | ax-11 2161 |
| [Megill] p. 448 | Scheme C7' | ax-c7 36023 |
| [Megill] p. 448 | Scheme C8' | ax-7 2015 |
| [Megill] p. 448 | Scheme C9' | ax-c9 36028 |
| [Megill] p. 448 | Scheme C10' | ax-6 1970 ax-c10 36024 |
| [Megill] p. 448 | Scheme C11' | ax-c11 36025 |
| [Megill] p. 448 | Scheme C12' | ax-8 2116 |
| [Megill] p. 448 | Scheme C13' | ax-9 2124 |
| [Megill] p. 448 | Scheme C14' | ax-c14 36029 |
| [Megill] p. 448 | Scheme C15' | ax-c15 36027 |
| [Megill] p. 448 | Scheme C16' | ax-c16 36030 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 36042 dral1 2461 dral2-o 36068 dral2 2460 drex1 2463 drex2 2464 drsb1 2535 drsb2 2267 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2168 sbequ 2090 sbid2v 2551 |
| [Megill] p. 450 | Example in Appendix | hba1-o 36035 hba1 2301 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 43135 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3864 rspsbca 3865 stdpc4 2073 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 36022 ra4 3871 stdpc5 2208 |
| [Mendelson] p. 81 | Rule C | exlimiv 1931 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 2035 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 2252 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3773 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 5406 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 4350 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 4351 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 4245 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 4294 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 4246 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 4115 |
| [Mendelson] p. 231 | Definition of union | dfun3 4244 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 5346 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4837 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5456 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4561 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5458 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4864 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5700 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 6123 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 7499 |
| [Mendelson] p. 246 | Definition of successor | df-suc 6199 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 8223 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8682 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8603 xpsneng 8604 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8610 xpcomeng 8611 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8613 |
| [Mendelson] p. 255 | Definition | brsdom 8534 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8606 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 8412 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8591 mapsnend 8590 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8688 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8687 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 8448 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8594 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8607 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 9606 djucomen 9605 |
| [Mendelson] p. 258 | Exercise 4.56(f) | djudom1 9610 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 9604 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 8158 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 8186 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 9983 |
| [Mendelson] p. 281 | Definition | df-r1 9195 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 9244 |
| [Mendelson] p. 287 | Axiom system MK | ru 3773 |
| [MertziosUnger] p. 152 | Definition | df-frgr 28040 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 28075 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 28077 vdgn1frgrv3 28078 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 28079 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 28072 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 28065 2pthfrgrrn 28063 2pthfrgrrn2 28064 |
| [Mittelstaedt] p. 9 | Definition | df-oc 29031 |
| [Monk1] p. 22 | Remark | conventions 28181 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 28181 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 4209 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5659 ssrelf 30368 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5660 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 5131 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 6117 coi2 6118 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5792 rn0 5798 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 6002 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5575 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5801 rnxp 6029 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5651 xp0 6017 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5947 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5944 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7623 imaexALTV 35589 imaexg 7622 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5942 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6845 funfvop 6822 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6723 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6733 |
| [Monk1] p. 43 | Theorem 4.6 | funun 6402 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 7015 dff13f 7016 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 6984 funrnex 7657 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 7008 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 6086 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4894 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7708 df-1st 7691 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7709 df-2nd 7692 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 9285 ranksnb 9258 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 9286 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 9287 rankunb 9281 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 9269 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 9195 r1val2 9268 |
| [Monk1] p. 117 | Lemma | zorn2 9930 zorn2g 9927 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 9417 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 9985 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 9412 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1810 |
| [Monk2] p. 105 | Axiom C7 | ax-7 2015 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2177 ax-c15 36027 ax12v2 2179 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 36022 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2161 |
| [Monk2] p. 109 | Lemma 15 | equvini 2477 equvinv 2036 eqvinop 5380 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1911 ax5ALT 36045 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2145 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2161 |
| [Monk2] p. 114 | Lemma 21 | sp 2182 |
| [Monk2] p. 114 | Lemma 22 | axc4 2340 hba1-o 36035 hba1 2301 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2157 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2176 nfra2 3230 nfra2w 3229 |
| [Moore] p. 53 | Part I | df-mre 16859 |
| [Munkres] p. 77 | Example 2 | distop 21605 indistop 21612 indistopon 21611 |
| [Munkres] p. 77 | Example 3 | fctop 21614 fctop2 21615 |
| [Munkres] p. 77 | Example 4 | cctop 21616 |
| [Munkres] p. 78 | Definition of basis | df-bases 21556 isbasis3g 21559 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 16719 tgval2 21566 |
| [Munkres] p. 79 | Remark | tgcl 21579 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 21573 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 21597 tgss3 21596 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 21598 basgen2 21599 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 34632 topdifinfeq 34633 topdifinffin 34631 topdifinfindis 34629 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 21770 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 21648 topcld 21645 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 21649 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 21651 |
| [Munkres] p. 94 | Definition of closure | clsval 21647 |
| [Munkres] p. 94 | Definition of interior | ntrval 21646 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 21685 elcls 21683 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 21693 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 21758 neindisj 21727 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 21760 |
| [Munkres] p. 97 | Definition of limit point | islp2 21755 lpval 21749 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 21925 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 21837 iscn 21845 iscn2 21848 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 21890 cncnp2 21891 cncnpi 21888 df-cnp 21838 iscnp 21847 iscnp2 21849 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 23155 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 23916 |
| [Nathanson] p. 123 | Remark | reprgt 31894 reprinfz1 31895 reprlt 31892 |
| [Nathanson] p. 123 | Definition | df-repr 31882 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 31914 |
| [Nathanson] p. 123 | Proposition | breprexp 31906 breprexpnat 31907 itgexpif 31879 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 29883 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 43982 |
| [Pfenning] p. 17 | Definition XM | natded 28184 |
| [Pfenning] p. 17 | Definition NNC | natded 28184 notnotrd 135 |
| [Pfenning] p. 17 | Definition ` `C | natded 28184 |
| [Pfenning] p. 18 | Rule" | natded 28184 |
| [Pfenning] p. 18 | Definition /\I | natded 28184 |
| [Pfenning] p. 18 | Definition ` `E | natded 28184 natded 28184 natded 28184 natded 28184 natded 28184 |
| [Pfenning] p. 18 | Definition ` `I | natded 28184 natded 28184 natded 28184 natded 28184 natded 28184 |
| [Pfenning] p. 18 | Definition ` `EL | natded 28184 |
| [Pfenning] p. 18 | Definition ` `ER | natded 28184 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 28184 |
| [Pfenning] p. 18 | Definition ` `IR | natded 28184 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 28184 |
| [Pfenning] p. 127 | Definition =E | natded 28184 |
| [Pfenning] p. 127 | Definition =I | natded 28184 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 23808 df-dip 28480 dip0l 28497 ip0l 20782 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 23848 ipval 28482 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 28493 ipcj 20780 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 23811 dipdir 28621 ipdir 20785 ipdiri 28609 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 28489 nmsq 23800 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 28604 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 28606 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 28607 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 23817 dipass 28624 ipass 20791 ipassi 28620 |
| [Prugovecki] p. 186 | Definition of bra | braval 29723 df-bra 29629 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 29630 kbval 29733 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 30161 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 37026 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 30175 atcvat4i 30176 cvrat3 36580 cvrat4 36581 lsatcvat3 36190 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 30061 cvrval 36407 df-cv 30058 df-lcv 36157 lspsncv0 19920 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 37038 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 37039 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2802 rabid 3380 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2285 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2816 |
| [Quine] p. 19 | Definition 2.9 | conventions 28181 df-v 3498 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2947 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2958 abid2f 3014 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2276 |
| [Quine] p. 40 | Theorem 6.2 | sb56 2277 sb6 2093 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2895 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2823 eqid1 28248 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2830 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3775 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3776 dfsbcq2 3777 |
| [Quine] p. 43 | Theorem 6.8 | vex 3499 |
| [Quine] p. 43 | Theorem 6.9 | isset 3508 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3592 spcgv 3597 spcimgf 3590 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3787 spsbcd 3788 |
| [Quine] p. 44 | Theorem 6.12 | elex 3514 |
| [Quine] p. 44 | Theorem 6.13 | elab 3669 elabg 3668 elabgf 3666 |
| [Quine] p. 44 | Theorem 6.14 | noel 4298 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4655 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4572 df-sn 4570 |
| [Quine] p. 49 | Theorem 7.4 | snss 4720 snssg 4719 |
| [Quine] p. 49 | Theorem 7.5 | prss 4755 prssg 4754 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4700 prid1g 4698 prid2 4701 prid2g 4699 snid 4603 snidg 4601 |
| [Quine] p. 51 | Theorem 7.12 | snex 5334 |
| [Quine] p. 51 | Theorem 7.13 | prex 5335 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4860 unisnALT 41267 unisng 4859 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4863 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4870 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4868 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 6330 |
| [Quine] p. 56 | Definition 8.18 | dfaiota2 43293 dfiota2 6317 |
| [Quine] p. 57 | Theorem 8.19 | aiotaval 43300 iotaval 6331 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 6335 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 6337 |
| [Quine] p. 58 | Definition 9.1 | df-op 4576 |
| [Quine] p. 61 | Theorem 9.5 | opabid 5415 opabidw 5414 opelopab 5431 opelopaba 5425 opelopabaf 5433 opelopabf 5434 opelopabg 5427 opelopabga 5422 opelopabgf 5429 oprabid 7190 oprabidw 7189 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5563 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5565 |
| [Quine] p. 64 | Definition 9.15 | df-id 5462 |
| [Quine] p. 65 | Theorem 10.3 | fun0 6421 |
| [Quine] p. 65 | Theorem 10.4 | funi 6389 |
| [Quine] p. 65 | Theorem 10.5 | funsn 6409 funsng 6407 |
| [Quine] p. 65 | Definition 10.1 | df-fun 6359 |
| [Quine] p. 65 | Definition 10.2 | args 5959 dffv4 6669 |
| [Quine] p. 68 | Definition 10.11 | conventions 28181 df-fv 6365 fv2 6667 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13635 nn0opth2i 13634 nn0opthi 13633 omopthi 8286 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 8048 |
| [Quine] p. 232 | Equation i | carddom 9978 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 6443 funimaexg 6442 |
| [Quine] p. 331 | Axiom system NF | ru 3773 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 28863 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 28480 polid 28938 polid2i 28936 polidi 28937 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 28592 |
| [ReedSimon] p. 195 | Remark | lnophm 29798 lnophmi 29797 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 29911 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 29913 leopmuli 29912 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 29916 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 29631 leoppos 29905 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 29915 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 29904 |
| [Roman] p. 4 | Definition | df-dmat 21101 df-dmatalt 44460 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 44153 |
| [Roman] p. 19 | Part Preliminaries | df-ring 19301 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 44547 |
| [Roman] p. 112 | Note | isldepslvec2 44547 ldepsnlinc 44570 zlmodzxznm 44559 |
| [Roman] p. 112 | Example | zlmodzxzequa 44558 zlmodzxzequap 44561 zlmodzxzldep 44566 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 21500 |
| [Rosenlicht] p. 80 | Theorem | heicant 34929 |
| [Rosser] p. 281 | Definition | df-op 4576 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 31918 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 31919 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 44421 pmtr3ncom 18605 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 18601 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 18544 cayleyth 18545 |
| [Rudin] p. 164 | Equation 27 | efcan 15451 |
| [Rudin] p. 164 | Equation 30 | efzval 15457 |
| [Rudin] p. 167 | Equation 48 | absefi 15551 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 199 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1772 |
| [Sanford] p. 39 | Rule 4 | mptxor 1770 |
| [Sanford] p. 40 | Rule 1 | mptnan 1769 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5977 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5980 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5976 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5974 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 16859 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 16860 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 16860 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 16862 |
| [Schechter] p. 139 | Definition AC3 | dfac9 9564 |
| [Schechter] p. 141 | Definition (MC) | dfac11 39669 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 9870 axdc3 9878 |
| [Schechter] p. 187 | Definition of ring with unit | isring 19303 isrngo 35177 |
| [Schechter] p. 276 | Remark 11.6.e | span0 29321 |
| [Schechter] p. 276 | Definition of span | df-span 29088 spanval 29112 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 21603 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 26702 axtgcgrrflx 26250 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 26703 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 26704 axtgcgrid 26251 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 26236 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 26715 axtgsegcon 26252 df-trkgcb 26238 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 26726 axtg5seg 26253 df-trkgcb 26238 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 26727 axtgbtwnid 26254 df-trkgb 26237 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 26729 axtgpasch 26255 df-trkgb 26237 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 26748 df-trkg2d 31938 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 26258 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 26259 df-trkg2d 31938 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 26751 axtgeucl 26260 df-trkge 26239 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 26764 axtgcont 26257 axtgcont1 26256 df-trkgb 26237 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 33450 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 33452 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 33455 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 33459 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 33460 tgcgrcomimp 26265 tgcgrcoml 26267 tgcgrcomr 26266 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 33465 tgcgrtriv 26272 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 33469 tg5segofs 31946 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 31943 df-ofs 33446 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 33471 tgcgrextend 26273 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 33473 tgsegconeq 26274 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 33485 btwntriv2 33475 tgbtwntriv2 26275 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 33476 tgbtwncom 26276 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 33479 tgbtwntriv1 26279 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 33480 tgbtwnswapid 26280 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 33486 btwnintr 33482 tgbtwnexch2 26284 tgbtwnintr 26281 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 33488 btwnexch3 33483 tgbtwnexch 26286 tgbtwnexch3 26282 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 33487 tgbtwnouttr 26285 tgbtwnouttr2 26283 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 26747 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 33490 tgbtwndiff 26294 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 26287 trisegint 33491 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 33507 tgifscgr 26296 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 26346 colrot1 26347 colrot2 26348 lncom 26410 lnrot1 26411 lnrot2 26412 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 33503 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 33508 tgcgrsub 26297 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 33518 tgcgrxfr 26306 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 26305 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 33504 df-cgrg 26299 |
| [Schwabhauser] p. 35 | Definition instead (given | df-cgrg 26299 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 33519 tgbtwnxfr 26318 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 33525 colinearperm2 33527 colinearperm3 33526 colinearperm4 33528 colinearperm5 33529 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 26321 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 33502 tgellng 26341 tglng 26334 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 33530 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 33538 lnxfr 26354 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 33539 lnext 26355 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 33543 tgfscgr 26356 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 33544 lncgr 26357 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 33505 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 33546 lnid 26358 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 33547 tgidinside 26359 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 33564 tgbtwnconn1 26363 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 33565 tgbtwnconn2 26364 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 33566 tgbtwnconn3 26365 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 33572 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 33570 legov 26373 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 26374 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 26387 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 33573 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 33575 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 33577 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 33578 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 33579 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 33576 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 33581 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 26375 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 26377 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 26378 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 26379 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 26380 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 33588 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 33589 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 33584 df-outsideof 33583 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 33585 ishlg 26390 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 26395 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 26397 outsideofrflx 33590 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 26391 hlcomd 26392 outsideofcom 33591 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 26398 outsideoftr 33592 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 26406 outsideofeu 33594 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 33601 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 33602 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 33595 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 33610 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 33611 tglineelsb2 26420 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 33613 linerflx1 33612 linerflx2 33614 tglinecom 26423 tglinerflx1 26421 tglinerflx2 26422 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 33616 tglinethru 26424 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 33600 tglng 26334 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 26382 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 33619 tglinethrueu 26427 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 33620 tglineineq 26431 tglineinteq 26433 tglineintmo 26430 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 26437 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 26438 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 26439 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 26454 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 26450 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 26442 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 26441 ismir 26447 mirbtwn 26446 mircgr 26445 mirfv 26444 mirval 26443 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 26452 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 26453 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 26454 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 26457 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 26458 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 26463 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 26460 mirbtwni 26459 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 26461 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 26473 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 26477 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 26474 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 26475 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 26476 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 26479 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 26480 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 26486 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 26482 israg 26485 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 26487 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 26488 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 26490 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 26491 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 26492 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 26493 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 26494 ragncol 26497 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 26495 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 26501 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 26505 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 26502 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 26484 isperp 26500 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 26503 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 26510 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 26518 colperpexlem2 26519 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 26521 colperpexlem3 26520 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 26526 midex 26525 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 26523 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 26532 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 26527 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 26536 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 26539 opphllem6 26540 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 26542 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 26255 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 26543 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 26551 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 26546 hpgbr 26548 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 26553 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 26552 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 26554 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 26555 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 26556 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 26557 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 26558 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 26572 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 26562 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 26576 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 26577 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 26578 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 26579 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 26580 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 26583 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 26585 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 26563 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 26586 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 26589 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 26590 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 26591 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 26592 trgcopyeu 26594 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 26618 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 26597 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 26606 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 26604 cgrahl2 26605 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 26607 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 26608 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 26610 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 26611 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 26614 cgrahl 26615 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 26619 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 26620 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 26621 acopyeu 26622 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 26629 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 26633 |
| [Schwabhauser] p. 101 | Definition 11.23 | isinag 26626 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 26641 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 26634 isleag 26635 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 26643 tgsas1 26642 tgsas2 26644 tgsas3 26645 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 26647 tgasa1 26646 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 26648 tgsss2 26649 tgsss3 26650 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 25849 dchrsum 25847 dchrsum2 25846 sumdchr 25850 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 25851 sum2dchr 25852 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 19190 ablfacrp2 19191 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 25794 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 25795 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 25802 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 26060 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 26063 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 26117 vmalogdivsum2 26116 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 26107 dirith2 26106 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 26105 rpvmasum 26104 rpvmasum2 26090 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 26065 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 26103 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 26070 dchrisumlem1 26067 dchrisumlem2 26068 dchrisumlem3 26069 dchrisumlema 26066 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 26073 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 26102 dchrmusumlem 26100 dchrvmasumlem 26101 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 26072 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 26074 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 26098 dchrisum0re 26091 dchrisumn0 26099 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 26084 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 26088 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 26089 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 26144 pntrsumbnd2 26145 pntrsumo1 26143 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 26108 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 26110 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 26112 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 26115 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 26120 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 26121 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 26126 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 26128 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 26129 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 26137 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 26138 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 26135 selberg3lem2 26136 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 26139 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 26133 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 26146 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 26147 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 26148 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 26162 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 26174 pntlemb 26175 pntlemc 26173 pntlemd 26172 pntlemg 26176 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 26174 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 26166 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 26171 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 26174 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 26187 pntleml 26189 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 4271 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 4357 dif0 4334 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4439 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4425 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 4264 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 4265 |
| [Stoll] p. 20 | Remark | invdif 4247 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4578 |
| [Stoll] p. 43 | Definition | uniiun 4984 |
| [Stoll] p. 44 | Definition | intiin 4985 |
| [Stoll] p. 45 | Definition | df-iin 4924 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4923 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 404 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 4271 |
| [Strang] p. 242 | Section 6.3 | expgrowth 40674 |
| [Suppes] p. 22 | Theorem 2 | eq0 4310 eq0f 4307 |
| [Suppes] p. 22 | Theorem 4 | eqss 3984 eqssd 3986 eqssi 3985 |
| [Suppes] p. 23 | Theorem 5 | ss0 4354 ss0b 4353 |
| [Suppes] p. 23 | Theorem 6 | sstr 3977 sstrALT2 41176 |
| [Suppes] p. 23 | Theorem 7 | pssirr 4079 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 4080 |
| [Suppes] p. 23 | Theorem 9 | psstr 4083 |
| [Suppes] p. 23 | Theorem 10 | pssss 4074 |
| [Suppes] p. 25 | Theorem 12 | elin 4171 elun 4127 |
| [Suppes] p. 26 | Theorem 15 | inidm 4197 |
| [Suppes] p. 26 | Theorem 16 | in0 4347 |
| [Suppes] p. 27 | Theorem 23 | unidm 4130 |
| [Suppes] p. 27 | Theorem 24 | un0 4346 |
| [Suppes] p. 27 | Theorem 25 | ssun1 4150 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 4158 |
| [Suppes] p. 27 | Theorem 27 | unss 4162 |
| [Suppes] p. 27 | Theorem 28 | indir 4254 |
| [Suppes] p. 27 | Theorem 29 | undir 4255 |
| [Suppes] p. 28 | Theorem 32 | difid 4332 |
| [Suppes] p. 29 | Theorem 33 | difin 4240 |
| [Suppes] p. 29 | Theorem 34 | indif 4248 |
| [Suppes] p. 29 | Theorem 35 | undif1 4426 |
| [Suppes] p. 29 | Theorem 36 | difun2 4431 |
| [Suppes] p. 29 | Theorem 37 | difin0 4424 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4423 |
| [Suppes] p. 29 | Theorem 39 | difundi 4258 |
| [Suppes] p. 29 | Theorem 40 | difindi 4260 |
| [Suppes] p. 30 | Theorem 41 | nalset 5219 |
| [Suppes] p. 39 | Theorem 61 | uniss 4848 |
| [Suppes] p. 39 | Theorem 65 | uniop 5407 |
| [Suppes] p. 41 | Theorem 70 | intsn 4914 |
| [Suppes] p. 42 | Theorem 71 | intpr 4911 intprg 4912 |
| [Suppes] p. 42 | Theorem 73 | op1stb 5365 |
| [Suppes] p. 42 | Theorem 78 | intun 4910 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4960 dfiun2g 4957 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4961 |
| [Suppes] p. 47 | Theorem 86 | elpw 4545 elpw2 5250 elpw2g 5249 elpwg 4544 elpwgdedVD 41258 |
| [Suppes] p. 47 | Theorem 87 | pwid 4565 |
| [Suppes] p. 47 | Theorem 89 | pw0 4747 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4748 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5572 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5706 xpindir 5707 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5622 xpundir 5623 |
| [Suppes] p. 54 | Theorem 105 | elirrv 9062 |
| [Suppes] p. 58 | Theorem 2 | relss 5658 |
| [Suppes] p. 59 | Theorem 4 | eldm 5771 eldm2 5772 eldm2g 5770 eldmg 5769 |
| [Suppes] p. 59 | Definition 3 | df-dm 5567 |
| [Suppes] p. 60 | Theorem 6 | dmin 5782 |
| [Suppes] p. 60 | Theorem 8 | rnun 6006 |
| [Suppes] p. 60 | Theorem 9 | rnin 6007 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5761 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5755 brcnvg 5752 |
| [Suppes] p. 62 | Equation 5 | elcnv 5749 elcnv2 5750 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5969 |
| [Suppes] p. 62 | Theorem 15 | cnvin 6005 |
| [Suppes] p. 62 | Theorem 16 | cnvun 6003 |
| [Suppes] p. 63 | Definition | dftrrels2 35813 |
| [Suppes] p. 63 | Theorem 20 | co02 6115 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5844 |
| [Suppes] p. 63 | Definition 7 | df-co 5566 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5758 |
| [Suppes] p. 64 | Theorem 27 | coass 6120 |
| [Suppes] p. 65 | Theorem 31 | resundi 5869 |
| [Suppes] p. 65 | Theorem 34 | elima 5936 elima2 5937 elima3 5938 elimag 5935 |
| [Suppes] p. 65 | Theorem 35 | imaundi 6010 |
| [Suppes] p. 66 | Theorem 40 | dminss 6012 |
| [Suppes] p. 66 | Theorem 41 | imainss 6013 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 6016 |
| [Suppes] p. 81 | Definition 34 | dfec2 8294 |
| [Suppes] p. 82 | Theorem 72 | elec 8335 elecALTV 35529 elecg 8334 |
| [Suppes] p. 82 | Theorem 73 | eqvrelth 35848 erth 8340 erth2 8341 |
| [Suppes] p. 83 | Theorem 74 | eqvreldisj 35851 erdisj 8343 |
| [Suppes] p. 89 | Theorem 96 | map0b 8449 |
| [Suppes] p. 89 | Theorem 97 | map0 8453 map0g 8450 |
| [Suppes] p. 89 | Theorem 98 | mapsn 8454 mapsnd 8452 |
| [Suppes] p. 89 | Theorem 99 | mapss 8455 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 9496 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 9495 |
| [Suppes] p. 92 | Theorem 1 | enref 8544 enrefg 8543 |
| [Suppes] p. 92 | Theorem 2 | ensym 8560 ensymb 8559 ensymi 8561 |
| [Suppes] p. 92 | Theorem 3 | entr 8563 |
| [Suppes] p. 92 | Theorem 4 | unen 8598 |
| [Suppes] p. 94 | Theorem 15 | endom 8538 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8557 |
| [Suppes] p. 94 | Theorem 17 | domtr 8564 |
| [Suppes] p. 95 | Theorem 18 | sbth 8639 |
| [Suppes] p. 97 | Theorem 23 | canth2 8672 canth2g 8673 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8643 df-sdom 8514 dfsdom2 8642 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8656 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8645 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8644 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8654 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 8541 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8657 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8652 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8585 fundmeng 8586 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8617 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8653 |
| [Suppes] p. 104 | Theorem 37 | fofi 8812 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8821 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8821 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 9975 |
| [Suppes] p. 130 | Definition 3 | df-tr 5175 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 7503 |
| [Suppes] p. 134 | Definition 6 | df-suc 6199 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7614 finds 7610 finds1 7613 finds2 7612 |
| [Suppes] p. 151 | Theorem 42 | isfinite 9117 isfinite2 8778 isfiniteg 8780 unbnn 8776 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 10342 df-ltpq 10334 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7579 tfinds 7576 tfinds2 7580 |
| [Suppes] p. 209 | Theorem 18 | oaord1 8179 |
| [Suppes] p. 209 | Theorem 21 | oaword2 8181 |
| [Suppes] p. 211 | Theorem 25 | oaass 8189 |
| [Suppes] p. 225 | Definition 8 | iscard2 9407 |
| [Suppes] p. 227 | Theorem 56 | ondomon 9987 |
| [Suppes] p. 228 | Theorem 59 | harcard 9409 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 9494 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 6243 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 7515 onminsb 7516 |
| [Suppes] p. 229 | Theorem 64 | alephval2 9996 |
| [Suppes] p. 229 | Theorem 65 | alephcard 9498 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 9505 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 9499 |
| [Suppes] p. 229 | Definition 12 | df-aleph 9371 |
| [Suppes] p. 242 | Theorem 6 | weth 9919 |
| [Suppes] p. 242 | Theorem 8 | entric 9981 |
| [Suppes] p. 242 | Theorem 9 | carden 9975 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2795 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2816 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2895 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2818 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2843 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 7162 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3773 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 5324 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4592 elpr2 4593 elprg 4590 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4584 elsn2 4606 elsn2g 4605 elsng 4583 velsn 4585 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 5361 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4579 sneqr 4773 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4588 dfsn2 4582 dfsn2ALT 4589 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 7469 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 5370 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 5358 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 5343 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 7471 unexg 7474 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4629 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4841 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3945 df-un 3943 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4857 uniprg 4858 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 5280 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4628 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 6262 elsucg 6260 sstr2 3976 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 4131 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 4180 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 4144 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 4198 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 4252 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 4253 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3956 dfss2 3957 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4543 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 4159 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3954 sseqin2 4194 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3991 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 4207 inss2 4208 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 4031 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4851 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 5344 sspwimp 41259 sspwimpALT 41266 sspwimpALT2 41269 sspwimpcf 41261 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 5351 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 5192 |
| [TakeutiZaring] p. 20 | Definition | df-rab 3149 df-wl-rab 34862 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 5213 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3941 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 4295 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 4332 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 4312 n0f 4309 neq0 4311 neq0f 4308 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 9061 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 9176 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 9178 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3498 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 5221 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 4352 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 5227 ssexg 5229 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 5223 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 9068 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 9063 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 4325 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 4109 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 4267 undif3VD 41223 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 4110 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 4117 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 3145 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 3146 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 7478 xpexg 7475 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5564 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 6427 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6586 fun11 6430 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 6369 svrelfun 6428 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5760 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5762 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5569 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5570 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5566 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 6053 dfrel2 6048 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5573 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5686 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5693 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5705 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5884 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5861 opelresi 5863 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5877 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5880 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5885 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 6399 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 6099 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 6397 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6587 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2693 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 28181 df-fv 6365 fv3 6690 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7632 cnvexg 7631 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7618 dmexg 7615 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7619 rnexg 7616 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 40793 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7627 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6685 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 43380 tz6.12-1-afv2 43447 tz6.12-1 6694 tz6.12-afv 43379 tz6.12-afv2 43446 tz6.12 6695 tz6.12c-afv2 43448 tz6.12c 6697 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2-afv2 43443 tz6.12-2 6662 tz6.12i-afv2 43449 tz6.12i 6698 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 6360 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 6361 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 6363 wfo 6355 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 6362 wf1 6354 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 6364 wf1o 6356 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6804 eqfnfv2 6805 eqfnfv2f 6808 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6761 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 6982 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 6980 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 6443 funimaexg 6442 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 5069 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5477 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5522 dffr3 5964 eliniseg 5960 iniseg 5962 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5467 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5535 fr3nr 7496 frirr 5534 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5516 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 7498 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5524 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5544 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 6181 tz6.26i 6182 wefrc 5551 wereu2 5554 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 6183 wfii 6184 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 6366 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 7084 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 7085 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 7091 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 7092 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 7093 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 7097 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 7104 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 7106 |
| [TakeutiZaring] p. 35 | Notation | wtr 5174 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 40794 tz7.2 5541 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 5178 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 6206 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 6214 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 6215 ordelordALT 40878 ordelordALTVD 41208 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 6221 ordelssne 6220 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 6219 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 6223 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 7505 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 7506 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 6197 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 6225 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 40890 ordon 7500 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 7501 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7570 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 6240 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 5176 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 7514 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7548 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 6294 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 6293 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 7502 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4870 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 6199 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 6270 sucidg 6271 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7530 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 6284 ordnbtwn 6283 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7545 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 6198 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7596 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7601 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7558 ordelsuc 7537 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7539 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7568 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7584 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7603 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7604 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7605 |
| [TakeutiZaring] p. 43 | Remark | omon 7593 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 9100 omex 9108 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7591 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7609 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7606 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7607 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7587 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4892 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 5191 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4893 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 5242 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7517 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 6242 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4879 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 9125 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 7512 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 8014 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 8035 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 8036 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 8037 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 8044 tz7.44-2 8045 tz7.44-3 8046 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 8006 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 8001 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 7985 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 8083 tz7.49c 8084 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 8081 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 8080 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 8082 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2740 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 9439 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 9440 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 8159 oasuc 8151 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7577 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 8162 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 8143 oa0r 8165 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 8163 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 8176 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 8247 nnaordi 8246 oaord 8175 oaordi 8174 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4975 uniss2 4873 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 8178 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 8183 oawordex 8185 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 8239 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 8273 |
| [TakeutiZaring] p. 60 | Remark | oancom 9116 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 8188 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 8244 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 8180 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0x 8146 omlim 8160 omsuc 8153 |
| [TakeutiZaring] p. 62 | Definition 8.15(a) | om0 8144 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 8241 nnmcl 8240 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 8260 nnmordi 8259 omord 8196 omordi 8194 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 8197 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 8264 omwordri 8200 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 8166 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 8170 om1r 8171 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 8203 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 8205 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 8206 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 8207 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 8208 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 8236 oe0 8149 oelim 8161 oesuc 8154 onesuc 8157 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 8147 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 8214 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 8215 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 8148 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 8173 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 8216 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 8222 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 8220 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 8221 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 8225 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 8227 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 9172 tz9.1 9173 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 9195 r10 9199 r1lim 9203 r1limg 9202 r1suc 9201 r1sucg 9200 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 9211 r1ord2 9212 r1ordg 9209 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 9221 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 9246 tz9.13 9222 tz9.13g 9223 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 9196 rankval 9247 rankvalb 9228 rankvalg 9248 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 9270 rankelb 9255 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 9284 rankval3 9271 rankval3b 9257 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 9260 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 9226 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 9265 rankr1c 9252 rankr1g 9263 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 9266 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 9280 rankssb 9279 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 9273 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 9272 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 9899 dfac3 9549 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 9458 numth 9896 numth2 9895 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 9970 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 9971 cardid2 9384 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 9391 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 9975 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 9390 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 9375 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 9396 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 9388 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8692 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8574 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8697 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8621 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 9394 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 9526 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8702 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 8710 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 9527 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8707 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 9516 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 9494 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 9403 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9641 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 8794 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 8515 isfi 8535 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 8711 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 9958 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8614 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 9950 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | djuxpdom 9613 unxpdom 8727 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 9405 cardsdomelir 9404 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 8729 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 9442 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 8410 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 9986 infxpidm2 9445 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infdju 9632 infxp 9639 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8626 pw2f1o 8624 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8685 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 9911 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 9906 ac6s5 9915 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 9967 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 9968 uniimadomf 9969 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 9698 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 9693 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 9678 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 9675 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 9681 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 9688 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 9697 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 10006 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 9676 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 9700 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 9525 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 9524 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 9536 alephfp2 9537 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 10123 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 9540 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 9993 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 10007 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 10008 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 36021 |
| [Tarski] p. 67 | Scheme B5 | sp 2182 |
| [Tarski] p. 68 | Lemma 6 | avril1 28244 equid 2019 |
| [Tarski] p. 69 | Lemma 7 | equcomi 2024 |
| [Tarski] p. 70 | Lemma 14 | spim 2405 spime 2407 spimew 1974 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2177 ax-c15 36027 ax12i 1969 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2093 |
| [Tarski] p. 75 | Axiom B7 | ax6v 1971 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1911 ax5ALT 36045 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 2015 ax-8 2116 ax-9 2124 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 26252 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 26253 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 26255 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 26255 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 26256 |
| [Truss] p. 114 | Theorem 5.18 | ruc 15598 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 34933 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 34935 |
| [Weierstrass] p. 272 | Definition | df-mdet 21196 mdetuni 21233 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 900 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 864 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 865 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 916 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 964 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 191 |
| [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 34728 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 40153 imim2 58 wl-luk-imim2 34723 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | adh-minimp-imim1 43262 imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 893 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2748 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 899 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-luk-id 34726 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 891 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 144 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 894 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 132 notnotrALT2 41268 wl-luk-notnotr 34727 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 148 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 40183 axfrege28 40182 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 863 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 921 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 123 wl-luk-pm2.21 34720 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 124 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 886 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 936 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-labels 28182 pm2.27 42 wl-luk-pm2.27 34718 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 919 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 920 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 966 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 967 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 965 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1084 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 903 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 904 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 939 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 878 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 879 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5 171 pm2.5g 170 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6 193 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 880 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 881 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 882 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 174 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 175 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 847 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 848 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 885 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 887 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 194 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 896 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 937 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 938 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 195 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 888 pm2.67 889 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 178 pm2.521g 176 pm2.521g2 177 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 895 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 969 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 897 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 205 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 970 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 971 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 930 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 928 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 968 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 972 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 929 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 109 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 988 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 472 pm3.2im 162 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 989 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 990 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 991 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 992 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 474 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 462 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 405 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 801 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 451 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 452 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 485 simplim 169 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 487 simprim 168 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 763 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 764 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 806 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 623 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 808 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 495 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 496 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 957 pm3.44 956 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 807 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 476 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 960 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34b 318 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 263 |
| [WhiteheadRussell] p. 117 | Theorem *4.11 | notbi 321 |
| [WhiteheadRussell] p. 117 | Theorem *4.12 | con2bi 356 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotb 317 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14 805 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 830 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 224 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 804 bitr 803 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 566 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 901 pm4.25 902 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 463 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 1004 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 866 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 471 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 918 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 633 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 914 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 636 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 973 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1085 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 1002 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1048 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 1019 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 993 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 995 pm4.45 994 pm4.45im 825 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 979 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 849 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 548 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 978 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 981 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 982 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 983 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 984 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 980 pm4.56 985 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 986 pm4.57 987 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 407 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 852 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 400 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 845 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 408 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 846 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67 401 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 560 pm4.71d 564 pm4.71i 562 pm4.71r 561 pm4.71rd 565 pm4.71ri 563 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 946 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 530 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 933 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 520 pm4.76 521 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 958 pm4.77 959 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 931 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 1000 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 395 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81 396 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 1020 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 1021 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 350 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 351 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 354 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 391 impexp 453 pm4.87 839 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 821 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 941 pm5.11g 940 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 942 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 944 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 943 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 1009 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 1010 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 1008 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbn 387 pm5.18 385 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 390 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 822 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 1011 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 1044 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 1045 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 898 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 575 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 392 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 364 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6 998 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 950 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 828 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 576 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 833 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 823 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 831 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 393 pm5.41 394 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 546 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 545 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 1001 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 1014 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 945 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 997 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 1015 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 1016 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 1024 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 369 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 272 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 1025 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 40697 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 40698 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1871 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 40699 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 40700 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 40701 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1894 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 40702 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 40703 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 40704 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 40705 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 40706 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 40708 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 40709 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 40710 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 40707 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2100 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 40713 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 40714 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2075 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2164 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1829 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1830 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 40715 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 40716 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 40717 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 40718 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 40720 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 40719 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1888 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 40722 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 40723 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 40721 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1828 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 40724 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 40725 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1846 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 40726 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2367 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 1860 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 40731 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 40727 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 40728 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 40729 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 40730 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 40735 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 40732 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 40733 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 40734 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 40736 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2654 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 40746 pm13.13b 40747 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 40748 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 3099 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 3101 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3661 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 40754 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 40755 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 40749 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 40893 pm13.193 40750 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 40751 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 40752 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 40753 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 40760 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 40759 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 40758 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3838 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 40761 pm14.122b 40762 pm14.122c 40763 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 40764 pm14.123b 40765 pm14.123c 40766 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 40768 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 40767 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 40769 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 6338 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 40770 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 6339 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 40771 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 40773 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2718 eupickbi 2721 sbaniota 40774 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 40772 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 2669 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 40776 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 28181 df-fv 6365 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 9431 pm54.43lem 9430 |
| [Young] p. 141 | Definition of operator ordering | leop2 29903 |
| [Young] p. 142 | Example 12.2(i) | 0leop 29909 idleop 29910 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 39432 |
| [vandenDries] p. 43 | Theorem 62 | pellex 39439 pellexlem1 39433 |