Bibliographic Cross-References
|
|
Intuitionistic Logic Explorer Bibliographic Cross-References |
|
| Mirrors > Home > ILE Home > Bibliographic Cross-References | ||
| Bibliographic Reference | Description | Intuitionistic Logic Explorer Page(s) |
|---|---|---|
| [AczelRathjen], p. 71 | Definition 8.1.4 | enumct 6873 fidcenum 6745 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 6745 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 6873 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 6720 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 6708 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | znnen 11638 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 10299 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4381 |
| [Apostol] p. 18 | Theorem I.1 | addcan 7759 addcan2d 7764 addcan2i 7762 addcand 7763 addcani 7761 |
| [Apostol] p. 18 | Theorem I.2 | negeu 7770 |
| [Apostol] p. 18 | Theorem I.3 | negsub 7827 negsubd 7896 negsubi 7857 |
| [Apostol] p. 18 | Theorem I.4 | negneg 7829 negnegd 7881 negnegi 7849 |
| [Apostol] p. 18 | Theorem I.5 | subdi 7960 subdid 7989 subdii 7982 subdir 7961 subdird 7990 subdiri 7983 |
| [Apostol] p. 18 | Theorem I.6 | mul01 7964 mul01d 7968 mul01i 7966 mul02 7962 mul02d 7967 mul02i 7965 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8357 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8308 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 7973 mul2negd 7988 mul2negi 7981 mulneg1 7970 mulneg1d 7986 mulneg1i 7979 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8277 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9256 rpaddcld 9288 rpmulcl 9257 rpmulcld 9289 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9266 |
| [Apostol] p. 20 | Theorem I.17 | lttri 7686 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8112 ltadd1dd 8130 ltadd1i 8077 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8166 ltmul1a 8165 ltmul1i 8478 ltmul1ii 8486 ltmul2 8414 ltmul2d 9315 ltmul2dd 9329 ltmul2i 8481 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 7707 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8043 lt0neg1d 8090 ltneg 8037 ltnegd 8097 ltnegi 8068 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8020 lt2addd 8141 lt2addi 8085 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9234 |
| [Apostol] p. 21 | Exercise 4 | recgt0 8408 recgt0d 8492 recgt0i 8464 recgt0ii 8465 |
| [Apostol] p. 22 | Definition of integers | df-z 8849 |
| [Apostol] p. 22 | Definition of rationals | df-q 9204 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 6769 |
| [Apostol] p. 26 | Theorem I.29 | arch 8768 |
| [Apostol] p. 28 | Exercise 2 | btwnz 8964 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 8769 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 9817 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 11298 zneo 8946 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 10579 sqrtthi 10667 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 8523 |
| [Apostol] p. 363 | Remark | absgt0api 10694 |
| [Apostol] p. 363 | Example | abssubd 10741 abssubi 10698 |
| [ApostolNT] p. 14 | Definition | df-dvds 11224 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 11236 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 11260 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 11256 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 11250 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 11252 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 11237 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 11238 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 11243 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 11273 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 11275 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 11277 |
| [ApostolNT] p. 15 | Definition | dfgcd2 11430 |
| [ApostolNT] p. 16 | Definition | isprm2 11526 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 11501 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 11392 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 11431 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 11433 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 11405 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 11398 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 11550 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 11552 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 11351 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 11468 |
| [ApostolNT] p. 25 | Definition | df-phi 11614 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 11625 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 11629 |
| [ApostolNT] p. 104 | Definition | congr 11509 |
| [ApostolNT] p. 106 | Remark | dvdsval3 11227 |
| [ApostolNT] p. 106 | Definition | moddvds 11232 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 11305 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 11306 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 9897 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 9934 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 11255 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 11512 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 11514 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 584 pm2.65 623 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5689 onsucelsucexmidlem 4373 |
| [Bauer], p. 483 | Definition | n0rf 3314 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6672 |
| [BauerSwan], p. 14 | Remark | 0ct 6869 ctm 6871 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 6873 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7157 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7070 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7159 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7193 addlocpr 7192 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7219 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7222 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7227 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 1958 |
| [BellMachover] p. 460 | Notation | df-mo 1959 |
| [BellMachover] p. 460 | Definition | mo3 2009 mo3h 2008 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2080 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 3981 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4033 |
| [BellMachover] p. 466 | Axiom Union | axun2 4286 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4386 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4235 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4389 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4341 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4220 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4432 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4456 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1372 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1370 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1373 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5600 fcofo 5601 |
| [BourbakiTop1] p. | Remark | xnegmnf 9395 xnegpnf 9394 |
| [BourbakiTop1] p. | Remark | rexneg 9396 |
| [BourbakiTop1] p. | Property V_i | ssnei2 12009 |
| [BourbakiTop1] p. | Property V_ii | innei 12015 |
| [BourbakiTop1] p. | Property V_iv | neissex 12017 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 12006 neiss 12002 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 12073 |
| [BourbakiTop1] p. | Property V_iii | elnei 12004 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 11849 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 3923 |
| [Crosilla] p. | Axiom 1 | ax-ext 2077 |
| [Crosilla] p. | Axiom 2 | ax-pr 4060 |
| [Crosilla] p. | Axiom 3 | ax-un 4284 |
| [Crosilla] p. | Axiom 4 | ax-nul 3986 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4431 |
| [Crosilla] p. | Axiom 6 | ru 2853 |
| [Crosilla] p. | Axiom 8 | ax-pow 4030 |
| [Crosilla] p. | Axiom 9 | ax-setind 4381 |
| [Crosilla], p. | Axiom 6 | ax-sep 3978 |
| [Crosilla], p. | Axiom 7 | ax-coll 3975 |
| [Crosilla], p. | Axiom 7' | repizf 3976 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4366 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5689 |
| [Crosilla], p. | Definition of ordinal | df-iord 4217 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4379 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3015 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4434 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6447 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 3985 |
| [Enderton] p. 19 | Definition | df-tp 3474 |
| [Enderton] p. 26 | Exercise 5 | unissb 3705 |
| [Enderton] p. 26 | Exercise 10 | pwel 4069 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4137 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3821 iinin2m 3820 iunin1 3816 iunin2 3815 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3819 iundif2ss 3817 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 3833 |
| [Enderton] p. 33 | Exercise 25 | iununir 3834 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 3841 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4330 iunpwss 3842 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4068 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4048 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4300 rnex 4732 rnexg 4730 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4677 rnuni 4876 |
| [Enderton] p. 42 | Definition of a function | dffun7 5076 dffun8 5077 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5403 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5109 |
| [Enderton] p. 44 | Definition (d) | dfima2 4809 dfima3 4810 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5408 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5578 |
| [Enderton] p. 52 | Definition | df-map 6447 |
| [Enderton] p. 53 | Exercise 21 | coass 4983 |
| [Enderton] p. 53 | Exercise 27 | dmco 4973 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5119 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 4841 |
| [Enderton] p. 54 | Remark | ixpf 6517 ixpssmap 6529 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6496 |
| [Enderton] p. 56 | Theorem 3M | erref 6352 |
| [Enderton] p. 57 | Lemma 3N | erthi 6378 |
| [Enderton] p. 57 | Definition | df-ec 6334 |
| [Enderton] p. 58 | Definition | df-qs 6338 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6437 th3qcor 6436 th3qlem1 6434 th3qlem2 6435 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6334 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4674 |
| [Enderton] p. 68 | Definition of successor | df-suc 4222 |
| [Enderton] p. 71 | Definition | df-tr 3959 dftr4 3963 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4264 unisucg 4265 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4264 unisucg 4265 |
| [Enderton] p. 73 | Exercise 5(a) | truni 3972 |
| [Enderton] p. 73 | Exercise 5(b) | trint 3973 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6275 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6277 onasuc 6267 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5693 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6276 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6278 onmsuc 6274 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6286 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6279 nnacom 6285 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6287 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6288 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6290 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6280 nnmsucr 6289 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6326 |
| [Enderton] p. 129 | Definition | df-en 6538 |
| [Enderton] p. 133 | Exercise 1 | xpomen 11635 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6661 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6653 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 6642 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3377 |
| [Enderton] p. 145 | Figure 38 | ffoss 5320 |
| [Enderton] p. 145 | Definition | df-dom 6539 |
| [Enderton] p. 146 | Example 1 | domen 6548 domeng 6549 |
| [Enderton] p. 146 | Example 3 | nndomo 6660 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6631 xpdom1g 6629 xpdom2g 6628 |
| [Enderton] p. 168 | Definition | df-po 4147 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4279 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4240 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4387 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4243 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4361 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4334 |
| [Enderton] p. 194 | Remark | onprc 4396 |
| [Enderton] p. 194 | Exercise 16 | suc11 4402 |
| [Enderton] p. 197 | Definition | df-card 6905 |
| [Enderton] p. 200 | Exercise 25 | tfis 4426 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4398 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4400 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4401 |
| [Geuvers], p. 1 | Remark | expap0 10100 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8189 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8220 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8190 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 7561 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 10751 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 10759 maxle2 10760 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 10761 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 10764 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 10765 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8156 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7003 enqer 7014 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7007 df-nqqs 7004 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7000 df-plqqs 7005 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7001 df-mqqs 7006 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7008 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7064 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7067 ltbtwnnq 7072 ltbtwnnqq 7071 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7056 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7057 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7193 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7235 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7234 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7253 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7269 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7275 ltaprlem 7274 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7272 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7228 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7248 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7237 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7236 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7244 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7294 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7369 enrer 7378 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7374 df-1r 7375 df-nr 7370 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7372 df-plr 7371 negexsr 7415 recexsrlem 7417 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7373 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 8518 creur 8517 cru 8176 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 7553 axcnre 7513 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 10407 crimd 10526 crimi 10486 crre 10406 crred 10525 crrei 10485 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 10409 remimd 10491 |
| [Gleason] p. 133 | Definition 10.36 | absval2 10605 absval2d 10733 absval2i 10692 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 10433 cjaddd 10514 cjaddi 10481 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 10434 cjmuld 10515 cjmuli 10482 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 10432 cjcjd 10492 cjcji 10464 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 10431 cjreb 10415 cjrebd 10495 cjrebi 10467 cjred 10520 rere 10414 rereb 10412 rerebd 10494 rerebi 10466 rered 10518 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 10440 addcjd 10506 addcji 10476 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 10549 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 10600 abscjd 10738 abscji 10696 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 10612 abs00d 10734 abs00i 10693 absne0d 10735 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 10644 releabsd 10739 releabsi 10697 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 10617 absmuld 10742 absmuli 10699 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 10603 sqabsaddi 10700 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 10652 abstrid 10744 abstrii 10703 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 10075 df-exp 10070 exp0 10074 expp1 10077 expp1d 10202 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10112 expaddd 10203 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | expmul 10115 expmuld 10204 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10109 mulexpd 10216 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 9575 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 10869 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 10871 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 10870 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 10874 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 10867 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 10863 climcj 10864 climim 10866 climre 10865 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 7624 df-xr 7623 ltxr 9345 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 10890 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 9856 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 11842 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 12150 xmet0 12149 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 12157 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 12159 mstri 12259 xmettri 12158 xmstri 12258 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 12293 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 10853 mulcn2 10855 subcn2 10854 |
| [Gleason] p. 295 | Remark | bcval3 10274 bcval4 10275 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10289 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10272 df-bc 10271 |
| [Gleason] p. 296 | Remark | bcn0 10278 bcnn 10280 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 11027 |
| [Gleason] p. 308 | Equation 2 | ef0 11111 |
| [Gleason] p. 308 | Equation 3 | efcj 11112 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 11117 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 11121 |
| [Gleason] p. 310 | Equation 14 | sinadd 11176 |
| [Gleason] p. 310 | Equation 15 | cosadd 11177 |
| [Gleason] p. 311 | Equation 17 | sincossq 11188 |
| [Gleason] p. 311 | Equation 18 | cosbnd 11193 sinbnd 11192 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 11092 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 7 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1390 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 12623 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1366 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1367 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1369 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6300 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8223 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7126 df-imp 7125 df-iplp 7124 df-reap 8149 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7318 |
| [HoTT], p. | Corollary 11.4.3 | conventions 12356 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 7532 caucvgpr 7338 caucvgprpr 7368 caucvgsr 7444 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7122 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4148 ltpopr 7251 ltsopr 7252 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8180 reapcotr 8172 reapirr 8151 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 7707 gt0add 8147 leadd1 8005 lelttr 7670 lemul1a 8416 lenlt 7658 ltadd1 8004 ltletr 7671 ltmul1 8166 reaplt 8162 |
| [Jech] p. 4 | Definition of class | cv 1295 cvjust 2090 |
| [Jech] p. 78 | Note | opthprc 4518 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1475 |
| [Kreyszig] p. 3 | Property M1 | metcl 12139 xmetcl 12138 |
| [Kreyszig] p. 4 | Property M2 | meteq0 12146 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8234 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 12228 |
| [Kreyszig] p. 19 | Remark | mopntopon 12229 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 12274 mopnm 12234 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 12272 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 12277 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 12295 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 12064 |
| [Kunen] p. 10 | Axiom 0 | a9e 1638 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 3977 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6457 mapvalg 6455 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6451 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3762 |
| [Levy] p. 338 | Axiom | df-clab 2082 df-clel 2091 df-cleq 2088 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1366 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1367 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1369 |
| [Margaris] p. 40 | Rule C | exlimiv 1541 |
| [Margaris] p. 49 | Axiom A1 | ax-1 5 |
| [Margaris] p. 49 | Axiom A2 | ax-2 6 |
| [Margaris] p. 49 | Axiom A3 | condc 790 |
| [Margaris] p. 49 | Definition | dfbi2 381 dfordc 832 exalim 1443 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | mth8 617 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1581 r19.2m 3388 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1498 19.3h 1497 rr19.3v 2769 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1419 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1562 alexim 1588 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1440 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1534 spsbe 1777 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1587 19.9h 1586 19.9v 1806 exlimd 1540 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1606 excomim 1605 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1607 r19.12 2491 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1589 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1409 ralbi 2515 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1499 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1500 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1547 rexbi 2516 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1608 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1398 alimd 1466 alimdh 1408 alimdv 1814 ralimdaa 2452 ralimdv 2454 ralimdva 2453 sbcimdv 2918 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1609 19.21 1527 19.21bi 1502 19.21h 1501 19.21ht 1525 19.21t 1526 19.21v 1808 alrimd 1553 alrimdd 1552 alrimdh 1420 alrimdv 1811 alrimi 1467 alrimih 1410 alrimiv 1809 alrimivv 1810 r19.21 2461 r19.21be 2476 r19.21bi 2473 r19.21t 2460 r19.21v 2462 ralrimd 2463 ralrimdv 2464 ralrimdva 2465 ralrimdvv 2469 ralrimdvva 2470 ralrimi 2456 ralrimiv 2457 ralrimiva 2458 ralrimivv 2466 ralrimivva 2467 ralrimivvva 2468 ralrimivw 2459 rexlimi 2495 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1816 2eximdv 1817 exim 1542 eximd 1555 eximdh 1554 eximdv 1815 rexim 2479 reximdai 2483 reximddv 2488 reximddv2 2490 reximdv 2486 reximdv2 2484 reximdva 2487 reximdvai 2485 reximi2 2481 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1620 19.23bi 1535 19.23h 1439 19.23ht 1438 19.23t 1619 19.23v 1818 19.23vv 1819 exlimd2 1538 exlimdh 1539 exlimdv 1754 exlimdvv 1832 exlimi 1537 exlimih 1536 exlimiv 1541 exlimivv 1831 r19.23 2493 r19.23v 2494 rexlimd 2499 rexlimdv 2501 rexlimdv3a 2504 rexlimdva 2502 rexlimdva2 2505 rexlimdvaa 2503 rexlimdvv 2509 rexlimdvva 2510 rexlimdvw 2506 rexlimiv 2496 rexlimiva 2497 rexlimivv 2508 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1582 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1569 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1423 19.26-3an 1424 19.26 1422 r19.26-2 2512 r19.26-3 2513 r19.26 2511 r19.26m 2514 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1505 19.27h 1504 19.27v 1834 r19.27av 2518 r19.27m 3397 r19.27mv 3398 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1507 19.28h 1506 19.28v 1835 r19.28av 2519 r19.28m 3391 r19.28mv 3394 rr19.28v 2770 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1563 19.29r 1564 19.29r2 1565 19.29x 1566 r19.29 2520 r19.29d2r 2526 r19.29r 2521 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1570 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1623 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1621 19.32r 1622 r19.32r 2528 r19.32vdc 2530 r19.32vr 2529 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1425 19.33b2 1572 19.33bdc 1573 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1626 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1567 19.35i 1568 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1615 19.36aiv 1836 19.36i 1614 r19.36av 2532 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1616 19.37aiv 1617 r19.37 2533 r19.37av 2534 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1618 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1583 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1575 19.40 1574 r19.40 2535 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1628 19.41h 1627 19.41v 1837 19.41vv 1838 19.41vvv 1839 19.41vvvv 1840 r19.41 2536 r19.41v 2537 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1630 19.42h 1629 19.42v 1841 19.42vv 1843 19.42vvv 1844 19.42vvvv 1845 r19.42v 2538 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1571 r19.43 2539 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1624 r19.44av 2540 r19.44mv 3396 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1625 r19.45av 2541 r19.45mv 3395 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 1980 |
| [Megill] p. 444 | Axiom C5 | ax-17 1471 |
| [Megill] p. 445 | Lemma L12 | alequcom 1460 ax-10 1448 |
| [Megill] p. 446 | Lemma L17 | equtrr 1650 |
| [Megill] p. 446 | Lemma L19 | hbnae 1663 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1700 sbid 1711 |
| [Megill] p. 448 | Scheme C5' | ax-4 1452 |
| [Megill] p. 448 | Scheme C6' | ax-7 1389 |
| [Megill] p. 448 | Scheme C8' | ax-8 1447 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1450 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1658 |
| [Megill] p. 448 | Scheme C12' | ax-13 1456 |
| [Megill] p. 448 | Scheme C13' | ax-14 1457 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1758 |
| [Megill] p. 448 | Scheme C16' | ax-16 1749 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1672 dral2 1673 drex1 1733 drex2 1674 drsb1 1734 drsb2 1776 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 1918 sbequ 1775 sbid2v 1927 |
| [Megill] p. 450 | Example in Appendix | hba1 1485 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 2935 rspsbca 2936 stdpc4 1712 |
| [Mendelson] p. 69 | Axiom 5 | ra5 2941 stdpc5 1528 |
| [Mendelson] p. 81 | Rule C | exlimiv 1541 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1643 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1707 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3338 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3339 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3255 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3303 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3256 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3146 |
| [Mendelson] p. 231 | Definition of union | unssin 3254 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4326 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3674 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4133 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4134 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4135 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3695 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4596 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 4985 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4222 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 6641 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6617 xpsneng 6618 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6623 xpcomeng 6624 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6626 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6620 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6449 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6608 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 6646 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6483 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6609 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6268 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3237 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4555 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4556 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 3922 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 4980 coi2 4981 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4681 rn0 4721 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 4869 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4576 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4687 rnxpm 4894 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4547 xp0 4884 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 4824 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 4821 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 4820 imaexg 4819 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 4818 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5468 funfvop 5450 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5383 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5391 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5092 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5585 dff13f 5587 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5559 funrnex 5923 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5579 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 4948 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3726 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 5964 df-1st 5949 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 5965 df-2nd 5950 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1388 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1447 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1449 ax-11o 1758 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1762 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1389 |
| [Monk2] p. 109 | Lemma 15 | equvin 1798 equvini 1695 eqvinop 4094 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1471 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1593 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1389 |
| [Monk2] p. 114 | Lemma 22 | hba1 1485 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1496 nfia1 1524 |
| [Monk2] p. 114 | Lemma 24 | hba2 1495 nfa2 1523 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 779 dftest 863 |
| [Munkres] p. 77 | Example 2 | distop 11937 |
| [Munkres] p. 78 | Definition of basis | df-bases 11893 isbasis3g 11896 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 11825 tgval2 11903 |
| [Munkres] p. 79 | Remark | tgcl 11916 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 11910 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 11931 tgss3 11930 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 11932 basgen2 11933 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 12022 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 11964 topcld 11961 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 11965 |
| [Munkres] p. 94 | Definition of closure | clsval 11963 |
| [Munkres] p. 94 | Definition of interior | ntrval 11962 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 12040 iscn 12048 iscn2 12051 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 12081 cncnp2m 12082 cncnpi 12079 df-cnp 12041 iscnp 12050 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 12296 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 6699 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 6896 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3125 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 6877 exmidomniim 6884 finomni 6883 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 6878 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 12618 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 6704 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 6924 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 6925 exmidfodomrlemrALT 6926 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 6892 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 12602 peano4nninf 12601 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 12605 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 12614 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 12616 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 12600 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2082 rabid 2556 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 1922 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2088 |
| [Quine] p. 19 | Definition 2.9 | df-v 2635 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2203 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2215 abid2f 2260 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1822 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1820 sb6 1821 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2091 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2095 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2097 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 2855 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 2856 dfsbcq2 2857 |
| [Quine] p. 43 | Theorem 6.8 | vex 2636 |
| [Quine] p. 43 | Theorem 6.9 | isset 2639 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2715 spcgv 2720 spcimgf 2713 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 2865 spsbcd 2866 |
| [Quine] p. 44 | Theorem 6.12 | elex 2644 |
| [Quine] p. 44 | Theorem 6.13 | elab 2774 elabg 2775 elabgf 2772 |
| [Quine] p. 44 | Theorem 6.14 | noel 3306 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3527 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3473 df-sn 3472 |
| [Quine] p. 49 | Theorem 7.4 | snss 3588 snssg 3595 |
| [Quine] p. 49 | Theorem 7.5 | prss 3615 prssg 3616 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3568 prid1g 3566 prid2 3569 prid2g 3567 snid 3495 snidg 3493 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4040 snexprc 4042 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4062 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3691 unisng 3692 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3694 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3703 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3702 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5024 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5015 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5025 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5029 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5030 |
| [Quine] p. 58 | Definition 9.1 | df-op 3475 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4108 opelopab 4122 opelopaba 4117 opelopabaf 4124 opelopabf 4125 opelopabg 4119 opelopabga 4114 oprabid 5719 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4473 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4475 |
| [Quine] p. 64 | Definition 9.15 | df-id 4144 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5106 |
| [Quine] p. 65 | Theorem 10.4 | funi 5080 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5096 funsng 5094 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5051 |
| [Quine] p. 65 | Definition 10.2 | args 4834 dffv4g 5337 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5057 fv2 5335 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10247 nn0opth2d 10246 nn0opthd 10245 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5133 funimaexg 5132 |
| [Rudin] p. 164 | Equation 27 | efcan 11115 |
| [Rudin] p. 164 | Equation 30 | efzval 11122 |
| [Rudin] p. 167 | Equation 48 | absefi 11207 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1369 |
| [Sanford] p. 39 | Rule 4 | mptxor 1367 |
| [Sanford] p. 40 | Rule 1 | mptnan 1366 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 4849 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 4851 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 4848 |
| [Schechter] p. 51 | Definition of transitivity | cotr 4846 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 11935 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3280 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3373 dif0 3372 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3386 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3273 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3274 |
| [Stoll] p. 20 | Remark | invdif 3257 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3476 |
| [Stoll] p. 43 | Definition | uniiun 3805 |
| [Stoll] p. 44 | Definition | intiin 3806 |
| [Stoll] p. 45 | Definition | df-iin 3755 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3754 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 827 imanst 782 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3280 |
| [Suppes] p. 22 | Theorem 2 | eq0 3320 |
| [Suppes] p. 22 | Theorem 4 | eqss 3054 eqssd 3056 eqssi 3055 |
| [Suppes] p. 23 | Theorem 5 | ss0 3342 ss0b 3341 |
| [Suppes] p. 23 | Theorem 6 | sstr 3047 |
| [Suppes] p. 25 | Theorem 12 | elin 3198 elun 3156 |
| [Suppes] p. 26 | Theorem 15 | inidm 3224 |
| [Suppes] p. 26 | Theorem 16 | in0 3336 |
| [Suppes] p. 27 | Theorem 23 | unidm 3158 |
| [Suppes] p. 27 | Theorem 24 | un0 3335 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3178 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3185 |
| [Suppes] p. 27 | Theorem 27 | unss 3189 |
| [Suppes] p. 27 | Theorem 28 | indir 3264 |
| [Suppes] p. 27 | Theorem 29 | undir 3265 |
| [Suppes] p. 28 | Theorem 32 | difid 3370 difidALT 3371 |
| [Suppes] p. 29 | Theorem 33 | difin 3252 |
| [Suppes] p. 29 | Theorem 34 | indif 3258 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3376 |
| [Suppes] p. 29 | Theorem 36 | difun2 3381 |
| [Suppes] p. 29 | Theorem 37 | difin0 3375 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3374 |
| [Suppes] p. 29 | Theorem 39 | difundi 3267 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3269 |
| [Suppes] p. 30 | Theorem 41 | nalset 3990 |
| [Suppes] p. 39 | Theorem 61 | uniss 3696 |
| [Suppes] p. 39 | Theorem 65 | uniop 4106 |
| [Suppes] p. 41 | Theorem 70 | intsn 3745 |
| [Suppes] p. 42 | Theorem 71 | intpr 3742 intprg 3743 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4328 op1stbg 4329 |
| [Suppes] p. 42 | Theorem 78 | intun 3741 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3786 dfiun2g 3784 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3787 |
| [Suppes] p. 47 | Theorem 86 | elpw 3455 elpw2 4014 elpw2g 4013 elpwg 3457 |
| [Suppes] p. 47 | Theorem 87 | pwid 3464 |
| [Suppes] p. 47 | Theorem 89 | pw0 3606 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3670 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4574 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4602 xpindir 4603 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4523 xpundir 4524 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4392 |
| [Suppes] p. 58 | Theorem 2 | relss 4554 |
| [Suppes] p. 59 | Theorem 4 | eldm 4664 eldm2 4665 eldm2g 4663 eldmg 4662 |
| [Suppes] p. 59 | Definition 3 | df-dm 4477 |
| [Suppes] p. 60 | Theorem 6 | dmin 4675 |
| [Suppes] p. 60 | Theorem 8 | rnun 4873 |
| [Suppes] p. 60 | Theorem 9 | rnin 4874 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4655 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4650 brcnvg 4648 |
| [Suppes] p. 62 | Equation 5 | elcnv 4644 elcnv2 4645 |
| [Suppes] p. 62 | Theorem 12 | relcnv 4843 |
| [Suppes] p. 62 | Theorem 15 | cnvin 4872 |
| [Suppes] p. 62 | Theorem 16 | cnvun 4870 |
| [Suppes] p. 63 | Theorem 20 | co02 4978 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4734 |
| [Suppes] p. 63 | Definition 7 | df-co 4476 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4652 |
| [Suppes] p. 64 | Theorem 27 | coass 4983 |
| [Suppes] p. 65 | Theorem 31 | resundi 4758 |
| [Suppes] p. 65 | Theorem 34 | elima 4812 elima2 4813 elima3 4814 elimag 4811 |
| [Suppes] p. 65 | Theorem 35 | imaundi 4877 |
| [Suppes] p. 66 | Theorem 40 | dminss 4879 |
| [Suppes] p. 66 | Theorem 41 | imainss 4880 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 4883 |
| [Suppes] p. 81 | Definition 34 | dfec2 6335 |
| [Suppes] p. 82 | Theorem 72 | elec 6371 elecg 6370 |
| [Suppes] p. 82 | Theorem 73 | erth 6376 erth2 6377 |
| [Suppes] p. 89 | Theorem 96 | map0b 6484 |
| [Suppes] p. 89 | Theorem 97 | map0 6486 map0g 6485 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6487 |
| [Suppes] p. 89 | Theorem 99 | mapss 6488 |
| [Suppes] p. 92 | Theorem 1 | enref 6562 enrefg 6561 |
| [Suppes] p. 92 | Theorem 2 | ensym 6578 ensymb 6577 ensymi 6579 |
| [Suppes] p. 92 | Theorem 3 | entr 6581 |
| [Suppes] p. 92 | Theorem 4 | unen 6613 |
| [Suppes] p. 94 | Theorem 15 | endom 6560 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6575 |
| [Suppes] p. 94 | Theorem 17 | domtr 6582 |
| [Suppes] p. 95 | Theorem 18 | isbth 6756 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6603 fundmeng 6604 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6630 |
| [Suppes] p. 130 | Definition 3 | df-tr 3959 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4333 |
| [Suppes] p. 134 | Definition 6 | df-suc 4222 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4446 finds 4443 finds1 4445 finds2 4444 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7009 df-ltpq 7002 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4241 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2077 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2088 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2091 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2090 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2112 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5694 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2853 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3487 elpr2 3488 elprg 3486 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3482 elsn2 3498 elsn2g 3497 elsng 3481 velsn 3483 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4082 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3477 sneqr 3626 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3485 dfsn2 3480 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4288 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4088 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4066 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4291 unexg 4293 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3511 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3676 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3019 df-un 3017 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3689 uniprg 3690 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4035 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3510 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4257 elsucg 4255 sstr2 3046 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3159 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3207 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3172 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3225 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3262 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3263 |
| [TakeutiZaring] p. 17 | Definition 5.9 | dfss2 3028 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3451 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3186 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3026 sseqin2 3234 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3059 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3235 inss2 3236 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3099 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3684 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4067 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4074 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2379 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 3987 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3015 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3304 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3370 difidALT 3371 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3314 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4383 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2635 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 3992 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3340 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 3997 ssexg 3999 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 3994 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4394 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4385 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3366 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3140 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3276 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3141 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3149 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2375 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2376 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4582 xpexg 4581 xpexgALT 5942 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4474 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5112 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5262 fun11 5115 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5060 svrelfun 5113 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4654 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4656 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4479 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4480 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4476 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 4919 dfrel2 4915 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4575 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4584 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4590 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4601 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4773 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4750 opelresg 4752 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4766 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4769 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4774 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5089 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 4963 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5088 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5263 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 1999 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5057 fv3 5363 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5003 cnvexg 5002 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4731 dmexg 4729 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4732 rnexg 4730 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5357 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5366 tz6.12 5367 tz6.12c 5369 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5331 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5052 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5053 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5055 wfo 5047 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5054 wf1 5046 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5056 wf1o 5048 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5436 eqfnfv2 5437 eqfnfv2f 5440 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5409 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5558 fnexALT 5922 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5557 resfunexgALT 5919 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5133 funimaexg 5132 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 3868 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 4835 iniseg 4837 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4140 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5058 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5627 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5628 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5633 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5635 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5643 |
| [TakeutiZaring] p. 35 | Notation | wtr 3958 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4205 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 3962 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4419 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4232 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4236 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4337 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4219 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4331 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4396 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4425 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 3960 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4356 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4332 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3703 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4222 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4266 sucidg 4267 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 4346 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4220 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4351 ordelsuc 4350 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4437 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4438 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4439 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4436 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4449 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4442 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4440 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4441 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3724 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 3974 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3725 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4362 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3711 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6111 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6168 tfri1d 6138 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6169 tfri2d 6139 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6170 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6105 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6089 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6265 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6261 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6258 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6262 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6308 nnaordi 6307 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3797 uniss2 3706 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6271 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6281 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6272 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6259 omsuc 6273 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6282 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6316 nnmordi 6315 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6260 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 6912 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6592 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6653 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6654 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6540 isfi 6558 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6627 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6447 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 6644 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1452 |
| [Tarski] p. 68 | Lemma 6 | equid 1641 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1644 |
| [Tarski] p. 70 | Lemma 14 | spim 1680 spime 1683 spimeh 1681 spimh 1679 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1449 ax-11o 1758 ax11i 1656 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1821 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1471 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 1456 ax-14 1457 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 670 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 684 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 711 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 720 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 741 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 584 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 5 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 610 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 786 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2053 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 694 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 785 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 597 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 820 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 792 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 794 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 609 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 790 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 791 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 671 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 730 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 585 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 589 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 833 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 854 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 723 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 724 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 756 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 757 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 755 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 928 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 733 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 731 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 732 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 695 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 696 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 804 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 800 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 697 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 698 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 699 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 619 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 620 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 679 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 831 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 682 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 683 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 803 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 705 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 752 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 753 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 623 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 672 pm2.67 700 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 805 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 704 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 762 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 834 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 862 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 758 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 759 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 761 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 760 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 6 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 763 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 764 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 852 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 100 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 709 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 138 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 906 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 907 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 908 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 708 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 261 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 262 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 665 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 340 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 258 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 259 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 108 simplimdc 798 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 109 simprimdc 797 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 338 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 339 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 829 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 565 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 327 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 325 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 326 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 710 pm3.44 673 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | prth 337 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 570 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 737 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 806 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 170 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 807 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 828 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 830 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 139 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 901 bitr 457 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 388 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 712 pm4.25 713 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 263 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 770 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 685 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 394 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 722 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 455 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 744 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 573 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 774 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 929 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 768 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 920 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 898 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 734 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 766 pm4.45 736 pm4.45im 328 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1422 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 837 imorr 838 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 313 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 840 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 844 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 845 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 846 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 887 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 707 pm4.56 847 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 888 oranim 848 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 823 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 839 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 821 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 842 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 824 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 843 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 822 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 382 pm4.71d 386 pm4.71i 384 pm4.71r 383 pm4.71rd 387 pm4.71ri 385 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 775 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 295 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 701 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 571 pm4.76 572 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 669 pm4.77 751 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 849 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 850 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 661 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 855 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 899 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 900 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 235 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 239 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 247 impexp 260 pm4.87 525 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 569 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 856 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 857 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 859 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 858 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1332 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 776 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 851 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1337 pm5.18dc 818 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 660 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 649 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1335 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1340 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1341 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 835 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 460 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 248 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 241 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 876 pm5.6r 877 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 903 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 341 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 442 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 577 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 867 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 578 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 249 pm5.41 250 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 314 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 875 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 754 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 868 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 860 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 746 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 894 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 895 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 910 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 243 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 178 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 911 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1578 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1426 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1575 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1830 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 1958 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2343 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2344 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2768 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 2909 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5032 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5033 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2034 eupickbi 2037 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5057 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 6915 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |