Bibliographic Cross-Reference for the Intuitionistic Logic
Explorer
Bibliographic Reference |
Description | Intuitionistic Logic Explorer Page(s)
|
---|
[AczelRathjen], p.
71 | Definition 8.1.4 | enumct 7104 fidcenum 6945 |
[AczelRathjen], p.
72 | Proposition 8.1.11 | fidcenum 6945 |
[AczelRathjen], p.
73 | Lemma 8.1.14 | enumct 7104 |
[AczelRathjen], p.
73 | Corollary 8.1.13 | ennnfone 12391 |
[AczelRathjen], p.
74 | Lemma 8.1.16 | xpfi 6919 |
[AczelRathjen], p.
74 | Remark 8.1.17 | unfiexmid 6907 |
[AczelRathjen], p.
74 | Theorem 8.1.19 | ctiunct 12406 |
[AczelRathjen], p.
75 | Corollary 8.1.20 | unct 12408 |
[AczelRathjen], p.
75 | Corollary 8.1.23 | qnnen 12397 znnen 12364 |
[AczelRathjen], p.
77 | Lemma 8.1.27 | omctfn 12409 |
[AczelRathjen], p.
78 | Theorem 8.1.28 | omiunct 12410 |
[AczelRathjen], p.
80 | Corollary 8.2.4 | df-ihash 10722 |
[AczelRathjen], p.
183 | Chapter 20 | ax-setind 4530 |
[Apostol] p. 18 | Theorem
I.1 | addcan 8111 addcan2d 8116 addcan2i 8114 addcand 8115 addcani 8113 |
[Apostol] p. 18 | Theorem
I.2 | negeu 8122 |
[Apostol] p. 18 | Theorem
I.3 | negsub 8179 negsubd 8248 negsubi 8209 |
[Apostol] p. 18 | Theorem
I.4 | negneg 8181 negnegd 8233 negnegi 8201 |
[Apostol] p. 18 | Theorem
I.5 | subdi 8316 subdid 8345 subdii 8338 subdir 8317 subdird 8346 subdiri 8339 |
[Apostol] p. 18 | Theorem
I.6 | mul01 8320 mul01d 8324 mul01i 8322 mul02 8318 mul02d 8323 mul02i 8321 |
[Apostol] p. 18 | Theorem
I.9 | divrecapd 8722 |
[Apostol] p. 18 | Theorem
I.10 | recrecapi 8673 |
[Apostol] p. 18 | Theorem
I.12 | mul2neg 8329 mul2negd 8344 mul2negi 8337 mulneg1 8326 mulneg1d 8342 mulneg1i 8335 |
[Apostol] p. 18 | Theorem
I.15 | divdivdivap 8642 |
[Apostol] p. 20 | Axiom
7 | rpaddcl 9646 rpaddcld 9681 rpmulcl 9647 rpmulcld 9682 |
[Apostol] p. 20 | Axiom
9 | 0nrp 9658 |
[Apostol] p. 20 | Theorem
I.17 | lttri 8036 |
[Apostol] p. 20 | Theorem
I.18 | ltadd1d 8469 ltadd1dd 8487 ltadd1i 8433 |
[Apostol] p. 20 | Theorem
I.19 | ltmul1 8523 ltmul1a 8522 ltmul1i 8848 ltmul1ii 8856 ltmul2 8784 ltmul2d 9708 ltmul2dd 9722 ltmul2i 8851 |
[Apostol] p. 20 | Theorem
I.21 | 0lt1 8058 |
[Apostol] p. 20 | Theorem
I.23 | lt0neg1 8399 lt0neg1d 8446 ltneg 8393 ltnegd 8454 ltnegi 8424 |
[Apostol] p. 20 | Theorem
I.25 | lt2add 8376 lt2addd 8498 lt2addi 8441 |
[Apostol] p.
20 | Definition of positive numbers | df-rp 9623 |
[Apostol] p. 21 | Exercise
4 | recgt0 8778 recgt0d 8862 recgt0i 8834 recgt0ii 8835 |
[Apostol] p.
22 | Definition of integers | df-z 9225 |
[Apostol] p.
22 | Definition of rationals | df-q 9591 |
[Apostol] p. 24 | Theorem
I.26 | supeuti 6983 |
[Apostol] p. 26 | Theorem
I.29 | arch 9144 |
[Apostol] p. 28 | Exercise
2 | btwnz 9343 |
[Apostol] p. 28 | Exercise
3 | nnrecl 9145 |
[Apostol] p. 28 | Exercise
6 | qbtwnre 10225 |
[Apostol] p. 28 | Exercise
10(a) | zeneo 11841 zneo 9325 |
[Apostol] p. 29 | Theorem
I.35 | resqrtth 11006 sqrtthi 11094 |
[Apostol] p. 34 | Theorem
I.36 (principle of mathematical induction) | peano5nni 8893 |
[Apostol] p. 34 | Theorem
I.37 (well-ordering principle) | nnwodc 12002 |
[Apostol] p.
363 | Remark | absgt0api 11121 |
[Apostol] p.
363 | Example | abssubd 11168 abssubi 11125 |
[ApostolNT] p.
14 | Definition | df-dvds 11761 |
[ApostolNT] p.
14 | Theorem 1.1(a) | iddvds 11777 |
[ApostolNT] p.
14 | Theorem 1.1(b) | dvdstr 11801 |
[ApostolNT] p.
14 | Theorem 1.1(c) | dvds2ln 11797 |
[ApostolNT] p.
14 | Theorem 1.1(d) | dvdscmul 11791 |
[ApostolNT] p.
14 | Theorem 1.1(e) | dvdscmulr 11793 |
[ApostolNT] p.
14 | Theorem 1.1(f) | 1dvds 11778 |
[ApostolNT] p.
14 | Theorem 1.1(g) | dvds0 11779 |
[ApostolNT] p.
14 | Theorem 1.1(h) | 0dvds 11784 |
[ApostolNT] p.
14 | Theorem 1.1(i) | dvdsleabs 11816 |
[ApostolNT] p.
14 | Theorem 1.1(j) | dvdsabseq 11818 |
[ApostolNT] p.
14 | Theorem 1.1(k) | divconjdvds 11820 |
[ApostolNT] p.
15 | Definition | dfgcd2 11980 |
[ApostolNT] p.
16 | Definition | isprm2 12082 |
[ApostolNT] p.
16 | Theorem 1.5 | coprmdvds 12057 |
[ApostolNT] p.
16 | Theorem 1.7 | prminf 12421 |
[ApostolNT] p.
16 | Theorem 1.4(a) | gcdcom 11939 |
[ApostolNT] p.
16 | Theorem 1.4(b) | gcdass 11981 |
[ApostolNT] p.
16 | Theorem 1.4(c) | absmulgcd 11983 |
[ApostolNT] p.
16 | Theorem 1.4(d)1 | gcd1 11953 |
[ApostolNT] p.
16 | Theorem 1.4(d)2 | gcdid0 11946 |
[ApostolNT] p.
17 | Theorem 1.8 | coprm 12109 |
[ApostolNT] p.
17 | Theorem 1.9 | euclemma 12111 |
[ApostolNT] p.
17 | Theorem 1.10 | 1arith2 12331 |
[ApostolNT] p.
19 | Theorem 1.14 | divalg 11894 |
[ApostolNT] p.
20 | Theorem 1.15 | eucalg 12024 |
[ApostolNT] p.
25 | Definition | df-phi 12176 |
[ApostolNT] p.
26 | Theorem 2.2 | phisum 12205 |
[ApostolNT] p.
28 | Theorem 2.5(a) | phiprmpw 12187 |
[ApostolNT] p.
28 | Theorem 2.5(c) | phimul 12191 |
[ApostolNT] p.
104 | Definition | congr 12065 |
[ApostolNT] p.
106 | Remark | dvdsval3 11764 |
[ApostolNT] p.
106 | Definition | moddvds 11772 |
[ApostolNT] p.
107 | Example 2 | mod2eq0even 11848 |
[ApostolNT] p.
107 | Example 3 | mod2eq1n2dvds 11849 |
[ApostolNT] p.
107 | Example 4 | zmod1congr 10309 |
[ApostolNT] p.
107 | Theorem 5.2(b) | modqmul12d 10346 |
[ApostolNT] p.
107 | Theorem 5.2(c) | modqexp 10614 |
[ApostolNT] p.
108 | Theorem 5.3 | modmulconst 11796 |
[ApostolNT] p.
109 | Theorem 5.4 | cncongr1 12068 |
[ApostolNT] p.
109 | Theorem 5.4 "Cancellation law" | cncongr 12070 |
[ApostolNT] p.
113 | Theorem 5.17 | eulerth 12198 |
[ApostolNT] p.
113 | Theorem 5.18 | vfermltl 12216 |
[ApostolNT] p.
114 | Theorem 5.19 | fermltl 12199 |
[ApostolNT] p.
179 | Definition | df-lgs 13950 lgsprme0 13994 |
[ApostolNT] p.
180 | Example 1 | 1lgs 13995 |
[ApostolNT] p.
180 | Theorem 9.2 | lgsvalmod 13971 |
[ApostolNT] p.
180 | Theorem 9.3 | lgsdirprm 13986 |
[ApostolNT] p.
188 | Definition | df-lgs 13950 lgs1 13996 |
[ApostolNT] p.
188 | Theorem 9.9(a) | lgsdir 13987 |
[ApostolNT] p.
188 | Theorem 9.9(b) | lgsdi 13989 |
[ApostolNT] p.
188 | Theorem 9.9(c) | lgsmodeq 13997 |
[ApostolNT] p.
188 | Theorem 9.9(d) | lgsmulsqcoprm 13998 |
[Bauer] p. 482 | Section
1.2 | pm2.01 616 pm2.65 659 |
[Bauer] p. 483 | Theorem
1.3 | acexmid 5864 onsucelsucexmidlem 4522 |
[Bauer], p.
481 | Section 1.1 | pwtrufal 14287 |
[Bauer], p.
483 | Definition | n0rf 3433 |
[Bauer], p. 483 | Theorem
1.2 | 2irrexpq 13945 2irrexpqap 13947 |
[Bauer], p. 485 | Theorem
2.1 | ssfiexmid 6866 |
[Bauer], p. 494 | Theorem
5.5 | ivthinc 13672 |
[BauerHanson], p.
27 | Proposition 5.2 | cnstab 8576 |
[BauerSwan], p.
14 | Remark | 0ct 7096 ctm 7098 |
[BauerSwan],
p. 14 | Proposition 2.6 | subctctexmid 14291 |
[BauerSwan], p.
14 | Table" is defined as ` ` per | enumct 7104 |
[BauerTaylor], p.
32 | Lemma 6.16 | prarloclem 7475 |
[BauerTaylor], p.
50 | Lemma 11.4 | subhalfnqq 7388 |
[BauerTaylor], p.
52 | Proposition 11.15 | prarloc 7477 |
[BauerTaylor], p.
53 | Lemma 11.16 | addclpr 7511 addlocpr 7510 |
[BauerTaylor], p.
55 | Proposition 12.7 | appdivnq 7537 |
[BauerTaylor], p.
56 | Lemma 12.8 | prmuloc 7540 |
[BauerTaylor], p.
56 | Lemma 12.9 | mullocpr 7545 |
[BellMachover] p.
36 | Lemma 10.3 | idALT 20 |
[BellMachover] p.
97 | Definition 10.1 | df-eu 2027 |
[BellMachover] p.
460 | Notation | df-mo 2028 |
[BellMachover] p.
460 | Definition | mo3 2078 mo3h 2077 |
[BellMachover] p.
462 | Theorem 1.1 | bm1.1 2160 |
[BellMachover] p.
463 | Theorem 1.3ii | bm1.3ii 4119 |
[BellMachover] p.
466 | Axiom Pow | axpow3 4172 |
[BellMachover] p.
466 | Axiom Union | axun2 4429 |
[BellMachover] p.
469 | Theorem 2.2(i) | ordirr 4535 |
[BellMachover] p.
469 | Theorem 2.2(iii) | onelon 4378 |
[BellMachover] p.
469 | Theorem 2.2(vii) | ordn2lp 4538 |
[BellMachover] p.
471 | Problem 2.5(ii) | bm2.5ii 4489 |
[BellMachover] p.
471 | Definition of Lim | df-ilim 4363 |
[BellMachover] p.
472 | Axiom Inf | zfinf2 4582 |
[BellMachover] p.
473 | Theorem 2.8 | limom 4607 |
[Bobzien] p.
116 | Statement T3 | stoic3 1429 |
[Bobzien] p.
117 | Statement T2 | stoic2a 1427 |
[Bobzien] p.
117 | Statement T4 | stoic4a 1430 |
[BourbakiAlg1] p.
1 | Definition 1 | df-mgm 12639 |
[BourbakiAlg1] p.
4 | Definition 5 | df-sgrp 12672 |
[BourbakiAlg1] p.
12 | Definition 2 | df-mnd 12682 |
[BourbakiAlg1] p.
92 | Definition 1 | df-ring 12974 |
[BourbakiEns] p.
| Proposition 8 | fcof1 5774 fcofo 5775 |
[BourbakiTop1] p.
| Remark | xnegmnf 9798 xnegpnf 9797 |
[BourbakiTop1] p.
| Remark | rexneg 9799 |
[BourbakiTop1] p.
| Proposition | ishmeo 13355 |
[BourbakiTop1] p.
| Property V_i | ssnei2 13208 |
[BourbakiTop1] p.
| Property V_ii | innei 13214 |
[BourbakiTop1] p.
| Property V_iv | neissex 13216 |
[BourbakiTop1] p.
| Proposition 1 | neipsm 13205 neiss 13201 |
[BourbakiTop1] p.
| Proposition 2 | cnptopco 13273 |
[BourbakiTop1] p.
| Proposition 4 | imasnopn 13350 |
[BourbakiTop1] p.
| Property V_iii | elnei 13203 |
[BourbakiTop1] p.
| Definition is due to Bourbaki (Def. 1 | df-top 13047 |
[Bruck] p. 1 | Section
I.1 | df-mgm 12639 |
[Bruck] p. 23 | Section
II.1 | df-sgrp 12672 |
[Bruck] p. 28 | Theorem
3.2 | dfgrp3m 12828 |
[ChoquetDD] p.
2 | Definition of mapping | df-mpt 4061 |
[Cohen] p.
301 | Remark | relogoprlem 13840 |
[Cohen] p. 301 | Property
2 | relogmul 13841 relogmuld 13856 |
[Cohen] p. 301 | Property
3 | relogdiv 13842 relogdivd 13857 |
[Cohen] p. 301 | Property
4 | relogexp 13844 |
[Cohen] p. 301 | Property
1a | log1 13838 |
[Cohen] p. 301 | Property
1b | loge 13839 |
[Cohen4] p.
348 | Observation | relogbcxpbap 13934 |
[Cohen4] p.
352 | Definition | rpelogb 13918 |
[Cohen4] p. 361 | Property
2 | rprelogbmul 13924 |
[Cohen4] p. 361 | Property
3 | logbrec 13929 rprelogbdiv 13926 |
[Cohen4] p. 361 | Property
4 | rplogbreexp 13922 |
[Cohen4] p. 361 | Property
6 | relogbexpap 13927 |
[Cohen4] p. 361 | Property
1(a) | rplogbid1 13916 |
[Cohen4] p. 361 | Property
1(b) | rplogb1 13917 |
[Cohen4] p.
367 | Property | rplogbchbase 13919 |
[Cohen4] p. 377 | Property
2 | logblt 13931 |
[Crosilla] p. | Axiom
1 | ax-ext 2157 |
[Crosilla] p. | Axiom
2 | ax-pr 4203 |
[Crosilla] p. | Axiom
3 | ax-un 4427 |
[Crosilla] p. | Axiom
4 | ax-nul 4124 |
[Crosilla] p. | Axiom
5 | ax-iinf 4581 |
[Crosilla] p. | Axiom
6 | ru 2959 |
[Crosilla] p. | Axiom
8 | ax-pow 4169 |
[Crosilla] p. | Axiom
9 | ax-setind 4530 |
[Crosilla], p. | Axiom
6 | ax-sep 4116 |
[Crosilla], p. | Axiom
7 | ax-coll 4113 |
[Crosilla], p. | Axiom
7' | repizf 4114 |
[Crosilla], p. | Theorem
is stated | ordtriexmid 4514 |
[Crosilla], p. | Axiom
of choice implies instances | acexmid 5864 |
[Crosilla], p.
| Definition of ordinal | df-iord 4360 |
[Crosilla], p. | Theorem
"Foundation implies instances of EM" | regexmid 4528 |
[Eisenberg] p.
67 | Definition 5.3 | df-dif 3129 |
[Eisenberg] p.
82 | Definition 6.3 | df-iom 4584 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 6640 |
[Enderton] p. 18 | Axiom
of Empty Set | axnul 4123 |
[Enderton] p.
19 | Definition | df-tp 3597 |
[Enderton] p.
26 | Exercise 5 | unissb 3835 |
[Enderton] p.
26 | Exercise 10 | pwel 4212 |
[Enderton] p.
28 | Exercise 7(b) | pwunim 4280 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1m 3951 iinin2m 3950 iunin1 3946 iunin2 3945 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2m 3949 iundif2ss 3947 |
[Enderton] p.
33 | Exercise 23 | iinuniss 3964 |
[Enderton] p.
33 | Exercise 25 | iununir 3965 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 3972 |
[Enderton] p.
33 | Exercise 24(b) | iunpw 4474 iunpwss 3973 |
[Enderton] p.
38 | Exercise 6(a) | unipw 4211 |
[Enderton] p.
38 | Exercise 6(b) | pwuni 4187 |
[Enderton] p. 41 | Lemma
3D | opeluu 4444 rnex 4887
rnexg 4885 |
[Enderton] p.
41 | Exercise 8 | dmuni 4830 rnuni 5032 |
[Enderton] p.
42 | Definition of a function | dffun7 5235 dffun8 5236 |
[Enderton] p.
43 | Definition of function value | funfvdm2 5572 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 5269 |
[Enderton] p.
44 | Definition (d) | dfima2 4965 dfima3 4966 |
[Enderton] p.
47 | Theorem 3H | fvco2 5577 |
[Enderton] p. 49 | Axiom
of Choice (first form) | df-ac 7195 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 5752 |
[Enderton] p.
52 | Definition | df-map 6640 |
[Enderton] p.
53 | Exercise 21 | coass 5139 |
[Enderton] p.
53 | Exercise 27 | dmco 5129 |
[Enderton] p.
53 | Exercise 14(a) | funin 5279 |
[Enderton] p.
53 | Exercise 22(a) | imass2 4997 |
[Enderton] p.
54 | Remark | ixpf 6710 ixpssmap 6722 |
[Enderton] p.
54 | Definition of infinite Cartesian product | df-ixp 6689 |
[Enderton] p.
56 | Theorem 3M | erref 6545 |
[Enderton] p. 57 | Lemma
3N | erthi 6571 |
[Enderton] p.
57 | Definition | df-ec 6527 |
[Enderton] p.
58 | Definition | df-qs 6531 |
[Enderton] p.
60 | Theorem 3Q | th3q 6630 th3qcor 6629 th3qlem1 6627 th3qlem2 6628 |
[Enderton] p.
61 | Exercise 35 | df-ec 6527 |
[Enderton] p.
65 | Exercise 56(a) | dmun 4827 |
[Enderton] p.
68 | Definition of successor | df-suc 4365 |
[Enderton] p.
71 | Definition | df-tr 4097 dftr4 4101 |
[Enderton] p.
72 | Theorem 4E | unisuc 4407 unisucg 4408 |
[Enderton] p.
73 | Exercise 6 | unisuc 4407 unisucg 4408 |
[Enderton] p.
73 | Exercise 5(a) | truni 4110 |
[Enderton] p.
73 | Exercise 5(b) | trint 4111 |
[Enderton] p.
79 | Theorem 4I(A1) | nna0 6465 |
[Enderton] p.
79 | Theorem 4I(A2) | nnasuc 6467 onasuc 6457 |
[Enderton] p.
79 | Definition of operation value | df-ov 5868 |
[Enderton] p.
80 | Theorem 4J(A1) | nnm0 6466 |
[Enderton] p.
80 | Theorem 4J(A2) | nnmsuc 6468 onmsuc 6464 |
[Enderton] p.
81 | Theorem 4K(1) | nnaass 6476 |
[Enderton] p.
81 | Theorem 4K(2) | nna0r 6469 nnacom 6475 |
[Enderton] p.
81 | Theorem 4K(3) | nndi 6477 |
[Enderton] p.
81 | Theorem 4K(4) | nnmass 6478 |
[Enderton] p.
81 | Theorem 4K(5) | nnmcom 6480 |
[Enderton] p.
82 | Exercise 16 | nnm0r 6470 nnmsucr 6479 |
[Enderton] p.
88 | Exercise 23 | nnaordex 6519 |
[Enderton] p.
129 | Definition | df-en 6731 |
[Enderton] p.
132 | Theorem 6B(b) | canth 5819 |
[Enderton] p.
133 | Exercise 1 | xpomen 12361 |
[Enderton] p.
134 | Theorem (Pigeonhole Principle) | phpm 6855 |
[Enderton] p.
136 | Corollary 6E | nneneq 6847 |
[Enderton] p.
139 | Theorem 6H(c) | mapen 6836 |
[Enderton] p.
142 | Theorem 6I(3) | xpdjuen 7207 |
[Enderton] p.
143 | Theorem 6J | dju0en 7203 dju1en 7202 |
[Enderton] p.
144 | Corollary 6K | undif2ss 3496 |
[Enderton] p.
145 | Figure 38 | ffoss 5485 |
[Enderton] p.
145 | Definition | df-dom 6732 |
[Enderton] p.
146 | Example 1 | domen 6741 domeng 6742 |
[Enderton] p.
146 | Example 3 | nndomo 6854 |
[Enderton] p.
149 | Theorem 6L(c) | xpdom1 6825 xpdom1g 6823 xpdom2g 6822 |
[Enderton] p.
168 | Definition | df-po 4290 |
[Enderton] p.
192 | Theorem 7M(a) | oneli 4422 |
[Enderton] p.
192 | Theorem 7M(b) | ontr1 4383 |
[Enderton] p.
192 | Theorem 7M(c) | onirri 4536 |
[Enderton] p.
193 | Corollary 7N(b) | 0elon 4386 |
[Enderton] p.
193 | Corollary 7N(c) | onsuci 4509 |
[Enderton] p.
193 | Corollary 7N(d) | ssonunii 4482 |
[Enderton] p.
194 | Remark | onprc 4545 |
[Enderton] p.
194 | Exercise 16 | suc11 4551 |
[Enderton] p.
197 | Definition | df-card 7169 |
[Enderton] p.
200 | Exercise 25 | tfis 4576 |
[Enderton] p.
206 | Theorem 7X(b) | en2lp 4547 |
[Enderton] p.
207 | Exercise 34 | opthreg 4549 |
[Enderton] p.
208 | Exercise 35 | suc11g 4550 |
[Geuvers], p.
1 | Remark | expap0 10518 |
[Geuvers], p. 6 | Lemma
2.13 | mulap0r 8546 |
[Geuvers], p. 6 | Lemma
2.15 | mulap0 8584 |
[Geuvers], p. 9 | Lemma
2.35 | msqge0 8547 |
[Geuvers], p.
9 | Definition 3.1(2) | ax-arch 7905 |
[Geuvers], p. 10 | Lemma
3.9 | maxcom 11178 |
[Geuvers], p. 10 | Lemma
3.10 | maxle1 11186 maxle2 11187 |
[Geuvers], p. 10 | Lemma
3.11 | maxleast 11188 |
[Geuvers], p. 10 | Lemma
3.12 | maxleb 11191 |
[Geuvers], p.
11 | Definition 3.13 | dfabsmax 11192 |
[Geuvers], p.
17 | Definition 6.1 | df-ap 8513 |
[Gleason] p.
117 | Proposition 9-2.1 | df-enq 7321 enqer 7332 |
[Gleason] p.
117 | Proposition 9-2.2 | df-1nqqs 7325 df-nqqs 7322 |
[Gleason] p.
117 | Proposition 9-2.3 | df-plpq 7318 df-plqqs 7323 |
[Gleason] p.
119 | Proposition 9-2.4 | df-mpq 7319 df-mqqs 7324 |
[Gleason] p.
119 | Proposition 9-2.5 | df-rq 7326 |
[Gleason] p.
119 | Proposition 9-2.6 | ltexnqq 7382 |
[Gleason] p.
120 | Proposition 9-2.6(i) | halfnq 7385 ltbtwnnq 7390 ltbtwnnqq 7389 |
[Gleason] p.
120 | Proposition 9-2.6(ii) | ltanqg 7374 |
[Gleason] p.
120 | Proposition 9-2.6(iii) | ltmnqg 7375 |
[Gleason] p.
123 | Proposition 9-3.5 | addclpr 7511 |
[Gleason] p.
123 | Proposition 9-3.5(i) | addassprg 7553 |
[Gleason] p.
123 | Proposition 9-3.5(ii) | addcomprg 7552 |
[Gleason] p.
123 | Proposition 9-3.5(iii) | ltaddpr 7571 |
[Gleason] p.
123 | Proposition 9-3.5(iv) | ltexpri 7587 |
[Gleason] p.
123 | Proposition 9-3.5(v) | ltaprg 7593 ltaprlem 7592 |
[Gleason] p.
123 | Proposition 9-3.5(vi) | addcanprg 7590 |
[Gleason] p.
124 | Proposition 9-3.7 | mulclpr 7546 |
[Gleason] p. 124 | Theorem
9-3.7(iv) | 1idpr 7566 |
[Gleason] p.
124 | Proposition 9-3.7(i) | mulassprg 7555 |
[Gleason] p.
124 | Proposition 9-3.7(ii) | mulcomprg 7554 |
[Gleason] p.
124 | Proposition 9-3.7(iii) | distrprg 7562 |
[Gleason] p.
124 | Proposition 9-3.7(v) | recexpr 7612 |
[Gleason] p.
126 | Proposition 9-4.1 | df-enr 7700 enrer 7709 |
[Gleason] p.
126 | Proposition 9-4.2 | df-0r 7705 df-1r 7706 df-nr 7701 |
[Gleason] p.
126 | Proposition 9-4.3 | df-mr 7703 df-plr 7702 negexsr 7746 recexsrlem 7748 |
[Gleason] p.
127 | Proposition 9-4.4 | df-ltr 7704 |
[Gleason] p.
130 | Proposition 10-1.3 | creui 8888 creur 8887 cru 8533 |
[Gleason] p.
130 | Definition 10-1.1(v) | ax-cnre 7897 axcnre 7855 |
[Gleason] p.
132 | Definition 10-3.1 | crim 10833 crimd 10952 crimi 10912 crre 10832 crred 10951 crrei 10911 |
[Gleason] p.
132 | Definition 10-3.2 | remim 10835 remimd 10917 |
[Gleason] p.
133 | Definition 10.36 | absval2 11032 absval2d 11160 absval2i 11119 |
[Gleason] p.
133 | Proposition 10-3.4(a) | cjadd 10859 cjaddd 10940 cjaddi 10907 |
[Gleason] p.
133 | Proposition 10-3.4(c) | cjmul 10860 cjmuld 10941 cjmuli 10908 |
[Gleason] p.
133 | Proposition 10-3.4(e) | cjcj 10858 cjcjd 10918 cjcji 10890 |
[Gleason] p.
133 | Proposition 10-3.4(f) | cjre 10857 cjreb 10841 cjrebd 10921 cjrebi 10893 cjred 10946 rere 10840 rereb 10838 rerebd 10920 rerebi 10892 rered 10944 |
[Gleason] p.
133 | Proposition 10-3.4(h) | addcj 10866 addcjd 10932 addcji 10902 |
[Gleason] p.
133 | Proposition 10-3.7(a) | absval 10976 |
[Gleason] p.
133 | Proposition 10-3.7(b) | abscj 11027 abscjd 11165 abscji 11123 |
[Gleason] p.
133 | Proposition 10-3.7(c) | abs00 11039 abs00d 11161 abs00i 11120 absne0d 11162 |
[Gleason] p.
133 | Proposition 10-3.7(d) | releabs 11071 releabsd 11166 releabsi 11124 |
[Gleason] p.
133 | Proposition 10-3.7(f) | absmul 11044 absmuld 11169 absmuli 11126 |
[Gleason] p.
133 | Proposition 10-3.7(g) | sqabsadd 11030 sqabsaddi 11127 |
[Gleason] p.
133 | Proposition 10-3.7(h) | abstri 11079 abstrid 11171 abstrii 11130 |
[Gleason] p.
134 | Definition 10-4.1 | df-exp 10488 exp0 10492 expp1 10495 expp1d 10622 |
[Gleason] p.
135 | Proposition 10-4.2(a) | expadd 10530 expaddd 10623 |
[Gleason] p.
135 | Proposition 10-4.2(b) | cxpmul 13884 cxpmuld 13907 expmul 10533 expmuld 10624 |
[Gleason] p.
135 | Proposition 10-4.2(c) | mulexp 10527 mulexpd 10636 rpmulcxp 13881 |
[Gleason] p.
141 | Definition 11-2.1 | fzval 9979 |
[Gleason] p.
168 | Proposition 12-2.1(a) | climadd 11300 |
[Gleason] p.
168 | Proposition 12-2.1(b) | climsub 11302 |
[Gleason] p.
168 | Proposition 12-2.1(c) | climmul 11301 |
[Gleason] p.
171 | Corollary 12-2.2 | climmulc2 11305 |
[Gleason] p.
172 | Corollary 12-2.5 | climrecl 11298 |
[Gleason] p.
172 | Proposition 12-2.4(c) | climabs 11294 climcj 11295 climim 11297 climre 11296 |
[Gleason] p.
173 | Definition 12-3.1 | df-ltxr 7971 df-xr 7970 ltxr 9744 |
[Gleason] p. 180 | Theorem
12-5.3 | climcau 11321 |
[Gleason] p. 217 | Lemma
13-4.1 | btwnzge0 10268 |
[Gleason] p.
223 | Definition 14-1.1 | df-met 13040 |
[Gleason] p.
223 | Definition 14-1.1(a) | met0 13415 xmet0 13414 |
[Gleason] p.
223 | Definition 14-1.1(c) | metsym 13422 |
[Gleason] p.
223 | Definition 14-1.1(d) | mettri 13424 mstri 13524 xmettri 13423 xmstri 13523 |
[Gleason] p.
230 | Proposition 14-2.6 | txlm 13330 |
[Gleason] p.
240 | Proposition 14-4.2 | metcnp3 13562 |
[Gleason] p.
243 | Proposition 14-4.16 | addcn2 11284 addcncntop 13603 mulcn2 11286 mulcncntop 13605 subcn2 11285 subcncntop 13604 |
[Gleason] p.
295 | Remark | bcval3 10697 bcval4 10698 |
[Gleason] p.
295 | Equation 2 | bcpasc 10712 |
[Gleason] p.
295 | Definition of binomial coefficient | bcval 10695 df-bc 10694 |
[Gleason] p.
296 | Remark | bcn0 10701 bcnn 10703 |
[Gleason] p. 296 | Theorem
15-2.8 | binom 11458 |
[Gleason] p.
308 | Equation 2 | ef0 11646 |
[Gleason] p.
308 | Equation 3 | efcj 11647 |
[Gleason] p.
309 | Corollary 15-4.3 | efne0 11652 |
[Gleason] p.
309 | Corollary 15-4.4 | efexp 11656 |
[Gleason] p.
310 | Equation 14 | sinadd 11710 |
[Gleason] p.
310 | Equation 15 | cosadd 11711 |
[Gleason] p.
311 | Equation 17 | sincossq 11722 |
[Gleason] p.
311 | Equation 18 | cosbnd 11727 sinbnd 11726 |
[Gleason] p.
311 | Definition of ` ` | df-pi 11627 |
[Golan] p.
1 | Remark | srgisid 12962 |
[Golan] p.
1 | Definition | df-srg 12940 |
[Hamilton] p.
31 | Example 2.7(a) | idALT 20 |
[Hamilton] p. 73 | Rule
1 | ax-mp 5 |
[Hamilton] p. 74 | Rule
2 | ax-gen 1447 |
[Herstein] p. 55 | Lemma
2.2.1(a) | grpideu 12748 mndideu 12691 |
[Herstein] p. 55 | Lemma
2.2.1(b) | grpinveu 12771 |
[Herstein] p. 55 | Lemma
2.2.1(c) | grpinvinv 12796 |
[Herstein] p. 55 | Lemma
2.2.1(d) | grpinvadd 12807 |
[Herstein] p.
57 | Exercise 1 | dfgrp3me 12829 |
[Heyting] p.
127 | Axiom #1 | ax1hfs 14360 |
[Hitchcock] p. 5 | Rule
A3 | mptnan 1423 |
[Hitchcock] p. 5 | Rule
A4 | mptxor 1424 |
[Hitchcock] p. 5 | Rule
A5 | mtpxor 1426 |
[HoTT], p. | Lemma
10.4.1 | exmidontriim 7214 |
[HoTT], p. | Theorem
7.2.6 | nndceq 6490 |
[HoTT], p.
| Exercise 11.10 | neapmkv 14356 |
[HoTT], p. | Exercise
11.11 | mulap0bd 8587 |
[HoTT], p. | Section
11.2.1 | df-iltp 7444 df-imp 7443 df-iplp 7442 df-reap 8506 |
[HoTT], p. | Theorem
11.2.12 | cauappcvgpr 7636 |
[HoTT], p. | Corollary
11.4.3 | conventions 14013 |
[HoTT], p.
| Exercise 11.6(i) | dcapnconst 14349 dceqnconst 14348 |
[HoTT], p. | Corollary
11.2.13 | axcaucvg 7874 caucvgpr 7656 caucvgprpr 7686 caucvgsr 7776 |
[HoTT], p. | Definition
11.2.1 | df-inp 7440 |
[HoTT], p.
| Exercise 11.6(ii) | nconstwlpo 14354 |
[HoTT], p. | Proposition
11.2.3 | df-iso 4291 ltpopr 7569 ltsopr 7570 |
[HoTT], p. | Definition
11.2.7(v) | apsym 8537 reapcotr 8529 reapirr 8508 |
[HoTT], p. | Definition
11.2.7(vi) | 0lt1 8058 gt0add 8504 leadd1 8361 lelttr 8020 lemul1a 8786 lenlt 8007 ltadd1 8360 ltletr 8021 ltmul1 8523 reaplt 8519 |
[Jech] p. 4 | Definition of
class | cv 1352 cvjust 2170 |
[Jech] p.
78 | Note | opthprc 4671 |
[KalishMontague] p.
81 | Note 1 | ax-i9 1528 |
[Kreyszig] p.
3 | Property M1 | metcl 13404 xmetcl 13403 |
[Kreyszig] p.
4 | Property M2 | meteq0 13411 |
[Kreyszig] p.
12 | Equation 5 | muleqadd 8598 |
[Kreyszig] p.
18 | Definition 1.3-2 | mopnval 13493 |
[Kreyszig] p.
19 | Remark | mopntopon 13494 |
[Kreyszig] p.
19 | Theorem T1 | mopn0 13539 mopnm 13499 |
[Kreyszig] p.
19 | Theorem T2 | unimopn 13537 |
[Kreyszig] p.
19 | Definition of neighborhood | neibl 13542 |
[Kreyszig] p.
20 | Definition 1.3-3 | metcnp2 13564 |
[Kreyszig] p.
25 | Definition 1.4-1 | lmbr 13264 |
[Kunen] p. 10 | Axiom
0 | a9e 1694 |
[Kunen] p. 12 | Axiom
6 | zfrep6 4115 |
[Kunen] p. 24 | Definition
10.24 | mapval 6650 mapvalg 6648 |
[Kunen] p. 31 | Definition
10.24 | mapex 6644 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 3892 |
[Lang] p.
3 | Statement | lidrideqd 12664 mndbn0 12696 |
[Lang] p.
3 | Definition | df-mnd 12682 |
[Lang] p.
7 | Definition | dfgrp2e 12763 |
[Levy] p.
338 | Axiom | df-clab 2162 df-clel 2171 df-cleq 2168 |
[Lopez-Astorga] p.
12 | Rule 1 | mptnan 1423 |
[Lopez-Astorga] p.
12 | Rule 2 | mptxor 1424 |
[Lopez-Astorga] p.
12 | Rule 3 | mtpxor 1426 |
[Margaris] p. 40 | Rule
C | exlimiv 1596 |
[Margaris] p. 49 | Axiom
A1 | ax-1 6 |
[Margaris] p. 49 | Axiom
A2 | ax-2 7 |
[Margaris] p. 49 | Axiom
A3 | condc 853 |
[Margaris] p.
49 | Definition | dfbi2 388 dfordc 892 exalim 1500 |
[Margaris] p.
51 | Theorem 1 | idALT 20 |
[Margaris] p.
56 | Theorem 3 | syld 45 |
[Margaris] p.
60 | Theorem 8 | jcn 651 |
[Margaris] p.
89 | Theorem 19.2 | 19.2 1636 r19.2m 3507 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 1552 19.3h 1551 rr19.3v 2874 |
[Margaris] p.
89 | Theorem 19.5 | alcom 1476 |
[Margaris] p.
89 | Theorem 19.6 | alexdc 1617 alexim 1643 |
[Margaris] p.
89 | Theorem 19.7 | alnex 1497 |
[Margaris] p.
89 | Theorem 19.8 | 19.8a 1588 spsbe 1840 |
[Margaris] p.
89 | Theorem 19.9 | 19.9 1642 19.9h 1641 19.9v 1869 exlimd 1595 |
[Margaris] p.
89 | Theorem 19.11 | excom 1662 excomim 1661 |
[Margaris] p.
89 | Theorem 19.12 | 19.12 1663 r19.12 2581 |
[Margaris] p.
90 | Theorem 19.14 | exnalim 1644 |
[Margaris] p.
90 | Theorem 19.15 | albi 1466 ralbi 2607 |
[Margaris] p.
90 | Theorem 19.16 | 19.16 1553 |
[Margaris] p.
90 | Theorem 19.17 | 19.17 1554 |
[Margaris] p.
90 | Theorem 19.18 | exbi 1602 rexbi 2608 |
[Margaris] p.
90 | Theorem 19.19 | 19.19 1664 |
[Margaris] p.
90 | Theorem 19.20 | alim 1455 alimd 1519 alimdh 1465 alimdv 1877 ralimdaa 2541 ralimdv 2543 ralimdva 2542 ralimdvva 2544 sbcimdv 3026 |
[Margaris] p.
90 | Theorem 19.21 | 19.21-2 1665 19.21 1581 19.21bi 1556 19.21h 1555 19.21ht 1579 19.21t 1580 19.21v 1871 alrimd 1608 alrimdd 1607 alrimdh 1477 alrimdv 1874 alrimi 1520 alrimih 1467 alrimiv 1872 alrimivv 1873 r19.21 2551 r19.21be 2566 r19.21bi 2563 r19.21t 2550 r19.21v 2552 ralrimd 2553 ralrimdv 2554 ralrimdva 2555 ralrimdvv 2559 ralrimdvva 2560 ralrimi 2546 ralrimiv 2547 ralrimiva 2548 ralrimivv 2556 ralrimivva 2557 ralrimivvva 2558 ralrimivw 2549 rexlimi 2585 |
[Margaris] p.
90 | Theorem 19.22 | 2alimdv 1879 2eximdv 1880 exim 1597
eximd 1610 eximdh 1609 eximdv 1878 rexim 2569 reximdai 2573 reximddv 2578 reximddv2 2580 reximdv 2576 reximdv2 2574 reximdva 2577 reximdvai 2575 reximi2 2571 |
[Margaris] p.
90 | Theorem 19.23 | 19.23 1676 19.23bi 1590 19.23h 1496 19.23ht 1495 19.23t 1675 19.23v 1881 19.23vv 1882 exlimd2 1593 exlimdh 1594 exlimdv 1817 exlimdvv 1895 exlimi 1592 exlimih 1591 exlimiv 1596 exlimivv 1894 r19.23 2583 r19.23v 2584 rexlimd 2589 rexlimdv 2591 rexlimdv3a 2594 rexlimdva 2592 rexlimdva2 2595 rexlimdvaa 2593 rexlimdvv 2599 rexlimdvva 2600 rexlimdvw 2596 rexlimiv 2586 rexlimiva 2587 rexlimivv 2598 |
[Margaris] p.
90 | Theorem 19.24 | i19.24 1637 |
[Margaris] p.
90 | Theorem 19.25 | 19.25 1624 |
[Margaris] p.
90 | Theorem 19.26 | 19.26-2 1480 19.26-3an 1481 19.26 1479 r19.26-2 2604 r19.26-3 2605 r19.26 2601 r19.26m 2606 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 1559 19.27h 1558 19.27v 1897 r19.27av 2610 r19.27m 3516 r19.27mv 3517 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 1561 19.28h 1560 19.28v 1898 r19.28av 2611 r19.28m 3510 r19.28mv 3513 rr19.28v 2875 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1618 19.29r 1619 19.29r2 1620 19.29x 1621 r19.29 2612 r19.29d2r 2619 r19.29r 2613 |
[Margaris] p.
90 | Theorem 19.30 | 19.30dc 1625 |
[Margaris] p.
90 | Theorem 19.31 | 19.31r 1679 |
[Margaris] p.
90 | Theorem 19.32 | 19.32dc 1677 19.32r 1678 r19.32r 2621 r19.32vdc 2624 r19.32vr 2623 |
[Margaris] p.
90 | Theorem 19.33 | 19.33 1482 19.33b2 1627 19.33bdc 1628 |
[Margaris] p.
90 | Theorem 19.34 | 19.34 1682 |
[Margaris] p.
90 | Theorem 19.35 | 19.35-1 1622 19.35i 1623 |
[Margaris] p.
90 | Theorem 19.36 | 19.36-1 1671 19.36aiv 1899 19.36i 1670 r19.36av 2626 |
[Margaris] p.
90 | Theorem 19.37 | 19.37-1 1672 19.37aiv 1673 r19.37 2627 r19.37av 2628 |
[Margaris] p.
90 | Theorem 19.38 | 19.38 1674 |
[Margaris] p.
90 | Theorem 19.39 | i19.39 1638 |
[Margaris] p.
90 | Theorem 19.40 | 19.40-2 1630 19.40 1629 r19.40 2629 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 1684 19.41h 1683 19.41v 1900 19.41vv 1901 19.41vvv 1902 19.41vvvv 1903 r19.41 2630 r19.41v 2631 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 1686 19.42h 1685 19.42v 1904 19.42vv 1909 19.42vvv 1910 19.42vvvv 1911 r19.42v 2632 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1626 r19.43 2633 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 1680 r19.44av 2634 r19.44mv 3515 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 1681 r19.45av 2635 r19.45mv 3514 |
[Margaris] p.
110 | Exercise 2(b) | eu1 2049 |
[Megill] p. 444 | Axiom
C5 | ax-17 1524 |
[Megill] p. 445 | Lemma
L12 | alequcom 1513 ax-10 1503 |
[Megill] p. 446 | Lemma
L17 | equtrr 1708 |
[Megill] p. 446 | Lemma
L19 | hbnae 1719 |
[Megill] p. 447 | Remark
9.1 | df-sb 1761 sbid 1772 |
[Megill] p. 448 | Scheme
C5' | ax-4 1508 |
[Megill] p. 448 | Scheme
C6' | ax-7 1446 |
[Megill] p. 448 | Scheme
C8' | ax-8 1502 |
[Megill] p. 448 | Scheme
C9' | ax-i12 1505 |
[Megill] p. 448 | Scheme
C11' | ax-10o 1714 |
[Megill] p. 448 | Scheme
C12' | ax-13 2148 |
[Megill] p. 448 | Scheme
C13' | ax-14 2149 |
[Megill] p. 448 | Scheme
C15' | ax-11o 1821 |
[Megill] p. 448 | Scheme
C16' | ax-16 1812 |
[Megill] p. 448 | Theorem
9.4 | dral1 1728 dral2 1729 drex1 1796 drex2 1730 drsb1 1797 drsb2 1839 |
[Megill] p. 449 | Theorem
9.7 | sbcom2 1985 sbequ 1838 sbid2v 1994 |
[Megill] p. 450 | Example
in Appendix | hba1 1538 |
[Mendelson] p.
36 | Lemma 1.8 | idALT 20 |
[Mendelson] p.
69 | Axiom 4 | rspsbc 3043 rspsbca 3044 stdpc4 1773 |
[Mendelson] p.
69 | Axiom 5 | ra5 3049 stdpc5 1582 |
[Mendelson] p. 81 | Rule
C | exlimiv 1596 |
[Mendelson] p.
95 | Axiom 6 | stdpc6 1701 |
[Mendelson] p.
95 | Axiom 7 | stdpc7 1768 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 3457 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 3458 |
[Mendelson] p.
231 | Exercise 4.10(n) | inssun 3373 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 3421 |
[Mendelson] p.
231 | Exercise 4.10(q) | inssddif 3374 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddifnel 3264 |
[Mendelson] p.
231 | Definition of union | unssin 3372 |
[Mendelson] p.
235 | Exercise 4.12(c) | univ 4470 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 3804 |
[Mendelson] p.
235 | Exercise 4.12(j) | pwin 4276 |
[Mendelson] p.
235 | Exercise 4.12(k) | pwunss 4277 |
[Mendelson] p.
235 | Exercise 4.12(l) | pwssunim 4278 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 3825 |
[Mendelson] p.
235 | Exercise 4.12(p) | reli 4749 |
[Mendelson] p.
235 | Exercise 4.12(t) | relssdmrn 5141 |
[Mendelson] p.
246 | Definition of successor | df-suc 4365 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 6835 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 6811 xpsneng 6812 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 6817 xpcomeng 6818 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 6820 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 6814 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 6642 |
[Mendelson] p.
255 | Exercise 4.43 | mapsnen 6801 |
[Mendelson] p.
255 | Exercise 4.47 | xpmapen 6840 |
[Mendelson] p.
255 | Exercise 4.42(a) | map0e 6676 |
[Mendelson] p.
255 | Exercise 4.42(b) | map1 6802 |
[Mendelson] p.
258 | Exercise 4.56(c) | djuassen 7206 djucomen 7205 |
[Mendelson] p.
258 | Exercise 4.56(g) | xp2dju 7204 |
[Mendelson] p.
266 | Proposition 4.34(a) | oa1suc 6458 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 3355 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 4708 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 4709 |
[Monk1] p. 34 | Definition
3.3 | df-opab 4060 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5136 coi2 5137 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 4834 rn0 4876 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 5025 |
[Monk1] p. 37 | Theorem
3.13(i) | relxp 4729 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxpm 4840 rnxpm 5050 |
[Monk1] p. 37 | Theorem
3.13(ii) | 0xp 4700 xp0 5040 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 4980 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 4977 |
[Monk1] p. 39 | Theorem
3.17 | imaex 4976 imaexg 4975 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 4974 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 5638 funfvop 5620 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 5551 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 5559 |
[Monk1] p. 43 | Theorem
4.6 | funun 5252 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 5759 dff13f 5761 |
[Monk1] p. 46 | Theorem
4.15(v) | funex 5731 funrnex 6105 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 5753 |
[Monk1] p. 52 | Theorem
5.12(ii) | op2ndb 5104 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 3856 |
[Monk1] p. 52 | Definition
5.13 (i) | 1stval2 6146 df-1st 6131 |
[Monk1] p. 52 | Definition
5.13 (ii) | 2ndval2 6147 df-2nd 6132 |
[Monk2] p. 105 | Axiom
C4 | ax-5 1445 |
[Monk2] p. 105 | Axiom
C7 | ax-8 1502 |
[Monk2] p. 105 | Axiom
C8 | ax-11 1504 ax-11o 1821 |
[Monk2] p. 105 | Axiom
(C8) | ax11v 1825 |
[Monk2] p. 109 | Lemma
12 | ax-7 1446 |
[Monk2] p. 109 | Lemma
15 | equvin 1861 equvini 1756 eqvinop 4237 |
[Monk2] p. 113 | Axiom
C5-1 | ax-17 1524 |
[Monk2] p. 113 | Axiom
C5-2 | ax6b 1649 |
[Monk2] p. 113 | Axiom
C5-3 | ax-7 1446 |
[Monk2] p. 114 | Lemma
22 | hba1 1538 |
[Monk2] p. 114 | Lemma
23 | hbia1 1550 nfia1 1578 |
[Monk2] p. 114 | Lemma
24 | hba2 1549 nfa2 1577 |
[Moschovakis] p.
2 | Chapter 2 | df-stab 831 dftest 14361 |
[Munkres] p. 77 | Example
2 | distop 13136 |
[Munkres] p.
78 | Definition of basis | df-bases 13092 isbasis3g 13095 |
[Munkres] p.
78 | Definition of a topology generated by a basis | df-topgen 12629 tgval2 13102 |
[Munkres] p.
79 | Remark | tgcl 13115 |
[Munkres] p. 80 | Lemma
2.1 | tgval3 13109 |
[Munkres] p. 80 | Lemma
2.2 | tgss2 13130 tgss3 13129 |
[Munkres] p. 81 | Lemma
2.3 | basgen 13131 basgen2 13132 |
[Munkres] p.
89 | Definition of subspace topology | resttop 13221 |
[Munkres] p. 93 | Theorem
6.1(1) | 0cld 13163 topcld 13160 |
[Munkres] p. 93 | Theorem
6.1(3) | uncld 13164 |
[Munkres] p.
94 | Definition of closure | clsval 13162 |
[Munkres] p.
94 | Definition of interior | ntrval 13161 |
[Munkres] p.
102 | Definition of continuous function | df-cn 13239 iscn 13248 iscn2 13251 |
[Munkres] p. 107 | Theorem
7.2(g) | cncnp 13281 cncnp2m 13282 cncnpi 13279 df-cnp 13240 iscnp 13250 |
[Munkres] p. 127 | Theorem
10.1 | metcn 13565 |
[Pierik], p. 8 | Section
2.2.1 | dfrex2fin 6893 |
[Pierik], p. 9 | Definition
2.4 | df-womni 7152 |
[Pierik], p. 9 | Definition
2.5 | df-markov 7140 omniwomnimkv 7155 |
[Pierik], p. 10 | Section
2.3 | dfdif3 3243 |
[Pierik], p.
14 | Definition 3.1 | df-omni 7123 exmidomniim 7129 finomni 7128 |
[Pierik], p. 15 | Section
3.1 | df-nninf 7109 |
[PradicBrown2022], p. 1 | Theorem
1 | exmidsbthr 14312 |
[PradicBrown2022], p.
2 | Remark | exmidpw 6898 |
[PradicBrown2022], p.
2 | Proposition 1.1 | exmidfodomrlemim 7190 |
[PradicBrown2022], p.
2 | Proposition 1.2 | exmidfodomrlemr 7191 exmidfodomrlemrALT 7192 |
[PradicBrown2022], p.
4 | Lemma 3.2 | fodjuomni 7137 |
[PradicBrown2022], p. 5 | Lemma
3.4 | peano3nninf 14297 peano4nninf 14296 |
[PradicBrown2022], p. 5 | Lemma
3.5 | nninfall 14299 |
[PradicBrown2022], p. 5 | Theorem
3.6 | nninfsel 14307 |
[PradicBrown2022], p. 5 | Corollary
3.7 | nninfomni 14309 |
[PradicBrown2022], p. 5 | Definition
3.3 | nnsf 14295 |
[Quine] p. 16 | Definition
2.1 | df-clab 2162 rabid 2650 |
[Quine] p. 17 | Definition
2.1'' | dfsb7 1989 |
[Quine] p. 18 | Definition
2.7 | df-cleq 2168 |
[Quine] p. 19 | Definition
2.9 | df-v 2737 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2284 |
[Quine] p. 35 | Theorem
5.2 | abid2 2296 abid2f 2343 |
[Quine] p. 40 | Theorem
6.1 | sb5 1885 |
[Quine] p. 40 | Theorem
6.2 | sb56 1883 sb6 1884 |
[Quine] p. 41 | Theorem
6.3 | df-clel 2171 |
[Quine] p. 41 | Theorem
6.4 | eqid 2175 |
[Quine] p. 41 | Theorem
6.5 | eqcom 2177 |
[Quine] p. 42 | Theorem
6.6 | df-sbc 2961 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 2962 dfsbcq2 2963 |
[Quine] p. 43 | Theorem
6.8 | vex 2738 |
[Quine] p. 43 | Theorem
6.9 | isset 2741 |
[Quine] p. 44 | Theorem
7.3 | spcgf 2817 spcgv 2822 spcimgf 2815 |
[Quine] p. 44 | Theorem
6.11 | spsbc 2972 spsbcd 2973 |
[Quine] p. 44 | Theorem
6.12 | elex 2746 |
[Quine] p. 44 | Theorem
6.13 | elab 2879 elabg 2881 elabgf 2877 |
[Quine] p. 44 | Theorem
6.14 | noel 3424 |
[Quine] p. 48 | Theorem
7.2 | snprc 3654 |
[Quine] p. 48 | Definition
7.1 | df-pr 3596 df-sn 3595 |
[Quine] p. 49 | Theorem
7.4 | snss 3724 snssg 3723 |
[Quine] p. 49 | Theorem
7.5 | prss 3745 prssg 3746 |
[Quine] p. 49 | Theorem
7.6 | prid1 3695 prid1g 3693 prid2 3696 prid2g 3694 snid 3620
snidg 3618 |
[Quine] p. 51 | Theorem
7.12 | snexg 4179 snexprc 4181 |
[Quine] p. 51 | Theorem
7.13 | prexg 4205 |
[Quine] p. 53 | Theorem
8.2 | unisn 3821 unisng 3822 |
[Quine] p. 53 | Theorem
8.3 | uniun 3824 |
[Quine] p. 54 | Theorem
8.6 | elssuni 3833 |
[Quine] p. 54 | Theorem
8.7 | uni0 3832 |
[Quine] p. 56 | Theorem
8.17 | uniabio 5180 |
[Quine] p. 56 | Definition
8.18 | dfiota2 5171 |
[Quine] p. 57 | Theorem
8.19 | iotaval 5181 |
[Quine] p. 57 | Theorem
8.22 | iotanul 5185 |
[Quine] p. 58 | Theorem
8.23 | euiotaex 5186 |
[Quine] p. 58 | Definition
9.1 | df-op 3598 |
[Quine] p. 61 | Theorem
9.5 | opabid 4251 opelopab 4265 opelopaba 4260 opelopabaf 4267 opelopabf 4268 opelopabg 4262 opelopabga 4257 oprabid 5897 |
[Quine] p. 64 | Definition
9.11 | df-xp 4626 |
[Quine] p. 64 | Definition
9.12 | df-cnv 4628 |
[Quine] p. 64 | Definition
9.15 | df-id 4287 |
[Quine] p. 65 | Theorem
10.3 | fun0 5266 |
[Quine] p. 65 | Theorem
10.4 | funi 5240 |
[Quine] p. 65 | Theorem
10.5 | funsn 5256 funsng 5254 |
[Quine] p. 65 | Definition
10.1 | df-fun 5210 |
[Quine] p. 65 | Definition
10.2 | args 4990 dffv4g 5504 |
[Quine] p. 68 | Definition
10.11 | df-fv 5216 fv2 5502 |
[Quine] p. 124 | Theorem
17.3 | nn0opth2 10670 nn0opth2d 10669 nn0opthd 10668 |
[Quine] p. 284 | Axiom
39(vi) | funimaex 5293 funimaexg 5292 |
[Roman] p. 19 | Part
Preliminaries | df-ring 12974 |
[Rudin] p. 164 | Equation
27 | efcan 11650 |
[Rudin] p. 164 | Equation
30 | efzval 11657 |
[Rudin] p. 167 | Equation
48 | absefi 11742 |
[Sanford] p.
39 | Remark | ax-mp 5 |
[Sanford] p. 39 | Rule
3 | mtpxor 1426 |
[Sanford] p. 39 | Rule
4 | mptxor 1424 |
[Sanford] p. 40 | Rule
1 | mptnan 1423 |
[Schechter] p.
51 | Definition of antisymmetry | intasym 5005 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 5007 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 5004 |
[Schechter] p.
51 | Definition of transitivity | cotr 5002 |
[Schechter] p.
187 | Definition of ring with unit | isring 12976 |
[Schechter] p.
428 | Definition 15.35 | bastop1 13134 |
[Stoll] p. 13 | Definition
of symmetric difference | symdif1 3398 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 3492 dif0 3491 |
[Stoll] p. 16 | Exercise
4.8 | difdifdirss 3505 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 3391 |
[Stoll] p. 19 | Theorem
5.2(13') | indmss 3392 |
[Stoll] p.
20 | Remark | invdif 3375 |
[Stoll] p. 25 | Definition
of ordered triple | df-ot 3599 |
[Stoll] p.
43 | Definition | uniiun 3935 |
[Stoll] p.
44 | Definition | intiin 3936 |
[Stoll] p.
45 | Definition | df-iin 3885 |
[Stoll] p. 45 | Definition
indexed union | df-iun 3884 |
[Stoll] p. 176 | Theorem
3.4(27) | imandc 889 imanst 888 |
[Stoll] p. 262 | Example
4.1 | symdif1 3398 |
[Suppes] p. 22 | Theorem
2 | eq0 3439 |
[Suppes] p. 22 | Theorem
4 | eqss 3168 eqssd 3170 eqssi 3169 |
[Suppes] p. 23 | Theorem
5 | ss0 3461 ss0b 3460 |
[Suppes] p. 23 | Theorem
6 | sstr 3161 |
[Suppes] p. 25 | Theorem
12 | elin 3316 elun 3274 |
[Suppes] p. 26 | Theorem
15 | inidm 3342 |
[Suppes] p. 26 | Theorem
16 | in0 3455 |
[Suppes] p. 27 | Theorem
23 | unidm 3276 |
[Suppes] p. 27 | Theorem
24 | un0 3454 |
[Suppes] p. 27 | Theorem
25 | ssun1 3296 |
[Suppes] p. 27 | Theorem
26 | ssequn1 3303 |
[Suppes] p. 27 | Theorem
27 | unss 3307 |
[Suppes] p. 27 | Theorem
28 | indir 3382 |
[Suppes] p. 27 | Theorem
29 | undir 3383 |
[Suppes] p. 28 | Theorem
32 | difid 3489 difidALT 3490 |
[Suppes] p. 29 | Theorem
33 | difin 3370 |
[Suppes] p. 29 | Theorem
34 | indif 3376 |
[Suppes] p. 29 | Theorem
35 | undif1ss 3495 |
[Suppes] p. 29 | Theorem
36 | difun2 3500 |
[Suppes] p. 29 | Theorem
37 | difin0 3494 |
[Suppes] p. 29 | Theorem
38 | disjdif 3493 |
[Suppes] p. 29 | Theorem
39 | difundi 3385 |
[Suppes] p. 29 | Theorem
40 | difindiss 3387 |
[Suppes] p. 30 | Theorem
41 | nalset 4128 |
[Suppes] p. 39 | Theorem
61 | uniss 3826 |
[Suppes] p. 39 | Theorem
65 | uniop 4249 |
[Suppes] p. 41 | Theorem
70 | intsn 3875 |
[Suppes] p. 42 | Theorem
71 | intpr 3872 intprg 3873 |
[Suppes] p. 42 | Theorem
73 | op1stb 4472 op1stbg 4473 |
[Suppes] p. 42 | Theorem
78 | intun 3871 |
[Suppes] p. 44 | Definition
15(a) | dfiun2 3916 dfiun2g 3914 |
[Suppes] p. 44 | Definition
15(b) | dfiin2 3917 |
[Suppes] p. 47 | Theorem
86 | elpw 3578 elpw2 4152 elpw2g 4151 elpwg 3580 |
[Suppes] p. 47 | Theorem
87 | pwid 3587 |
[Suppes] p. 47 | Theorem
89 | pw0 3736 |
[Suppes] p. 48 | Theorem
90 | pwpw0ss 3800 |
[Suppes] p. 52 | Theorem
101 | xpss12 4727 |
[Suppes] p. 52 | Theorem
102 | xpindi 4755 xpindir 4756 |
[Suppes] p. 52 | Theorem
103 | xpundi 4676 xpundir 4677 |
[Suppes] p. 54 | Theorem
105 | elirrv 4541 |
[Suppes] p. 58 | Theorem
2 | relss 4707 |
[Suppes] p. 59 | Theorem
4 | eldm 4817 eldm2 4818 eldm2g 4816 eldmg 4815 |
[Suppes] p. 59 | Definition
3 | df-dm 4630 |
[Suppes] p. 60 | Theorem
6 | dmin 4828 |
[Suppes] p. 60 | Theorem
8 | rnun 5029 |
[Suppes] p. 60 | Theorem
9 | rnin 5030 |
[Suppes] p. 60 | Definition
4 | dfrn2 4808 |
[Suppes] p. 61 | Theorem
11 | brcnv 4803 brcnvg 4801 |
[Suppes] p. 62 | Equation
5 | elcnv 4797 elcnv2 4798 |
[Suppes] p. 62 | Theorem
12 | relcnv 4999 |
[Suppes] p. 62 | Theorem
15 | cnvin 5028 |
[Suppes] p. 62 | Theorem
16 | cnvun 5026 |
[Suppes] p. 63 | Theorem
20 | co02 5134 |
[Suppes] p. 63 | Theorem
21 | dmcoss 4889 |
[Suppes] p. 63 | Definition
7 | df-co 4629 |
[Suppes] p. 64 | Theorem
26 | cnvco 4805 |
[Suppes] p. 64 | Theorem
27 | coass 5139 |
[Suppes] p. 65 | Theorem
31 | resundi 4913 |
[Suppes] p. 65 | Theorem
34 | elima 4968 elima2 4969 elima3 4970 elimag 4967 |
[Suppes] p. 65 | Theorem
35 | imaundi 5033 |
[Suppes] p. 66 | Theorem
40 | dminss 5035 |
[Suppes] p. 66 | Theorem
41 | imainss 5036 |
[Suppes] p. 67 | Exercise
11 | cnvxp 5039 |
[Suppes] p. 81 | Definition
34 | dfec2 6528 |
[Suppes] p. 82 | Theorem
72 | elec 6564 elecg 6563 |
[Suppes] p. 82 | Theorem
73 | erth 6569 erth2 6570 |
[Suppes] p. 89 | Theorem
96 | map0b 6677 |
[Suppes] p. 89 | Theorem
97 | map0 6679 map0g 6678 |
[Suppes] p. 89 | Theorem
98 | mapsn 6680 |
[Suppes] p. 89 | Theorem
99 | mapss 6681 |
[Suppes] p. 92 | Theorem
1 | enref 6755 enrefg 6754 |
[Suppes] p. 92 | Theorem
2 | ensym 6771 ensymb 6770 ensymi 6772 |
[Suppes] p. 92 | Theorem
3 | entr 6774 |
[Suppes] p. 92 | Theorem
4 | unen 6806 |
[Suppes] p. 94 | Theorem
15 | endom 6753 |
[Suppes] p. 94 | Theorem
16 | ssdomg 6768 |
[Suppes] p. 94 | Theorem
17 | domtr 6775 |
[Suppes] p. 95 | Theorem
18 | isbth 6956 |
[Suppes] p. 98 | Exercise
4 | fundmen 6796 fundmeng 6797 |
[Suppes] p. 98 | Exercise
6 | xpdom3m 6824 |
[Suppes] p.
130 | Definition 3 | df-tr 4097 |
[Suppes] p. 132 | Theorem
9 | ssonuni 4481 |
[Suppes] p.
134 | Definition 6 | df-suc 4365 |
[Suppes] p. 136 | Theorem
Schema 22 | findes 4596 finds 4593 finds1 4595 finds2 4594 |
[Suppes] p.
162 | Definition 5 | df-ltnqqs 7327 df-ltpq 7320 |
[Suppes] p. 228 | Theorem
Schema 61 | onintss 4384 |
[TakeutiZaring] p.
8 | Axiom 1 | ax-ext 2157 |
[TakeutiZaring] p.
13 | Definition 4.5 | df-cleq 2168 |
[TakeutiZaring] p.
13 | Proposition 4.6 | df-clel 2171 |
[TakeutiZaring] p.
13 | Proposition 4.9 | cvjust 2170 |
[TakeutiZaring] p.
13 | Proposition 4.7(3) | eqtr 2193 |
[TakeutiZaring] p.
14 | Definition 4.16 | df-oprab 5869 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 2959 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 3610 elpr2 3611 elprg 3609 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 3605 elsn2 3623 elsn2g 3622 elsng 3604 velsn 3606 |
[TakeutiZaring] p.
15 | Exercise 3 | elop 4225 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 3600 sneqr 3756 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 3608 dfsn2 3603 |
[TakeutiZaring] p.
16 | Axiom 3 | uniex 4431 |
[TakeutiZaring] p.
16 | Exercise 6 | opth 4231 |
[TakeutiZaring] p.
16 | Exercise 8 | rext 4209 |
[TakeutiZaring] p.
16 | Corollary 5.8 | unex 4435 unexg 4437 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 3638 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 3806 |
[TakeutiZaring] p.
16 | Definition 5.6 | df-in 3133 df-un 3131 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 3819 uniprg 3820 |
[TakeutiZaring] p.
17 | Axiom 4 | vpwex 4174 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 3637 |
[TakeutiZaring] p.
17 | Exercise 5 | elsuc 4400 elsucg 4398 sstr2 3160 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3277 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 3325 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3290 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 3343 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 3380 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 3381 |
[TakeutiZaring] p.
17 | Definition 5.9 | dfss2 3142 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 3574 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 3304 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3140 sseqin2 3352 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3173 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 3353 inss2 3354 |
[TakeutiZaring] p.
18 | Exercise 13 | nssr 3213 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 3814 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 4210 |
[TakeutiZaring] p.
18 | Exercise 19 | pweqb 4217 |
[TakeutiZaring] p.
20 | Definition | df-rab 2462 |
[TakeutiZaring] p.
20 | Corollary 5.16 | 0ex 4125 |
[TakeutiZaring] p.
20 | Definition 5.12 | df-dif 3129 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 3422 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 3489 difidALT 3490 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0rf 3433 |
[TakeutiZaring] p.
21 | Theorem 5.22 | setind 4532 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 2737 |
[TakeutiZaring] p.
21 | Proposition 5.21 | vprc 4130 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 3459 |
[TakeutiZaring] p.
22 | Exercise 3 | ssex 4135 ssexg 4137 |
[TakeutiZaring] p.
22 | Exercise 4 | inex1 4132 |
[TakeutiZaring] p.
22 | Exercise 5 | ruv 4543 |
[TakeutiZaring] p.
22 | Exercise 6 | elirr 4534 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0im 3485 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3258 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3ss 3394 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3259 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3267 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 2458 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 2459 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 4735 xpexg 4734 xpexgALT 6124 |
[TakeutiZaring] p.
23 | Definition 6.4(1) | df-rel 4627 |
[TakeutiZaring] p.
23 | Definition 6.4(2) | fun2cnv 5272 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1cnvcnv 5424 fun11 5275 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 5219 svrelfun 5273 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 4807 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 4809 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 4632 |
[TakeutiZaring] p.
24 | Definition 6.6(2) | df-ima 4633 |
[TakeutiZaring] p.
24 | Definition 6.6(3) | df-co 4629 |
[TakeutiZaring] p.
25 | Exercise 2 | cnvcnvss 5075 dfrel2 5071 |
[TakeutiZaring] p.
25 | Exercise 3 | xpss 4728 |
[TakeutiZaring] p.
25 | Exercise 5 | relun 4737 |
[TakeutiZaring] p.
25 | Exercise 6 | reluni 4743 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 4754 |
[TakeutiZaring] p.
25 | Exercise 12 | relres 4928 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 4905 opelresg 4907 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 4921 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 4924 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 4929 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 5249 |
[TakeutiZaring] p.
25 | Exercise 24 | relco 5119 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 5248 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 5425 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2068 |
[TakeutiZaring] p.
26 | Definition 6.11 | df-fv 5216 fv3 5530 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 5159 cnvexg 5158 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 4886 dmexg 4884 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 4887 rnexg 4885 |
[TakeutiZaring] p.
27 | Corollary 6.13 | funfvex 5524 |
[TakeutiZaring] p.
27 | Theorem 6.12(1) | tz6.12-1 5534 tz6.12 5535 tz6.12c 5537 |
[TakeutiZaring] p.
27 | Theorem 6.12(2) | tz6.12-2 5498 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 5211 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 5212 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 5214 wfo 5206 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 5213 wf1 5205 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 5215 wf1o 5207 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 5605 eqfnfv2 5606 eqfnfv2f 5609 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 5578 |
[TakeutiZaring] p.
28 | Theorem 6.16(1) | fnex 5730 fnexALT 6102 |
[TakeutiZaring] p.
28 | Proposition 6.17 | resfunexg 5729 resfunexgALT 6099 |
[TakeutiZaring] p.
29 | Exercise 9 | funimaex 5293 funimaexg 5292 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 3999 |
[TakeutiZaring] p.
30 | Definition 6.21 | eliniseg 4991 iniseg 4993 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 4283 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-isom 5217 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 5801 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 5802 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 5807 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 5809 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 5817 |
[TakeutiZaring] p.
35 | Notation | wtr 4096 |
[TakeutiZaring] p.
35 | Theorem 7.2 | tz7.2 4348 |
[TakeutiZaring] p.
35 | Definition 7.1 | dftr3 4100 |
[TakeutiZaring] p.
36 | Proposition 7.4 | ordwe 4569 |
[TakeutiZaring] p.
36 | Proposition 7.6 | ordelord 4375 |
[TakeutiZaring] p.
37 | Proposition 7.9 | ordin 4379 |
[TakeutiZaring] p.
38 | Corollary 7.15 | ordsson 4485 |
[TakeutiZaring] p.
38 | Definition 7.11 | df-on 4362 |
[TakeutiZaring] p.
38 | Proposition 7.12 | ordon 4479 |
[TakeutiZaring] p.
38 | Proposition 7.13 | onprc 4545 |
[TakeutiZaring] p.
39 | Theorem 7.17 | tfi 4575 |
[TakeutiZaring] p.
40 | Exercise 7 | dftr2 4098 |
[TakeutiZaring] p.
40 | Exercise 11 | unon 4504 |
[TakeutiZaring] p.
40 | Proposition 7.19 | ssorduni 4480 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 3833 |
[TakeutiZaring] p.
41 | Definition 7.22 | df-suc 4365 |
[TakeutiZaring] p.
41 | Proposition 7.23 | sssucid 4409 sucidg 4410 |
[TakeutiZaring] p.
41 | Proposition 7.24 | suceloni 4494 |
[TakeutiZaring] p.
42 | Exercise 1 | df-ilim 4363 |
[TakeutiZaring] p.
42 | Exercise 8 | onsucssi 4499 ordelsuc 4498 |
[TakeutiZaring] p.
42 | Proposition 7.30(1) | peano1 4587 |
[TakeutiZaring] p.
42 | Proposition 7.30(2) | peano2 4588 |
[TakeutiZaring] p.
42 | Proposition 7.30(3) | peano3 4589 |
[TakeutiZaring] p.
43 | Axiom 7 | omex 4586 |
[TakeutiZaring] p.
43 | Theorem 7.32 | ordom 4600 |
[TakeutiZaring] p.
43 | Corollary 7.31 | find 4592 |
[TakeutiZaring] p.
43 | Proposition 7.30(4) | peano4 4590 |
[TakeutiZaring] p.
43 | Proposition 7.30(5) | peano5 4591 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 3854 |
[TakeutiZaring] p.
44 | Exercise 3 | trintssm 4112 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 3855 |
[TakeutiZaring] p.
44 | Exercise 6 | onintonm 4510 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 3841 |
[TakeutiZaring] p.
47 | Lemma 1 | tfrlem1 6299 |
[TakeutiZaring] p.
47 | Theorem 7.41(1) | tfri1 6356 tfri1d 6326 |
[TakeutiZaring] p.
47 | Theorem 7.41(2) | tfri2 6357 tfri2d 6327 |
[TakeutiZaring] p.
47 | Theorem 7.41(3) | tfri3 6358 |
[TakeutiZaring] p.
50 | Exercise 3 | smoiso 6293 |
[TakeutiZaring] p.
50 | Definition 7.46 | df-smo 6277 |
[TakeutiZaring] p.
56 | Definition 8.1 | oasuc 6455 |
[TakeutiZaring] p.
57 | Proposition 8.2 | oacl 6451 |
[TakeutiZaring] p.
57 | Proposition 8.3 | oa0 6448 |
[TakeutiZaring] p.
57 | Proposition 8.16 | omcl 6452 |
[TakeutiZaring] p.
58 | Proposition 8.4 | nnaord 6500 nnaordi 6499 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 3927 uniss2 3836 |
[TakeutiZaring] p.
59 | Proposition 8.7 | oawordriexmid 6461 |
[TakeutiZaring] p.
59 | Proposition 8.9 | nnacl 6471 |
[TakeutiZaring] p.
62 | Exercise 5 | oaword1 6462 |
[TakeutiZaring] p.
62 | Definition 8.15 | om0 6449 omsuc 6463 |
[TakeutiZaring] p.
63 | Proposition 8.17 | nnmcl 6472 |
[TakeutiZaring] p.
63 | Proposition 8.19 | nnmord 6508 nnmordi 6507 |
[TakeutiZaring] p.
67 | Definition 8.30 | oei0 6450 |
[TakeutiZaring] p.
85 | Proposition 10.6(3) | cardonle 7176 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 6785 |
[TakeutiZaring] p.
90 | Proposition 10.20 | nneneq 6847 |
[TakeutiZaring] p.
90 | Corollary 10.21(1) | php5 6848 |
[TakeutiZaring] p.
91 | Definition 10.29 | df-fin 6733 isfi 6751 |
[TakeutiZaring] p.
92 | Proposition 10.33(2) | xpdom2 6821 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 6640 |
[TakeutiZaring] p.
96 | Proposition 10.45 | mapxpen 6838 |
[Tarski] p. 67 | Axiom
B5 | ax-4 1508 |
[Tarski] p. 68 | Lemma
6 | equid 1699 |
[Tarski] p. 69 | Lemma
7 | equcomi 1702 |
[Tarski] p. 70 | Lemma
14 | spim 1736 spime 1739 spimeh 1737 spimh 1735 |
[Tarski] p. 70 | Lemma
16 | ax-11 1504 ax-11o 1821 ax11i 1712 |
[Tarski] p. 70 | Lemmas 16
and 17 | sb6 1884 |
[Tarski] p. 77 | Axiom B6
(p. 75) of system S2 | ax-17 1524 |
[Tarski] p. 77 | Axiom B8
(p. 75) of system S2 | ax-13 2148 ax-14 2149 |
[WhiteheadRussell] p.
96 | Axiom *1.3 | olc 711 |
[WhiteheadRussell] p.
96 | Axiom *1.4 | pm1.4 727 |
[WhiteheadRussell] p.
96 | Axiom *1.2 (Taut) | pm1.2 756 |
[WhiteheadRussell] p.
96 | Axiom *1.5 (Assoc) | pm1.5 765 |
[WhiteheadRussell] p.
97 | Axiom *1.6 (Sum) | orim2 789 |
[WhiteheadRussell] p.
100 | Theorem *2.01 | pm2.01 616 |
[WhiteheadRussell] p.
100 | Theorem *2.02 | ax-1 6 |
[WhiteheadRussell] p.
100 | Theorem *2.03 | con2 643 |
[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 837 |
[WhiteheadRussell] p.
101 | Theorem *2.06 | barbara 2122 syl 14 |
[WhiteheadRussell] p.
101 | Theorem *2.07 | pm2.07 737 |
[WhiteheadRussell] p.
101 | Theorem *2.08 | id 19 idALT 20 |
[WhiteheadRussell] p.
101 | Theorem *2.11 | exmiddc 836 |
[WhiteheadRussell] p.
101 | Theorem *2.12 | notnot 629 |
[WhiteheadRussell] p.
101 | Theorem *2.13 | pm2.13dc 885 |
[WhiteheadRussell] p.
102 | Theorem *2.14 | notnotrdc 843 |
[WhiteheadRussell] p.
102 | Theorem *2.15 | con1dc 856 |
[WhiteheadRussell] p.
103 | Theorem *2.16 | con3 642 |
[WhiteheadRussell] p.
103 | Theorem *2.17 | condc 853 |
[WhiteheadRussell] p.
103 | Theorem *2.18 | pm2.18dc 855 |
[WhiteheadRussell] p.
104 | Theorem *2.2 | orc 712 |
[WhiteheadRussell] p.
104 | Theorem *2.3 | pm2.3 775 |
[WhiteheadRussell] p.
104 | Theorem *2.21 | pm2.21 617 |
[WhiteheadRussell] p.
104 | Theorem *2.24 | pm2.24 621 |
[WhiteheadRussell] p.
104 | Theorem *2.25 | pm2.25dc 893 |
[WhiteheadRussell] p.
104 | Theorem *2.26 | pm2.26dc 907 |
[WhiteheadRussell] p.
104 | Theorem *2.27 | pm2.27 40 |
[WhiteheadRussell] p.
104 | Theorem *2.31 | pm2.31 768 |
[WhiteheadRussell] p.
105 | Theorem *2.32 | pm2.32 769 |
[WhiteheadRussell] p.
105 | Theorem *2.36 | pm2.36 804 |
[WhiteheadRussell] p.
105 | Theorem *2.37 | pm2.37 805 |
[WhiteheadRussell] p.
105 | Theorem *2.38 | pm2.38 803 |
[WhiteheadRussell] p.
105 | Definition *2.33 | df-3or 979 |
[WhiteheadRussell] p.
106 | Theorem *2.4 | pm2.4 778 |
[WhiteheadRussell] p.
106 | Theorem *2.41 | pm2.41 776 |
[WhiteheadRussell] p.
106 | Theorem *2.42 | pm2.42 777 |
[WhiteheadRussell] p.
106 | Theorem *2.43 | pm2.43 53 |
[WhiteheadRussell] p.
106 | Theorem *2.45 | pm2.45 738 |
[WhiteheadRussell] p.
106 | Theorem *2.46 | pm2.46 739 |
[WhiteheadRussell] p.
107 | Theorem *2.5 | pm2.5dc 867 pm2.5gdc 866 |
[WhiteheadRussell] p.
107 | Theorem *2.6 | pm2.6dc 862 |
[WhiteheadRussell] p.
107 | Theorem *2.47 | pm2.47 740 |
[WhiteheadRussell] p.
107 | Theorem *2.48 | pm2.48 741 |
[WhiteheadRussell] p.
107 | Theorem *2.49 | pm2.49 742 |
[WhiteheadRussell] p.
107 | Theorem *2.51 | pm2.51 655 |
[WhiteheadRussell] p.
107 | Theorem *2.52 | pm2.52 656 |
[WhiteheadRussell] p.
107 | Theorem *2.53 | pm2.53 722 |
[WhiteheadRussell] p.
107 | Theorem *2.54 | pm2.54dc 891 |
[WhiteheadRussell] p.
107 | Theorem *2.55 | orel1 725 |
[WhiteheadRussell] p.
107 | Theorem *2.56 | orel2 726 |
[WhiteheadRussell] p.
107 | Theorem *2.61 | pm2.61dc 865 |
[WhiteheadRussell] p.
107 | Theorem *2.62 | pm2.62 748 |
[WhiteheadRussell] p.
107 | Theorem *2.63 | pm2.63 800 |
[WhiteheadRussell] p.
107 | Theorem *2.64 | pm2.64 801 |
[WhiteheadRussell] p.
107 | Theorem *2.65 | pm2.65 659 |
[WhiteheadRussell] p.
107 | Theorem *2.67 | pm2.67-2 713 pm2.67 743 |
[WhiteheadRussell] p.
107 | Theorem *2.521 | pm2.521dc 869 pm2.521gdc 868 |
[WhiteheadRussell] p.
107 | Theorem *2.621 | pm2.621 747 |
[WhiteheadRussell] p.
108 | Theorem *2.8 | pm2.8 810 |
[WhiteheadRussell] p.
108 | Theorem *2.68 | pm2.68dc 894 |
[WhiteheadRussell] p.
108 | Theorem *2.69 | looinvdc 915 |
[WhiteheadRussell] p.
108 | Theorem *2.73 | pm2.73 806 |
[WhiteheadRussell] p.
108 | Theorem *2.74 | pm2.74 807 |
[WhiteheadRussell] p.
108 | Theorem *2.75 | pm2.75 809 |
[WhiteheadRussell] p.
108 | Theorem *2.76 | pm2.76 808 |
[WhiteheadRussell] p.
108 | Theorem *2.77 | ax-2 7 |
[WhiteheadRussell] p.
108 | Theorem *2.81 | pm2.81 811 |
[WhiteheadRussell] p.
108 | Theorem *2.82 | pm2.82 812 |
[WhiteheadRussell] p.
108 | Theorem *2.83 | pm2.83 77 |
[WhiteheadRussell] p.
108 | Theorem *2.85 | pm2.85dc 905 |
[WhiteheadRussell] p.
108 | Theorem *2.86 | pm2.86 101 |
[WhiteheadRussell] p.
111 | Theorem *3.1 | pm3.1 754 |
[WhiteheadRussell] p.
111 | Theorem *3.2 | pm3.2 139 |
[WhiteheadRussell] p.
111 | Theorem *3.11 | pm3.11dc 957 |
[WhiteheadRussell] p.
111 | Theorem *3.12 | pm3.12dc 958 |
[WhiteheadRussell] p.
111 | Theorem *3.13 | pm3.13dc 959 |
[WhiteheadRussell] p.
111 | Theorem *3.14 | pm3.14 753 |
[WhiteheadRussell] p.
111 | Theorem *3.21 | pm3.21 264 |
[WhiteheadRussell] p.
111 | Theorem *3.22 | pm3.22 265 |
[WhiteheadRussell] p.
111 | Theorem *3.24 | pm3.24 693 |
[WhiteheadRussell] p.
112 | Theorem *3.35 | pm3.35 347 |
[WhiteheadRussell] p.
112 | Theorem *3.3 (Exp) | pm3.3 261 |
[WhiteheadRussell] p.
112 | Theorem *3.31 (Imp) | pm3.31 262 |
[WhiteheadRussell] p.
112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 860 |
[WhiteheadRussell] p.
112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 859 |
[WhiteheadRussell] p.
112 | Theorem *3.33 (Syll) | pm3.33 345 |
[WhiteheadRussell] p.
112 | Theorem *3.34 (Syll) | pm3.34 346 |
[WhiteheadRussell] p.
112 | Theorem *3.37 (Transp) | pm3.37 689 |
[WhiteheadRussell] p.
113 | Fact) | pm3.45 597 |
[WhiteheadRussell] p.
113 | Theorem *3.4 | pm3.4 333 |
[WhiteheadRussell] p.
113 | Theorem *3.41 | pm3.41 331 |
[WhiteheadRussell] p.
113 | Theorem *3.42 | pm3.42 332 |
[WhiteheadRussell] p.
113 | Theorem *3.44 | jao 755 pm3.44 715 |
[WhiteheadRussell] p.
113 | Theorem *3.47 | anim12 344 |
[WhiteheadRussell] p.
113 | Theorem *3.43 (Comp) | pm3.43 602 |
[WhiteheadRussell] p.
114 | Theorem *3.48 | pm3.48 785 |
[WhiteheadRussell] p.
116 | Theorem *4.1 | con34bdc 871 |
[WhiteheadRussell] p.
117 | Theorem *4.2 | biid 171 |
[WhiteheadRussell] p.
117 | Theorem *4.13 | notnotbdc 872 |
[WhiteheadRussell] p.
117 | Theorem *4.14 | pm4.14dc 890 |
[WhiteheadRussell] p.
117 | Theorem *4.15 | pm4.15 694 |
[WhiteheadRussell] p.
117 | Theorem *4.21 | bicom 140 |
[WhiteheadRussell] p.
117 | Theorem *4.22 | biantr 952 bitr 472 |
[WhiteheadRussell] p.
117 | Theorem *4.24 | pm4.24 395 |
[WhiteheadRussell] p.
117 | Theorem *4.25 | oridm 757 pm4.25 758 |
[WhiteheadRussell] p.
118 | Theorem *4.3 | ancom 266 |
[WhiteheadRussell] p.
118 | Theorem *4.4 | andi 818 |
[WhiteheadRussell] p.
118 | Theorem *4.31 | orcom 728 |
[WhiteheadRussell] p.
118 | Theorem *4.32 | anass 401 |
[WhiteheadRussell] p.
118 | Theorem *4.33 | orass 767 |
[WhiteheadRussell] p.
118 | Theorem *4.36 | anbi1 466 |
[WhiteheadRussell] p.
118 | Theorem *4.37 | orbi1 792 |
[WhiteheadRussell] p.
118 | Theorem *4.38 | pm4.38 605 |
[WhiteheadRussell] p.
118 | Theorem *4.39 | pm4.39 822 |
[WhiteheadRussell] p.
118 | Definition *4.34 | df-3an 980 |
[WhiteheadRussell] p.
119 | Theorem *4.41 | ordi 816 |
[WhiteheadRussell] p.
119 | Theorem *4.42 | pm4.42r 971 |
[WhiteheadRussell] p.
119 | Theorem *4.43 | pm4.43 949 |
[WhiteheadRussell] p.
119 | Theorem *4.44 | pm4.44 779 |
[WhiteheadRussell] p.
119 | Theorem *4.45 | orabs 814 pm4.45 784 pm4.45im 334 |
[WhiteheadRussell] p.
119 | Theorem *10.22 | 19.26 1479 |
[WhiteheadRussell] p.
120 | Theorem *4.5 | anordc 956 |
[WhiteheadRussell] p.
120 | Theorem *4.6 | imordc 897 imorr 721 |
[WhiteheadRussell] p.
120 | Theorem *4.7 | anclb 319 |
[WhiteheadRussell] p.
120 | Theorem *4.51 | ianordc 899 |
[WhiteheadRussell] p.
120 | Theorem *4.52 | pm4.52im 750 |
[WhiteheadRussell] p.
120 | Theorem *4.53 | pm4.53r 751 |
[WhiteheadRussell] p.
120 | Theorem *4.54 | pm4.54dc 902 |
[WhiteheadRussell] p.
120 | Theorem *4.55 | pm4.55dc 938 |
[WhiteheadRussell] p.
120 | Theorem *4.56 | ioran 752 pm4.56 780 |
[WhiteheadRussell] p.
120 | Theorem *4.57 | orandc 939 oranim 781 |
[WhiteheadRussell] p.
120 | Theorem *4.61 | annimim 686 |
[WhiteheadRussell] p.
120 | Theorem *4.62 | pm4.62dc 898 |
[WhiteheadRussell] p.
120 | Theorem *4.63 | pm4.63dc 886 |
[WhiteheadRussell] p.
120 | Theorem *4.64 | pm4.64dc 900 |
[WhiteheadRussell] p.
120 | Theorem *4.65 | pm4.65r 687 |
[WhiteheadRussell] p.
120 | Theorem *4.66 | pm4.66dc 901 |
[WhiteheadRussell] p.
120 | Theorem *4.67 | pm4.67dc 887 |
[WhiteheadRussell] p.
120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
[WhiteheadRussell] p.
121 | Theorem *4.72 | pm4.72 827 |
[WhiteheadRussell] p.
121 | Theorem *4.73 | iba 300 |
[WhiteheadRussell] p.
121 | Theorem *4.74 | biorf 744 |
[WhiteheadRussell] p.
121 | Theorem *4.76 | jcab 603 pm4.76 604 |
[WhiteheadRussell] p.
121 | Theorem *4.77 | jaob 710 pm4.77 799 |
[WhiteheadRussell] p.
121 | Theorem *4.78 | pm4.78i 782 |
[WhiteheadRussell] p.
121 | Theorem *4.79 | pm4.79dc 903 |
[WhiteheadRussell] p.
122 | Theorem *4.8 | pm4.8 707 |
[WhiteheadRussell] p.
122 | Theorem *4.81 | pm4.81dc 908 |
[WhiteheadRussell] p.
122 | Theorem *4.82 | pm4.82 950 |
[WhiteheadRussell] p.
122 | Theorem *4.83 | pm4.83dc 951 |
[WhiteheadRussell] p.
122 | Theorem *4.84 | imbi1 236 |
[WhiteheadRussell] p.
122 | Theorem *4.85 | imbi2 237 |
[WhiteheadRussell] p.
122 | Theorem *4.86 | bibi1 240 |
[WhiteheadRussell] p.
122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 557 |
[WhiteheadRussell] p.
123 | Theorem *5.1 | pm5.1 601 |
[WhiteheadRussell] p.
123 | Theorem *5.11 | pm5.11dc 909 |
[WhiteheadRussell] p.
123 | Theorem *5.12 | pm5.12dc 910 |
[WhiteheadRussell] p.
123 | Theorem *5.13 | pm5.13dc 912 |
[WhiteheadRussell] p.
123 | Theorem *5.14 | pm5.14dc 911 |
[WhiteheadRussell] p.
124 | Theorem *5.15 | pm5.15dc 1389 |
[WhiteheadRussell] p.
124 | Theorem *5.16 | pm5.16 828 |
[WhiteheadRussell] p.
124 | Theorem *5.17 | pm5.17dc 904 |
[WhiteheadRussell] p.
124 | Theorem *5.18 | nbbndc 1394 pm5.18dc 883 |
[WhiteheadRussell] p.
124 | Theorem *5.19 | pm5.19 706 |
[WhiteheadRussell] p.
124 | Theorem *5.21 | pm5.21 695 |
[WhiteheadRussell] p.
124 | Theorem *5.22 | xordc 1392 |
[WhiteheadRussell] p.
124 | Theorem *5.23 | dfbi3dc 1397 |
[WhiteheadRussell] p.
124 | Theorem *5.24 | pm5.24dc 1398 |
[WhiteheadRussell] p.
124 | Theorem *5.25 | dfor2dc 895 |
[WhiteheadRussell] p.
125 | Theorem *5.3 | pm5.3 475 |
[WhiteheadRussell] p.
125 | Theorem *5.4 | pm5.4 249 |
[WhiteheadRussell] p.
125 | Theorem *5.5 | pm5.5 242 |
[WhiteheadRussell] p.
125 | Theorem *5.6 | pm5.6dc 926 pm5.6r 927 |
[WhiteheadRussell] p.
125 | Theorem *5.7 | pm5.7dc 954 |
[WhiteheadRussell] p.
125 | Theorem *5.31 | pm5.31 348 |
[WhiteheadRussell] p.
125 | Theorem *5.32 | pm5.32 453 |
[WhiteheadRussell] p.
125 | Theorem *5.33 | pm5.33 609 |
[WhiteheadRussell] p.
125 | Theorem *5.35 | pm5.35 917 |
[WhiteheadRussell] p.
125 | Theorem *5.36 | pm5.36 610 |
[WhiteheadRussell] p.
125 | Theorem *5.41 | imdi 250 pm5.41 251 |
[WhiteheadRussell] p.
125 | Theorem *5.42 | pm5.42 320 |
[WhiteheadRussell] p.
125 | Theorem *5.44 | pm5.44 925 |
[WhiteheadRussell] p.
125 | Theorem *5.53 | pm5.53 802 |
[WhiteheadRussell] p.
125 | Theorem *5.54 | pm5.54dc 918 |
[WhiteheadRussell] p.
125 | Theorem *5.55 | pm5.55dc 913 |
[WhiteheadRussell] p.
125 | Theorem *5.61 | pm5.61 794 |
[WhiteheadRussell] p.
125 | Theorem *5.62 | pm5.62dc 945 |
[WhiteheadRussell] p.
125 | Theorem *5.63 | pm5.63dc 946 |
[WhiteheadRussell] p.
125 | Theorem *5.71 | pm5.71dc 961 |
[WhiteheadRussell] p.
125 | Theorem *5.501 | pm5.501 244 |
[WhiteheadRussell] p.
126 | Theorem *5.74 | pm5.74 179 |
[WhiteheadRussell] p.
126 | Theorem *5.75 | pm5.75 962 |
[WhiteheadRussell] p.
150 | Theorem *10.3 | alsyl 1633 |
[WhiteheadRussell] p.
160 | Theorem *11.21 | alrot3 1483 |
[WhiteheadRussell] p.
163 | Theorem *11.42 | 19.40-2 1630 |
[WhiteheadRussell] p.
164 | Theorem *11.53 | pm11.53 1893 |
[WhiteheadRussell] p.
175 | Definition *14.02 | df-eu 2027 |
[WhiteheadRussell] p.
178 | Theorem *13.18 | pm13.18 2426 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 2427 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 2873 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 3017 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 5188 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 5189 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2103 eupickbi 2106 |
[WhiteheadRussell] p.
235 | Definition *30.01 | df-fv 5216 |
[WhiteheadRussell] p.
360 | Theorem *54.43 | pm54.43 7179 |