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 17377 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 17377 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 17791 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 17398 |
| [Adamek] p. 24 | Example 3.3(4.d) | df-prstc 46344 prsthinc 46335 |
| [Adamek] p. 24 | Example 3.3(4.e) | df-mndtc 46365 df-mndtc 46365 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 17421 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 17493 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 17481 invisoinvl 17502 |
| [Adamek] p. 28 | Example 3.13 | idinv 17501 idiso 17500 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 17486 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 17460 df-iso 17461 dfiso2 17484 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 17467 |
| [Adamek] p. 29 | Remark 3.16 | cicer 17518 |
| [Adamek] p. 29 | Definition 3.15 | cic 17511 df-cic 17508 |
| [Adamek] p. 29 | Definition 3.17 | df-func 17573 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 17482 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 17483 isoco 17489 |
| [Adamek] p. 30 | Remark 3.19 | df-func 17573 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 17596 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 17589 |
| [Adamek] p. 33 | Example 3.26(2) | df-thinc 46301 prsthinc 46335 thincciso 46330 |
| [Adamek] p. 33 | Example 3.26(3) | df-mndtc 46365 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 17603 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 17826 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 17884 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 17621 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 17620 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 17884 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 17645 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 17651 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 17650 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 17869 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 17869 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 17590 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 17814 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 17639 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 17638 |
| [Adamek] p. 40 | Remark 3.48 | catccat 17823 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 17814 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 17553 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 17554 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 17565 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 17524 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 17654 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 17659 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 17682 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 17686 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 17660 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 17688 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 17699 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 45627 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 17700 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 17727 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 17731 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 17701 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 45630 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 17734 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 17459 |
| [Adamek] p. 185 | Section 10.67 | updjud 9692 |
| [Adamek] p. 478 | Item Rng | df-ringc 45563 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 45894 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 45916 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 14274 df-pfx 14384 df-substr 14354 df-word 14218 lencl 14236 wrd0 14242 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 23872 df-nmoo 29107 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 30515 hmopidmchi 30513 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 30563 pjcmul2i 30564 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 30280 unoplin 30282 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 30281 unopadj2 30300 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 30375 lnopunii 30374 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 30448 |
| [Alling] p. 125 | Theorem 4.02(12) | cofcutrtime 34093 |
| [Alling] p. 184 | Axiom B | bdayfo 33880 |
| [Alling] p. 184 | Axiom O | sltso 33879 |
| [Alling] p. 184 | Axiom SD | nodense 33895 |
| [Alling] p. 185 | Lemma 0 | nocvxmin 33973 |
| [Alling] p. 185 | Theorem | conway 33993 |
| [Alling] p. 185 | Axiom FE | noeta 33946 |
| [Alling] p. 186 | Theorem 4 | slerec 34013 |
| [Apostol] p. 18 | Theorem I.1 | addcan 11159 addcan2d 11179 addcan2i 11169 addcand 11178 addcani 11168 |
| [Apostol] p. 18 | Theorem I.2 | negeu 11211 |
| [Apostol] p. 18 | Theorem I.3 | negsub 11269 negsubd 11338 negsubi 11299 |
| [Apostol] p. 18 | Theorem I.4 | negneg 11271 negnegd 11323 negnegi 11291 |
| [Apostol] p. 18 | Theorem I.5 | subdi 11408 subdid 11431 subdii 11424 subdir 11409 subdird 11432 subdiri 11425 |
| [Apostol] p. 18 | Theorem I.6 | mul01 11154 mul01d 11174 mul01i 11165 mul02 11153 mul02d 11173 mul02i 11164 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 11612 mulcan2d 11609 mulcand 11608 mulcani 11614 |
| [Apostol] p. 18 | Theorem I.8 | receu 11620 xreceu 31196 |
| [Apostol] p. 18 | Theorem I.9 | divrec 11649 divrecd 11754 divreci 11720 divreczi 11713 |
| [Apostol] p. 18 | Theorem I.10 | recrec 11672 recreci 11707 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 11615 mul0ord 11625 mul0ori 11623 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 11414 mul2negd 11430 mul2negi 11423 mulneg1 11411 mulneg1d 11428 mulneg1i 11421 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 11690 divadddivd 11795 divadddivi 11737 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 11675 divmuldivd 11792 divmuldivi 11735 rdivmuldivd 31488 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 11676 divdivdivd 11798 divdivdivi 11738 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 12752 rpaddcld 12787 rpmulcl 12753 rpmulcld 12788 |
| [Apostol] p. 20 | Axiom 8 | rpneg 12762 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 12765 |
| [Apostol] p. 20 | Theorem I.17 | lttri 11101 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 11568 ltadd1dd 11586 ltadd1i 11529 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 11825 ltmul1a 11824 ltmul1i 11893 ltmul1ii 11903 ltmul2 11826 ltmul2d 12814 ltmul2dd 12828 ltmul2i 11896 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 11495 msqgt0d 11542 msqgt0i 11512 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 11497 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 11481 lt0neg1d 11544 ltneg 11475 ltnegd 11553 ltnegi 11519 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 11460 lt2addd 11598 lt2addi 11537 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 12731 |
| [Apostol] p. 21 | Exercise 4 | recgt0 11821 recgt0d 11909 recgt0i 11880 recgt0ii 11881 |
| [Apostol] p. 22 | Definition of integers | df-z 12320 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11987 |
| [Apostol] p. 22 | Definition of rationals | df-q 12689 |
| [Apostol] p. 24 | Theorem I.26 | supeu 9213 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 12229 |
| [Apostol] p. 26 | Theorem I.29 | arch 12230 |
| [Apostol] p. 28 | Exercise 2 | btwnz 12423 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 12231 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 12687 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 12686 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12933 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 16048 zneo 12403 zneoALTV 45121 |
| [Apostol] p. 29 | Theorem I.35 | cxpsqrtth 25884 msqsqrtd 15152 resqrtth 14967 sqrtth 15076 sqrtthi 15082 sqsqrtd 15151 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11976 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 12653 |
| [Apostol] p. 361 | Remark | crreczi 13943 |
| [Apostol] p. 363 | Remark | absgt0i 15111 |
| [Apostol] p. 363 | Example | abssubd 15165 abssubi 15115 |
| [ApostolNT] p. 7 | Remark | fmtno0 44992 fmtno1 44993 fmtno2 45002 fmtno3 45003 fmtno4 45004 fmtno5fac 45034 fmtnofz04prm 45029 |
| [ApostolNT] p. 7 | Definition | df-fmtno 44980 |
| [ApostolNT] p. 8 | Definition | df-ppi 26249 |
| [ApostolNT] p. 14 | Definition | df-dvds 15964 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 15979 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 16003 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15998 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15992 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15994 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 15980 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 15981 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15986 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 16020 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 16022 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 16024 |
| [ApostolNT] p. 15 | Definition | df-gcd 16202 dfgcd2 16254 |
| [ApostolNT] p. 16 | Definition | isprm2 16387 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 16358 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 16616 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 16220 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 16255 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 16257 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 16235 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 16227 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 16416 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 16418 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 16629 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 16623 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 16112 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 16292 |
| [ApostolNT] p. 24 | Definition | df-mu 26250 |
| [ApostolNT] p. 25 | Definition | df-phi 16467 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 26340 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 16491 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 16477 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 16481 |
| [ApostolNT] p. 32 | Definition | df-vma 26247 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 26342 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 26364 |
| [ApostolNT] p. 38 | Remark | df-sgm 26251 |
| [ApostolNT] p. 38 | Definition | df-sgm 26251 |
| [ApostolNT] p. 75 | Definition | df-chp 26248 df-cht 26246 |
| [ApostolNT] p. 104 | Definition | congr 16369 |
| [ApostolNT] p. 106 | Remark | dvdsval3 15967 |
| [ApostolNT] p. 106 | Definition | moddvds 15974 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 16055 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 16056 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 13608 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 13645 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 13953 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15997 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 16372 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 16775 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 16374 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 16484 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 16502 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 16485 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 26221 |
| [ApostolNT] p. 179 | Definition | df-lgs 26443 lgsprme0 26487 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 26488 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 26464 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 26479 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 26536 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 26555 2lgsoddprm 26564 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 26522 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 26531 |
| [ApostolNT] p. 188 | Definition | df-lgs 26443 lgs1 26489 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 26480 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 26482 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 26490 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 26491 |
| [Baer] p. 40 | Property (b) | mapdord 39652 |
| [Baer] p. 40 | Property (c) | mapd11 39653 |
| [Baer] p. 40 | Property (e) | mapdin 39676 mapdlsm 39678 |
| [Baer] p. 40 | Property (f) | mapd0 39679 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 39639 mapd1o 39662 |
| [Baer] p. 41 | Property (g) | mapdat 39681 |
| [Baer] p. 44 | Part (1) | mapdpg 39720 |
| [Baer] p. 45 | Part (2) | hdmap1eq 39815 mapdheq 39742 mapdheq2 39743 mapdheq2biN 39744 |
| [Baer] p. 45 | Part (3) | baerlem3 39727 |
| [Baer] p. 46 | Part (4) | mapdheq4 39746 mapdheq4lem 39745 |
| [Baer] p. 46 | Part (5) | baerlem5a 39728 baerlem5abmN 39732 baerlem5amN 39730 baerlem5b 39729 baerlem5bmN 39731 |
| [Baer] p. 47 | Part (6) | hdmap1l6 39835 hdmap1l6a 39823 hdmap1l6e 39828 hdmap1l6f 39829 hdmap1l6g 39830 hdmap1l6lem1 39821 hdmap1l6lem2 39822 mapdh6N 39761 mapdh6aN 39749 mapdh6eN 39754 mapdh6fN 39755 mapdh6gN 39756 mapdh6lem1N 39747 mapdh6lem2N 39748 |
| [Baer] p. 48 | Part 9 | hdmapval 39842 |
| [Baer] p. 48 | Part 10 | hdmap10 39854 |
| [Baer] p. 48 | Part 11 | hdmapadd 39857 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 39831 mapdh6hN 39757 |
| [Baer] p. 48 | Part (7) | mapdh75cN 39767 mapdh75d 39768 mapdh75e 39766 mapdh75fN 39769 mapdh7cN 39763 mapdh7dN 39764 mapdh7eN 39762 mapdh7fN 39765 |
| [Baer] p. 48 | Part (8) | mapdh8 39802 mapdh8a 39789 mapdh8aa 39790 mapdh8ab 39791 mapdh8ac 39792 mapdh8ad 39793 mapdh8b 39794 mapdh8c 39795 mapdh8d 39797 mapdh8d0N 39796 mapdh8e 39798 mapdh8g 39799 mapdh8i 39800 mapdh8j 39801 |
| [Baer] p. 48 | Part (9) | mapdh9a 39803 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 39783 |
| [Baer] p. 49 | Part 12 | hdmap11 39862 hdmapeq0 39858 hdmapf1oN 39879 hdmapneg 39860 hdmaprnN 39878 hdmaprnlem1N 39863 hdmaprnlem3N 39864 hdmaprnlem3uN 39865 hdmaprnlem4N 39867 hdmaprnlem6N 39868 hdmaprnlem7N 39869 hdmaprnlem8N 39870 hdmaprnlem9N 39871 hdmapsub 39861 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 39882 hdmap14lem10 39891 hdmap14lem1a 39880 hdmap14lem2N 39883 hdmap14lem2a 39881 hdmap14lem3 39884 hdmap14lem8 39889 hdmap14lem9 39890 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 39892 hdmap14lem12 39893 hdmap14lem13 39894 hdmap14lem14 39895 hdmap14lem15 39896 hgmapval 39901 |
| [Baer] p. 50 | Part 15 | hgmapadd 39908 hgmapmul 39909 hgmaprnlem2N 39911 hgmapvs 39905 |
| [Baer] p. 50 | Part 16 | hgmaprnN 39915 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 39931 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 39932 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 39933 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 39934 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 39936 hgmapvv 39940 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 39935 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 39937 |
| [Baer] p. 111 | Line 15 | hdmapg 39944 hdmapglem7 39943 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 25885 2irrexpqALT 25950 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2569 |
| [BellMachover] p. 460 | Notation | df-mo 2540 |
| [BellMachover] p. 460 | Definition | mo3 2564 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2709 |
| [BellMachover] p. 462 | Theorem 1.1 | axextmo 2713 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 5215 |
| [BellMachover] p. 463 | Scheme Sep | ax-sep 5223 |
| [BellMachover] p. 463 | Theorem 1.3(ii) | bj-bm1.3ii 35235 bm1.3ii 5226 |
| [BellMachover] p. 466 | Problem | axpow2 5290 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 5291 |
| [BellMachover] p. 466 | Axiom Union | axun2 7590 |
| [BellMachover] p. 468 | Definition | df-ord 6269 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 6284 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 6291 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 6286 |
| [BellMachover] p. 471 | Definition of N | df-om 7713 |
| [BellMachover] p. 471 | Problem 2.5(ii) | uniordint 7651 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 6271 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 9400 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7728 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 9522 |
| [BellMachover] p. 478 | Definition | rankval2 9576 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 9540 r1ord3g 9537 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 9354 |
| [BellMachover] p. 488 | Axiom AC | ac5 10233 dfac4 9878 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 9866 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 37333 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 30715 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 30757 chirredi 30756 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 30745 |
| [Beran] p. 3 | Definition of join | sshjval3 29716 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 29978 cmcm2i 29955 cmcm2ii 29960 cmt2N 37264 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 29979 lecmi 29964 lecmii 29965 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 29953 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 29982 cm2ji 29987 cm2mi 29988 |
| [Beran] p. 95 | Definition | df-sh 29569 issh2 29571 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 29448 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 29461 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 29452 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 30190 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 30192 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 30191 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 30193 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 29444 his1i 29462 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 29445 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 29446 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 29447 |
| [Beran] p. 96 | Definition of norm | df-hnorm 29330 dfhnorm2 29484 normval 29486 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 29546 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 29335 |
| [Beran] p. 96 | Definition of complete subspace | isch3 29603 |
| [Beran] p. 96 | Definition of converge | df-hlim 29334 hlimi 29550 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 29495 norm-i 29491 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 29499 norm-ii 29500 normlem0 29471 normlem1 29472 normlem2 29473 normlem3 29474 normlem4 29475 normlem5 29476 normlem6 29477 normlem7 29478 normlem7tALT 29481 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 29501 norm-iii 29502 |
| [Beran] p. 98 | Remark 3.4 | bcs 29543 bcsiALT 29541 bcsiHIL 29542 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 29483 normpar 29517 normpari 29516 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 29508 normpyth 29507 normpythi 29504 |
| [Beran] p. 99 | Remark | lnfn0 30409 lnfn0i 30404 lnop0 30328 lnop0i 30332 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 30388 nmcfnex 30415 nmcfnexi 30413 nmcopex 30391 nmcopexi 30389 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 30416 nmcfnlbi 30414 nmcoplb 30392 nmcoplbi 30390 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 30418 lnfnconi 30417 lnopcon 30397 lnopconi 30396 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 29518 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 29515 norm3adifii 29510 norm3dif 29512 norm3difi 29509 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 29663 pjhth 29755 pjhtheu 29756 pjpjhth 29787 pjpjhthi 29788 pjth 24603 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 29768 ococi 29767 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 30423 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 30424 riesz4 30426 riesz4i 30425 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 30441 cnlnadjeu 30440 cnlnadjeui 30439 cnlnadji 30438 cnlnadjlem1 30429 nmopadjlei 30450 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 30453 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 30452 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 30454 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 30298 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 30464 nmopcoadji 30463 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 30455 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 30465 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 30462 pjadj2coi 30566 pjadjcoi 30523 |
| [Beran] p. 107 | Definition | df-ch 29583 isch2 29585 |
| [Beran] p. 107 | Remark 3.12 | choccl 29668 isch3 29603 occl 29666 ocsh 29645 shoccl 29667 shocsh 29646 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 29770 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 29694 |
| [Beran] p. 109 | Property (i) | pjadj2 30549 pjadj3 30550 pjadji 30047 pjadjii 30036 |
| [Beran] p. 109 | Property (ii) | pjidmco 30543 pjidmcoi 30539 pjidmi 30035 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 30535 |
| [Beran] p. 111 | Remark | ho0val 30112 pjch1 30032 |
| [Beran] p. 111 | Definition | df-hfmul 30096 df-hfsum 30095 df-hodif 30094 df-homul 30093 df-hosum 30092 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 30033 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 30056 pjchi 29794 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 29801 pjoc2i 29800 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 30042 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 30527 pjssmii 30043 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 30526 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 30525 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 30530 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 30528 pjssge0ii 30044 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 30529 pjdifnormii 30045 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1779 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1777 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1780 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1775 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 32259 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 32267 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 32265 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 32269 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 32289 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 32320 df-sitm 32298 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 32320 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 32297 |
| [Bollobas] p. 1 | Section I.1 | df-edg 27418 isuhgrop 27440 isusgrop 27532 isuspgrop 27531 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 27635 uhgrspan1 27670 uhgrspansubgr 27658 |
| [Bollobas] p. 3 | Definition | isomuspgr 45286 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 27821 df-cusgr 27779 df-nbgr 27700 fusgrmaxsize 27831 |
| [Bollobas] p. 4 | Definition | df-upwlks 45296 df-wlks 27966 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 27917 finsumvtxdgeven 27919 fusgr1th 27918 fusgrvtxdgonume 27921 vtxdgoddnumeven 27920 |
| [Bollobas] p. 5 | Notation | df-pths 28084 |
| [Bollobas] p. 5 | Definition | df-crcts 28154 df-cycls 28155 df-trls 28060 df-wlkson 27967 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 27429 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 45394 df-cllaw 45380 df-mgm 18326 df-mgm2 45413 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 45395 df-asslaw 45382 df-sgrp 18375 df-sgrp2 45415 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 45414 df-comlaw 45381 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 18386 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 19785 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 45433 |
| [BourbakiEns] p. | Proposition 8 | fcof1 7159 fcofo 7160 |
| [BourbakiTop1] p. | Remark | xnegmnf 12944 xnegpnf 12943 |
| [BourbakiTop1] p. | Remark | rexneg 12945 |
| [BourbakiTop1] p. | Remark 3 | ust0 23371 ustfilxp 23364 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 23241 |
| [BourbakiTop1] p. | Criterion | ishmeo 22910 |
| [BourbakiTop1] p. | Example 1 | cstucnd 23436 iducn 23435 snfil 23015 |
| [BourbakiTop1] p. | Example 2 | neifil 23031 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 23218 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 23456 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 31907 |
| [BourbakiTop1] p. | Paragraph 3 | infil 23014 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 23428 df-ust 23352 filintn0 23012 filn0 23013 istgp 23228 ucnprima 23434 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 23439 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 23450 df-usp 23409 df-utop 23383 trust 23381 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 31806 |
| [BourbakiTop1] p. | Property V_i | ssnei2 22267 |
| [BourbakiTop1] p. | Theorem 1(d) | iscncl 22420 |
| [BourbakiTop1] p. | Condition F_I | ustssel 23357 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 23360 |
| [BourbakiTop1] p. | Property V_ii | innei 22276 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 22284 neissex 22278 |
| [BourbakiTop1] p. | Proposition 1 | neips 22264 neiss 22260 ucncn 23437 ustund 23373 ustuqtop 23398 |
| [BourbakiTop1] p. | Proposition 2 | cnpco 22418 neiptopreu 22284 utop2nei 23402 utop3cls 23403 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 23444 uspreg 23426 utopreg 23404 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 22842 imasncls 22843 imasnopn 22841 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 23151 |
| [BourbakiTop1] p. | Condition F_II | ustincl 23359 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 23361 |
| [BourbakiTop1] p. | Property V_iii | elnei 22262 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 23455 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 23358 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 23362 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 22538 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 22997 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 22043 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 31803 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 43603 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 43605 stoweid 43604 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 43542 stoweidlem10 43551 stoweidlem14 43555 stoweidlem15 43556 stoweidlem35 43576 stoweidlem36 43577 stoweidlem37 43578 stoweidlem38 43579 stoweidlem40 43581 stoweidlem41 43582 stoweidlem43 43584 stoweidlem44 43585 stoweidlem46 43587 stoweidlem5 43546 stoweidlem50 43591 stoweidlem52 43593 stoweidlem53 43594 stoweidlem55 43596 stoweidlem56 43597 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 43564 stoweidlem24 43565 stoweidlem27 43568 stoweidlem28 43569 stoweidlem30 43571 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 43575 stoweidlem59 43600 stoweidlem60 43601 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 43586 stoweidlem49 43590 stoweidlem7 43548 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 43572 stoweidlem39 43580 stoweidlem42 43583 stoweidlem48 43589 stoweidlem51 43592 stoweidlem54 43595 stoweidlem57 43598 stoweidlem58 43599 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 43566 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 43558 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 43552 stoweidlem13 43554 stoweidlem26 43567 stoweidlem61 43602 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 43559 |
| [Bruck] p. 1 | Section I.1 | df-clintop 45394 df-mgm 18326 df-mgm2 45413 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 18375 df-sgrp2 45415 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 18674 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 5158 |
| [Church] p. 129 | Section II.24 | df-ifp 1061 dfifp2 1062 |
| [Clemente] p. 10 | Definition IT | natded 28767 |
| [Clemente] p. 10 | Definition I` `m,n | natded 28767 |
| [Clemente] p. 11 | Definition E=>m,n | natded 28767 |
| [Clemente] p. 11 | Definition I=>m,n | natded 28767 |
| [Clemente] p. 11 | Definition E` `(1) | natded 28767 |
| [Clemente] p. 11 | Definition E` `(2) | natded 28767 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 28767 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 28767 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 28767 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 28767 |
| [Clemente] p. 14 | Proof 5.11 | natded 28767 |
| [Clemente] p. 14 | Definition E` `n | natded 28767 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 28769 ex-natded5.2 28768 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 28772 ex-natded5.3 28771 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 28774 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 28776 ex-natded5.7 28775 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 28778 ex-natded5.8 28777 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 28780 ex-natded5.13 28779 |
| [Clemente] p. 32 | Definition I` `n | natded 28767 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 28767 |
| [Clemente] p. 32 | Definition E` `n,t | natded 28767 |
| [Clemente] p. 32 | Definition I` `n,t | natded 28767 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 28781 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 28782 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 28784 ex-natded9.26 28783 |
| [Cohen] p. 301 | Remark | relogoprlem 25746 |
| [Cohen] p. 301 | Property 2 | relogmul 25747 relogmuld 25780 |
| [Cohen] p. 301 | Property 3 | relogdiv 25748 relogdivd 25781 |
| [Cohen] p. 301 | Property 4 | relogexp 25751 |
| [Cohen] p. 301 | Property 1a | log1 25741 |
| [Cohen] p. 301 | Property 1b | loge 25742 |
| [Cohen4] p. 348 | Observation | relogbcxpb 25937 |
| [Cohen4] p. 349 | Property | relogbf 25941 |
| [Cohen4] p. 352 | Definition | elogb 25920 |
| [Cohen4] p. 361 | Property 2 | relogbmul 25927 |
| [Cohen4] p. 361 | Property 3 | logbrec 25932 relogbdiv 25929 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 25925 |
| [Cohen4] p. 361 | Property 6 | relogbexp 25930 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 25918 |
| [Cohen4] p. 361 | Property 1(b) | logb1 25919 |
| [Cohen4] p. 367 | Property | logbchbase 25921 |
| [Cohen4] p. 377 | Property 2 | logblt 25934 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 32252 sxbrsigalem4 32254 |
| [Cohn] p. 81 | Section II.5 | acsdomd 18275 acsinfd 18274 acsinfdimd 18276 acsmap2d 18273 acsmapd 18272 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 32257 |
| [Connell] p. 57 | Definition | df-scmat 21640 df-scmatalt 45740 |
| [Conway] p. 4 | Definition | slerec 34013 |
| [Conway] p. 5 | Definition | addsval 34126 df-adds 34119 df-negs 34120 |
| [Conway] p. 7 | Theorem | 0slt1s 34023 |
| [Conway] p. 16 | Theorem 0(i) | ssltright 34055 |
| [Conway] p. 16 | Theorem 0(ii) | ssltleft 34054 |
| [Conway] p. 16 | Theorem 0(iii) | slerflex 33966 |
| [Conway] p. 17 | Theorem 3 | addscom 34129 addscomd 34130 addsid1 34127 addsid1d 34128 |
| [Conway] p. 17 | Definition | df-0s 34018 |
| [Conway] p. 18 | Definition | df-1s 34019 |
| [Conway] p. 29 | Remark | madebday 34080 newbday 34082 oldbday 34081 |
| [Conway] p. 29 | Definition | df-made 34031 df-new 34033 df-old 34032 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 13581 |
| [Crawley] p. 1 | Definition of poset | df-poset 18031 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 37400 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 38204 dalaw 37900 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 39979 |
| [Crawley] p. 111 | Definition of set W | df-watsN 38004 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 38120 df-ldil 38118 isldil 38124 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 38119 df-trnN 38121 isltrn 38133 ltrnu 38135 |
| [Crawley] p. 112 | Lemma A | cdlema1N 37805 cdlema2N 37806 exatleN 37418 |
| [Crawley] p. 112 | Lemma B | 1cvrat 37490 cdlemb 37808 cdlemb2 38055 cdlemb3 38620 idltrn 38164 l1cvat 37069 lhpat 38057 lhpat2 38059 lshpat 37070 ltrnel 38153 ltrnmw 38165 |
| [Crawley] p. 112 | Lemma C | cdlemc1 38205 cdlemc2 38206 ltrnnidn 38188 trlat 38183 trljat1 38180 trljat2 38181 trljat3 38182 trlne 38199 trlnidat 38187 trlnle 38200 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 38005 |
| [Crawley] p. 113 | Lemma C | cdlemc 38211 cdlemc3 38207 cdlemc4 38208 |
| [Crawley] p. 113 | Lemma D | cdlemd 38221 cdlemd1 38212 cdlemd2 38213 cdlemd3 38214 cdlemd4 38215 cdlemd5 38216 cdlemd6 38217 cdlemd7 38218 cdlemd8 38219 cdlemd9 38220 cdleme31sde 38399 cdleme31se 38396 cdleme31se2 38397 cdleme31snd 38400 cdleme32a 38455 cdleme32b 38456 cdleme32c 38457 cdleme32d 38458 cdleme32e 38459 cdleme32f 38460 cdleme32fva 38451 cdleme32fva1 38452 cdleme32fvcl 38454 cdleme32le 38461 cdleme48fv 38513 cdleme4gfv 38521 cdleme50eq 38555 cdleme50f 38556 cdleme50f1 38557 cdleme50f1o 38560 cdleme50laut 38561 cdleme50ldil 38562 cdleme50lebi 38554 cdleme50rn 38559 cdleme50rnlem 38558 cdlemeg49le 38525 cdlemeg49lebilem 38553 |
| [Crawley] p. 113 | Lemma E | cdleme 38574 cdleme00a 38223 cdleme01N 38235 cdleme02N 38236 cdleme0a 38225 cdleme0aa 38224 cdleme0b 38226 cdleme0c 38227 cdleme0cp 38228 cdleme0cq 38229 cdleme0dN 38230 cdleme0e 38231 cdleme0ex1N 38237 cdleme0ex2N 38238 cdleme0fN 38232 cdleme0gN 38233 cdleme0moN 38239 cdleme1 38241 cdleme10 38268 cdleme10tN 38272 cdleme11 38284 cdleme11a 38274 cdleme11c 38275 cdleme11dN 38276 cdleme11e 38277 cdleme11fN 38278 cdleme11g 38279 cdleme11h 38280 cdleme11j 38281 cdleme11k 38282 cdleme11l 38283 cdleme12 38285 cdleme13 38286 cdleme14 38287 cdleme15 38292 cdleme15a 38288 cdleme15b 38289 cdleme15c 38290 cdleme15d 38291 cdleme16 38299 cdleme16aN 38273 cdleme16b 38293 cdleme16c 38294 cdleme16d 38295 cdleme16e 38296 cdleme16f 38297 cdleme16g 38298 cdleme19a 38317 cdleme19b 38318 cdleme19c 38319 cdleme19d 38320 cdleme19e 38321 cdleme19f 38322 cdleme1b 38240 cdleme2 38242 cdleme20aN 38323 cdleme20bN 38324 cdleme20c 38325 cdleme20d 38326 cdleme20e 38327 cdleme20f 38328 cdleme20g 38329 cdleme20h 38330 cdleme20i 38331 cdleme20j 38332 cdleme20k 38333 cdleme20l 38336 cdleme20l1 38334 cdleme20l2 38335 cdleme20m 38337 cdleme20y 38316 cdleme20zN 38315 cdleme21 38351 cdleme21d 38344 cdleme21e 38345 cdleme22a 38354 cdleme22aa 38353 cdleme22b 38355 cdleme22cN 38356 cdleme22d 38357 cdleme22e 38358 cdleme22eALTN 38359 cdleme22f 38360 cdleme22f2 38361 cdleme22g 38362 cdleme23a 38363 cdleme23b 38364 cdleme23c 38365 cdleme26e 38373 cdleme26eALTN 38375 cdleme26ee 38374 cdleme26f 38377 cdleme26f2 38379 cdleme26f2ALTN 38378 cdleme26fALTN 38376 cdleme27N 38383 cdleme27a 38381 cdleme27cl 38380 cdleme28c 38386 cdleme3 38251 cdleme30a 38392 cdleme31fv 38404 cdleme31fv1 38405 cdleme31fv1s 38406 cdleme31fv2 38407 cdleme31id 38408 cdleme31sc 38398 cdleme31sdnN 38401 cdleme31sn 38394 cdleme31sn1 38395 cdleme31sn1c 38402 cdleme31sn2 38403 cdleme31so 38393 cdleme35a 38462 cdleme35b 38464 cdleme35c 38465 cdleme35d 38466 cdleme35e 38467 cdleme35f 38468 cdleme35fnpq 38463 cdleme35g 38469 cdleme35h 38470 cdleme35h2 38471 cdleme35sn2aw 38472 cdleme35sn3a 38473 cdleme36a 38474 cdleme36m 38475 cdleme37m 38476 cdleme38m 38477 cdleme38n 38478 cdleme39a 38479 cdleme39n 38480 cdleme3b 38243 cdleme3c 38244 cdleme3d 38245 cdleme3e 38246 cdleme3fN 38247 cdleme3fa 38250 cdleme3g 38248 cdleme3h 38249 cdleme4 38252 cdleme40m 38481 cdleme40n 38482 cdleme40v 38483 cdleme40w 38484 cdleme41fva11 38491 cdleme41sn3aw 38488 cdleme41sn4aw 38489 cdleme41snaw 38490 cdleme42a 38485 cdleme42b 38492 cdleme42c 38486 cdleme42d 38487 cdleme42e 38493 cdleme42f 38494 cdleme42g 38495 cdleme42h 38496 cdleme42i 38497 cdleme42k 38498 cdleme42ke 38499 cdleme42keg 38500 cdleme42mN 38501 cdleme42mgN 38502 cdleme43aN 38503 cdleme43bN 38504 cdleme43cN 38505 cdleme43dN 38506 cdleme5 38254 cdleme50ex 38573 cdleme50ltrn 38571 cdleme51finvN 38570 cdleme51finvfvN 38569 cdleme51finvtrN 38572 cdleme6 38255 cdleme7 38263 cdleme7a 38257 cdleme7aa 38256 cdleme7b 38258 cdleme7c 38259 cdleme7d 38260 cdleme7e 38261 cdleme7ga 38262 cdleme8 38264 cdleme8tN 38269 cdleme9 38267 cdleme9a 38265 cdleme9b 38266 cdleme9tN 38271 cdleme9taN 38270 cdlemeda 38312 cdlemedb 38311 cdlemednpq 38313 cdlemednuN 38314 cdlemefr27cl 38417 cdlemefr32fva1 38424 cdlemefr32fvaN 38423 cdlemefrs32fva 38414 cdlemefrs32fva1 38415 cdlemefs27cl 38427 cdlemefs32fva1 38437 cdlemefs32fvaN 38436 cdlemesner 38310 cdlemeulpq 38234 |
| [Crawley] p. 114 | Lemma E | 4atex 38090 4atexlem7 38089 cdleme0nex 38304 cdleme17a 38300 cdleme17c 38302 cdleme17d 38512 cdleme17d1 38303 cdleme17d2 38509 cdleme18a 38305 cdleme18b 38306 cdleme18c 38307 cdleme18d 38309 cdleme4a 38253 |
| [Crawley] p. 115 | Lemma E | cdleme21a 38339 cdleme21at 38342 cdleme21b 38340 cdleme21c 38341 cdleme21ct 38343 cdleme21f 38346 cdleme21g 38347 cdleme21h 38348 cdleme21i 38349 cdleme22gb 38308 |
| [Crawley] p. 116 | Lemma F | cdlemf 38577 cdlemf1 38575 cdlemf2 38576 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 38581 cdlemg16 38671 cdlemg28 38718 cdlemg28a 38707 cdlemg28b 38717 cdlemg3a 38611 cdlemg42 38743 cdlemg43 38744 cdlemg44 38747 cdlemg44a 38745 cdlemg46 38749 cdlemg47 38750 cdlemg9 38648 ltrnco 38733 ltrncom 38752 tgrpabl 38765 trlco 38741 |
| [Crawley] p. 116 | Definition of G | df-tgrp 38757 |
| [Crawley] p. 117 | Lemma G | cdlemg17 38691 cdlemg17b 38676 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 38770 df-edring 38771 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 38774 |
| [Crawley] p. 118 | Remark | tendopltp 38794 |
| [Crawley] p. 118 | Lemma H | cdlemh 38831 cdlemh1 38829 cdlemh2 38830 |
| [Crawley] p. 118 | Lemma I | cdlemi 38834 cdlemi1 38832 cdlemi2 38833 |
| [Crawley] p. 118 | Lemma J | cdlemj1 38835 cdlemj2 38836 cdlemj3 38837 tendocan 38838 |
| [Crawley] p. 118 | Lemma K | cdlemk 38988 cdlemk1 38845 cdlemk10 38857 cdlemk11 38863 cdlemk11t 38960 cdlemk11ta 38943 cdlemk11tb 38945 cdlemk11tc 38959 cdlemk11u-2N 38903 cdlemk11u 38885 cdlemk12 38864 cdlemk12u-2N 38904 cdlemk12u 38886 cdlemk13-2N 38890 cdlemk13 38866 cdlemk14-2N 38892 cdlemk14 38868 cdlemk15-2N 38893 cdlemk15 38869 cdlemk16-2N 38894 cdlemk16 38871 cdlemk16a 38870 cdlemk17-2N 38895 cdlemk17 38872 cdlemk18-2N 38900 cdlemk18-3N 38914 cdlemk18 38882 cdlemk19-2N 38901 cdlemk19 38883 cdlemk19u 38984 cdlemk1u 38873 cdlemk2 38846 cdlemk20-2N 38906 cdlemk20 38888 cdlemk21-2N 38905 cdlemk21N 38887 cdlemk22-3 38915 cdlemk22 38907 cdlemk23-3 38916 cdlemk24-3 38917 cdlemk25-3 38918 cdlemk26-3 38920 cdlemk26b-3 38919 cdlemk27-3 38921 cdlemk28-3 38922 cdlemk29-3 38925 cdlemk3 38847 cdlemk30 38908 cdlemk31 38910 cdlemk32 38911 cdlemk33N 38923 cdlemk34 38924 cdlemk35 38926 cdlemk36 38927 cdlemk37 38928 cdlemk38 38929 cdlemk39 38930 cdlemk39u 38982 cdlemk4 38848 cdlemk41 38934 cdlemk42 38955 cdlemk42yN 38958 cdlemk43N 38977 cdlemk45 38961 cdlemk46 38962 cdlemk47 38963 cdlemk48 38964 cdlemk49 38965 cdlemk5 38850 cdlemk50 38966 cdlemk51 38967 cdlemk52 38968 cdlemk53 38971 cdlemk54 38972 cdlemk55 38975 cdlemk55u 38980 cdlemk56 38985 cdlemk5a 38849 cdlemk5auN 38874 cdlemk5u 38875 cdlemk6 38851 cdlemk6u 38876 cdlemk7 38862 cdlemk7u-2N 38902 cdlemk7u 38884 cdlemk8 38852 cdlemk9 38853 cdlemk9bN 38854 cdlemki 38855 cdlemkid 38950 cdlemkj-2N 38896 cdlemkj 38877 cdlemksat 38860 cdlemksel 38859 cdlemksv 38858 cdlemksv2 38861 cdlemkuat 38880 cdlemkuel-2N 38898 cdlemkuel-3 38912 cdlemkuel 38879 cdlemkuv-2N 38897 cdlemkuv2-2 38899 cdlemkuv2-3N 38913 cdlemkuv2 38881 cdlemkuvN 38878 cdlemkvcl 38856 cdlemky 38940 cdlemkyyN 38976 tendoex 38989 |
| [Crawley] p. 120 | Remark | dva1dim 38999 |
| [Crawley] p. 120 | Lemma L | cdleml1N 38990 cdleml2N 38991 cdleml3N 38992 cdleml4N 38993 cdleml5N 38994 cdleml6 38995 cdleml7 38996 cdleml8 38997 cdleml9 38998 dia1dim 39075 |
| [Crawley] p. 120 | Lemma M | dia11N 39062 diaf11N 39063 dialss 39060 diaord 39061 dibf11N 39175 djajN 39151 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 39046 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 39132 dia2dimlem1 39078 dia2dimlem2 39079 dia2dimlem3 39080 dia2dimlem4 39081 dia2dimlem5 39082 diaf1oN 39144 diarnN 39143 dvheveccl 39126 dvhopN 39130 |
| [Crawley] p. 121 | Lemma N | cdlemn 39226 cdlemn10 39220 cdlemn11 39225 cdlemn11a 39221 cdlemn11b 39222 cdlemn11c 39223 cdlemn11pre 39224 cdlemn2 39209 cdlemn2a 39210 cdlemn3 39211 cdlemn4 39212 cdlemn4a 39213 cdlemn5 39215 cdlemn5pre 39214 cdlemn6 39216 cdlemn7 39217 cdlemn8 39218 cdlemn9 39219 diclspsn 39208 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 39187 |
| [Crawley] p. 122 | Lemma N | dih11 39279 dihf11 39281 dihjust 39231 dihjustlem 39230 dihord 39278 dihord1 39232 dihord10 39237 dihord11b 39236 dihord11c 39238 dihord2 39241 dihord2a 39233 dihord2b 39234 dihord2cN 39235 dihord2pre 39239 dihord2pre2 39240 dihordlem6 39227 dihordlem7 39228 dihordlem7b 39229 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 39244 dihfval 39245 dihval 39246 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 27779 df-nbgr 27700 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 27635 uhgrspan1 27670 uhgrspansubgr 27658 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 27921 vtxdgoddnumeven 27920 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 27429 |
| [EGA] p. 80 | Notation 1.1.1 | rspecval 31814 |
| [EGA] p. 80 | Proposition 1.1.2 | zartop 31826 |
| [EGA] p. 80 | Proposition 1.1.2(i) | zarcls0 31818 zarcls1 31819 |
| [EGA] p. 81 | Corollary 1.1.8 | zart0 31829 |
| [EGA], p. 82 | Proposition 1.1.10(ii) | zarcmp 31832 |
| [EGA], p. 83 | Corollary 1.2.3 | rhmpreimacn 31835 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3890 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 9405 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 8617 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 9413 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 9738 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 10311 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 5229 |
| [Enderton] p. 19 | Definition | df-tp 4566 |
| [Enderton] p. 26 | Exercise 5 | unissb 4873 |
| [Enderton] p. 26 | Exercise 10 | pwel 5304 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5487 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 5008 iinin2 5007 iinun2 5002 iunin1 5001 iunin1f 30897 iunin2 5000 uniin1 30891 uniin2 30892 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 5006 iundif2 5003 |
| [Enderton] p. 32 | Exercise 20 | unineq 4211 |
| [Enderton] p. 33 | Exercise 23 | iinuni 5027 |
| [Enderton] p. 33 | Exercise 25 | iununi 5028 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 5035 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 7621 iunpwss 5036 |
| [Enderton] p. 36 | Definition | opthwiener 5428 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 5366 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4878 |
| [Enderton] p. 41 | Lemma 3D | opeluu 5385 rnex 7759 rnexg 7751 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5823 rnuni 6052 |
| [Enderton] p. 42 | Definition of a function | dffun7 6461 dffun8 6462 |
| [Enderton] p. 43 | Definition of function value | funfv2 6856 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 6503 |
| [Enderton] p. 44 | Definition (d) | dfima2 5971 dfima3 5972 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6865 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 10229 ac7g 10230 df-ac 9872 dfac2 9887 dfac2a 9885 dfac2b 9886 dfac3 9877 dfac7 9888 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 7119 |
| [Enderton] p. 52 | Definition | df-map 8617 |
| [Enderton] p. 53 | Exercise 21 | coass 6169 |
| [Enderton] p. 53 | Exercise 27 | dmco 6158 |
| [Enderton] p. 53 | Exercise 14(a) | funin 6510 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 6010 |
| [Enderton] p. 54 | Remark | ixpf 8708 ixpssmap 8720 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 8686 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 10239 ac9s 10249 |
| [Enderton] p. 56 | Theorem 3M | eqvrelref 36723 erref 8518 |
| [Enderton] p. 57 | Lemma 3N | eqvrelthi 36726 erthi 8549 |
| [Enderton] p. 57 | Definition | df-ec 8500 |
| [Enderton] p. 58 | Definition | df-qs 8504 |
| [Enderton] p. 61 | Exercise 35 | df-ec 8500 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5819 |
| [Enderton] p. 68 | Definition of successor | df-suc 6272 |
| [Enderton] p. 71 | Definition | df-tr 5192 dftr4 5196 |
| [Enderton] p. 72 | Theorem 4E | unisuc 6342 |
| [Enderton] p. 73 | Exercise 6 | unisuc 6342 |
| [Enderton] p. 73 | Exercise 5(a) | truni 5205 |
| [Enderton] p. 73 | Exercise 5(b) | trint 5207 trintALT 42501 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 8435 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 8437 onasuc 8358 |
| [Enderton] p. 79 | Definition of operation value | df-ov 7278 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 8436 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 8438 onmsuc 8359 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 8453 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 8440 nnacom 8448 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 8454 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 8455 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 8457 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 8441 nnmsucr 8456 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 8469 |
| [Enderton] p. 129 | Definition | df-en 8734 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 7229 |
| [Enderton] p. 133 | Exercise 1 | xpomen 9771 |
| [Enderton] p. 133 | Exercise 2 | qnnen 15922 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8993 |
| [Enderton] p. 135 | Corollary 6C | php3 8995 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8992 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 9033 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 9035 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8951 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8956 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8928 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 9935 |
| [Enderton] p. 142 | Theorem 6I(4) | mapdjuen 9936 |
| [Enderton] p. 143 | Theorem 6J | dju0en 9931 dju1en 9927 |
| [Enderton] p. 144 | Exercise 13 | iunfi 9107 unifi 9108 unifi2 9109 |
| [Enderton] p. 144 | Corollary 6K | undif2 4410 unfi 8955 unfi2 9083 |
| [Enderton] p. 145 | Figure 38 | ffoss 7788 |
| [Enderton] p. 145 | Definition | df-dom 8735 |
| [Enderton] p. 146 | Example 1 | domen 8751 domeng 8752 |
| [Enderton] p. 146 | Example 3 | nndomo 9016 nnsdom 9412 nnsdomg 9073 |
| [Enderton] p. 149 | Theorem 6L(a) | djudom2 9939 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8929 xpdom1 8858 xpdom1g 8856 xpdom2g 8855 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8935 |
| [Enderton] p. 151 | Theorem 6M | zorn 10263 zorng 10260 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 10248 dfac5 9884 |
| [Enderton] p. 159 | Theorem 6Q | unictb 10331 |
| [Enderton] p. 164 | Example | infdif 9965 |
| [Enderton] p. 168 | Definition | df-po 5503 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 6374 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 6312 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 6373 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 6319 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7685 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 7631 |
| [Enderton] p. 194 | Remark | onprc 7628 |
| [Enderton] p. 194 | Exercise 16 | suc11 6369 |
| [Enderton] p. 197 | Definition | df-card 9697 |
| [Enderton] p. 197 | Theorem 7P | carden 10307 |
| [Enderton] p. 200 | Exercise 25 | tfis 7701 |
| [Enderton] p. 202 | Lemma 7T | r1tr 9534 |
| [Enderton] p. 202 | Definition | df-r1 9522 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 9544 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 9625 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 9364 |
| [Enderton] p. 207 | Exercise 30 | rankpr 9615 rankprb 9609 rankpw 9601 rankpwi 9581 rankuniss 9624 |
| [Enderton] p. 207 | Exercise 34 | opthreg 9376 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 9377 |
| [Enderton] p. 212 | Definition of aleph | alephval3 9866 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 9832 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 9846 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 8172 |
| [Enderton] p. 222 | Definition of kard | karden 9653 kardex 9652 |
| [Enderton] p. 238 | Theorem 8R | oeoa 8428 |
| [Enderton] p. 238 | Theorem 8S | oeoe 8430 |
| [Enderton] p. 240 | Exercise 25 | oarec 8393 |
| [Enderton] p. 257 | Definition of cofinality | cflm 10006 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 17351 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 17297 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 18271 mrieqv2d 17348 mrieqvd 17347 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 17352 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 17357 mreexexlem2d 17354 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 18277 mreexfidimd 17359 |
| [Frege1879] p. 11 | Statement | df3or2 41376 |
| [Frege1879] p. 12 | Statement | df3an2 41377 dfxor4 41374 dfxor5 41375 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 41398 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 41399 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 41403 |
| [Frege1879] p. 31 | Proposition 4 | frege4 41407 |
| [Frege1879] p. 32 | Proposition 5 | frege5 41408 |
| [Frege1879] p. 33 | Proposition 6 | frege6 41414 |
| [Frege1879] p. 34 | Proposition 7 | frege7 41416 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 41417 axfrege8 41415 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-luk-pm2.04 35616 |
| [Frege1879] p. 35 | Proposition 9 | frege9 41420 |
| [Frege1879] p. 36 | Proposition 10 | frege10 41428 |
| [Frege1879] p. 36 | Proposition 11 | frege11 41422 |
| [Frege1879] p. 37 | Proposition 12 | frege12 41421 |
| [Frege1879] p. 37 | Proposition 13 | frege13 41430 |
| [Frege1879] p. 37 | Proposition 14 | frege14 41431 |
| [Frege1879] p. 38 | Proposition 15 | frege15 41434 |
| [Frege1879] p. 38 | Proposition 16 | frege16 41424 |
| [Frege1879] p. 39 | Proposition 17 | frege17 41429 |
| [Frege1879] p. 39 | Proposition 18 | frege18 41426 |
| [Frege1879] p. 39 | Proposition 19 | frege19 41432 |
| [Frege1879] p. 40 | Proposition 20 | frege20 41436 |
| [Frege1879] p. 40 | Proposition 21 | frege21 41435 |
| [Frege1879] p. 41 | Proposition 22 | frege22 41427 |
| [Frege1879] p. 42 | Proposition 23 | frege23 41433 |
| [Frege1879] p. 42 | Proposition 24 | frege24 41423 |
| [Frege1879] p. 42 | Proposition 25 | frege25 41425 rp-frege25 41413 |
| [Frege1879] p. 42 | Proposition 26 | frege26 41418 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 41438 |
| [Frege1879] p. 43 | Proposition 27 | frege27 41419 |
| [Frege1879] p. 43 | Proposition 28 | con3 153 |
| [Frege1879] p. 43 | Proposition 29 | frege29 41439 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 41442 axfrege31 41441 |
| [Frege1879] p. 44 | Proposition 30 | frege30 41440 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 130 |
| [Frege1879] p. 44 | Proposition 32 | frege32 41443 |
| [Frege1879] p. 44 | Proposition 33 | frege33 41444 |
| [Frege1879] p. 45 | Proposition 34 | frege34 41445 |
| [Frege1879] p. 45 | Proposition 35 | frege35 41446 |
| [Frege1879] p. 45 | Proposition 36 | frege36 41447 |
| [Frege1879] p. 46 | Proposition 37 | frege37 41448 |
| [Frege1879] p. 46 | Proposition 38 | frege38 41449 |
| [Frege1879] p. 46 | Proposition 39 | frege39 41450 |
| [Frege1879] p. 46 | Proposition 40 | frege40 41451 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 41453 axfrege41 41452 |
| [Frege1879] p. 47 | Proposition 41 | notnot 142 |
| [Frege1879] p. 47 | Proposition 42 | frege42 41454 |
| [Frege1879] p. 47 | Proposition 43 | frege43 41455 |
| [Frege1879] p. 47 | Proposition 44 | frege44 41456 |
| [Frege1879] p. 47 | Proposition 45 | frege45 41457 |
| [Frege1879] p. 48 | Proposition 46 | frege46 41458 |
| [Frege1879] p. 48 | Proposition 47 | frege47 41459 |
| [Frege1879] p. 49 | Proposition 48 | frege48 41460 |
| [Frege1879] p. 49 | Proposition 49 | frege49 41461 |
| [Frege1879] p. 49 | Proposition 50 | frege50 41462 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 41465 ax-frege52c 41496 frege52aid 41466 frege52b 41497 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 41470 ax-frege54c 41500 frege54b 41501 |
| [Frege1879] p. 50 | Proposition 51 | frege51 41463 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3718 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 41468 frege53aid 41467 frege53b 41498 frege53c 41522 |
| [Frege1879] p. 50 | Proposition 54 | biid 260 eqid 2738 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 41476 frege55aid 41473 frege55b 41505 frege55c 41526 frege55cor1a 41477 frege55lem2a 41475 frege55lem2b 41504 frege55lem2c 41525 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 41479 frege56aid 41478 frege56b 41506 frege56c 41527 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 41483 ax-frege58b 41509 frege58bid 41510 frege58c 41529 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 41481 frege57aid 41480 frege57b 41507 frege57c 41528 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3729 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 41485 frege59b 41512 frege59c 41530 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 41486 frege60b 41513 frege60c 41531 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 41487 frege61b 41514 frege61c 41532 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 41488 frege62b 41515 frege62c 41533 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 41489 frege63b 41516 frege63c 41534 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 41490 frege64b 41517 frege64c 41535 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 41491 frege65b 41518 frege65c 41536 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 41492 frege66b 41519 frege66c 41537 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 41493 frege67b 41520 frege67c 41538 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 41494 frege68b 41521 frege68c 41539 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 41540 |
| [Frege1879] p. 58 | Proposition 70 | frege70 41541 |
| [Frege1879] p. 59 | Proposition 71 | frege71 41542 |
| [Frege1879] p. 59 | Proposition 72 | frege72 41543 |
| [Frege1879] p. 59 | Proposition 73 | frege73 41544 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 41547 |
| [Frege1879] p. 60 | Proposition 74 | frege74 41545 |
| [Frege1879] p. 60 | Proposition 75 | frege75 41546 |
| [Frege1879] p. 62 | Proposition 77 | frege77 41548 frege77d 41354 |
| [Frege1879] p. 63 | Proposition 78 | frege78 41549 |
| [Frege1879] p. 63 | Proposition 79 | frege79 41550 |
| [Frege1879] p. 63 | Proposition 80 | frege80 41551 |
| [Frege1879] p. 63 | Proposition 81 | frege81 41552 frege81d 41355 |
| [Frege1879] p. 64 | Proposition 82 | frege82 41553 |
| [Frege1879] p. 65 | Proposition 83 | frege83 41554 frege83d 41356 |
| [Frege1879] p. 65 | Proposition 84 | frege84 41555 |
| [Frege1879] p. 66 | Proposition 85 | frege85 41556 |
| [Frege1879] p. 66 | Proposition 86 | frege86 41557 |
| [Frege1879] p. 66 | Proposition 87 | frege87 41558 frege87d 41358 |
| [Frege1879] p. 67 | Proposition 88 | frege88 41559 |
| [Frege1879] p. 68 | Proposition 89 | frege89 41560 |
| [Frege1879] p. 68 | Proposition 90 | frege90 41561 |
| [Frege1879] p. 68 | Proposition 91 | frege91 41562 frege91d 41359 |
| [Frege1879] p. 69 | Proposition 92 | frege92 41563 |
| [Frege1879] p. 70 | Proposition 93 | frege93 41564 |
| [Frege1879] p. 70 | Proposition 94 | frege94 41565 |
| [Frege1879] p. 70 | Proposition 95 | frege95 41566 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 41570 |
| [Frege1879] p. 71 | Proposition 96 | frege96 41567 frege96d 41357 |
| [Frege1879] p. 71 | Proposition 97 | frege97 41568 frege97d 41360 |
| [Frege1879] p. 71 | Proposition 98 | frege98 41569 frege98d 41361 |
| [Frege1879] p. 72 | Proposition 100 | frege100 41571 |
| [Frege1879] p. 72 | Proposition 101 | frege101 41572 |
| [Frege1879] p. 72 | Proposition 102 | frege102 41573 frege102d 41362 |
| [Frege1879] p. 73 | Proposition 103 | frege103 41574 |
| [Frege1879] p. 73 | Proposition 104 | frege104 41575 |
| [Frege1879] p. 73 | Proposition 105 | frege105 41576 |
| [Frege1879] p. 73 | Proposition 106 | frege106 41577 frege106d 41363 |
| [Frege1879] p. 74 | Proposition 107 | frege107 41578 |
| [Frege1879] p. 74 | Proposition 108 | frege108 41579 frege108d 41364 |
| [Frege1879] p. 74 | Proposition 109 | frege109 41580 frege109d 41365 |
| [Frege1879] p. 75 | Proposition 110 | frege110 41581 |
| [Frege1879] p. 75 | Proposition 111 | frege111 41582 frege111d 41367 |
| [Frege1879] p. 76 | Proposition 112 | frege112 41583 |
| [Frege1879] p. 76 | Proposition 113 | frege113 41584 |
| [Frege1879] p. 76 | Proposition 114 | frege114 41585 frege114d 41366 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 41586 |
| [Frege1879] p. 77 | Proposition 116 | frege116 41587 |
| [Frege1879] p. 78 | Proposition 117 | frege117 41588 |
| [Frege1879] p. 78 | Proposition 118 | frege118 41589 |
| [Frege1879] p. 78 | Proposition 119 | frege119 41590 |
| [Frege1879] p. 78 | Proposition 120 | frege120 41591 |
| [Frege1879] p. 79 | Proposition 121 | frege121 41592 |
| [Frege1879] p. 79 | Proposition 122 | frege122 41593 frege122d 41368 |
| [Frege1879] p. 79 | Proposition 123 | frege123 41594 |
| [Frege1879] p. 80 | Proposition 124 | frege124 41595 frege124d 41369 |
| [Frege1879] p. 81 | Proposition 125 | frege125 41596 |
| [Frege1879] p. 81 | Proposition 126 | frege126 41597 frege126d 41370 |
| [Frege1879] p. 82 | Proposition 127 | frege127 41598 |
| [Frege1879] p. 83 | Proposition 128 | frege128 41599 |
| [Frege1879] p. 83 | Proposition 129 | frege129 41600 frege129d 41371 |
| [Frege1879] p. 84 | Proposition 130 | frege130 41601 |
| [Frege1879] p. 85 | Proposition 131 | frege131 41602 frege131d 41372 |
| [Frege1879] p. 86 | Proposition 132 | frege132 41603 |
| [Frege1879] p. 86 | Proposition 133 | frege133 41604 frege133d 41373 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 43854 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 44174 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 43875 |
| [Fremlin1] p. 14 | Definition 112A | ismea 43989 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 44009 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 44000 meadjunre 44014 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 44001 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 44002 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 43998 meaiunle 44007 meaiunlelem 44006 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 44019 meaiuninc2 44020 meaiuninc3 44023 meaiuninc3v 44022 meaiunincf 44021 meaiuninclem 44018 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 44025 meaiininc2 44026 meaiininclem 44024 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 44044 caragendifcl 44052 caratheodory 44066 omelesplit 44056 |
| [Fremlin1] p. 19 | Definition 113A | isome 44032 isomennd 44069 isomenndlem 44068 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 44054 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 44073 voncmpl 44159 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 44036 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 44061 carageniuncllem1 44059 carageniuncllem2 44060 caragenuncl 44051 caragenuncllem 44050 caragenunicl 44062 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 44070 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 44064 caratheodorylem2 44065 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 44073 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 44132 hoidmv1lelem1 44129 hoidmv1lelem2 44130 hoidmv1lelem3 44131 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 44176 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 44132 hoidmvle 44138 hoidmvlelem1 44133 hoidmvlelem2 44134 hoidmvlelem3 44135 hoidmvlelem4 44136 hoidmvlelem5 44137 hsphoidmvle2 44123 hsphoif 44114 hsphoival 44117 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 44086 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 44094 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 44121 hoidmvn0val 44122 hoidmvval 44115 hoidmvval0 44125 hoidmvval0b 44128 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 44126 hsphoidmvle 44124 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 44075 df-voln 44077 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 44142 ovn0 44104 ovn0lem 44103 ovnf 44101 ovnome 44111 ovnssle 44099 ovnsslelem 44098 ovnsupge0 44095 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 44141 ovnhoilem1 44139 ovnhoilem2 44140 vonhoi 44205 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 44158 hoidifhspf 44156 hoidifhspval 44146 hoidifhspval2 44153 hoidifhspval3 44157 hspmbl 44167 hspmbllem1 44164 hspmbllem2 44165 hspmbllem3 44166 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 44159 vonmea 44112 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 44110 ovnsubadd2 44184 ovnsubadd2lem 44183 ovnsubaddlem1 44108 ovnsubaddlem2 44109 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 44169 hoimbl2 44203 hoimbllem 44168 hspdifhsp 44154 opnvonmbl 44172 opnvonmbllem2 44171 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 44174 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 44217 iccvonmbllem 44216 ioovonmbl 44215 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 44223 vonicclem2 44222 vonioo 44220 vonioolem2 44219 vonn0icc 44226 vonn0icc2 44230 vonn0ioo 44225 vonn0ioo2 44228 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 44227 snvonmbl 44224 vonct 44231 vonsn 44229 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 43898 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 43897 subsaliuncllem 43896 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 44261 salpreimalegt 44246 salpreimaltle 44262 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 44264 issmff 44270 issmflem 44263 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 44281 issmflelem 44280 smfpreimale 44290 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 44292 issmfgtlem 44291 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 44234 issmf 44264 issmff 44270 issmfge 44305 issmfgelem 44304 issmfgt 44292 issmfgtlem 44291 issmfle 44281 issmflelem 44280 issmflem 44263 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 44244 salpreimagtlt 44266 salpreimalelt 44265 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 44305 issmfgelem 44304 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 44289 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 44287 cnfsmf 44276 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 44302 decsmflem 44301 incsmf 44278 incsmflem 44277 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 44239 pimconstlt1 44240 smfconst 44285 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 44300 smfaddlem1 44298 smfaddlem2 44299 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 44330 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 44329 smfmullem1 44325 smfmullem2 44326 smfmullem3 44327 smfmullem4 44328 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 44331 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 44334 smfpimbor1lem2 44333 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 44336 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 44324 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 44323 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 44332 smfresal 44322 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 44312 smflim2 44339 smflimlem1 44306 smflimlem2 44307 smflimlem3 44308 smflimlem4 44309 smflimlem5 44310 smflimlem6 44311 smflimmpt 44343 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 44347 smfsuplem1 44344 smfsuplem2 44345 smfsuplem3 44346 smfsupmpt 44348 smfsupxr 44349 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 44351 smfinflem 44350 smfinfmpt 44352 |
| [Fremlin1] p. 39 | Remark 121G | smflim 44312 smflim2 44339 smflimmpt 44343 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 44341 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 44361 smflimsuplem2 44354 smflimsuplem6 44358 smflimsuplem7 44359 smflimsuplem8 44360 smflimsupmpt 44362 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 44364 smfliminflem 44363 smfliminfmpt 44365 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 44234 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 24700 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 24743 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 24753 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 35855 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 35858 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 9396 inf1 9380 inf2 9381 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 10667 enqer 10677 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 10672 df-nq 10668 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 10664 df-plq 10670 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 7509 df-mpq 10665 df-mq 10671 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 10673 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 10731 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 10732 ltbtwnnq 10734 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 10727 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 10728 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 10735 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 10737 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 10749 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 10751 |
| [Gleason] p. 122 | Definition | df-1p 10738 |
| [Gleason] p. 122 | Remark (1) | prub 10750 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 10789 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 10741 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 10788 psslinpr 10787 supexpr 10810 suplem1pr 10808 suplem2pr 10809 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 10774 addclprlem1 10772 addclprlem2 10773 df-plp 10739 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 10778 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 10777 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 10790 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 10799 ltexprlem1 10792 ltexprlem2 10793 ltexprlem3 10794 ltexprlem4 10795 ltexprlem5 10796 ltexprlem6 10797 ltexprlem7 10798 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 10801 ltaprlem 10800 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 10802 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 10803 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 10740 mulclpr 10776 mulclprlem 10775 reclem2pr 10804 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 10785 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 10780 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 10779 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 10784 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 10807 reclem3pr 10805 reclem4pr 10806 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 10811 enrer 10819 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 10816 df-1r 10817 df-nr 10812 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 10814 df-plr 10813 negexsr 10858 recexsr 10863 recexsrlem 10859 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 10815 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11968 creur 11967 cru 11965 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10944 axcnre 10920 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 14826 crimd 14943 crimi 14904 crre 14825 crred 14942 crrei 14903 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 14828 remimd 14909 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14996 absval2d 15157 absval2i 15109 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 14852 cjaddd 14931 cjaddi 14899 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 14853 cjmuld 14932 cjmuli 14900 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 14851 cjcjd 14910 cjcji 14882 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 14850 cjreb 14834 cjrebd 14913 cjrebi 14885 cjred 14937 rere 14833 rereb 14831 rerebd 14912 rerebi 14884 rered 14935 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 14859 addcjd 14923 addcji 14894 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 14949 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14991 abscjd 15162 abscji 15113 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 15001 abs00d 15158 abs00i 15110 absne0d 15159 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 15033 releabsd 15163 releabsi 15114 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 15006 absmuld 15166 absmuli 15116 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14994 sqabsaddi 15117 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 15042 abstrid 15168 abstrii 15120 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 13783 exp0 13786 expp1 13789 expp1d 13865 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 25834 cxpaddd 25872 expadd 13825 expaddd 13866 expaddz 13827 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 25843 cxpmuld 25891 expmul 13828 expmuld 13867 expmulz 13829 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 25840 mulcxpd 25883 mulexp 13822 mulexpd 13879 mulexpz 13823 |
| [Gleason] p. 140 | Exercise 1 | znnen 15921 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 13241 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 15341 rlimadd 15352 rlimdiv 15357 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 15343 rlimsub 15354 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 15342 rlimmul 15355 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 15346 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 15292 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 15313 climcj 15314 climim 15316 climre 15315 rlimabs 15318 rlimcj 15319 rlimim 15321 rlimre 15320 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 11014 df-xr 11013 ltxr 12851 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 15180 limsupval 15183 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 15381 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 15390 caucvgb 15391 caucvgr 15387 climcau 15382 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 15528 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 15595 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 15047 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 13548 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 20591 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 23496 xmet0 23495 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 23512 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 23503 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 23505 mstri 23622 xmettri 23504 xmstri 23621 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 23535 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 22799 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 24474 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 23696 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 24028 addcn2 15303 mulcn 24030 mulcn2 15305 subcn 24029 subcn2 15304 |
| [Gleason] p. 295 | Remark | bcval3 14020 bcval4 14021 |
| [Gleason] p. 295 | Equation 2 | bcpasc 14035 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 14018 df-bc 14017 |
| [Gleason] p. 296 | Remark | bcn0 14024 bcnn 14026 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 15542 |
| [Gleason] p. 308 | Equation 2 | ef0 15800 |
| [Gleason] p. 308 | Equation 3 | efcj 15801 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 15806 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 15810 |
| [Gleason] p. 310 | Equation 14 | sinadd 15873 |
| [Gleason] p. 310 | Equation 15 | cosadd 15874 |
| [Gleason] p. 311 | Equation 17 | sincossq 15885 |
| [Gleason] p. 311 | Equation 18 | cosbnd 15890 sinbnd 15889 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 13932 sqeqori 13930 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 15782 |
| [Godowski] p. 730 | Equation SF | goeqi 30635 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 30030 |
| [Golan] p. 1 | Remark | srgisid 19764 |
| [Golan] p. 1 | Definition | df-srg 19742 |
| [Golan] p. 149 | Definition | df-slmd 31454 |
| [Gonshor] p. 7 | Definition | df-scut 33978 |
| [Gonshor] p. 9 | Theorem 2.5 | slerec 34013 |
| [Gonshor] p. 10 | Theorem 2.6 | cofcut1 34090 |
| [Gonshor] p. 10 | Theorem 2.7 | cofcut2 34091 |
| [Gonshor] p. 12 | Theorem 2.9 | cofcutr 34092 |
| [Gonshor] p. 13 | Definition | df-adds 34119 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 34461 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 17295 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 17297 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 45382 df-cllaw 45380 df-comlaw 45381 |
| [Hall] p. 2 | Section 1.2 | df-clintop 45394 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 45415 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 30427 riesz2 30428 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 30303 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 30535 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 30547 elpjidm 30546 pjnmopi 30510 |
| [Halmos] p. 44 | Remark | pjinormi 30049 pjinormii 30038 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 30551 pjrn 30069 pjrni 30064 pjvec 30058 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 30089 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 30516 hmopidmpji 30514 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 30553 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 30542 pjocvec 30059 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 30531 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 30534 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 30537 pjssdif2i 30536 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 30217 |
| [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 1798 |
| [Hatcher] p. 25 | Definition | df-phtpc 24155 df-phtpy 24134 |
| [Hatcher] p. 26 | Definition | df-pco 24168 df-pi1 24171 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 24158 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 24213 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 21639 df-dmatalt 45739 |
| [Helfgott] p. 2 | Theorem | tgoldbach 45269 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 45254 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 45266 bgoldbtbnd 45261 bgoldbtbnd 45261 tgblthelfgott 45267 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 32622 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 32623 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 32637 hgt750lemb 32636 hgt750leme 32638 hgt750lemf 32633 hgt750lemg 32634 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 45263 tgoldbachgt 32643 tgoldbachgtALTV 45264 tgoldbachgtd 32642 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 32624 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 28855 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 18588 grpoideu 28871 mndideu 18396 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 18614 grpoinveu 28881 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 18642 grpo2inv 28893 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 18653 grpoinvop 28895 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 18675 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1771 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1772 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1774 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 30782 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 30795 cdj3i 30803 cdj3lem1 30796 cdjreui 30794 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 30793 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 39979 |
| [Holland95] p. 14 | Line 15 | hgmapvs 39905 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 39927 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 39928 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 39925 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 39931 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 39850 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 39945 |
| [Holland95] p. 204 | Definition of involution | df-srng 20106 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 37517 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 39542 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 39495 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 37947 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 39391 poml4N 37967 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 39482 pexmidALTN 37992 pexmidN 37983 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 39547 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 37138 ldualset 37139 |
| [Holland95] p. 222 | Item 1 | df-lines 37515 df-pointsN 37516 |
| [Holland95] p. 222 | Item 2 | df-polarityN 37917 |
| [Holland95] p. 223 | Remark | ispsubcl2N 37961 omllaw4 37260 pol1N 37924 polcon3N 37931 |
| [Holland95] p. 223 | Definition | df-psubclN 37949 |
| [Holland95] p. 223 | Equation for polarity | polval2N 37920 |
| [Holmes] p. 40 | Definition | df-xrn 36501 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 29446 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 30544 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 30325 eigre 30197 eigrei 30196 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 30326 eigorth 30200 eigorthi 30199 |
| [Hughes] p. 137 | Remark (ii) | eigposi 30198 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 28673 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 28669 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 28670 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 28671 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 28689 frgrregorufr0 28688 frgrregorufrg 28690 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 28696 frrusgrord 28705 frrusgrord0 28704 |
| [Huneke] p. 2 | Statement | df-clwwlknon 28452 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 28679 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 28682 frgrwopreg2 28683 frgrwopregasn 28680 frgrwopregbsn 28681 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 28685 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 28699 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 28702 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 28450 numclwlk1 28735 numclwlk1lem1 28733 numclwlk1lem2 28734 numclwwlk1 28725 numclwwlk8 28756 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 28676 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 28139 |
| [Huneke] p. 2 | Definition 6 | 2clwwlk 28711 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 28737 numclwwlkovh0 28736 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 28745 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 28342 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 28749 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 28752 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 28755 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 28767 natded 28767 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 28767 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 28767 natded 28767 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 28767 |
| [Jech] p. 4 | Definition of class | cv 1538 cvjust 2732 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 10335 |
| [Jech] p. 42 | Equation 6.1 | alephadd 10333 alephmul 10334 |
| [Jech] p. 43 | Lemma 6.2 | infmap 10332 infmap2 9974 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 9572 |
| [Jech] p. 72 | Equation 9.3 | scott0 9644 scottex 9643 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 9625 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 9649 |
| [Jech] p. 78 | Note | opthprc 5651 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 40737 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 40825 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 40826 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 40749 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 40753 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 40754 rmyp1 40755 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 40756 rmym1 40757 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 40747 rmx1 40748 rmxluc 40758 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 40751 rmy1 40752 rmyluc 40759 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 40761 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 40762 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 40782 jm2.17b 40783 jm2.17c 40784 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 40815 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 40819 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 40810 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 40785 jm2.24nn 40781 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 40824 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 40830 rmygeid 40786 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 40842 |
| [Juillerat] p. 11 | Section *5 | etransc 43824 etransclem47 43822 etransclem48 43823 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 43819 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 43821 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 43807 |
| [Juillerat] p. 13 | Proof | etransclem35 43810 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 43813 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 43799 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 43816 |
| [Juillerat] p. 14 | Proof | etransclem23 43798 |
| [KalishMontague] p. 81 | Note 1 | ax-6 1971 |
| [KalishMontague] p. 85 | Lemma 2 | equid 2015 |
| [KalishMontague] p. 85 | Lemma 3 | equcomi 2020 |
| [KalishMontague] p. 86 | Lemma 7 | cbvalivw 2010 cbvaliw 2009 wl-cbvmotv 35672 wl-motae 35674 wl-moteq 35673 |
| [KalishMontague] p. 87 | Lemma 8 | spimvw 1999 spimw 1974 |
| [KalishMontague] p. 87 | Lemma 9 | spfw 2036 spw 2037 |
| [Kalmbach] p. 14 | Definition of lattice | chabs1 29878 chabs1i 29880 chabs2 29879 chabs2i 29881 chjass 29895 chjassi 29848 latabs1 18193 latabs2 18194 |
| [Kalmbach] p. 15 | Definition of atom | df-at 30700 ela 30701 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 30645 cvrval2 37288 |
| [Kalmbach] p. 16 | Definition | df-ol 37192 df-oml 37193 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 29946 cmbri 29952 cmtvalN 37225 df-cm 29945 df-cmtN 37191 |
| [Kalmbach] p. 22 | Remark | omllaw5N 37261 pjoml5 29975 pjoml5i 29950 |
| [Kalmbach] p. 22 | Definition | pjoml2 29973 pjoml2i 29947 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 29976 cmcmi 29954 cmcmii 29959 cmtcomN 37263 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 37259 omlsi 29766 pjoml 29798 pjomli 29797 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 37258 |
| [Kalmbach] p. 23 | Remark | cmbr2i 29958 cmcm3 29977 cmcm3i 29956 cmcm3ii 29961 cmcm4i 29957 cmt3N 37265 cmt4N 37266 cmtbr2N 37267 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 29970 cmbr3i 29962 cmtbr3N 37268 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 29980 fh1i 29983 fh2 29981 fh2i 29984 omlfh1N 37272 |
| [Kalmbach] p. 65 | Remark | chjatom 30719 chslej 29860 chsleji 29820 shslej 29742 shsleji 29732 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 29857 chocini 29816 chsupcl 29702 chsupval2 29772 h0elch 29617 helch 29605 hsupval2 29771 ocin 29658 ococss 29655 shococss 29656 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 29674 |
| [Kalmbach] p. 66 | Remark | df-pjh 29757 pjssmi 30527 pjssmii 30043 |
| [Kalmbach] p. 67 | Lemma 3 | osum 30007 osumi 30004 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 30562 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 30762 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 30672 |
| [Kalmbach] p. 140 | Remark | hatomic 30722 hatomici 30721 hatomistici 30724 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 37333 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 30743 lsatexch 37057 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 30717 cvlcvr1 37353 cvr1 37424 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 30736 cvexchi 30731 cvrexch 37434 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 30726 hlrelat 37416 hlrelat5N 37415 lrelat 37028 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 20403 lsmsatcv 37024 spansncv 30015 spansncvi 30014 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 37043 spansncv2 30655 |
| [Kalmbach] p. 266 | Definition | df-st 30573 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 30211 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 10402 fpwwe2 10399 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 10403 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 10410 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 10405 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 10407 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 10420 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchdjuidm 10424 gchxpidm 10425 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 10436 gchhar 10435 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwdjudom 9972 unxpwdom 9348 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 10426 |
| [Kreyszig] p. 3 | Property M1 | metcl 23485 xmetcl 23484 |
| [Kreyszig] p. 4 | Property M2 | meteq0 23492 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 23728 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 11692 muleqadd 11619 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 23591 |
| [Kreyszig] p. 19 | Remark | mopntopon 23592 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 23654 mopnm 23597 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 23652 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 23657 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 23698 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 22409 lmmbr 24422 lmmbr2 24423 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 22531 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 24477 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 24440 iscmet2 24458 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 24480 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 22612 metelcls 24469 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 24470 metcld2 24471 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 24262 lmodvneg1 20166 nvinv 29001 vcm 28938 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 24258 lmod0vs 20156 slmd0vs 31477 vc0 28936 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 20157 slmdvs0 31478 vcz 28937 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 29053 ngpmet 23759 nrmmetd 23730 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 29048 imsdval2 29049 ncvspds 24325 ngpds 23760 |
| [Kreyszig] p. 63 | Problem 1 | nmval 23745 nvnd 29050 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 23774 nmge0 23773 nvge0 29035 nvz 29031 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 23780 nvabs 29034 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 29163 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 29107 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 29169 blocni 29167 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 29168 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 24368 ipeq0 20843 ipz 29081 |
| [Kreyszig] p. 135 | Problem 2 | cphpyth 24380 pythi 29212 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 29216 |
| [Kreyszig] p. 137 | Lemma 3.2-1(a) | ipcau 24402 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 15568 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 24600 minveco 29246 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 29112 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 24493 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 29235 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 30485 leopg 30484 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 30503 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 29280 |
| [Kulpa] p. 547 | Theorem | poimir 35810 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 35809 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 35808 |
| [Kulpa] p. 548 | Theorem | broucube 35811 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 35803 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 35804 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2383 axnul 5229 |
| [Kunen] p. 11 | Axiom 3 | axnul 5229 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7797 |
| [Kunen] p. 24 | Definition 10.24 | mapval 8627 mapvalg 8625 |
| [Kunen] p. 30 | Lemma 10.20 | fodomg 10278 |
| [Kunen] p. 31 | Definition 10.24 | mapex 8621 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 9522 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 9564 r1elssi 9563 |
| [Kunen] p. 107 | Exercise 4 | rankop 9616 rankopb 9610 rankuni 9621 rankxplim 9637 rankxpsuc 9640 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4936 |
| [Lang] , p. 225 | Corollary 1.3 | finexttrb 31737 |
| [Lang] p. | Definition | df-rn 5600 |
| [Lang] p. 3 | Statement | lidrideqd 18353 mndbn0 18401 |
| [Lang] p. 3 | Definition | df-mnd 18386 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 18371 |
| [Lang] p. 4 | Property of composites. Second formula | gsumccat 18480 |
| [Lang] p. 5 | Equation | gsumreidx 19518 |
| [Lang] p. 5 | Definition of an (infinite) product | gsumfsupp 45376 |
| [Lang] p. 6 | Example | nn0mnd 45373 |
| [Lang] p. 6 | Equation | gsumxp2 19581 |
| [Lang] p. 6 | Statement | cycsubm 18821 |
| [Lang] p. 6 | Definition | mulgnn0gsum 18710 |
| [Lang] p. 6 | Observation | mndlsmidm 19276 |
| [Lang] p. 7 | Definition | dfgrp2e 18605 |
| [Lang] p. 30 | Definition | df-tocyc 31374 |
| [Lang] p. 32 | Property (a) | cyc3genpm 31419 |
| [Lang] p. 32 | Property (b) | cyc3conja 31424 cycpmconjv 31409 |
| [Lang] p. 53 | Definition | df-cat 17377 |
| [Lang] p. 53 | Axiom CAT 1 | cat1 17812 cat1lem 17811 |
| [Lang] p. 54 | Definition | df-iso 17461 |
| [Lang] p. 57 | Definition | df-inito 17699 df-termo 17700 |
| [Lang] p. 58 | Example | irinitoringc 45627 |
| [Lang] p. 58 | Statement | initoeu1 17726 termoeu1 17733 |
| [Lang] p. 62 | Definition | df-func 17573 |
| [Lang] p. 65 | Definition | df-nat 17659 |
| [Lang] p. 91 | Note | df-ringc 45563 |
| [Lang] p. 92 | Statement | mxidlprm 31640 |
| [Lang] p. 92 | Definition | isprmidlc 31623 |
| [Lang] p. 128 | Remark | dsmmlmod 20952 |
| [Lang] p. 129 | Proof | lincscm 45771 lincscmcl 45773 lincsum 45770 lincsumcl 45772 |
| [Lang] p. 129 | Statement | lincolss 45775 |
| [Lang] p. 129 | Observation | dsmmfi 20945 |
| [Lang] p. 141 | Theorem 5.3 | dimkerim 31708 qusdimsum 31709 |
| [Lang] p. 141 | Corollary 5.4 | lssdimle 31691 |
| [Lang] p. 147 | Definition | snlindsntor 45812 |
| [Lang] p. 504 | Statement | mat1 21596 matring 21592 |
| [Lang] p. 504 | Definition | df-mamu 21533 |
| [Lang] p. 505 | Statement | mamuass 21549 mamutpos 21607 matassa 21593 mattposvs 21604 tposmap 21606 |
| [Lang] p. 513 | Definition | mdet1 21750 mdetf 21744 |
| [Lang] p. 513 | Theorem 4.4 | cramer 21840 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 21736 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 21760 |
| [Lang] p. 515 | Definition | df-minmar1 21784 smadiadetr 21824 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 21759 mdetralt 21757 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 21772 |
| [Lang] p. 518 | Definition | df-madu 21783 |
| [Lang] p. 518 | Proposition 4.16 | madulid 21794 madurid 21793 matinv 21826 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 22039 |
| [Lang], p. 224 | Proposition 1.2 | extdgmul 31736 fedgmul 31712 |
| [Lang], p. 561 | Remark | chpmatply1 21981 |
| [Lang], p. 561 | Definition | df-chpmat 21976 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 41952 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 41947 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 41953 |
| [LeBlanc] p. 277 | Rule R2 | axnul 5229 |
| [Levy] p. 12 | Axiom 4.3.1 | df-clab 2716 |
| [Levy] p. 59 | Definition | df-ttrcl 9466 |
| [Levy] p. 64 | Theorem 5.6(ii) | frinsg 9509 |
| [Levy] p. 338 | Axiom | df-clel 2816 df-cleq 2730 |
| [Levy] p. 357 | Proof sketch of conservativity; for details see Appendix | df-clel 2816 df-cleq 2730 |
| [Levy] p. 357 | Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendix | df-clab 2716 |
| [Levy] p. 358 | Axiom | df-clab 2716 |
| [Levy58] p. 2 | Definition I | isfin1-3 10142 |
| [Levy58] p. 2 | Definition II | df-fin2 10042 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 10041 |
| [Levy58] p. 2 | Definition III | df-fin3 10044 |
| [Levy58] p. 3 | Definition V | df-fin5 10045 |
| [Levy58] p. 3 | Definition IV | df-fin4 10043 |
| [Levy58] p. 4 | Definition VI | df-fin6 10046 |
| [Levy58] p. 4 | Definition VII | df-fin7 10047 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 10171 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 33889 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 33900 |
| [Lipparini] p. 6 | Proposition 4.2 | noinfbnd1 33932 nosupbnd1 33917 |
| [Lipparini] p. 6 | Proposition 4.3 | noinfbnd2 33934 nosupbnd2 33919 |
| [Lipparini] p. 7 | Theorem 5.1 | noetasuplem3 33938 noetasuplem4 33939 |
| [Lipparini] p. 7 | Corollary 4.4 | nosupinfsep 33935 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1771 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1772 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1774 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 30770 |
| [Maeda] p. 168 | Lemma 5 | mdsym 30774 mdsymi 30773 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 30768 mdsymlem6 30770 mdsymlem7 30771 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 30772 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 30675 ssdmd2 30676 ssmd1 30673 ssmd2 30674 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 30671 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 30643 df-md 30642 mdbr 30656 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 30693 mdslj1i 30681 mdslj2i 30682 mdslle1i 30679 mdslle2i 30680 mdslmd1i 30691 mdslmd2i 30692 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 30683 mdsl2bi 30685 mdsl2i 30684 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 30697 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 30694 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 30695 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 30672 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 30677 mdsl3 30678 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 30696 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 30791 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 37335 hlrelat1 37414 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 37053 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 30698 cvmdi 30686 cvnbtwn4 30651 cvrnbtwn4 37293 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 30699 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 37354 cvp 30737 cvrp 37430 lcvp 37054 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 30761 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 30760 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 37347 hlexch4N 37406 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 30763 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 37457 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 37763 atpsubN 37767 df-pointsN 37516 pointpsubN 37765 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 37518 pmap11 37776 pmaple 37775 pmapsub 37782 pmapval 37771 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 37779 pmap1N 37781 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 37784 pmapglb2N 37785 pmapglb2xN 37786 pmapglbx 37783 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 37866 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 37491 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 37810 paddclN 37856 paddidm 37855 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 37492 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 37852 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 37491 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 37492 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 19281 lsmmod2 19282 lssats 37026 shatomici 30720 shatomistici 30723 shmodi 29752 shmodsi 29751 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 30662 mdsymlem7 30771 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 29951 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 29855 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 30777 |
| [Margaris] p. 40 | Rule C | exlimiv 1933 |
| [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 397 df-ex 1783 df-or 845 dfbi2 475 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 28764 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 42535 |
| [Margaris] p. 60 | Theorem 8 | jcn 162 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 42536 |
| [Margaris] p. 79 | Rule C | exinst01 42245 exinst11 42246 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1980 19.2g 2181 r19.2z 4425 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2195 rr19.3v 3598 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2156 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1828 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1784 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2174 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2198 19.9h 2283 exlimd 2211 exlimdh 2287 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2162 excomim 2163 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2321 |
| [Margaris] p. 90 | Section 19 | conventions-labels 28765 conventions-labels 28765 conventions-labels 28765 conventions-labels 28765 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1829 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 41996 albi 1821 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 2218 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 2219 |
| [Margaris] p. 90 | Theorem 19.18 | 2exbi 41998 exbi 1849 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2222 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 41995 2alimdv 1921 alimd 2205 alimdh 1820 alimdv 1919 ax-4 1812 ralimdaa 3142 ralimdv 3109 ralimdva 3108 ralimdvva 3126 sbcimdv 3790 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2200 19.21h 2284 19.21t 2199 19.21vv 41994 alrimd 2208 alrimdd 2207 alrimdh 1866 alrimdv 1932 alrimi 2206 alrimih 1826 alrimiv 1930 alrimivv 1931 hbralrimi 3101 r19.21be 3135 r19.21bi 3134 ralrimd 3143 ralrimdv 3105 ralrimdva 3106 ralrimdvv 3124 ralrimdvva 3125 ralrimi 3141 ralrimia 3430 ralrimiv 3102 ralrimiva 3103 ralrimivv 3122 ralrimivva 3123 ralrimivvva 3127 ralrimivw 3104 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 41997 2eximdv 1922 exim 1836 eximd 2209 eximdh 1867 eximdv 1920 rexim 3172 reximd2a 3245 reximdai 3244 reximdd 42701 reximddv 3204 reximddv2 3207 reximddv3 42700 reximdv 3202 reximdv2 3199 reximdva 3203 reximdvai 3200 reximdvva 3206 reximi2 3175 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2204 19.23bi 2184 19.23h 2285 19.23t 2203 exlimdv 1936 exlimdvv 1937 exlimexi 42144 exlimiv 1933 exlimivv 1935 rexlimd3 42693 rexlimdv 3212 rexlimdv3a 3215 rexlimdva 3213 rexlimdva2 3216 rexlimdvaa 3214 rexlimdvv 3222 rexlimdvva 3223 rexlimdvw 3219 rexlimiv 3209 rexlimiva 3210 rexlimivv 3221 |
| [Margaris] p. 90 | Theorem 19.24 | 19.24 1989 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1883 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26 1873 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 2220 r19.27z 4435 r19.27zv 4436 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2221 19.28vv 42004 r19.28z 4428 r19.28zv 4431 rr19.28v 3599 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1876 r19.29d2r 3264 r19.29imd 3186 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1884 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2227 19.31vv 42002 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2226 r19.32 44590 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 42000 19.33 1887 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1990 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35 1880 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36 2223 19.36vv 42001 r19.36zv 4437 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2225 19.37vv 42003 r19.37zv 4432 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1841 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 1988 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1890 19.40 1889 r19.40 3275 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2228 19.41rg 42170 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2229 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1885 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2230 r19.44zv 4434 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2231 r19.45zv 4433 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2612 |
| [Mayet] p. 370 | Remark | jpi 30632 largei 30629 stri 30619 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 30574 ishst 30576 |
| [Mayet3] p. 10 | Theorem | hstrbi 30628 hstri 30627 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 30090 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 30091 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 30640 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 29694 chsupcl 29702 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 30722 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 30716 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 30743 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 37997 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 18205 latj32 18203 latjass 18201 |
| [Megill] p. 444 | Axiom C5 | ax-5 1913 ax5ALT 36921 |
| [Megill] p. 444 | Section 7 | conventions 28764 |
| [Megill] p. 445 | Lemma L12 | aecom-o 36915 ax-c11n 36902 axc11n 2426 |
| [Megill] p. 446 | Lemma L17 | equtrr 2025 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 36910 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 36942 hbnae 2432 |
| [Megill] p. 447 | Remark 9.1 | dfsb1 2485 sbid 2248 sbidd-misc 46421 sbidd 46420 |
| [Megill] p. 448 | Remark 9.6 | axc14 2463 |
| [Megill] p. 448 | Scheme C4' | ax-c4 36898 |
| [Megill] p. 448 | Scheme C5' | ax-c5 36897 sp 2176 |
| [Megill] p. 448 | Scheme C6' | ax-11 2154 |
| [Megill] p. 448 | Scheme C7' | ax-c7 36899 |
| [Megill] p. 448 | Scheme C8' | ax-7 2011 |
| [Megill] p. 448 | Scheme C9' | ax-c9 36904 |
| [Megill] p. 448 | Scheme C10' | ax-6 1971 ax-c10 36900 |
| [Megill] p. 448 | Scheme C11' | ax-c11 36901 |
| [Megill] p. 448 | Scheme C12' | ax-8 2108 |
| [Megill] p. 448 | Scheme C13' | ax-9 2116 |
| [Megill] p. 448 | Scheme C14' | ax-c14 36905 |
| [Megill] p. 448 | Scheme C15' | ax-c15 36903 |
| [Megill] p. 448 | Scheme C16' | ax-c16 36906 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 36918 dral1 2439 dral2-o 36944 dral2 2438 drex1 2441 drex2 2442 drsb1 2499 drsb2 2258 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2161 sbequ 2086 sbid2v 2513 |
| [Megill] p. 450 | Example in Appendix | hba1-o 36911 hba1 2290 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 44387 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3812 rspsbca 3813 stdpc4 2071 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 36898 ra4 3819 stdpc5 2201 |
| [Mendelson] p. 81 | Rule C | exlimiv 1933 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 2031 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 2243 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3715 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 5428 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 4328 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 4329 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 4200 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 4257 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 4201 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 4071 |
| [Mendelson] p. 231 | Definition of union | dfun3 4199 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 5367 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4836 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5483 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4553 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5485 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4865 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5736 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 6172 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 7625 |
| [Mendelson] p. 246 | Definition of successor | df-suc 6272 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 8426 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8927 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8842 xpsneng 8843 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8850 xpcomeng 8851 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8853 |
| [Mendelson] p. 255 | Definition | brsdom 8763 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8845 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 8619 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8827 mapsnend 8826 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8933 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8932 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 8670 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8830 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8846 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 9934 djucomen 9933 |
| [Mendelson] p. 258 | Exercise 4.56(f) | djudom1 9938 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 9932 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 8361 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 8389 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 10315 |
| [Mendelson] p. 281 | Definition | df-r1 9522 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 9571 |
| [Mendelson] p. 287 | Axiom system MK | ru 3715 |
| [MertziosUnger] p. 152 | Definition | df-frgr 28623 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 28658 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 28660 vdgn1frgrv3 28661 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 28662 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 28655 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 28648 2pthfrgrrn 28646 2pthfrgrrn2 28647 |
| [Mittelstaedt] p. 9 | Definition | df-oc 29614 |
| [Monk1] p. 22 | Remark | conventions 28764 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 28764 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 4164 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5693 ssrelf 30955 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5695 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 5137 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 6166 coi2 6167 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5829 rn0 5835 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 6045 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5607 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5838 rnxp 6073 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5685 xp0 6061 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5985 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5982 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7763 imaexALTV 36465 imaexg 7762 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5980 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6953 funfvop 6927 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6825 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6835 |
| [Monk1] p. 43 | Theorem 4.6 | funun 6480 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 7128 dff13f 7129 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 7095 funrnex 7796 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 7120 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 6130 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4895 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7848 df-1st 7831 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7849 df-2nd 7832 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 9612 ranksnb 9585 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 9613 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 9614 rankunb 9608 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 9596 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 9522 r1val2 9595 |
| [Monk1] p. 117 | Lemma | zorn2 10262 zorn2g 10259 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 9744 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 10317 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 9739 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1812 |
| [Monk2] p. 105 | Axiom C7 | ax-7 2011 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2171 ax-c15 36903 ax12v2 2173 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 36898 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2154 |
| [Monk2] p. 109 | Lemma 15 | equvini 2455 equvinv 2032 eqvinop 5401 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1913 ax5ALT 36921 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2137 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2154 |
| [Monk2] p. 114 | Lemma 21 | sp 2176 |
| [Monk2] p. 114 | Lemma 22 | axc4 2315 hba1-o 36911 hba1 2290 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2150 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2170 nfra2 3157 nfra2w 3154 |
| [Moore] p. 53 | Part I | df-mre 17295 |
| [Munkres] p. 77 | Example 2 | distop 22145 indistop 22152 indistopon 22151 |
| [Munkres] p. 77 | Example 3 | fctop 22154 fctop2 22155 |
| [Munkres] p. 77 | Example 4 | cctop 22156 |
| [Munkres] p. 78 | Definition of basis | df-bases 22096 isbasis3g 22099 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 17154 tgval2 22106 |
| [Munkres] p. 79 | Remark | tgcl 22119 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 22113 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 22137 tgss3 22136 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 22138 basgen2 22139 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 35520 topdifinfeq 35521 topdifinffin 35519 topdifinfindis 35517 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 22311 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 22189 topcld 22186 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 22190 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 22192 |
| [Munkres] p. 94 | Definition of closure | clsval 22188 |
| [Munkres] p. 94 | Definition of interior | ntrval 22187 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 22226 elcls 22224 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 22234 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 22299 neindisj 22268 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 22301 |
| [Munkres] p. 97 | Definition of limit point | islp2 22296 lpval 22290 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 22466 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 22378 iscn 22386 iscn2 22389 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 22431 cncnp2 22432 cncnpi 22429 df-cnp 22379 iscnp 22388 iscnp2 22390 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 23699 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 24475 |
| [Nathanson] p. 123 | Remark | reprgt 32601 reprinfz1 32602 reprlt 32599 |
| [Nathanson] p. 123 | Definition | df-repr 32589 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 32621 |
| [Nathanson] p. 123 | Proposition | breprexp 32613 breprexpnat 32614 itgexpif 32586 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 30466 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 45262 |
| [Pfenning] p. 17 | Definition XM | natded 28767 |
| [Pfenning] p. 17 | Definition NNC | natded 28767 notnotrd 133 |
| [Pfenning] p. 17 | Definition ` `C | natded 28767 |
| [Pfenning] p. 18 | Rule" | natded 28767 |
| [Pfenning] p. 18 | Definition /\I | natded 28767 |
| [Pfenning] p. 18 | Definition ` `E | natded 28767 natded 28767 natded 28767 natded 28767 natded 28767 |
| [Pfenning] p. 18 | Definition ` `I | natded 28767 natded 28767 natded 28767 natded 28767 natded 28767 |
| [Pfenning] p. 18 | Definition ` `EL | natded 28767 |
| [Pfenning] p. 18 | Definition ` `ER | natded 28767 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 28767 |
| [Pfenning] p. 18 | Definition ` `IR | natded 28767 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 28767 |
| [Pfenning] p. 127 | Definition =E | natded 28767 |
| [Pfenning] p. 127 | Definition =I | natded 28767 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 24366 df-dip 29063 dip0l 29080 ip0l 20841 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 24407 ipval 29065 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 29076 ipcj 20839 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 24369 dipdir 29204 ipdir 20844 ipdiri 29192 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 29072 nmsq 24358 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 29187 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 29189 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 29190 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 24375 dipass 29207 ipass 20850 ipassi 29203 |
| [Prugovecki] p. 186 | Definition of bra | braval 30306 df-bra 30212 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 30213 kbval 30316 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 30744 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 37902 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 30758 atcvat4i 30759 cvrat3 37456 cvrat4 37457 lsatcvat3 37066 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 30644 cvrval 37283 df-cv 30641 df-lcv 37033 lspsncv0 20408 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 37914 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 37915 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2716 rabid 3310 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2276 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2730 |
| [Quine] p. 19 | Definition 2.9 | conventions 28764 df-v 3434 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2872 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2881 abid2f 2939 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2268 |
| [Quine] p. 40 | Theorem 6.2 | sb6 2088 sbalex 2235 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2816 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2738 eqid1 28831 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2745 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3717 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3718 dfsbcq2 3719 |
| [Quine] p. 43 | Theorem 6.8 | vex 3436 |
| [Quine] p. 43 | Theorem 6.9 | isset 3445 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3530 spcgv 3535 spcimgf 3528 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3729 spsbcd 3730 |
| [Quine] p. 44 | Theorem 6.12 | elex 3450 |
| [Quine] p. 44 | Theorem 6.13 | elab 3609 elabg 3607 elabgf 3605 |
| [Quine] p. 44 | Theorem 6.14 | noel 4264 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4653 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4564 df-sn 4562 |
| [Quine] p. 49 | Theorem 7.4 | snss 4719 snssg 4718 |
| [Quine] p. 49 | Theorem 7.5 | prss 4753 prssg 4752 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4698 prid1g 4696 prid2 4699 prid2g 4697 snid 4597 snidg 4595 |
| [Quine] p. 51 | Theorem 7.12 | snex 5354 |
| [Quine] p. 51 | Theorem 7.13 | prex 5355 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4861 unisnALT 42546 unisng 4860 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4864 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4871 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4869 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 6406 |
| [Quine] p. 56 | Definition 8.18 | dfaiota2 44578 dfiota2 6392 |
| [Quine] p. 57 | Theorem 8.19 | aiotaval 44587 iotaval 6407 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 6411 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 6413 |
| [Quine] p. 58 | Definition 9.1 | df-op 4568 |
| [Quine] p. 61 | Theorem 9.5 | opabid 5438 opabidw 5437 opelopab 5455 opelopaba 5449 opelopabaf 5457 opelopabf 5458 opelopabg 5451 opelopabga 5446 opelopabgf 5453 oprabid 7307 oprabidw 7306 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5595 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5597 |
| [Quine] p. 64 | Definition 9.15 | df-id 5489 |
| [Quine] p. 65 | Theorem 10.3 | fun0 6499 |
| [Quine] p. 65 | Theorem 10.4 | funi 6466 |
| [Quine] p. 65 | Theorem 10.5 | funsn 6487 funsng 6485 |
| [Quine] p. 65 | Definition 10.1 | df-fun 6435 |
| [Quine] p. 65 | Definition 10.2 | args 6000 dffv4 6771 |
| [Quine] p. 68 | Definition 10.11 | conventions 28764 df-fv 6441 fv2 6769 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13986 nn0opth2i 13985 nn0opthi 13984 omopthi 8491 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 8241 |
| [Quine] p. 232 | Equation i | carddom 10310 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 6521 funimaexg 6520 |
| [Quine] p. 331 | Axiom system NF | ru 3715 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 29446 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 29063 polid 29521 polid2i 29519 polidi 29520 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 29175 |
| [ReedSimon] p. 195 | Remark | lnophm 30381 lnophmi 30380 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 30494 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 30496 leopmuli 30495 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 30499 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 30214 leoppos 30488 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 30498 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 30487 |
| [Roman] p. 4 | Definition | df-dmat 21639 df-dmatalt 45739 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 45433 |
| [Roman] p. 19 | Part Preliminaries | df-ring 19785 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 45826 |
| [Roman] p. 112 | Note | isldepslvec2 45826 ldepsnlinc 45849 zlmodzxznm 45838 |
| [Roman] p. 112 | Example | zlmodzxzequa 45837 zlmodzxzequap 45840 zlmodzxzldep 45845 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 22039 |
| [Rosenlicht] p. 80 | Theorem | heicant 35812 |
| [Rosser] p. 281 | Definition | df-op 4568 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 32625 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 32626 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 45702 pmtr3ncom 19083 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 19079 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 19022 cayleyth 19023 |
| [Rudin] p. 164 | Equation 27 | efcan 15805 |
| [Rudin] p. 164 | Equation 30 | efzval 15811 |
| [Rudin] p. 167 | Equation 48 | absefi 15905 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 196 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1774 |
| [Sanford] p. 39 | Rule 4 | mptxor 1772 |
| [Sanford] p. 40 | Rule 1 | mptnan 1771 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 6020 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 6023 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 6019 |
| [Schechter] p. 51 | Definition of transitivity | cotr 6017 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 17295 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 17296 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 17296 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 17298 |
| [Schechter] p. 139 | Definition AC3 | dfac9 9892 |
| [Schechter] p. 141 | Definition (MC) | dfac11 40887 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 10202 axdc3 10210 |
| [Schechter] p. 187 | Definition of ring with unit | isring 19787 isrngo 36055 |
| [Schechter] p. 276 | Remark 11.6.e | span0 29904 |
| [Schechter] p. 276 | Definition of span | df-span 29671 spanval 29695 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 22143 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 27282 axtgcgrrflx 26823 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 27283 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 27284 axtgcgrid 26824 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 26809 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 27295 axtgsegcon 26825 df-trkgcb 26811 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 27306 axtg5seg 26826 df-trkgcb 26811 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 27307 axtgbtwnid 26827 df-trkgb 26810 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 27309 axtgpasch 26828 df-trkgb 26810 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 27328 df-trkg2d 32645 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 26831 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 26832 df-trkg2d 32645 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 27331 axtgeucl 26833 df-trkge 26812 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 27344 axtgcont 26830 axtgcont1 26829 df-trkgb 26810 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 34289 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 34291 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 34294 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 34298 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 34299 tgcgrcomimp 26838 tgcgrcoml 26840 tgcgrcomr 26839 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 34304 tgcgrtriv 26845 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 34308 tg5segofs 32653 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 32650 df-ofs 34285 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 34310 tgcgrextend 26846 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 34312 tgsegconeq 26847 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 34324 btwntriv2 34314 tgbtwntriv2 26848 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 34315 tgbtwncom 26849 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 34318 tgbtwntriv1 26852 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 34319 tgbtwnswapid 26853 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 34325 btwnintr 34321 tgbtwnexch2 26857 tgbtwnintr 26854 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 34327 btwnexch3 34322 tgbtwnexch 26859 tgbtwnexch3 26855 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 34326 tgbtwnouttr 26858 tgbtwnouttr2 26856 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 27327 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 34329 tgbtwndiff 26867 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 26860 trisegint 34330 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 34346 tgifscgr 26869 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 26919 colrot1 26920 colrot2 26921 lncom 26983 lnrot1 26984 lnrot2 26985 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 34342 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 34347 tgcgrsub 26870 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 34357 tgcgrxfr 26879 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 26878 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 34343 df-cgrg 26872 |
| [Schwabhauser] p. 35 | Definition instead (given | df-cgrg 26872 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 34358 tgbtwnxfr 26891 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 34364 colinearperm2 34366 colinearperm3 34365 colinearperm4 34367 colinearperm5 34368 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 26894 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 34341 tgellng 26914 tglng 26907 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 34369 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 34377 lnxfr 26927 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 34378 lnext 26928 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 34382 tgfscgr 26929 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 34383 lncgr 26930 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 34344 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 34385 lnid 26931 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 34386 tgidinside 26932 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 34403 tgbtwnconn1 26936 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 34404 tgbtwnconn2 26937 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 34405 tgbtwnconn3 26938 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 34411 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 34409 legov 26946 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 26947 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 26960 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 34412 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 34414 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 34416 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 34417 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 34418 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 34415 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 34420 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 26948 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 26950 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 26951 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 26952 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 26953 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 34427 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 34428 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 34423 df-outsideof 34422 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 34424 ishlg 26963 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 26968 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 26970 outsideofrflx 34429 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 26964 hlcomd 26965 outsideofcom 34430 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 26971 outsideoftr 34431 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 26979 outsideofeu 34433 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 34440 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 34441 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 34434 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 34449 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 34450 tglineelsb2 26993 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 34452 linerflx1 34451 linerflx2 34453 tglinecom 26996 tglinerflx1 26994 tglinerflx2 26995 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 34455 tglinethru 26997 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 34439 tglng 26907 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 26955 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 34458 tglinethrueu 27000 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 34459 tglineineq 27004 tglineinteq 27006 tglineintmo 27003 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 27010 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 27011 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 27012 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 27027 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 27023 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 27015 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 27014 ismir 27020 mirbtwn 27019 mircgr 27018 mirfv 27017 mirval 27016 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 27025 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 27026 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 27027 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 27030 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 27031 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 27036 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 27033 mirbtwni 27032 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 27034 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 27046 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 27050 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 27047 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 27048 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 27049 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 27052 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 27053 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 27059 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 27055 israg 27058 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 27060 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 27061 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 27063 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 27064 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 27065 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 27066 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 27067 ragncol 27070 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 27068 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 27074 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 27078 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 27075 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 27057 isperp 27073 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 27076 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 27083 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 27091 colperpexlem2 27092 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 27094 colperpexlem3 27093 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 27099 midex 27098 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 27096 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 27105 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 27100 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 27109 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 27112 opphllem6 27113 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 27115 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 26828 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 27116 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 27124 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 27119 hpgbr 27121 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 27126 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 27125 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 27127 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 27128 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 27129 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 27130 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 27131 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 27145 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 27135 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 27149 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 27150 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 27151 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 27152 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 27153 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 27156 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 27158 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 27136 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 27159 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 27162 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 27163 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 27164 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 27165 trgcopyeu 27167 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 27191 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 27170 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 27179 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 27177 cgrahl2 27178 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 27180 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 27181 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 27183 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 27184 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 27187 cgrahl 27188 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 27192 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 27193 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 27194 acopyeu 27195 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 27202 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 27206 |
| [Schwabhauser] p. 101 | Definition 11.23 | isinag 27199 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 27214 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 27207 isleag 27208 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 27216 tgsas1 27215 tgsas2 27217 tgsas3 27218 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 27220 tgasa1 27219 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 27221 tgsss2 27222 tgsss3 27223 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 26419 dchrsum 26417 dchrsum2 26416 sumdchr 26420 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 26421 sum2dchr 26422 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 19669 ablfacrp2 19670 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 26364 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 26365 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 26372 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 26630 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 26633 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 26687 vmalogdivsum2 26686 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 26677 dirith2 26676 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 26675 rpvmasum 26674 rpvmasum2 26660 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 26635 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 26673 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 26640 dchrisumlem1 26637 dchrisumlem2 26638 dchrisumlem3 26639 dchrisumlema 26636 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 26643 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 26672 dchrmusumlem 26670 dchrvmasumlem 26671 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 26642 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 26644 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 26668 dchrisum0re 26661 dchrisumn0 26669 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 26654 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 26658 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 26659 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 26714 pntrsumbnd2 26715 pntrsumo1 26713 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 26678 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 26680 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 26682 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 26685 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 26690 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 26691 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 26696 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 26698 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 26699 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 26707 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 26708 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 26705 selberg3lem2 26706 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 26709 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 26703 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 26716 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 26717 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 26718 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 26732 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 26744 pntlemb 26745 pntlemc 26743 pntlemd 26742 pntlemg 26746 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 26744 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 26736 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 26741 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 26744 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 26757 pntleml 26759 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 4230 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 4335 dif0 4306 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4422 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4408 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 4221 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 4222 |
| [Stoll] p. 20 | Remark | invdif 4202 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4570 |
| [Stoll] p. 43 | Definition | uniiun 4988 |
| [Stoll] p. 44 | Definition | intiin 4989 |
| [Stoll] p. 45 | Definition | df-iin 4927 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4926 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 402 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 4230 |
| [Strang] p. 242 | Section 6.3 | expgrowth 41953 |
| [Suppes] p. 22 | Theorem 2 | eq0 4277 eq0f 4274 |
| [Suppes] p. 22 | Theorem 4 | eqss 3936 eqssd 3938 eqssi 3937 |
| [Suppes] p. 23 | Theorem 5 | ss0 4332 ss0b 4331 |
| [Suppes] p. 23 | Theorem 6 | sstr 3929 sstrALT2 42455 |
| [Suppes] p. 23 | Theorem 7 | pssirr 4035 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 4036 |
| [Suppes] p. 23 | Theorem 9 | psstr 4039 |
| [Suppes] p. 23 | Theorem 10 | pssss 4030 |
| [Suppes] p. 25 | Theorem 12 | elin 3903 elun 4083 |
| [Suppes] p. 26 | Theorem 15 | inidm 4152 |
| [Suppes] p. 26 | Theorem 16 | in0 4325 |
| [Suppes] p. 27 | Theorem 23 | unidm 4086 |
| [Suppes] p. 27 | Theorem 24 | un0 4324 |
| [Suppes] p. 27 | Theorem 25 | ssun1 4106 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 4114 |
| [Suppes] p. 27 | Theorem 27 | unss 4118 |
| [Suppes] p. 27 | Theorem 28 | indir 4209 |
| [Suppes] p. 27 | Theorem 29 | undir 4210 |
| [Suppes] p. 28 | Theorem 32 | difid 4304 |
| [Suppes] p. 29 | Theorem 33 | difin 4195 |
| [Suppes] p. 29 | Theorem 34 | indif 4203 |
| [Suppes] p. 29 | Theorem 35 | undif1 4409 |
| [Suppes] p. 29 | Theorem 36 | difun2 4414 |
| [Suppes] p. 29 | Theorem 37 | difin0 4407 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4405 |
| [Suppes] p. 29 | Theorem 39 | difundi 4213 |
| [Suppes] p. 29 | Theorem 40 | difindi 4215 |
| [Suppes] p. 30 | Theorem 41 | nalset 5237 |
| [Suppes] p. 39 | Theorem 61 | uniss 4847 |
| [Suppes] p. 39 | Theorem 65 | uniop 5429 |
| [Suppes] p. 41 | Theorem 70 | intsn 4917 |
| [Suppes] p. 42 | Theorem 71 | intpr 4913 intprg 4912 |
| [Suppes] p. 42 | Theorem 73 | op1stb 5386 |
| [Suppes] p. 42 | Theorem 78 | intun 4911 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4963 dfiun2g 4960 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4964 |
| [Suppes] p. 47 | Theorem 86 | elpw 4537 elpw2 5269 elpw2g 5268 elpwg 4536 elpwgdedVD 42537 |
| [Suppes] p. 47 | Theorem 87 | pwid 4557 |
| [Suppes] p. 47 | Theorem 89 | pw0 4745 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4746 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5604 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5742 xpindir 5743 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5655 xpundir 5656 |
| [Suppes] p. 54 | Theorem 105 | elirrv 9355 |
| [Suppes] p. 58 | Theorem 2 | relss 5692 |
| [Suppes] p. 59 | Theorem 4 | eldm 5809 eldm2 5810 eldm2g 5808 eldmg 5807 |
| [Suppes] p. 59 | Definition 3 | df-dm 5599 |
| [Suppes] p. 60 | Theorem 6 | dmin 5820 |
| [Suppes] p. 60 | Theorem 8 | rnun 6049 |
| [Suppes] p. 60 | Theorem 9 | rnin 6050 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5797 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5791 brcnvg 5788 |
| [Suppes] p. 62 | Equation 5 | elcnv 5785 elcnv2 5786 |
| [Suppes] p. 62 | Theorem 12 | relcnv 6012 |
| [Suppes] p. 62 | Theorem 15 | cnvin 6048 |
| [Suppes] p. 62 | Theorem 16 | cnvun 6046 |
| [Suppes] p. 63 | Definition | dftrrels2 36689 |
| [Suppes] p. 63 | Theorem 20 | co02 6164 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5880 |
| [Suppes] p. 63 | Definition 7 | df-co 5598 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5794 |
| [Suppes] p. 64 | Theorem 27 | coass 6169 |
| [Suppes] p. 65 | Theorem 31 | resundi 5905 |
| [Suppes] p. 65 | Theorem 34 | elima 5974 elima2 5975 elima3 5976 elimag 5973 |
| [Suppes] p. 65 | Theorem 35 | imaundi 6053 |
| [Suppes] p. 66 | Theorem 40 | dminss 6056 |
| [Suppes] p. 66 | Theorem 41 | imainss 6057 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 6060 |
| [Suppes] p. 81 | Definition 34 | dfec2 8501 |
| [Suppes] p. 82 | Theorem 72 | elec 8542 elecALTV 36405 elecg 8541 |
| [Suppes] p. 82 | Theorem 73 | eqvrelth 36724 erth 8547 erth2 8548 |
| [Suppes] p. 83 | Theorem 74 | eqvreldisj 36727 erdisj 8550 |
| [Suppes] p. 89 | Theorem 96 | map0b 8671 |
| [Suppes] p. 89 | Theorem 97 | map0 8675 map0g 8672 |
| [Suppes] p. 89 | Theorem 98 | mapsn 8676 mapsnd 8674 |
| [Suppes] p. 89 | Theorem 99 | mapss 8677 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 9824 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 9823 |
| [Suppes] p. 92 | Theorem 1 | enref 8773 enrefg 8772 |
| [Suppes] p. 92 | Theorem 2 | ensym 8789 ensymb 8788 ensymi 8790 |
| [Suppes] p. 92 | Theorem 3 | entr 8792 |
| [Suppes] p. 92 | Theorem 4 | unen 8836 |
| [Suppes] p. 94 | Theorem 15 | endom 8767 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8786 |
| [Suppes] p. 94 | Theorem 17 | domtr 8793 |
| [Suppes] p. 95 | Theorem 18 | sbth 8880 |
| [Suppes] p. 97 | Theorem 23 | canth2 8917 canth2g 8918 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8884 df-sdom 8736 dfsdom2 8883 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8901 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8886 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8885 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8899 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 8770 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8902 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8897 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8821 fundmeng 8822 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8857 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8898 |
| [Suppes] p. 104 | Theorem 37 | fofi 9105 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8961 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8961 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 10307 |
| [Suppes] p. 130 | Definition 3 | df-tr 5192 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 7630 |
| [Suppes] p. 134 | Definition 6 | df-suc 6272 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7749 finds 7745 finds1 7748 finds2 7747 |
| [Suppes] p. 151 | Theorem 42 | isfinite 9410 isfinite2 9072 isfiniteg 9074 unbnn 9070 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 10674 df-ltpq 10666 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7709 tfinds 7706 tfinds2 7710 |
| [Suppes] p. 209 | Theorem 18 | oaord1 8382 |
| [Suppes] p. 209 | Theorem 21 | oaword2 8384 |
| [Suppes] p. 211 | Theorem 25 | oaass 8392 |
| [Suppes] p. 225 | Definition 8 | iscard2 9734 |
| [Suppes] p. 227 | Theorem 56 | ondomon 10319 |
| [Suppes] p. 228 | Theorem 59 | harcard 9736 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 9822 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 6316 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 7643 onminsb 7644 |
| [Suppes] p. 229 | Theorem 64 | alephval2 10328 |
| [Suppes] p. 229 | Theorem 65 | alephcard 9826 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 9833 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 9827 |
| [Suppes] p. 229 | Definition 12 | df-aleph 9698 |
| [Suppes] p. 242 | Theorem 6 | weth 10251 |
| [Suppes] p. 242 | Theorem 8 | entric 10313 |
| [Suppes] p. 242 | Theorem 9 | carden 10307 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2709 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2730 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2816 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2732 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2761 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 7279 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3715 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 5344 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4584 elpr2 4586 elpr2g 4585 elprg 4582 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4576 elsn2 4600 elsn2g 4599 elsng 4575 velsn 4577 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 5382 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4571 sneqr 4771 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4580 dfsn2 4574 dfsn2ALT 4581 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 7594 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 5391 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 5379 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 5364 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 7596 unexg 7599 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4625 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4840 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3894 df-un 3892 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4857 uniprg 4856 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 5300 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4624 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 6335 elsucg 6333 sstr2 3928 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 4087 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 4135 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 4100 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 4153 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 4207 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 4208 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3906 dfss2 3907 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4535 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 4115 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3904 sseqin2 4149 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3943 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 4162 inss2 4163 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 3983 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4850 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 5365 sspwimp 42538 sspwimpALT 42545 sspwimpALT2 42548 sspwimpcf 42540 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 5372 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 5209 |
| [TakeutiZaring] p. 20 | Definition | df-rab 3073 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 5231 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3890 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 4259 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 4304 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 4280 n0f 4276 neq0 4279 neq0f 4275 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 9354 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 9490 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 9492 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3434 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 5239 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 4330 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 5245 ssexg 5247 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 5241 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 9361 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 9356 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 4297 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 4065 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 4224 undif3VD 42502 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 4066 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 4073 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 3069 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 3070 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 7603 xpexg 7600 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5596 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 6505 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6680 fun11 6508 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 6446 svrelfun 6506 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5796 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5798 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5601 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5602 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5598 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 6097 dfrel2 6092 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5605 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5721 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5728 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5741 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5920 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5897 opelresi 5899 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5913 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5916 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5921 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 6476 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 6148 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 6474 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6682 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2611 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 28764 df-fv 6441 fv3 6792 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7772 cnvexg 7771 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7758 dmexg 7750 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7759 rnexg 7751 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 42072 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7767 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6787 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 44666 tz6.12-1-afv2 44733 tz6.12-1 6796 tz6.12-afv 44665 tz6.12-afv2 44732 tz6.12 6797 tz6.12c-afv2 44734 tz6.12c 6799 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2-afv2 44729 tz6.12-2 6762 tz6.12i-afv2 44735 tz6.12i 6800 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 6436 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 6437 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 6439 wfo 6431 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 6438 wf1 6430 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 6440 wf1o 6432 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6909 eqfnfv2 6910 eqfnfv2f 6913 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6866 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 7093 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 7091 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 6521 funimaexg 6520 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 5075 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5504 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5553 dffr3 6007 eliniseg 6002 iniseg 6005 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5495 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5567 fr3nr 7622 frirr 5566 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5544 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 7624 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5556 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5576 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 6250 tz6.26i 6252 wefrc 5583 wereu2 5586 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 6253 wfii 6255 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 6442 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 7200 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 7201 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 7207 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 7208 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 7209 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 7213 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 7220 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 7222 |
| [TakeutiZaring] p. 35 | Notation | wtr 5191 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 42073 tz7.2 5573 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 5195 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 6279 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 6287 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 6288 ordelordALT 42157 ordelordALTVD 42487 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 6294 ordelssne 6293 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 6292 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 6296 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 7632 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 7633 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 6270 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 6298 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 42169 ordon 7627 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 7628 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7700 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 6313 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 5193 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 7642 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7678 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 6367 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 6366 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 7629 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4871 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 6272 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 6343 sucidg 6344 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7659 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 6357 ordnbtwn 6356 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7675 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 6271 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7727 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7732 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7688 ordelsuc 7667 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7669 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7698 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7714 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7735 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7737 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7738 |
| [TakeutiZaring] p. 43 | Remark | omon 7724 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 9393 omex 9401 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7722 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7743 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7739 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7740 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7717 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4893 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 5208 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4894 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 5261 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7645 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 6315 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4880 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 9418 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 7640 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 8207 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 8228 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 8229 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 8230 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 8237 tz7.44-2 8238 tz7.44-3 8239 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 8198 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 8193 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 8177 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 8276 tz7.49c 8277 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 8274 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 8273 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 8275 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2657 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 9767 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 9768 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 8362 oasuc 8354 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7707 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 8365 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 8346 oa0r 8368 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 8366 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 8379 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 8450 nnaordi 8449 oaord 8378 oaordi 8377 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4979 uniss2 4874 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 8381 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 8386 oawordex 8388 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 8442 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 8478 |
| [TakeutiZaring] p. 60 | Remark | oancom 9409 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 8391 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 8447 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 8383 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0x 8349 omlim 8363 omsuc 8356 |
| [TakeutiZaring] p. 62 | Definition 8.15(a) | om0 8347 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 8444 nnmcl 8443 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 8463 nnmordi 8462 omord 8399 omordi 8397 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 8400 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 8467 omwordri 8403 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 8369 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 8373 om1r 8374 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 8406 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 8408 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 8409 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 8410 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 8411 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 8439 oe0 8352 oelim 8364 oesuc 8357 onesuc 8360 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 8350 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 8417 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 8418 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 8351 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 8376 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 8419 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 8425 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 8423 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 8424 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 8428 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 8430 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 9486 tz9.1 9487 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 9522 r10 9526 r1lim 9530 r1limg 9529 r1suc 9528 r1sucg 9527 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 9538 r1ord2 9539 r1ordg 9536 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 9548 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 9573 tz9.13 9549 tz9.13g 9550 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 9523 rankval 9574 rankvalb 9555 rankvalg 9575 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 9597 rankelb 9582 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 9611 rankval3 9598 rankval3b 9584 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 9587 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 9553 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 9592 rankr1c 9579 rankr1g 9590 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 9593 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 9607 rankssb 9606 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 9600 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 9599 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 10231 dfac3 9877 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 9786 numth 10228 numth2 10227 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 10302 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 10303 cardid2 9711 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 9718 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 10307 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 9717 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 9702 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 9723 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 9715 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8937 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8803 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8942 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8861 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 9721 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 9854 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8992 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 9011 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 9855 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8997 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 9844 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 9822 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 9730 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9973 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 9088 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 8737 isfi 8764 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 9013 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 10290 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8854 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 10282 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | djuxpdom 9941 unxpdom 9030 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 9732 cardsdomelir 9731 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 9032 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 9770 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 8617 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 10318 infxpidm2 9773 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infdju 9964 infxp 9971 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8866 pw2f1o 8864 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8930 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 10243 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 10238 ac6s5 10247 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 10299 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 10300 uniimadomf 10301 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 10030 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 10025 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 10010 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 10007 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 10013 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 10020 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 10029 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 10338 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 10008 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 10032 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 9853 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 9852 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 9864 alephfp2 9865 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 10455 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 9868 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 10325 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 10339 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 10340 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 36897 |
| [Tarski] p. 67 | Scheme B5 | sp 2176 |
| [Tarski] p. 68 | Lemma 6 | avril1 28827 equid 2015 |
| [Tarski] p. 69 | Lemma 7 | equcomi 2020 |
| [Tarski] p. 70 | Lemma 14 | spim 2387 spime 2389 spimew 1975 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2171 ax-c15 36903 ax12i 1970 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2088 |
| [Tarski] p. 75 | Axiom B7 | ax6v 1972 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1913 ax5ALT 36921 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 2011 ax-8 2108 ax-9 2116 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 26825 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 26826 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 26828 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 26828 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 26829 |
| [Truss] p. 114 | Theorem 5.18 | ruc 15952 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 35816 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 35818 |
| [Weierstrass] p. 272 | Definition | df-mdet 21734 mdetuni 21771 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 901 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 865 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 866 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 917 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 965 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 188 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 135 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 90 wl-luk-pm2.04 35616 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 41408 imim2 58 wl-luk-imim2 35611 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | adh-minimp-imim1 44514 imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 894 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2664 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 900 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-luk-id 35614 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 892 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 142 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 895 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 130 notnotrALT2 42547 wl-luk-notnotr 35615 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 146 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 41438 axfrege28 41437 con3 153 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | ax-3 8 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18 128 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 864 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 922 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 123 wl-luk-pm2.21 35608 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 124 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 887 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 937 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-labels 28765 pm2.27 42 wl-luk-pm2.27 35606 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 920 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 921 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 967 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 968 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 966 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1087 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 904 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 905 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 940 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 879 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 880 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5 169 pm2.5g 168 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6 190 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 881 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 882 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 883 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 172 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 173 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 848 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 849 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 886 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 888 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 191 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 897 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 938 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 939 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 192 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 889 pm2.67 890 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 176 pm2.521g 174 pm2.521g2 175 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 896 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 970 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 898 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 202 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 971 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 972 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 931 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 929 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 969 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 973 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 930 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 109 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 989 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 470 pm3.2im 160 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 990 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 991 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 992 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 993 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 472 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 460 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 403 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 800 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 449 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 450 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 483 simplim 167 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 485 simprim 166 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 762 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 763 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 805 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 622 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 807 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 493 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 494 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 958 pm3.44 957 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 806 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 474 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 961 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34b 316 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 260 |
| [WhiteheadRussell] p. 117 | Theorem *4.11 | notbi 319 |
| [WhiteheadRussell] p. 117 | Theorem *4.12 | con2bi 354 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotb 315 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14 804 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 830 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 221 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 803 bitr 802 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 564 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 902 pm4.25 903 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 461 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 1005 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 867 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 469 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 919 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 632 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 915 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 635 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 974 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1088 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 1003 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1051 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 1020 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 994 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 996 pm4.45 995 pm4.45im 825 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 980 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 850 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 546 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 979 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 982 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 983 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 984 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 985 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 981 pm4.56 986 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 987 pm4.57 988 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 405 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 853 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 398 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 846 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 406 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 847 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67 399 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 558 pm4.71d 562 pm4.71i 560 pm4.71r 559 pm4.71rd 563 pm4.71ri 561 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 947 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 528 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 934 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 518 pm4.76 519 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 959 pm4.77 960 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 932 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 1001 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 393 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81 394 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 1021 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 1022 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 348 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 349 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 352 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 389 impexp 451 pm4.87 840 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 821 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 942 pm5.11g 941 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 943 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 945 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 944 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 1010 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 1011 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 1009 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbn 385 pm5.18 383 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 388 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 822 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 1012 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 1047 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 1048 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 899 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 573 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 390 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 362 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6 999 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 951 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 828 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 574 |
| [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 391 pm5.41 392 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 544 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 543 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 1002 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 1015 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 946 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 998 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 1016 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 1017 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 1025 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 367 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 269 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 1026 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 41976 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 41977 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1873 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 41978 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 41979 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 41980 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1896 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 41981 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 41982 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 41983 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 41984 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 41985 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 41987 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 41988 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 41989 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 41986 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2093 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 41992 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 41993 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2073 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2157 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1831 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1832 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 41994 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 41995 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 41996 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 41997 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 41999 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 41998 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1890 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 42001 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 42002 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 42000 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1830 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 42003 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 42004 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1848 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 42005 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2344 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 1863 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 42010 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 42006 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 42007 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 42008 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 42009 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 42014 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 42011 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 42012 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 42013 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 42015 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2569 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 42025 pm13.13b 42026 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 42027 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 3025 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 3026 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3597 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 42033 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 42034 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 42028 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 42172 pm13.193 42029 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 42030 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 42031 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 42032 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 42039 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 42038 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 42037 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3784 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 42040 pm14.122b 42041 pm14.122c 42042 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 42043 pm14.123b 42044 pm14.123c 42045 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 42047 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 42046 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 42048 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 6414 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 42049 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 6415 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 42050 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 42052 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2635 eupickbi 2638 sbaniota 42053 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 42051 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 2584 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 42055 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 28764 df-fv 6441 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 9759 pm54.43lem 9758 |
| [Young] p. 141 | Definition of operator ordering | leop2 30486 |
| [Young] p. 142 | Example 12.2(i) | 0leop 30492 idleop 30493 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 40650 |
| [vandenDries] p. 43 | Theorem 62 | pellex 40657 pellexlem1 40651 |