Bibliographic Cross-Reference for the Intuitionistic Logic
Explorer
Bibliographic Reference |
Description | Intuitionistic Logic Explorer Page(s)
|
---|
[AczelRathjen], p.
71 | Definition 8.1.4 | enumct 6993 fidcenum 6837 |
[AczelRathjen], p.
72 | Proposition 8.1.11 | fidcenum 6837 |
[AczelRathjen], p.
73 | Lemma 8.1.14 | enumct 6993 |
[AczelRathjen], p.
73 | Corollary 8.1.13 | ennnfone 11927 |
[AczelRathjen], p.
74 | Lemma 8.1.16 | xpfi 6811 |
[AczelRathjen], p.
74 | Remark 8.1.17 | unfiexmid 6799 |
[AczelRathjen], p.
75 | Corollary 8.1.23 | qnnen 11933 znnen 11900 |
[AczelRathjen], p.
80 | Corollary 8.2.4 | df-ihash 10515 |
[AczelRathjen], p.
183 | Chapter 20 | ax-setind 4447 |
[Apostol] p. 18 | Theorem
I.1 | addcan 7935 addcan2d 7940 addcan2i 7938 addcand 7939 addcani 7937 |
[Apostol] p. 18 | Theorem
I.2 | negeu 7946 |
[Apostol] p. 18 | Theorem
I.3 | negsub 8003 negsubd 8072 negsubi 8033 |
[Apostol] p. 18 | Theorem
I.4 | negneg 8005 negnegd 8057 negnegi 8025 |
[Apostol] p. 18 | Theorem
I.5 | subdi 8140 subdid 8169 subdii 8162 subdir 8141 subdird 8170 subdiri 8163 |
[Apostol] p. 18 | Theorem
I.6 | mul01 8144 mul01d 8148 mul01i 8146 mul02 8142 mul02d 8147 mul02i 8145 |
[Apostol] p. 18 | Theorem
I.9 | divrecapd 8546 |
[Apostol] p. 18 | Theorem
I.10 | recrecapi 8497 |
[Apostol] p. 18 | Theorem
I.12 | mul2neg 8153 mul2negd 8168 mul2negi 8161 mulneg1 8150 mulneg1d 8166 mulneg1i 8159 |
[Apostol] p. 18 | Theorem
I.15 | divdivdivap 8466 |
[Apostol] p. 20 | Axiom
7 | rpaddcl 9458 rpaddcld 9492 rpmulcl 9459 rpmulcld 9493 |
[Apostol] p. 20 | Axiom
9 | 0nrp 9470 |
[Apostol] p. 20 | Theorem
I.17 | lttri 7861 |
[Apostol] p. 20 | Theorem
I.18 | ltadd1d 8293 ltadd1dd 8311 ltadd1i 8257 |
[Apostol] p. 20 | Theorem
I.19 | ltmul1 8347 ltmul1a 8346 ltmul1i 8671 ltmul1ii 8679 ltmul2 8607 ltmul2d 9519 ltmul2dd 9533 ltmul2i 8674 |
[Apostol] p. 20 | Theorem
I.21 | 0lt1 7882 |
[Apostol] p. 20 | Theorem
I.23 | lt0neg1 8223 lt0neg1d 8270 ltneg 8217 ltnegd 8278 ltnegi 8248 |
[Apostol] p. 20 | Theorem
I.25 | lt2add 8200 lt2addd 8322 lt2addi 8265 |
[Apostol] p.
20 | Definition of positive numbers | df-rp 9435 |
[Apostol] p. 21 | Exercise
4 | recgt0 8601 recgt0d 8685 recgt0i 8657 recgt0ii 8658 |
[Apostol] p.
22 | Definition of integers | df-z 9048 |
[Apostol] p.
22 | Definition of rationals | df-q 9405 |
[Apostol] p. 24 | Theorem
I.26 | supeuti 6874 |
[Apostol] p. 26 | Theorem
I.29 | arch 8967 |
[Apostol] p. 28 | Exercise
2 | btwnz 9163 |
[Apostol] p. 28 | Exercise
3 | nnrecl 8968 |
[Apostol] p. 28 | Exercise
6 | qbtwnre 10027 |
[Apostol] p. 28 | Exercise
10(a) | zeneo 11557 zneo 9145 |
[Apostol] p. 29 | Theorem
I.35 | resqrtth 10796 sqrtthi 10884 |
[Apostol] p. 34 | Theorem
I.36 (principle of mathematical induction) | peano5nni 8716 |
[Apostol] p.
363 | Remark | absgt0api 10911 |
[Apostol] p.
363 | Example | abssubd 10958 abssubi 10915 |
[ApostolNT] p.
14 | Definition | df-dvds 11483 |
[ApostolNT] p.
14 | Theorem 1.1(a) | iddvds 11495 |
[ApostolNT] p.
14 | Theorem 1.1(b) | dvdstr 11519 |
[ApostolNT] p.
14 | Theorem 1.1(c) | dvds2ln 11515 |
[ApostolNT] p.
14 | Theorem 1.1(d) | dvdscmul 11509 |
[ApostolNT] p.
14 | Theorem 1.1(e) | dvdscmulr 11511 |
[ApostolNT] p.
14 | Theorem 1.1(f) | 1dvds 11496 |
[ApostolNT] p.
14 | Theorem 1.1(g) | dvds0 11497 |
[ApostolNT] p.
14 | Theorem 1.1(h) | 0dvds 11502 |
[ApostolNT] p.
14 | Theorem 1.1(i) | dvdsleabs 11532 |
[ApostolNT] p.
14 | Theorem 1.1(j) | dvdsabseq 11534 |
[ApostolNT] p.
14 | Theorem 1.1(k) | divconjdvds 11536 |
[ApostolNT] p.
15 | Definition | dfgcd2 11691 |
[ApostolNT] p.
16 | Definition | isprm2 11787 |
[ApostolNT] p.
16 | Theorem 1.5 | coprmdvds 11762 |
[ApostolNT] p.
16 | Theorem 1.4(a) | gcdcom 11651 |
[ApostolNT] p.
16 | Theorem 1.4(b) | gcdass 11692 |
[ApostolNT] p.
16 | Theorem 1.4(c) | absmulgcd 11694 |
[ApostolNT] p.
16 | Theorem 1.4(d)1 | gcd1 11664 |
[ApostolNT] p.
16 | Theorem 1.4(d)2 | gcdid0 11657 |
[ApostolNT] p.
17 | Theorem 1.8 | coprm 11811 |
[ApostolNT] p.
17 | Theorem 1.9 | euclemma 11813 |
[ApostolNT] p.
19 | Theorem 1.14 | divalg 11610 |
[ApostolNT] p.
20 | Theorem 1.15 | eucalg 11729 |
[ApostolNT] p.
25 | Definition | df-phi 11876 |
[ApostolNT] p.
28 | Theorem 2.5(a) | phiprmpw 11887 |
[ApostolNT] p.
28 | Theorem 2.5(c) | phimul 11891 |
[ApostolNT] p.
104 | Definition | congr 11770 |
[ApostolNT] p.
106 | Remark | dvdsval3 11486 |
[ApostolNT] p.
106 | Definition | moddvds 11491 |
[ApostolNT] p.
107 | Example 2 | mod2eq0even 11564 |
[ApostolNT] p.
107 | Example 3 | mod2eq1n2dvds 11565 |
[ApostolNT] p.
107 | Example 4 | zmod1congr 10107 |
[ApostolNT] p.
107 | Theorem 5.2(b) | modqmul12d 10144 |
[ApostolNT] p.
108 | Theorem 5.3 | modmulconst 11514 |
[ApostolNT] p.
109 | Theorem 5.4 | cncongr1 11773 |
[ApostolNT] p.
109 | Theorem 5.4 "Cancellation law" | cncongr 11775 |
[Bauer] p. 482 | Section
1.2 | pm2.01 605 pm2.65 648 |
[Bauer] p. 483 | Theorem
1.3 | acexmid 5766 onsucelsucexmidlem 4439 |
[Bauer], p.
481 | Section 1.1 | pwtrufal 13181 |
[Bauer], p.
483 | Definition | n0rf 3370 |
[Bauer], p. 485 | Theorem
2.1 | ssfiexmid 6763 |
[Bauer], p. 494 | Theorem
5.5 | ivthinc 12779 |
[BauerHanson], p.
27 | Proposition 5.2 | cnstab 8400 |
[BauerSwan], p.
14 | Remark | 0ct 6985 ctm 6987 |
[BauerSwan],
p. 14 | Proposition 2.6 | subctctexmid 13185 |
[BauerSwan], p.
14 | Table" is defined as ` ` per | enumct 6993 |
[BauerTaylor], p.
32 | Lemma 6.16 | prarloclem 7302 |
[BauerTaylor], p.
50 | Lemma 11.4 | subhalfnqq 7215 |
[BauerTaylor], p.
52 | Proposition 11.15 | prarloc 7304 |
[BauerTaylor], p.
53 | Lemma 11.16 | addclpr 7338 addlocpr 7337 |
[BauerTaylor], p.
55 | Proposition 12.7 | appdivnq 7364 |
[BauerTaylor], p.
56 | Lemma 12.8 | prmuloc 7367 |
[BauerTaylor], p.
56 | Lemma 12.9 | mullocpr 7372 |
[BellMachover] p.
36 | Lemma 10.3 | idALT 20 |
[BellMachover] p.
97 | Definition 10.1 | df-eu 2000 |
[BellMachover] p.
460 | Notation | df-mo 2001 |
[BellMachover] p.
460 | Definition | mo3 2051 mo3h 2050 |
[BellMachover] p.
462 | Theorem 1.1 | bm1.1 2122 |
[BellMachover] p.
463 | Theorem 1.3ii | bm1.3ii 4044 |
[BellMachover] p.
466 | Axiom Pow | axpow3 4096 |
[BellMachover] p.
466 | Axiom Union | axun2 4352 |
[BellMachover] p.
469 | Theorem 2.2(i) | ordirr 4452 |
[BellMachover] p.
469 | Theorem 2.2(iii) | onelon 4301 |
[BellMachover] p.
469 | Theorem 2.2(vii) | ordn2lp 4455 |
[BellMachover] p.
471 | Problem 2.5(ii) | bm2.5ii 4407 |
[BellMachover] p.
471 | Definition of Lim | df-ilim 4286 |
[BellMachover] p.
472 | Axiom Inf | zfinf2 4498 |
[BellMachover] p.
473 | Theorem 2.8 | limom 4522 |
[Bobzien] p.
116 | Statement T3 | stoic3 1407 |
[Bobzien] p.
117 | Statement T2 | stoic2a 1405 |
[Bobzien] p.
117 | Statement T4 | stoic4a 1408 |
[BourbakiEns] p.
| Proposition 8 | fcof1 5677 fcofo 5678 |
[BourbakiTop1] p.
| Remark | xnegmnf 9605 xnegpnf 9604 |
[BourbakiTop1] p.
| Remark | rexneg 9606 |
[BourbakiTop1] p.
| Proposition | ishmeo 12462 |
[BourbakiTop1] p.
| Property V_i | ssnei2 12315 |
[BourbakiTop1] p.
| Property V_ii | innei 12321 |
[BourbakiTop1] p.
| Property V_iv | neissex 12323 |
[BourbakiTop1] p.
| Proposition 1 | neipsm 12312 neiss 12308 |
[BourbakiTop1] p.
| Proposition 2 | cnptopco 12380 |
[BourbakiTop1] p.
| Proposition 4 | imasnopn 12457 |
[BourbakiTop1] p.
| Property V_iii | elnei 12310 |
[BourbakiTop1] p.
| Definition is due to Bourbaki (Def. 1 | df-top 12154 |
[ChoquetDD] p.
2 | Definition of mapping | df-mpt 3986 |
[Crosilla] p. | Axiom
1 | ax-ext 2119 |
[Crosilla] p. | Axiom
2 | ax-pr 4126 |
[Crosilla] p. | Axiom
3 | ax-un 4350 |
[Crosilla] p. | Axiom
4 | ax-nul 4049 |
[Crosilla] p. | Axiom
5 | ax-iinf 4497 |
[Crosilla] p. | Axiom
6 | ru 2903 |
[Crosilla] p. | Axiom
8 | ax-pow 4093 |
[Crosilla] p. | Axiom
9 | ax-setind 4447 |
[Crosilla], p. | Axiom
6 | ax-sep 4041 |
[Crosilla], p. | Axiom
7 | ax-coll 4038 |
[Crosilla], p. | Axiom
7' | repizf 4039 |
[Crosilla], p. | Theorem
is stated | ordtriexmid 4432 |
[Crosilla], p. | Axiom
of choice implies instances | acexmid 5766 |
[Crosilla], p.
| Definition of ordinal | df-iord 4283 |
[Crosilla], p. | Theorem
"Foundation implies instances of EM" | regexmid 4445 |
[Eisenberg] p.
67 | Definition 5.3 | df-dif 3068 |
[Eisenberg] p.
82 | Definition 6.3 | df-iom 4500 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 6537 |
[Enderton] p. 18 | Axiom
of Empty Set | axnul 4048 |
[Enderton] p.
19 | Definition | df-tp 3530 |
[Enderton] p.
26 | Exercise 5 | unissb 3761 |
[Enderton] p.
26 | Exercise 10 | pwel 4135 |
[Enderton] p.
28 | Exercise 7(b) | pwunim 4203 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1m 3877 iinin2m 3876 iunin1 3872 iunin2 3871 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2m 3875 iundif2ss 3873 |
[Enderton] p.
33 | Exercise 23 | iinuniss 3890 |
[Enderton] p.
33 | Exercise 25 | iununir 3891 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 3898 |
[Enderton] p.
33 | Exercise 24(b) | iunpw 4396 iunpwss 3899 |
[Enderton] p.
38 | Exercise 6(a) | unipw 4134 |
[Enderton] p.
38 | Exercise 6(b) | pwuni 4111 |
[Enderton] p. 41 | Lemma
3D | opeluu 4366 rnex 4801
rnexg 4799 |
[Enderton] p.
41 | Exercise 8 | dmuni 4744 rnuni 4945 |
[Enderton] p.
42 | Definition of a function | dffun7 5145 dffun8 5146 |
[Enderton] p.
43 | Definition of function value | funfvdm2 5478 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 5179 |
[Enderton] p.
44 | Definition (d) | dfima2 4878 dfima3 4879 |
[Enderton] p.
47 | Theorem 3H | fvco2 5483 |
[Enderton] p. 49 | Axiom
of Choice (first form) | df-ac 7055 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 5655 |
[Enderton] p.
52 | Definition | df-map 6537 |
[Enderton] p.
53 | Exercise 21 | coass 5052 |
[Enderton] p.
53 | Exercise 27 | dmco 5042 |
[Enderton] p.
53 | Exercise 14(a) | funin 5189 |
[Enderton] p.
53 | Exercise 22(a) | imass2 4910 |
[Enderton] p.
54 | Remark | ixpf 6607 ixpssmap 6619 |
[Enderton] p.
54 | Definition of infinite Cartesian product | df-ixp 6586 |
[Enderton] p.
56 | Theorem 3M | erref 6442 |
[Enderton] p. 57 | Lemma
3N | erthi 6468 |
[Enderton] p.
57 | Definition | df-ec 6424 |
[Enderton] p.
58 | Definition | df-qs 6428 |
[Enderton] p.
60 | Theorem 3Q | th3q 6527 th3qcor 6526 th3qlem1 6524 th3qlem2 6525 |
[Enderton] p.
61 | Exercise 35 | df-ec 6424 |
[Enderton] p.
65 | Exercise 56(a) | dmun 4741 |
[Enderton] p.
68 | Definition of successor | df-suc 4288 |
[Enderton] p.
71 | Definition | df-tr 4022 dftr4 4026 |
[Enderton] p.
72 | Theorem 4E | unisuc 4330 unisucg 4331 |
[Enderton] p.
73 | Exercise 6 | unisuc 4330 unisucg 4331 |
[Enderton] p.
73 | Exercise 5(a) | truni 4035 |
[Enderton] p.
73 | Exercise 5(b) | trint 4036 |
[Enderton] p.
79 | Theorem 4I(A1) | nna0 6363 |
[Enderton] p.
79 | Theorem 4I(A2) | nnasuc 6365 onasuc 6355 |
[Enderton] p.
79 | Definition of operation value | df-ov 5770 |
[Enderton] p.
80 | Theorem 4J(A1) | nnm0 6364 |
[Enderton] p.
80 | Theorem 4J(A2) | nnmsuc 6366 onmsuc 6362 |
[Enderton] p.
81 | Theorem 4K(1) | nnaass 6374 |
[Enderton] p.
81 | Theorem 4K(2) | nna0r 6367 nnacom 6373 |
[Enderton] p.
81 | Theorem 4K(3) | nndi 6375 |
[Enderton] p.
81 | Theorem 4K(4) | nnmass 6376 |
[Enderton] p.
81 | Theorem 4K(5) | nnmcom 6378 |
[Enderton] p.
82 | Exercise 16 | nnm0r 6368 nnmsucr 6377 |
[Enderton] p.
88 | Exercise 23 | nnaordex 6416 |
[Enderton] p.
129 | Definition | df-en 6628 |
[Enderton] p.
133 | Exercise 1 | xpomen 11897 |
[Enderton] p.
134 | Theorem (Pigeonhole Principle) | phpm 6752 |
[Enderton] p.
136 | Corollary 6E | nneneq 6744 |
[Enderton] p.
139 | Theorem 6H(c) | mapen 6733 |
[Enderton] p.
142 | Theorem 6I(3) | xpdjuen 7067 |
[Enderton] p.
143 | Theorem 6J | dju0en 7063 dju1en 7062 |
[Enderton] p.
144 | Corollary 6K | undif2ss 3433 |
[Enderton] p.
145 | Figure 38 | ffoss 5392 |
[Enderton] p.
145 | Definition | df-dom 6629 |
[Enderton] p.
146 | Example 1 | domen 6638 domeng 6639 |
[Enderton] p.
146 | Example 3 | nndomo 6751 |
[Enderton] p.
149 | Theorem 6L(c) | xpdom1 6722 xpdom1g 6720 xpdom2g 6719 |
[Enderton] p.
168 | Definition | df-po 4213 |
[Enderton] p.
192 | Theorem 7M(a) | oneli 4345 |
[Enderton] p.
192 | Theorem 7M(b) | ontr1 4306 |
[Enderton] p.
192 | Theorem 7M(c) | onirri 4453 |
[Enderton] p.
193 | Corollary 7N(b) | 0elon 4309 |
[Enderton] p.
193 | Corollary 7N(c) | onsuci 4427 |
[Enderton] p.
193 | Corollary 7N(d) | ssonunii 4400 |
[Enderton] p.
194 | Remark | onprc 4462 |
[Enderton] p.
194 | Exercise 16 | suc11 4468 |
[Enderton] p.
197 | Definition | df-card 7029 |
[Enderton] p.
200 | Exercise 25 | tfis 4492 |
[Enderton] p.
206 | Theorem 7X(b) | en2lp 4464 |
[Enderton] p.
207 | Exercise 34 | opthreg 4466 |
[Enderton] p.
208 | Exercise 35 | suc11g 4467 |
[Geuvers], p.
1 | Remark | expap0 10316 |
[Geuvers], p. 6 | Lemma
2.13 | mulap0r 8370 |
[Geuvers], p. 6 | Lemma
2.15 | mulap0 8408 |
[Geuvers], p. 9 | Lemma
2.35 | msqge0 8371 |
[Geuvers], p.
9 | Definition 3.1(2) | ax-arch 7732 |
[Geuvers], p. 10 | Lemma
3.9 | maxcom 10968 |
[Geuvers], p. 10 | Lemma
3.10 | maxle1 10976 maxle2 10977 |
[Geuvers], p. 10 | Lemma
3.11 | maxleast 10978 |
[Geuvers], p. 10 | Lemma
3.12 | maxleb 10981 |
[Geuvers], p.
11 | Definition 3.13 | dfabsmax 10982 |
[Geuvers], p.
17 | Definition 6.1 | df-ap 8337 |
[Gleason] p.
117 | Proposition 9-2.1 | df-enq 7148 enqer 7159 |
[Gleason] p.
117 | Proposition 9-2.2 | df-1nqqs 7152 df-nqqs 7149 |
[Gleason] p.
117 | Proposition 9-2.3 | df-plpq 7145 df-plqqs 7150 |
[Gleason] p.
119 | Proposition 9-2.4 | df-mpq 7146 df-mqqs 7151 |
[Gleason] p.
119 | Proposition 9-2.5 | df-rq 7153 |
[Gleason] p.
119 | Proposition 9-2.6 | ltexnqq 7209 |
[Gleason] p.
120 | Proposition 9-2.6(i) | halfnq 7212 ltbtwnnq 7217 ltbtwnnqq 7216 |
[Gleason] p.
120 | Proposition 9-2.6(ii) | ltanqg 7201 |
[Gleason] p.
120 | Proposition 9-2.6(iii) | ltmnqg 7202 |
[Gleason] p.
123 | Proposition 9-3.5 | addclpr 7338 |
[Gleason] p.
123 | Proposition 9-3.5(i) | addassprg 7380 |
[Gleason] p.
123 | Proposition 9-3.5(ii) | addcomprg 7379 |
[Gleason] p.
123 | Proposition 9-3.5(iii) | ltaddpr 7398 |
[Gleason] p.
123 | Proposition 9-3.5(iv) | ltexpri 7414 |
[Gleason] p.
123 | Proposition 9-3.5(v) | ltaprg 7420 ltaprlem 7419 |
[Gleason] p.
123 | Proposition 9-3.5(vi) | addcanprg 7417 |
[Gleason] p.
124 | Proposition 9-3.7 | mulclpr 7373 |
[Gleason] p. 124 | Theorem
9-3.7(iv) | 1idpr 7393 |
[Gleason] p.
124 | Proposition 9-3.7(i) | mulassprg 7382 |
[Gleason] p.
124 | Proposition 9-3.7(ii) | mulcomprg 7381 |
[Gleason] p.
124 | Proposition 9-3.7(iii) | distrprg 7389 |
[Gleason] p.
124 | Proposition 9-3.7(v) | recexpr 7439 |
[Gleason] p.
126 | Proposition 9-4.1 | df-enr 7527 enrer 7536 |
[Gleason] p.
126 | Proposition 9-4.2 | df-0r 7532 df-1r 7533 df-nr 7528 |
[Gleason] p.
126 | Proposition 9-4.3 | df-mr 7530 df-plr 7529 negexsr 7573 recexsrlem 7575 |
[Gleason] p.
127 | Proposition 9-4.4 | df-ltr 7531 |
[Gleason] p.
130 | Proposition 10-1.3 | creui 8711 creur 8710 cru 8357 |
[Gleason] p.
130 | Definition 10-1.1(v) | ax-cnre 7724 axcnre 7682 |
[Gleason] p.
132 | Definition 10-3.1 | crim 10623 crimd 10742 crimi 10702 crre 10622 crred 10741 crrei 10701 |
[Gleason] p.
132 | Definition 10-3.2 | remim 10625 remimd 10707 |
[Gleason] p.
133 | Definition 10.36 | absval2 10822 absval2d 10950 absval2i 10909 |
[Gleason] p.
133 | Proposition 10-3.4(a) | cjadd 10649 cjaddd 10730 cjaddi 10697 |
[Gleason] p.
133 | Proposition 10-3.4(c) | cjmul 10650 cjmuld 10731 cjmuli 10698 |
[Gleason] p.
133 | Proposition 10-3.4(e) | cjcj 10648 cjcjd 10708 cjcji 10680 |
[Gleason] p.
133 | Proposition 10-3.4(f) | cjre 10647 cjreb 10631 cjrebd 10711 cjrebi 10683 cjred 10736 rere 10630 rereb 10628 rerebd 10710 rerebi 10682 rered 10734 |
[Gleason] p.
133 | Proposition 10-3.4(h) | addcj 10656 addcjd 10722 addcji 10692 |
[Gleason] p.
133 | Proposition 10-3.7(a) | absval 10766 |
[Gleason] p.
133 | Proposition 10-3.7(b) | abscj 10817 abscjd 10955 abscji 10913 |
[Gleason] p.
133 | Proposition 10-3.7(c) | abs00 10829 abs00d 10951 abs00i 10910 absne0d 10952 |
[Gleason] p.
133 | Proposition 10-3.7(d) | releabs 10861 releabsd 10956 releabsi 10914 |
[Gleason] p.
133 | Proposition 10-3.7(f) | absmul 10834 absmuld 10959 absmuli 10916 |
[Gleason] p.
133 | Proposition 10-3.7(g) | sqabsadd 10820 sqabsaddi 10917 |
[Gleason] p.
133 | Proposition 10-3.7(h) | abstri 10869 abstrid 10961 abstrii 10920 |
[Gleason] p.
134 | Definition 10-4.1 | 0exp0e1 10291 df-exp 10286 exp0 10290 expp1 10293 expp1d 10418 |
[Gleason] p.
135 | Proposition 10-4.2(a) | expadd 10328 expaddd 10419 |
[Gleason] p.
135 | Proposition 10-4.2(b) | expmul 10331 expmuld 10420 |
[Gleason] p.
135 | Proposition 10-4.2(c) | mulexp 10325 mulexpd 10432 |
[Gleason] p.
141 | Definition 11-2.1 | fzval 9785 |
[Gleason] p.
168 | Proposition 12-2.1(a) | climadd 11088 |
[Gleason] p.
168 | Proposition 12-2.1(b) | climsub 11090 |
[Gleason] p.
168 | Proposition 12-2.1(c) | climmul 11089 |
[Gleason] p.
171 | Corollary 12-2.2 | climmulc2 11093 |
[Gleason] p.
172 | Corollary 12-2.5 | climrecl 11086 |
[Gleason] p.
172 | Proposition 12-2.4(c) | climabs 11082 climcj 11083 climim 11085 climre 11084 |
[Gleason] p.
173 | Definition 12-3.1 | df-ltxr 7798 df-xr 7797 ltxr 9555 |
[Gleason] p. 180 | Theorem
12-5.3 | climcau 11109 |
[Gleason] p. 217 | Lemma
13-4.1 | btwnzge0 10066 |
[Gleason] p.
223 | Definition 14-1.1 | df-met 12147 |
[Gleason] p.
223 | Definition 14-1.1(a) | met0 12522 xmet0 12521 |
[Gleason] p.
223 | Definition 14-1.1(c) | metsym 12529 |
[Gleason] p.
223 | Definition 14-1.1(d) | mettri 12531 mstri 12631 xmettri 12530 xmstri 12630 |
[Gleason] p.
230 | Proposition 14-2.6 | txlm 12437 |
[Gleason] p.
240 | Proposition 14-4.2 | metcnp3 12669 |
[Gleason] p.
243 | Proposition 14-4.16 | addcn2 11072 addcncntop 12710 mulcn2 11074 mulcncntop 12712 subcn2 11073 subcncntop 12711 |
[Gleason] p.
295 | Remark | bcval3 10490 bcval4 10491 |
[Gleason] p.
295 | Equation 2 | bcpasc 10505 |
[Gleason] p.
295 | Definition of binomial coefficient | bcval 10488 df-bc 10487 |
[Gleason] p.
296 | Remark | bcn0 10494 bcnn 10496 |
[Gleason] p. 296 | Theorem
15-2.8 | binom 11246 |
[Gleason] p.
308 | Equation 2 | ef0 11367 |
[Gleason] p.
308 | Equation 3 | efcj 11368 |
[Gleason] p.
309 | Corollary 15-4.3 | efne0 11373 |
[Gleason] p.
309 | Corollary 15-4.4 | efexp 11377 |
[Gleason] p.
310 | Equation 14 | sinadd 11432 |
[Gleason] p.
310 | Equation 15 | cosadd 11433 |
[Gleason] p.
311 | Equation 17 | sincossq 11444 |
[Gleason] p.
311 | Equation 18 | cosbnd 11449 sinbnd 11448 |
[Gleason] p.
311 | Definition of ` ` | df-pi 11348 |
[Hamilton] p.
31 | Example 2.7(a) | idALT 20 |
[Hamilton] p. 73 | Rule
1 | ax-mp 5 |
[Hamilton] p. 74 | Rule
2 | ax-gen 1425 |
[Heyting] p.
127 | Axiom #1 | ax1hfs 13229 |
[Hitchcock] p. 5 | Rule
A3 | mptnan 1401 |
[Hitchcock] p. 5 | Rule
A4 | mptxor 1402 |
[Hitchcock] p. 5 | Rule
A5 | mtpxor 1404 |
[HoTT], p. | Theorem
7.2.6 | nndceq 6388 |
[HoTT], p. | Exercise
11.11 | mulap0bd 8411 |
[HoTT], p. | Section
11.2.1 | df-iltp 7271 df-imp 7270 df-iplp 7269 df-reap 8330 |
[HoTT], p. | Theorem
11.2.12 | cauappcvgpr 7463 |
[HoTT], p. | Corollary
11.4.3 | conventions 12922 |
[HoTT], p. | Corollary
11.2.13 | axcaucvg 7701 caucvgpr 7483 caucvgprpr 7513 caucvgsr 7603 |
[HoTT], p. | Definition
11.2.1 | df-inp 7267 |
[HoTT], p. | Proposition
11.2.3 | df-iso 4214 ltpopr 7396 ltsopr 7397 |
[HoTT], p. | Definition
11.2.7(v) | apsym 8361 reapcotr 8353 reapirr 8332 |
[HoTT], p. | Definition
11.2.7(vi) | 0lt1 7882 gt0add 8328 leadd1 8185 lelttr 7845 lemul1a 8609 lenlt 7833 ltadd1 8184 ltletr 7846 ltmul1 8347 reaplt 8343 |
[Jech] p. 4 | Definition of
class | cv 1330 cvjust 2132 |
[Jech] p.
78 | Note | opthprc 4585 |
[KalishMontague] p.
81 | Note 1 | ax-i9 1510 |
[Kreyszig] p.
3 | Property M1 | metcl 12511 xmetcl 12510 |
[Kreyszig] p.
4 | Property M2 | meteq0 12518 |
[Kreyszig] p.
12 | Equation 5 | muleqadd 8422 |
[Kreyszig] p.
18 | Definition 1.3-2 | mopnval 12600 |
[Kreyszig] p.
19 | Remark | mopntopon 12601 |
[Kreyszig] p.
19 | Theorem T1 | mopn0 12646 mopnm 12606 |
[Kreyszig] p.
19 | Theorem T2 | unimopn 12644 |
[Kreyszig] p.
19 | Definition of neighborhood | neibl 12649 |
[Kreyszig] p.
20 | Definition 1.3-3 | metcnp2 12671 |
[Kreyszig] p.
25 | Definition 1.4-1 | lmbr 12371 |
[Kunen] p. 10 | Axiom
0 | a9e 1674 |
[Kunen] p. 12 | Axiom
6 | zfrep6 4040 |
[Kunen] p. 24 | Definition
10.24 | mapval 6547 mapvalg 6545 |
[Kunen] p. 31 | Definition
10.24 | mapex 6541 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 3818 |
[Levy] p.
338 | Axiom | df-clab 2124 df-clel 2133 df-cleq 2130 |
[Lopez-Astorga] p.
12 | Rule 1 | mptnan 1401 |
[Lopez-Astorga] p.
12 | Rule 2 | mptxor 1402 |
[Lopez-Astorga] p.
12 | Rule 3 | mtpxor 1404 |
[Margaris] p. 40 | Rule
C | exlimiv 1577 |
[Margaris] p. 49 | Axiom
A1 | ax-1 6 |
[Margaris] p. 49 | Axiom
A2 | ax-2 7 |
[Margaris] p. 49 | Axiom
A3 | condc 838 |
[Margaris] p.
49 | Definition | dfbi2 385 dfordc 877 exalim 1478 |
[Margaris] p.
51 | Theorem 1 | idALT 20 |
[Margaris] p.
56 | Theorem 3 | syld 45 |
[Margaris] p.
60 | Theorem 8 | mth8 639 |
[Margaris] p.
89 | Theorem 19.2 | 19.2 1617 r19.2m 3444 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 1533 19.3h 1532 rr19.3v 2818 |
[Margaris] p.
89 | Theorem 19.5 | alcom 1454 |
[Margaris] p.
89 | Theorem 19.6 | alexdc 1598 alexim 1624 |
[Margaris] p.
89 | Theorem 19.7 | alnex 1475 |
[Margaris] p.
89 | Theorem 19.8 | 19.8a 1569 spsbe 1814 |
[Margaris] p.
89 | Theorem 19.9 | 19.9 1623 19.9h 1622 19.9v 1843 exlimd 1576 |
[Margaris] p.
89 | Theorem 19.11 | excom 1642 excomim 1641 |
[Margaris] p.
89 | Theorem 19.12 | 19.12 1643 r19.12 2536 |
[Margaris] p.
90 | Theorem 19.14 | exnalim 1625 |
[Margaris] p.
90 | Theorem 19.15 | albi 1444 ralbi 2562 |
[Margaris] p.
90 | Theorem 19.16 | 19.16 1534 |
[Margaris] p.
90 | Theorem 19.17 | 19.17 1535 |
[Margaris] p.
90 | Theorem 19.18 | exbi 1583 rexbi 2563 |
[Margaris] p.
90 | Theorem 19.19 | 19.19 1644 |
[Margaris] p.
90 | Theorem 19.20 | alim 1433 alimd 1501 alimdh 1443 alimdv 1851 ralimdaa 2496 ralimdv 2498 ralimdva 2497 ralimdvva 2499 sbcimdv 2969 |
[Margaris] p.
90 | Theorem 19.21 | 19.21-2 1645 19.21 1562 19.21bi 1537 19.21h 1536 19.21ht 1560 19.21t 1561 19.21v 1845 alrimd 1589 alrimdd 1588 alrimdh 1455 alrimdv 1848 alrimi 1502 alrimih 1445 alrimiv 1846 alrimivv 1847 r19.21 2506 r19.21be 2521 r19.21bi 2518 r19.21t 2505 r19.21v 2507 ralrimd 2508 ralrimdv 2509 ralrimdva 2510 ralrimdvv 2514 ralrimdvva 2515 ralrimi 2501 ralrimiv 2502 ralrimiva 2503 ralrimivv 2511 ralrimivva 2512 ralrimivvva 2513 ralrimivw 2504 rexlimi 2540 |
[Margaris] p.
90 | Theorem 19.22 | 2alimdv 1853 2eximdv 1854 exim 1578
eximd 1591 eximdh 1590 eximdv 1852 rexim 2524 reximdai 2528 reximddv 2533 reximddv2 2535 reximdv 2531 reximdv2 2529 reximdva 2532 reximdvai 2530 reximi2 2526 |
[Margaris] p.
90 | Theorem 19.23 | 19.23 1656 19.23bi 1571 19.23h 1474 19.23ht 1473 19.23t 1655 19.23v 1855 19.23vv 1856 exlimd2 1574 exlimdh 1575 exlimdv 1791 exlimdvv 1869 exlimi 1573 exlimih 1572 exlimiv 1577 exlimivv 1868 r19.23 2538 r19.23v 2539 rexlimd 2544 rexlimdv 2546 rexlimdv3a 2549 rexlimdva 2547 rexlimdva2 2550 rexlimdvaa 2548 rexlimdvv 2554 rexlimdvva 2555 rexlimdvw 2551 rexlimiv 2541 rexlimiva 2542 rexlimivv 2553 |
[Margaris] p.
90 | Theorem 19.24 | i19.24 1618 |
[Margaris] p.
90 | Theorem 19.25 | 19.25 1605 |
[Margaris] p.
90 | Theorem 19.26 | 19.26-2 1458 19.26-3an 1459 19.26 1457 r19.26-2 2559 r19.26-3 2560 r19.26 2556 r19.26m 2561 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 1540 19.27h 1539 19.27v 1871 r19.27av 2565 r19.27m 3453 r19.27mv 3454 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 1542 19.28h 1541 19.28v 1872 r19.28av 2566 r19.28m 3447 r19.28mv 3450 rr19.28v 2819 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1599 19.29r 1600 19.29r2 1601 19.29x 1602 r19.29 2567 r19.29d2r 2574 r19.29r 2568 |
[Margaris] p.
90 | Theorem 19.30 | 19.30dc 1606 |
[Margaris] p.
90 | Theorem 19.31 | 19.31r 1659 |
[Margaris] p.
90 | Theorem 19.32 | 19.32dc 1657 19.32r 1658 r19.32r 2576 r19.32vdc 2578 r19.32vr 2577 |
[Margaris] p.
90 | Theorem 19.33 | 19.33 1460 19.33b2 1608 19.33bdc 1609 |
[Margaris] p.
90 | Theorem 19.34 | 19.34 1662 |
[Margaris] p.
90 | Theorem 19.35 | 19.35-1 1603 19.35i 1604 |
[Margaris] p.
90 | Theorem 19.36 | 19.36-1 1651 19.36aiv 1873 19.36i 1650 r19.36av 2580 |
[Margaris] p.
90 | Theorem 19.37 | 19.37-1 1652 19.37aiv 1653 r19.37 2581 r19.37av 2582 |
[Margaris] p.
90 | Theorem 19.38 | 19.38 1654 |
[Margaris] p.
90 | Theorem 19.39 | i19.39 1619 |
[Margaris] p.
90 | Theorem 19.40 | 19.40-2 1611 19.40 1610 r19.40 2583 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 1664 19.41h 1663 19.41v 1874 19.41vv 1875 19.41vvv 1876 19.41vvvv 1877 r19.41 2584 r19.41v 2585 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 1666 19.42h 1665 19.42v 1878 19.42vv 1883 19.42vvv 1884 19.42vvvv 1885 r19.42v 2586 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1607 r19.43 2587 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 1660 r19.44av 2588 r19.44mv 3452 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 1661 r19.45av 2589 r19.45mv 3451 |
[Margaris] p.
110 | Exercise 2(b) | eu1 2022 |
[Megill] p. 444 | Axiom
C5 | ax-17 1506 |
[Megill] p. 445 | Lemma
L12 | alequcom 1495 ax-10 1483 |
[Megill] p. 446 | Lemma
L17 | equtrr 1686 |
[Megill] p. 446 | Lemma
L19 | hbnae 1699 |
[Megill] p. 447 | Remark
9.1 | df-sb 1736 sbid 1747 |
[Megill] p. 448 | Scheme
C5' | ax-4 1487 |
[Megill] p. 448 | Scheme
C6' | ax-7 1424 |
[Megill] p. 448 | Scheme
C8' | ax-8 1482 |
[Megill] p. 448 | Scheme
C9' | ax-i12 1485 |
[Megill] p. 448 | Scheme
C11' | ax-10o 1694 |
[Megill] p. 448 | Scheme
C12' | ax-13 1491 |
[Megill] p. 448 | Scheme
C13' | ax-14 1492 |
[Megill] p. 448 | Scheme
C15' | ax-11o 1795 |
[Megill] p. 448 | Scheme
C16' | ax-16 1786 |
[Megill] p. 448 | Theorem
9.4 | dral1 1708 dral2 1709 drex1 1770 drex2 1710 drsb1 1771 drsb2 1813 |
[Megill] p. 449 | Theorem
9.7 | sbcom2 1960 sbequ 1812 sbid2v 1969 |
[Megill] p. 450 | Example
in Appendix | hba1 1520 |
[Mendelson] p.
36 | Lemma 1.8 | idALT 20 |
[Mendelson] p.
69 | Axiom 4 | rspsbc 2986 rspsbca 2987 stdpc4 1748 |
[Mendelson] p.
69 | Axiom 5 | ra5 2992 stdpc5 1563 |
[Mendelson] p. 81 | Rule
C | exlimiv 1577 |
[Mendelson] p.
95 | Axiom 6 | stdpc6 1679 |
[Mendelson] p.
95 | Axiom 7 | stdpc7 1743 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 3394 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 3395 |
[Mendelson] p.
231 | Exercise 4.10(n) | inssun 3311 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 3359 |
[Mendelson] p.
231 | Exercise 4.10(q) | inssddif 3312 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddifnel 3202 |
[Mendelson] p.
231 | Definition of union | unssin 3310 |
[Mendelson] p.
235 | Exercise 4.12(c) | univ 4392 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 3730 |
[Mendelson] p.
235 | Exercise 4.12(j) | pwin 4199 |
[Mendelson] p.
235 | Exercise 4.12(k) | pwunss 4200 |
[Mendelson] p.
235 | Exercise 4.12(l) | pwssunim 4201 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 3751 |
[Mendelson] p.
235 | Exercise 4.12(p) | reli 4663 |
[Mendelson] p.
235 | Exercise 4.12(t) | relssdmrn 5054 |
[Mendelson] p.
246 | Definition of successor | df-suc 4288 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 6732 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 6708 xpsneng 6709 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 6714 xpcomeng 6715 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 6717 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 6711 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 6539 |
[Mendelson] p.
255 | Exercise 4.43 | mapsnen 6698 |
[Mendelson] p.
255 | Exercise 4.47 | xpmapen 6737 |
[Mendelson] p.
255 | Exercise 4.42(a) | map0e 6573 |
[Mendelson] p.
255 | Exercise 4.42(b) | map1 6699 |
[Mendelson] p.
258 | Exercise 4.56(c) | djuassen 7066 djucomen 7065 |
[Mendelson] p.
258 | Exercise 4.56(g) | xp2dju 7064 |
[Mendelson] p.
266 | Proposition 4.34(a) | oa1suc 6356 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 3293 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 4622 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 4623 |
[Monk1] p. 34 | Definition
3.3 | df-opab 3985 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5049 coi2 5050 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 4748 rn0 4790 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 4938 |
[Monk1] p. 37 | Theorem
3.13(i) | relxp 4643 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxpm 4754 rnxpm 4963 |
[Monk1] p. 37 | Theorem
3.13(ii) | 0xp 4614 xp0 4953 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 4893 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 4890 |
[Monk1] p. 39 | Theorem
3.17 | imaex 4889 imaexg 4888 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 4887 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 5543 funfvop 5525 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 5458 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 5466 |
[Monk1] p. 43 | Theorem
4.6 | funun 5162 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 5662 dff13f 5664 |
[Monk1] p. 46 | Theorem
4.15(v) | funex 5636 funrnex 6005 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 5656 |
[Monk1] p. 52 | Theorem
5.12(ii) | op2ndb 5017 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 3782 |
[Monk1] p. 52 | Definition
5.13 (i) | 1stval2 6046 df-1st 6031 |
[Monk1] p. 52 | Definition
5.13 (ii) | 2ndval2 6047 df-2nd 6032 |
[Monk2] p. 105 | Axiom
C4 | ax-5 1423 |
[Monk2] p. 105 | Axiom
C7 | ax-8 1482 |
[Monk2] p. 105 | Axiom
C8 | ax-11 1484 ax-11o 1795 |
[Monk2] p. 105 | Axiom
(C8) | ax11v 1799 |
[Monk2] p. 109 | Lemma
12 | ax-7 1424 |
[Monk2] p. 109 | Lemma
15 | equvin 1835 equvini 1731 eqvinop 4160 |
[Monk2] p. 113 | Axiom
C5-1 | ax-17 1506 |
[Monk2] p. 113 | Axiom
C5-2 | ax6b 1629 |
[Monk2] p. 113 | Axiom
C5-3 | ax-7 1424 |
[Monk2] p. 114 | Lemma
22 | hba1 1520 |
[Monk2] p. 114 | Lemma
23 | hbia1 1531 nfia1 1559 |
[Monk2] p. 114 | Lemma
24 | hba2 1530 nfa2 1558 |
[Moschovakis] p.
2 | Chapter 2 | df-stab 816 dftest 13230 |
[Munkres] p. 77 | Example
2 | distop 12243 |
[Munkres] p.
78 | Definition of basis | df-bases 12199 isbasis3g 12202 |
[Munkres] p.
78 | Definition of a topology generated by a basis | df-topgen 12130 tgval2 12209 |
[Munkres] p.
79 | Remark | tgcl 12222 |
[Munkres] p. 80 | Lemma
2.1 | tgval3 12216 |
[Munkres] p. 80 | Lemma
2.2 | tgss2 12237 tgss3 12236 |
[Munkres] p. 81 | Lemma
2.3 | basgen 12238 basgen2 12239 |
[Munkres] p.
89 | Definition of subspace topology | resttop 12328 |
[Munkres] p. 93 | Theorem
6.1(1) | 0cld 12270 topcld 12267 |
[Munkres] p. 93 | Theorem
6.1(3) | uncld 12271 |
[Munkres] p.
94 | Definition of closure | clsval 12269 |
[Munkres] p.
94 | Definition of interior | ntrval 12268 |
[Munkres] p.
102 | Definition of continuous function | df-cn 12346 iscn 12355 iscn2 12358 |
[Munkres] p. 107 | Theorem
7.2(g) | cncnp 12388 cncnp2m 12389 cncnpi 12386 df-cnp 12347 iscnp 12357 |
[Munkres] p. 127 | Theorem
10.1 | metcn 12672 |
[Pierik], p. 8 | Section
2.2.1 | dfrex2fin 6790 |
[Pierik], p. 9 | Definition
2.5 | df-markov 7019 |
[Pierik], p. 10 | Section
2.3 | dfdif3 3181 |
[Pierik], p.
14 | Definition 3.1 | df-omni 6999 exmidomniim 7006 finomni 7005 |
[Pierik], p. 15 | Section
3.1 | df-nninf 7000 |
[PradicBrown2022], p. 1 | Theorem
1 | exmidsbthr 13207 |
[PradicBrown2022], p.
2 | Remark | exmidpw 6795 |
[PradicBrown2022], p.
2 | Proposition 1.1 | exmidfodomrlemim 7050 |
[PradicBrown2022], p.
2 | Proposition 1.2 | exmidfodomrlemr 7051 exmidfodomrlemrALT 7052 |
[PradicBrown2022], p.
4 | Lemma 3.2 | fodjuomni 7014 |
[PradicBrown2022], p. 5 | Lemma
3.4 | peano3nninf 13190 peano4nninf 13189 |
[PradicBrown2022], p. 5 | Lemma
3.5 | nninfall 13193 |
[PradicBrown2022], p. 5 | Theorem
3.6 | nninfsel 13202 |
[PradicBrown2022], p. 5 | Corollary
3.7 | nninfomni 13204 |
[PradicBrown2022], p. 5 | Definition
3.3 | nnsf 13188 |
[Quine] p. 16 | Definition
2.1 | df-clab 2124 rabid 2604 |
[Quine] p. 17 | Definition
2.1'' | dfsb7 1964 |
[Quine] p. 18 | Definition
2.7 | df-cleq 2130 |
[Quine] p. 19 | Definition
2.9 | df-v 2683 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2246 |
[Quine] p. 35 | Theorem
5.2 | abid2 2258 abid2f 2304 |
[Quine] p. 40 | Theorem
6.1 | sb5 1859 |
[Quine] p. 40 | Theorem
6.2 | sb56 1857 sb6 1858 |
[Quine] p. 41 | Theorem
6.3 | df-clel 2133 |
[Quine] p. 41 | Theorem
6.4 | eqid 2137 |
[Quine] p. 41 | Theorem
6.5 | eqcom 2139 |
[Quine] p. 42 | Theorem
6.6 | df-sbc 2905 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 2906 dfsbcq2 2907 |
[Quine] p. 43 | Theorem
6.8 | vex 2684 |
[Quine] p. 43 | Theorem
6.9 | isset 2687 |
[Quine] p. 44 | Theorem
7.3 | spcgf 2763 spcgv 2768 spcimgf 2761 |
[Quine] p. 44 | Theorem
6.11 | spsbc 2915 spsbcd 2916 |
[Quine] p. 44 | Theorem
6.12 | elex 2692 |
[Quine] p. 44 | Theorem
6.13 | elab 2823 elabg 2825 elabgf 2821 |
[Quine] p. 44 | Theorem
6.14 | noel 3362 |
[Quine] p. 48 | Theorem
7.2 | snprc 3583 |
[Quine] p. 48 | Definition
7.1 | df-pr 3529 df-sn 3528 |
[Quine] p. 49 | Theorem
7.4 | snss 3644 snssg 3651 |
[Quine] p. 49 | Theorem
7.5 | prss 3671 prssg 3672 |
[Quine] p. 49 | Theorem
7.6 | prid1 3624 prid1g 3622 prid2 3625 prid2g 3623 snid 3551
snidg 3549 |
[Quine] p. 51 | Theorem
7.12 | snexg 4103 snexprc 4105 |
[Quine] p. 51 | Theorem
7.13 | prexg 4128 |
[Quine] p. 53 | Theorem
8.2 | unisn 3747 unisng 3748 |
[Quine] p. 53 | Theorem
8.3 | uniun 3750 |
[Quine] p. 54 | Theorem
8.6 | elssuni 3759 |
[Quine] p. 54 | Theorem
8.7 | uni0 3758 |
[Quine] p. 56 | Theorem
8.17 | uniabio 5093 |
[Quine] p. 56 | Definition
8.18 | dfiota2 5084 |
[Quine] p. 57 | Theorem
8.19 | iotaval 5094 |
[Quine] p. 57 | Theorem
8.22 | iotanul 5098 |
[Quine] p. 58 | Theorem
8.23 | euiotaex 5099 |
[Quine] p. 58 | Definition
9.1 | df-op 3531 |
[Quine] p. 61 | Theorem
9.5 | opabid 4174 opelopab 4188 opelopaba 4183 opelopabaf 4190 opelopabf 4191 opelopabg 4185 opelopabga 4180 oprabid 5796 |
[Quine] p. 64 | Definition
9.11 | df-xp 4540 |
[Quine] p. 64 | Definition
9.12 | df-cnv 4542 |
[Quine] p. 64 | Definition
9.15 | df-id 4210 |
[Quine] p. 65 | Theorem
10.3 | fun0 5176 |
[Quine] p. 65 | Theorem
10.4 | funi 5150 |
[Quine] p. 65 | Theorem
10.5 | funsn 5166 funsng 5164 |
[Quine] p. 65 | Definition
10.1 | df-fun 5120 |
[Quine] p. 65 | Definition
10.2 | args 4903 dffv4g 5411 |
[Quine] p. 68 | Definition
10.11 | df-fv 5126 fv2 5409 |
[Quine] p. 124 | Theorem
17.3 | nn0opth2 10463 nn0opth2d 10462 nn0opthd 10461 |
[Quine] p. 284 | Axiom
39(vi) | funimaex 5203 funimaexg 5202 |
[Rudin] p. 164 | Equation
27 | efcan 11371 |
[Rudin] p. 164 | Equation
30 | efzval 11378 |
[Rudin] p. 167 | Equation
48 | absefi 11464 |
[Sanford] p.
39 | Remark | ax-mp 5 |
[Sanford] p. 39 | Rule
3 | mtpxor 1404 |
[Sanford] p. 39 | Rule
4 | mptxor 1402 |
[Sanford] p. 40 | Rule
1 | mptnan 1401 |
[Schechter] p.
51 | Definition of antisymmetry | intasym 4918 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 4920 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 4917 |
[Schechter] p.
51 | Definition of transitivity | cotr 4915 |
[Schechter] p.
428 | Definition 15.35 | bastop1 12241 |
[Stoll] p. 13 | Definition
of symmetric difference | symdif1 3336 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 3429 dif0 3428 |
[Stoll] p. 16 | Exercise
4.8 | difdifdirss 3442 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 3329 |
[Stoll] p. 19 | Theorem
5.2(13') | indmss 3330 |
[Stoll] p.
20 | Remark | invdif 3313 |
[Stoll] p. 25 | Definition
of ordered triple | df-ot 3532 |
[Stoll] p.
43 | Definition | uniiun 3861 |
[Stoll] p.
44 | Definition | intiin 3862 |
[Stoll] p.
45 | Definition | df-iin 3811 |
[Stoll] p. 45 | Definition
indexed union | df-iun 3810 |
[Stoll] p. 176 | Theorem
3.4(27) | imandc 874 imanst 873 |
[Stoll] p. 262 | Example
4.1 | symdif1 3336 |
[Suppes] p. 22 | Theorem
2 | eq0 3376 |
[Suppes] p. 22 | Theorem
4 | eqss 3107 eqssd 3109 eqssi 3108 |
[Suppes] p. 23 | Theorem
5 | ss0 3398 ss0b 3397 |
[Suppes] p. 23 | Theorem
6 | sstr 3100 |
[Suppes] p. 25 | Theorem
12 | elin 3254 elun 3212 |
[Suppes] p. 26 | Theorem
15 | inidm 3280 |
[Suppes] p. 26 | Theorem
16 | in0 3392 |
[Suppes] p. 27 | Theorem
23 | unidm 3214 |
[Suppes] p. 27 | Theorem
24 | un0 3391 |
[Suppes] p. 27 | Theorem
25 | ssun1 3234 |
[Suppes] p. 27 | Theorem
26 | ssequn1 3241 |
[Suppes] p. 27 | Theorem
27 | unss 3245 |
[Suppes] p. 27 | Theorem
28 | indir 3320 |
[Suppes] p. 27 | Theorem
29 | undir 3321 |
[Suppes] p. 28 | Theorem
32 | difid 3426 difidALT 3427 |
[Suppes] p. 29 | Theorem
33 | difin 3308 |
[Suppes] p. 29 | Theorem
34 | indif 3314 |
[Suppes] p. 29 | Theorem
35 | undif1ss 3432 |
[Suppes] p. 29 | Theorem
36 | difun2 3437 |
[Suppes] p. 29 | Theorem
37 | difin0 3431 |
[Suppes] p. 29 | Theorem
38 | disjdif 3430 |
[Suppes] p. 29 | Theorem
39 | difundi 3323 |
[Suppes] p. 29 | Theorem
40 | difindiss 3325 |
[Suppes] p. 30 | Theorem
41 | nalset 4053 |
[Suppes] p. 39 | Theorem
61 | uniss 3752 |
[Suppes] p. 39 | Theorem
65 | uniop 4172 |
[Suppes] p. 41 | Theorem
70 | intsn 3801 |
[Suppes] p. 42 | Theorem
71 | intpr 3798 intprg 3799 |
[Suppes] p. 42 | Theorem
73 | op1stb 4394 op1stbg 4395 |
[Suppes] p. 42 | Theorem
78 | intun 3797 |
[Suppes] p. 44 | Definition
15(a) | dfiun2 3842 dfiun2g 3840 |
[Suppes] p. 44 | Definition
15(b) | dfiin2 3843 |
[Suppes] p. 47 | Theorem
86 | elpw 3511 elpw2 4077 elpw2g 4076 elpwg 3513 |
[Suppes] p. 47 | Theorem
87 | pwid 3520 |
[Suppes] p. 47 | Theorem
89 | pw0 3662 |
[Suppes] p. 48 | Theorem
90 | pwpw0ss 3726 |
[Suppes] p. 52 | Theorem
101 | xpss12 4641 |
[Suppes] p. 52 | Theorem
102 | xpindi 4669 xpindir 4670 |
[Suppes] p. 52 | Theorem
103 | xpundi 4590 xpundir 4591 |
[Suppes] p. 54 | Theorem
105 | elirrv 4458 |
[Suppes] p. 58 | Theorem
2 | relss 4621 |
[Suppes] p. 59 | Theorem
4 | eldm 4731 eldm2 4732 eldm2g 4730 eldmg 4729 |
[Suppes] p. 59 | Definition
3 | df-dm 4544 |
[Suppes] p. 60 | Theorem
6 | dmin 4742 |
[Suppes] p. 60 | Theorem
8 | rnun 4942 |
[Suppes] p. 60 | Theorem
9 | rnin 4943 |
[Suppes] p. 60 | Definition
4 | dfrn2 4722 |
[Suppes] p. 61 | Theorem
11 | brcnv 4717 brcnvg 4715 |
[Suppes] p. 62 | Equation
5 | elcnv 4711 elcnv2 4712 |
[Suppes] p. 62 | Theorem
12 | relcnv 4912 |
[Suppes] p. 62 | Theorem
15 | cnvin 4941 |
[Suppes] p. 62 | Theorem
16 | cnvun 4939 |
[Suppes] p. 63 | Theorem
20 | co02 5047 |
[Suppes] p. 63 | Theorem
21 | dmcoss 4803 |
[Suppes] p. 63 | Definition
7 | df-co 4543 |
[Suppes] p. 64 | Theorem
26 | cnvco 4719 |
[Suppes] p. 64 | Theorem
27 | coass 5052 |
[Suppes] p. 65 | Theorem
31 | resundi 4827 |
[Suppes] p. 65 | Theorem
34 | elima 4881 elima2 4882 elima3 4883 elimag 4880 |
[Suppes] p. 65 | Theorem
35 | imaundi 4946 |
[Suppes] p. 66 | Theorem
40 | dminss 4948 |
[Suppes] p. 66 | Theorem
41 | imainss 4949 |
[Suppes] p. 67 | Exercise
11 | cnvxp 4952 |
[Suppes] p. 81 | Definition
34 | dfec2 6425 |
[Suppes] p. 82 | Theorem
72 | elec 6461 elecg 6460 |
[Suppes] p. 82 | Theorem
73 | erth 6466 erth2 6467 |
[Suppes] p. 89 | Theorem
96 | map0b 6574 |
[Suppes] p. 89 | Theorem
97 | map0 6576 map0g 6575 |
[Suppes] p. 89 | Theorem
98 | mapsn 6577 |
[Suppes] p. 89 | Theorem
99 | mapss 6578 |
[Suppes] p. 92 | Theorem
1 | enref 6652 enrefg 6651 |
[Suppes] p. 92 | Theorem
2 | ensym 6668 ensymb 6667 ensymi 6669 |
[Suppes] p. 92 | Theorem
3 | entr 6671 |
[Suppes] p. 92 | Theorem
4 | unen 6703 |
[Suppes] p. 94 | Theorem
15 | endom 6650 |
[Suppes] p. 94 | Theorem
16 | ssdomg 6665 |
[Suppes] p. 94 | Theorem
17 | domtr 6672 |
[Suppes] p. 95 | Theorem
18 | isbth 6848 |
[Suppes] p. 98 | Exercise
4 | fundmen 6693 fundmeng 6694 |
[Suppes] p. 98 | Exercise
6 | xpdom3m 6721 |
[Suppes] p.
130 | Definition 3 | df-tr 4022 |
[Suppes] p. 132 | Theorem
9 | ssonuni 4399 |
[Suppes] p.
134 | Definition 6 | df-suc 4288 |
[Suppes] p. 136 | Theorem
Schema 22 | findes 4512 finds 4509 finds1 4511 finds2 4510 |
[Suppes] p.
162 | Definition 5 | df-ltnqqs 7154 df-ltpq 7147 |
[Suppes] p. 228 | Theorem
Schema 61 | onintss 4307 |
[TakeutiZaring] p.
8 | Axiom 1 | ax-ext 2119 |
[TakeutiZaring] p.
13 | Definition 4.5 | df-cleq 2130 |
[TakeutiZaring] p.
13 | Proposition 4.6 | df-clel 2133 |
[TakeutiZaring] p.
13 | Proposition 4.9 | cvjust 2132 |
[TakeutiZaring] p.
13 | Proposition 4.7(3) | eqtr 2155 |
[TakeutiZaring] p.
14 | Definition 4.16 | df-oprab 5771 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 2903 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 3543 elpr2 3544 elprg 3542 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 3538 elsn2 3554 elsn2g 3553 elsng 3537 velsn 3539 |
[TakeutiZaring] p.
15 | Exercise 3 | elop 4148 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 3533 sneqr 3682 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 3541 dfsn2 3536 |
[TakeutiZaring] p.
16 | Axiom 3 | uniex 4354 |
[TakeutiZaring] p.
16 | Exercise 6 | opth 4154 |
[TakeutiZaring] p.
16 | Exercise 8 | rext 4132 |
[TakeutiZaring] p.
16 | Corollary 5.8 | unex 4357 unexg 4359 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 3567 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 3732 |
[TakeutiZaring] p.
16 | Definition 5.6 | df-in 3072 df-un 3070 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 3745 uniprg 3746 |
[TakeutiZaring] p.
17 | Axiom 4 | vpwex 4098 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 3566 |
[TakeutiZaring] p.
17 | Exercise 5 | elsuc 4323 elsucg 4321 sstr2 3099 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3215 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 3263 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3228 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 3281 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 3318 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 3319 |
[TakeutiZaring] p.
17 | Definition 5.9 | dfss2 3081 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 3507 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 3242 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3079 sseqin2 3290 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3112 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 3291 inss2 3292 |
[TakeutiZaring] p.
18 | Exercise 13 | nssr 3152 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 3740 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 4133 |
[TakeutiZaring] p.
18 | Exercise 19 | pweqb 4140 |
[TakeutiZaring] p.
20 | Definition | df-rab 2423 |
[TakeutiZaring] p.
20 | Corollary 5.16 | 0ex 4050 |
[TakeutiZaring] p.
20 | Definition 5.12 | df-dif 3068 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 3360 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 3426 difidALT 3427 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0rf 3370 |
[TakeutiZaring] p.
21 | Theorem 5.22 | setind 4449 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 2683 |
[TakeutiZaring] p.
21 | Proposition 5.21 | vprc 4055 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 3396 |
[TakeutiZaring] p.
22 | Exercise 3 | ssex 4060 ssexg 4062 |
[TakeutiZaring] p.
22 | Exercise 4 | inex1 4057 |
[TakeutiZaring] p.
22 | Exercise 5 | ruv 4460 |
[TakeutiZaring] p.
22 | Exercise 6 | elirr 4451 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0im 3422 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3196 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3ss 3332 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3197 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3205 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 2419 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 2420 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 4649 xpexg 4648 xpexgALT 6024 |
[TakeutiZaring] p.
23 | Definition 6.4(1) | df-rel 4541 |
[TakeutiZaring] p.
23 | Definition 6.4(2) | fun2cnv 5182 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1cnvcnv 5334 fun11 5185 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 5129 svrelfun 5183 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 4721 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 4723 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 4546 |
[TakeutiZaring] p.
24 | Definition 6.6(2) | df-ima 4547 |
[TakeutiZaring] p.
24 | Definition 6.6(3) | df-co 4543 |
[TakeutiZaring] p.
25 | Exercise 2 | cnvcnvss 4988 dfrel2 4984 |
[TakeutiZaring] p.
25 | Exercise 3 | xpss 4642 |
[TakeutiZaring] p.
25 | Exercise 5 | relun 4651 |
[TakeutiZaring] p.
25 | Exercise 6 | reluni 4657 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 4668 |
[TakeutiZaring] p.
25 | Exercise 12 | relres 4842 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 4819 opelresg 4821 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 4835 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 4838 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 4843 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 5159 |
[TakeutiZaring] p.
25 | Exercise 24 | relco 5032 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 5158 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 5335 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2041 |
[TakeutiZaring] p.
26 | Definition 6.11 | df-fv 5126 fv3 5437 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 5072 cnvexg 5071 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 4800 dmexg 4798 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 4801 rnexg 4799 |
[TakeutiZaring] p.
27 | Corollary 6.13 | funfvex 5431 |
[TakeutiZaring] p.
27 | Theorem 6.12(1) | tz6.12-1 5441 tz6.12 5442 tz6.12c 5444 |
[TakeutiZaring] p.
27 | Theorem 6.12(2) | tz6.12-2 5405 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 5121 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 5122 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 5124 wfo 5116 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 5123 wf1 5115 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 5125 wf1o 5117 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 5511 eqfnfv2 5512 eqfnfv2f 5515 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 5484 |
[TakeutiZaring] p.
28 | Theorem 6.16(1) | fnex 5635 fnexALT 6004 |
[TakeutiZaring] p.
28 | Proposition 6.17 | resfunexg 5634 resfunexgALT 6001 |
[TakeutiZaring] p.
29 | Exercise 9 | funimaex 5203 funimaexg 5202 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 3925 |
[TakeutiZaring] p.
30 | Definition 6.21 | eliniseg 4904 iniseg 4906 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 4206 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-isom 5127 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 5704 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 5705 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 5710 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 5712 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 5720 |
[TakeutiZaring] p.
35 | Notation | wtr 4021 |
[TakeutiZaring] p.
35 | Theorem 7.2 | tz7.2 4271 |
[TakeutiZaring] p.
35 | Definition 7.1 | dftr3 4025 |
[TakeutiZaring] p.
36 | Proposition 7.4 | ordwe 4485 |
[TakeutiZaring] p.
36 | Proposition 7.6 | ordelord 4298 |
[TakeutiZaring] p.
37 | Proposition 7.9 | ordin 4302 |
[TakeutiZaring] p.
38 | Corollary 7.15 | ordsson 4403 |
[TakeutiZaring] p.
38 | Definition 7.11 | df-on 4285 |
[TakeutiZaring] p.
38 | Proposition 7.12 | ordon 4397 |
[TakeutiZaring] p.
38 | Proposition 7.13 | onprc 4462 |
[TakeutiZaring] p.
39 | Theorem 7.17 | tfi 4491 |
[TakeutiZaring] p.
40 | Exercise 7 | dftr2 4023 |
[TakeutiZaring] p.
40 | Exercise 11 | unon 4422 |
[TakeutiZaring] p.
40 | Proposition 7.19 | ssorduni 4398 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 3759 |
[TakeutiZaring] p.
41 | Definition 7.22 | df-suc 4288 |
[TakeutiZaring] p.
41 | Proposition 7.23 | sssucid 4332 sucidg 4333 |
[TakeutiZaring] p.
41 | Proposition 7.24 | suceloni 4412 |
[TakeutiZaring] p.
42 | Exercise 1 | df-ilim 4286 |
[TakeutiZaring] p.
42 | Exercise 8 | onsucssi 4417 ordelsuc 4416 |
[TakeutiZaring] p.
42 | Proposition 7.30(1) | peano1 4503 |
[TakeutiZaring] p.
42 | Proposition 7.30(2) | peano2 4504 |
[TakeutiZaring] p.
42 | Proposition 7.30(3) | peano3 4505 |
[TakeutiZaring] p.
43 | Axiom 7 | omex 4502 |
[TakeutiZaring] p.
43 | Theorem 7.32 | ordom 4515 |
[TakeutiZaring] p.
43 | Corollary 7.31 | find 4508 |
[TakeutiZaring] p.
43 | Proposition 7.30(4) | peano4 4506 |
[TakeutiZaring] p.
43 | Proposition 7.30(5) | peano5 4507 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 3780 |
[TakeutiZaring] p.
44 | Exercise 3 | trintssm 4037 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 3781 |
[TakeutiZaring] p.
44 | Exercise 6 | onintonm 4428 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 3767 |
[TakeutiZaring] p.
47 | Lemma 1 | tfrlem1 6198 |
[TakeutiZaring] p.
47 | Theorem 7.41(1) | tfri1 6255 tfri1d 6225 |
[TakeutiZaring] p.
47 | Theorem 7.41(2) | tfri2 6256 tfri2d 6226 |
[TakeutiZaring] p.
47 | Theorem 7.41(3) | tfri3 6257 |
[TakeutiZaring] p.
50 | Exercise 3 | smoiso 6192 |
[TakeutiZaring] p.
50 | Definition 7.46 | df-smo 6176 |
[TakeutiZaring] p.
56 | Definition 8.1 | oasuc 6353 |
[TakeutiZaring] p.
57 | Proposition 8.2 | oacl 6349 |
[TakeutiZaring] p.
57 | Proposition 8.3 | oa0 6346 |
[TakeutiZaring] p.
57 | Proposition 8.16 | omcl 6350 |
[TakeutiZaring] p.
58 | Proposition 8.4 | nnaord 6398 nnaordi 6397 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 3853 uniss2 3762 |
[TakeutiZaring] p.
59 | Proposition 8.7 | oawordriexmid 6359 |
[TakeutiZaring] p.
59 | Proposition 8.9 | nnacl 6369 |
[TakeutiZaring] p.
62 | Exercise 5 | oaword1 6360 |
[TakeutiZaring] p.
62 | Definition 8.15 | om0 6347 omsuc 6361 |
[TakeutiZaring] p.
63 | Proposition 8.17 | nnmcl 6370 |
[TakeutiZaring] p.
63 | Proposition 8.19 | nnmord 6406 nnmordi 6405 |
[TakeutiZaring] p.
67 | Definition 8.30 | oei0 6348 |
[TakeutiZaring] p.
85 | Proposition 10.6(3) | cardonle 7036 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 6682 |
[TakeutiZaring] p.
90 | Proposition 10.20 | nneneq 6744 |
[TakeutiZaring] p.
90 | Corollary 10.21(1) | php5 6745 |
[TakeutiZaring] p.
91 | Definition 10.29 | df-fin 6630 isfi 6648 |
[TakeutiZaring] p.
92 | Proposition 10.33(2) | xpdom2 6718 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 6537 |
[TakeutiZaring] p.
96 | Proposition 10.45 | mapxpen 6735 |
[Tarski] p. 67 | Axiom
B5 | ax-4 1487 |
[Tarski] p. 68 | Lemma
6 | equid 1677 |
[Tarski] p. 69 | Lemma
7 | equcomi 1680 |
[Tarski] p. 70 | Lemma
14 | spim 1716 spime 1719 spimeh 1717 spimh 1715 |
[Tarski] p. 70 | Lemma
16 | ax-11 1484 ax-11o 1795 ax11i 1692 |
[Tarski] p. 70 | Lemmas 16
and 17 | sb6 1858 |
[Tarski] p. 77 | Axiom B6
(p. 75) of system S2 | ax-17 1506 |
[Tarski] p. 77 | Axiom B8
(p. 75) of system S2 | ax-13 1491 ax-14 1492 |
[WhiteheadRussell] p.
96 | Axiom *1.3 | olc 700 |
[WhiteheadRussell] p.
96 | Axiom *1.4 | pm1.4 716 |
[WhiteheadRussell] p.
96 | Axiom *1.2 (Taut) | pm1.2 745 |
[WhiteheadRussell] p.
96 | Axiom *1.5 (Assoc) | pm1.5 754 |
[WhiteheadRussell] p.
97 | Axiom *1.6 (Sum) | orim2 778 |
[WhiteheadRussell] p.
100 | Theorem *2.01 | pm2.01 605 |
[WhiteheadRussell] p.
100 | Theorem *2.02 | ax-1 6 |
[WhiteheadRussell] p.
100 | Theorem *2.03 | con2 632 |
[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 822 |
[WhiteheadRussell] p.
101 | Theorem *2.06 | barbara 2095 syl 14 |
[WhiteheadRussell] p.
101 | Theorem *2.07 | pm2.07 726 |
[WhiteheadRussell] p.
101 | Theorem *2.08 | id 19 idALT 20 |
[WhiteheadRussell] p.
101 | Theorem *2.11 | exmiddc 821 |
[WhiteheadRussell] p.
101 | Theorem *2.12 | notnot 618 |
[WhiteheadRussell] p.
101 | Theorem *2.13 | pm2.13dc 870 |
[WhiteheadRussell] p.
102 | Theorem *2.14 | notnotrdc 828 |
[WhiteheadRussell] p.
102 | Theorem *2.15 | con1dc 841 |
[WhiteheadRussell] p.
103 | Theorem *2.16 | con3 631 |
[WhiteheadRussell] p.
103 | Theorem *2.17 | condc 838 |
[WhiteheadRussell] p.
103 | Theorem *2.18 | pm2.18dc 840 |
[WhiteheadRussell] p.
104 | Theorem *2.2 | orc 701 |
[WhiteheadRussell] p.
104 | Theorem *2.3 | pm2.3 764 |
[WhiteheadRussell] p.
104 | Theorem *2.21 | pm2.21 606 |
[WhiteheadRussell] p.
104 | Theorem *2.24 | pm2.24 610 |
[WhiteheadRussell] p.
104 | Theorem *2.25 | pm2.25dc 878 |
[WhiteheadRussell] p.
104 | Theorem *2.26 | pm2.26dc 892 |
[WhiteheadRussell] p.
104 | Theorem *2.27 | pm2.27 40 |
[WhiteheadRussell] p.
104 | Theorem *2.31 | pm2.31 757 |
[WhiteheadRussell] p.
105 | Theorem *2.32 | pm2.32 758 |
[WhiteheadRussell] p.
105 | Theorem *2.36 | pm2.36 793 |
[WhiteheadRussell] p.
105 | Theorem *2.37 | pm2.37 794 |
[WhiteheadRussell] p.
105 | Theorem *2.38 | pm2.38 792 |
[WhiteheadRussell] p.
105 | Definition *2.33 | df-3or 963 |
[WhiteheadRussell] p.
106 | Theorem *2.4 | pm2.4 767 |
[WhiteheadRussell] p.
106 | Theorem *2.41 | pm2.41 765 |
[WhiteheadRussell] p.
106 | Theorem *2.42 | pm2.42 766 |
[WhiteheadRussell] p.
106 | Theorem *2.43 | pm2.43 53 |
[WhiteheadRussell] p.
106 | Theorem *2.45 | pm2.45 727 |
[WhiteheadRussell] p.
106 | Theorem *2.46 | pm2.46 728 |
[WhiteheadRussell] p.
107 | Theorem *2.5 | pm2.5dc 852 pm2.5gdc 851 |
[WhiteheadRussell] p.
107 | Theorem *2.6 | pm2.6dc 847 |
[WhiteheadRussell] p.
107 | Theorem *2.47 | pm2.47 729 |
[WhiteheadRussell] p.
107 | Theorem *2.48 | pm2.48 730 |
[WhiteheadRussell] p.
107 | Theorem *2.49 | pm2.49 731 |
[WhiteheadRussell] p.
107 | Theorem *2.51 | pm2.51 644 |
[WhiteheadRussell] p.
107 | Theorem *2.52 | pm2.52 645 |
[WhiteheadRussell] p.
107 | Theorem *2.53 | pm2.53 711 |
[WhiteheadRussell] p.
107 | Theorem *2.54 | pm2.54dc 876 |
[WhiteheadRussell] p.
107 | Theorem *2.55 | orel1 714 |
[WhiteheadRussell] p.
107 | Theorem *2.56 | orel2 715 |
[WhiteheadRussell] p.
107 | Theorem *2.61 | pm2.61dc 850 |
[WhiteheadRussell] p.
107 | Theorem *2.62 | pm2.62 737 |
[WhiteheadRussell] p.
107 | Theorem *2.63 | pm2.63 789 |
[WhiteheadRussell] p.
107 | Theorem *2.64 | pm2.64 790 |
[WhiteheadRussell] p.
107 | Theorem *2.65 | pm2.65 648 |
[WhiteheadRussell] p.
107 | Theorem *2.67 | pm2.67-2 702 pm2.67 732 |
[WhiteheadRussell] p.
107 | Theorem *2.521 | pm2.521dc 854 pm2.521gdc 853 |
[WhiteheadRussell] p.
107 | Theorem *2.621 | pm2.621 736 |
[WhiteheadRussell] p.
108 | Theorem *2.8 | pm2.8 799 |
[WhiteheadRussell] p.
108 | Theorem *2.68 | pm2.68dc 879 |
[WhiteheadRussell] p.
108 | Theorem *2.69 | looinvdc 900 |
[WhiteheadRussell] p.
108 | Theorem *2.73 | pm2.73 795 |
[WhiteheadRussell] p.
108 | Theorem *2.74 | pm2.74 796 |
[WhiteheadRussell] p.
108 | Theorem *2.75 | pm2.75 798 |
[WhiteheadRussell] p.
108 | Theorem *2.76 | pm2.76 797 |
[WhiteheadRussell] p.
108 | Theorem *2.77 | ax-2 7 |
[WhiteheadRussell] p.
108 | Theorem *2.81 | pm2.81 800 |
[WhiteheadRussell] p.
108 | Theorem *2.82 | pm2.82 801 |
[WhiteheadRussell] p.
108 | Theorem *2.83 | pm2.83 77 |
[WhiteheadRussell] p.
108 | Theorem *2.85 | pm2.85dc 890 |
[WhiteheadRussell] p.
108 | Theorem *2.86 | pm2.86 100 |
[WhiteheadRussell] p.
111 | Theorem *3.1 | pm3.1 743 |
[WhiteheadRussell] p.
111 | Theorem *3.2 | pm3.2 138 |
[WhiteheadRussell] p.
111 | Theorem *3.11 | pm3.11dc 941 |
[WhiteheadRussell] p.
111 | Theorem *3.12 | pm3.12dc 942 |
[WhiteheadRussell] p.
111 | Theorem *3.13 | pm3.13dc 943 |
[WhiteheadRussell] p.
111 | Theorem *3.14 | pm3.14 742 |
[WhiteheadRussell] p.
111 | Theorem *3.21 | pm3.21 262 |
[WhiteheadRussell] p.
111 | Theorem *3.22 | pm3.22 263 |
[WhiteheadRussell] p.
111 | Theorem *3.24 | pm3.24 682 |
[WhiteheadRussell] p.
112 | Theorem *3.35 | pm3.35 344 |
[WhiteheadRussell] p.
112 | Theorem *3.3 (Exp) | pm3.3 259 |
[WhiteheadRussell] p.
112 | Theorem *3.31 (Imp) | pm3.31 260 |
[WhiteheadRussell] p.
112 | Theorem *3.26 (Simp) | simpl 108 simplimdc 845 |
[WhiteheadRussell] p.
112 | Theorem *3.27 (Simp) | simpr 109 simprimdc 844 |
[WhiteheadRussell] p.
112 | Theorem *3.33 (Syll) | pm3.33 342 |
[WhiteheadRussell] p.
112 | Theorem *3.34 (Syll) | pm3.34 343 |
[WhiteheadRussell] p.
112 | Theorem *3.37 (Transp) | pm3.37 678 |
[WhiteheadRussell] p.
113 | Fact) | pm3.45 586 |
[WhiteheadRussell] p.
113 | Theorem *3.4 | pm3.4 331 |
[WhiteheadRussell] p.
113 | Theorem *3.41 | pm3.41 329 |
[WhiteheadRussell] p.
113 | Theorem *3.42 | pm3.42 330 |
[WhiteheadRussell] p.
113 | Theorem *3.44 | jao 744 pm3.44 704 |
[WhiteheadRussell] p.
113 | Theorem *3.47 | anim12 341 |
[WhiteheadRussell] p.
113 | Theorem *3.43 (Comp) | pm3.43 591 |
[WhiteheadRussell] p.
114 | Theorem *3.48 | pm3.48 774 |
[WhiteheadRussell] p.
116 | Theorem *4.1 | con34bdc 856 |
[WhiteheadRussell] p.
117 | Theorem *4.2 | biid 170 |
[WhiteheadRussell] p.
117 | Theorem *4.13 | notnotbdc 857 |
[WhiteheadRussell] p.
117 | Theorem *4.14 | pm4.14dc 875 |
[WhiteheadRussell] p.
117 | Theorem *4.15 | pm4.15 683 |
[WhiteheadRussell] p.
117 | Theorem *4.21 | bicom 139 |
[WhiteheadRussell] p.
117 | Theorem *4.22 | biantr 936 bitr 463 |
[WhiteheadRussell] p.
117 | Theorem *4.24 | pm4.24 392 |
[WhiteheadRussell] p.
117 | Theorem *4.25 | oridm 746 pm4.25 747 |
[WhiteheadRussell] p.
118 | Theorem *4.3 | ancom 264 |
[WhiteheadRussell] p.
118 | Theorem *4.4 | andi 807 |
[WhiteheadRussell] p.
118 | Theorem *4.31 | orcom 717 |
[WhiteheadRussell] p.
118 | Theorem *4.32 | anass 398 |
[WhiteheadRussell] p.
118 | Theorem *4.33 | orass 756 |
[WhiteheadRussell] p.
118 | Theorem *4.36 | anbi1 461 |
[WhiteheadRussell] p.
118 | Theorem *4.37 | orbi1 781 |
[WhiteheadRussell] p.
118 | Theorem *4.38 | pm4.38 594 |
[WhiteheadRussell] p.
118 | Theorem *4.39 | pm4.39 811 |
[WhiteheadRussell] p.
118 | Definition *4.34 | df-3an 964 |
[WhiteheadRussell] p.
119 | Theorem *4.41 | ordi 805 |
[WhiteheadRussell] p.
119 | Theorem *4.42 | pm4.42r 955 |
[WhiteheadRussell] p.
119 | Theorem *4.43 | pm4.43 933 |
[WhiteheadRussell] p.
119 | Theorem *4.44 | pm4.44 768 |
[WhiteheadRussell] p.
119 | Theorem *4.45 | orabs 803 pm4.45 773 pm4.45im 332 |
[WhiteheadRussell] p.
119 | Theorem *10.22 | 19.26 1457 |
[WhiteheadRussell] p.
120 | Theorem *4.5 | anordc 940 |
[WhiteheadRussell] p.
120 | Theorem *4.6 | imordc 882 imorr 710 |
[WhiteheadRussell] p.
120 | Theorem *4.7 | anclb 317 |
[WhiteheadRussell] p.
120 | Theorem *4.51 | ianordc 884 |
[WhiteheadRussell] p.
120 | Theorem *4.52 | pm4.52im 739 |
[WhiteheadRussell] p.
120 | Theorem *4.53 | pm4.53r 740 |
[WhiteheadRussell] p.
120 | Theorem *4.54 | pm4.54dc 887 |
[WhiteheadRussell] p.
120 | Theorem *4.55 | pm4.55dc 922 |
[WhiteheadRussell] p.
120 | Theorem *4.56 | ioran 741 pm4.56 769 |
[WhiteheadRussell] p.
120 | Theorem *4.57 | orandc 923 oranim 770 |
[WhiteheadRussell] p.
120 | Theorem *4.61 | annimim 675 |
[WhiteheadRussell] p.
120 | Theorem *4.62 | pm4.62dc 883 |
[WhiteheadRussell] p.
120 | Theorem *4.63 | pm4.63dc 871 |
[WhiteheadRussell] p.
120 | Theorem *4.64 | pm4.64dc 885 |
[WhiteheadRussell] p.
120 | Theorem *4.65 | pm4.65r 676 |
[WhiteheadRussell] p.
120 | Theorem *4.66 | pm4.66dc 886 |
[WhiteheadRussell] p.
120 | Theorem *4.67 | pm4.67dc 872 |
[WhiteheadRussell] p.
120 | Theorem *4.71 | pm4.71 386 pm4.71d 390 pm4.71i 388 pm4.71r 387 pm4.71rd 391 pm4.71ri 389 |
[WhiteheadRussell] p.
121 | Theorem *4.72 | pm4.72 812 |
[WhiteheadRussell] p.
121 | Theorem *4.73 | iba 298 |
[WhiteheadRussell] p.
121 | Theorem *4.74 | biorf 733 |
[WhiteheadRussell] p.
121 | Theorem *4.76 | jcab 592 pm4.76 593 |
[WhiteheadRussell] p.
121 | Theorem *4.77 | jaob 699 pm4.77 788 |
[WhiteheadRussell] p.
121 | Theorem *4.78 | pm4.78i 771 |
[WhiteheadRussell] p.
121 | Theorem *4.79 | pm4.79dc 888 |
[WhiteheadRussell] p.
122 | Theorem *4.8 | pm4.8 696 |
[WhiteheadRussell] p.
122 | Theorem *4.81 | pm4.81dc 893 |
[WhiteheadRussell] p.
122 | Theorem *4.82 | pm4.82 934 |
[WhiteheadRussell] p.
122 | Theorem *4.83 | pm4.83dc 935 |
[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 261 pm4.87 546 |
[WhiteheadRussell] p.
123 | Theorem *5.1 | pm5.1 590 |
[WhiteheadRussell] p.
123 | Theorem *5.11 | pm5.11dc 894 |
[WhiteheadRussell] p.
123 | Theorem *5.12 | pm5.12dc 895 |
[WhiteheadRussell] p.
123 | Theorem *5.13 | pm5.13dc 897 |
[WhiteheadRussell] p.
123 | Theorem *5.14 | pm5.14dc 896 |
[WhiteheadRussell] p.
124 | Theorem *5.15 | pm5.15dc 1367 |
[WhiteheadRussell] p.
124 | Theorem *5.16 | pm5.16 813 |
[WhiteheadRussell] p.
124 | Theorem *5.17 | pm5.17dc 889 |
[WhiteheadRussell] p.
124 | Theorem *5.18 | nbbndc 1372 pm5.18dc 868 |
[WhiteheadRussell] p.
124 | Theorem *5.19 | pm5.19 695 |
[WhiteheadRussell] p.
124 | Theorem *5.21 | pm5.21 684 |
[WhiteheadRussell] p.
124 | Theorem *5.22 | xordc 1370 |
[WhiteheadRussell] p.
124 | Theorem *5.23 | dfbi3dc 1375 |
[WhiteheadRussell] p.
124 | Theorem *5.24 | pm5.24dc 1376 |
[WhiteheadRussell] p.
124 | Theorem *5.25 | dfor2dc 880 |
[WhiteheadRussell] p.
125 | Theorem *5.3 | pm5.3 466 |
[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 911 pm5.6r 912 |
[WhiteheadRussell] p.
125 | Theorem *5.7 | pm5.7dc 938 |
[WhiteheadRussell] p.
125 | Theorem *5.31 | pm5.31 345 |
[WhiteheadRussell] p.
125 | Theorem *5.32 | pm5.32 448 |
[WhiteheadRussell] p.
125 | Theorem *5.33 | pm5.33 598 |
[WhiteheadRussell] p.
125 | Theorem *5.35 | pm5.35 902 |
[WhiteheadRussell] p.
125 | Theorem *5.36 | pm5.36 599 |
[WhiteheadRussell] p.
125 | Theorem *5.41 | imdi 249 pm5.41 250 |
[WhiteheadRussell] p.
125 | Theorem *5.42 | pm5.42 318 |
[WhiteheadRussell] p.
125 | Theorem *5.44 | pm5.44 910 |
[WhiteheadRussell] p.
125 | Theorem *5.53 | pm5.53 791 |
[WhiteheadRussell] p.
125 | Theorem *5.54 | pm5.54dc 903 |
[WhiteheadRussell] p.
125 | Theorem *5.55 | pm5.55dc 898 |
[WhiteheadRussell] p.
125 | Theorem *5.61 | pm5.61 783 |
[WhiteheadRussell] p.
125 | Theorem *5.62 | pm5.62dc 929 |
[WhiteheadRussell] p.
125 | Theorem *5.63 | pm5.63dc 930 |
[WhiteheadRussell] p.
125 | Theorem *5.71 | pm5.71dc 945 |
[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 946 |
[WhiteheadRussell] p.
150 | Theorem *10.3 | alsyl 1614 |
[WhiteheadRussell] p.
160 | Theorem *11.21 | alrot3 1461 |
[WhiteheadRussell] p.
163 | Theorem *11.42 | 19.40-2 1611 |
[WhiteheadRussell] p.
164 | Theorem *11.53 | pm11.53 1867 |
[WhiteheadRussell] p.
175 | Definition *14.02 | df-eu 2000 |
[WhiteheadRussell] p.
178 | Theorem *13.18 | pm13.18 2387 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 2388 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 2817 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 2960 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 5101 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 5102 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2076 eupickbi 2079 |
[WhiteheadRussell] p.
235 | Definition *30.01 | df-fv 5126 |
[WhiteheadRussell] p.
360 | Theorem *54.43 | pm54.43 7039 |