Bibliographic Cross-Reference for the Intuitionistic Logic
Explorer
Bibliographic Reference |
Description | Intuitionistic Logic Explorer Page(s)
|
---|
[AczelRathjen], p.
71 | Definition 8.1.4 | enumct 7108 fidcenum 6949 |
[AczelRathjen], p.
72 | Proposition 8.1.11 | fidcenum 6949 |
[AczelRathjen], p.
73 | Lemma 8.1.14 | enumct 7108 |
[AczelRathjen], p.
73 | Corollary 8.1.13 | ennnfone 12409 |
[AczelRathjen], p.
74 | Lemma 8.1.16 | xpfi 6923 |
[AczelRathjen], p.
74 | Remark 8.1.17 | unfiexmid 6911 |
[AczelRathjen], p.
74 | Theorem 8.1.19 | ctiunct 12424 |
[AczelRathjen], p.
75 | Corollary 8.1.20 | unct 12426 |
[AczelRathjen], p.
75 | Corollary 8.1.23 | qnnen 12415 znnen 12382 |
[AczelRathjen], p.
77 | Lemma 8.1.27 | omctfn 12427 |
[AczelRathjen], p.
78 | Theorem 8.1.28 | omiunct 12428 |
[AczelRathjen], p.
80 | Corollary 8.2.4 | df-ihash 10740 |
[AczelRathjen], p.
183 | Chapter 20 | ax-setind 4533 |
[Apostol] p. 18 | Theorem
I.1 | addcan 8127 addcan2d 8132 addcan2i 8130 addcand 8131 addcani 8129 |
[Apostol] p. 18 | Theorem
I.2 | negeu 8138 |
[Apostol] p. 18 | Theorem
I.3 | negsub 8195 negsubd 8264 negsubi 8225 |
[Apostol] p. 18 | Theorem
I.4 | negneg 8197 negnegd 8249 negnegi 8217 |
[Apostol] p. 18 | Theorem
I.5 | subdi 8332 subdid 8361 subdii 8354 subdir 8333 subdird 8362 subdiri 8355 |
[Apostol] p. 18 | Theorem
I.6 | mul01 8336 mul01d 8340 mul01i 8338 mul02 8334 mul02d 8339 mul02i 8337 |
[Apostol] p. 18 | Theorem
I.9 | divrecapd 8739 |
[Apostol] p. 18 | Theorem
I.10 | recrecapi 8690 |
[Apostol] p. 18 | Theorem
I.12 | mul2neg 8345 mul2negd 8360 mul2negi 8353 mulneg1 8342 mulneg1d 8358 mulneg1i 8351 |
[Apostol] p. 18 | Theorem
I.15 | divdivdivap 8659 |
[Apostol] p. 20 | Axiom
7 | rpaddcl 9664 rpaddcld 9699 rpmulcl 9665 rpmulcld 9700 |
[Apostol] p. 20 | Axiom
9 | 0nrp 9676 |
[Apostol] p. 20 | Theorem
I.17 | lttri 8052 |
[Apostol] p. 20 | Theorem
I.18 | ltadd1d 8485 ltadd1dd 8503 ltadd1i 8449 |
[Apostol] p. 20 | Theorem
I.19 | ltmul1 8539 ltmul1a 8538 ltmul1i 8866 ltmul1ii 8874 ltmul2 8802 ltmul2d 9726 ltmul2dd 9740 ltmul2i 8869 |
[Apostol] p. 20 | Theorem
I.21 | 0lt1 8074 |
[Apostol] p. 20 | Theorem
I.23 | lt0neg1 8415 lt0neg1d 8462 ltneg 8409 ltnegd 8470 ltnegi 8440 |
[Apostol] p. 20 | Theorem
I.25 | lt2add 8392 lt2addd 8514 lt2addi 8457 |
[Apostol] p.
20 | Definition of positive numbers | df-rp 9641 |
[Apostol] p. 21 | Exercise
4 | recgt0 8796 recgt0d 8880 recgt0i 8852 recgt0ii 8853 |
[Apostol] p.
22 | Definition of integers | df-z 9243 |
[Apostol] p.
22 | Definition of rationals | df-q 9609 |
[Apostol] p. 24 | Theorem
I.26 | supeuti 6987 |
[Apostol] p. 26 | Theorem
I.29 | arch 9162 |
[Apostol] p. 28 | Exercise
2 | btwnz 9361 |
[Apostol] p. 28 | Exercise
3 | nnrecl 9163 |
[Apostol] p. 28 | Exercise
6 | qbtwnre 10243 |
[Apostol] p. 28 | Exercise
10(a) | zeneo 11859 zneo 9343 |
[Apostol] p. 29 | Theorem
I.35 | resqrtth 11024 sqrtthi 11112 |
[Apostol] p. 34 | Theorem
I.36 (principle of mathematical induction) | peano5nni 8911 |
[Apostol] p. 34 | Theorem
I.37 (well-ordering principle) | nnwodc 12020 |
[Apostol] p.
363 | Remark | absgt0api 11139 |
[Apostol] p.
363 | Example | abssubd 11186 abssubi 11143 |
[ApostolNT] p.
14 | Definition | df-dvds 11779 |
[ApostolNT] p.
14 | Theorem 1.1(a) | iddvds 11795 |
[ApostolNT] p.
14 | Theorem 1.1(b) | dvdstr 11819 |
[ApostolNT] p.
14 | Theorem 1.1(c) | dvds2ln 11815 |
[ApostolNT] p.
14 | Theorem 1.1(d) | dvdscmul 11809 |
[ApostolNT] p.
14 | Theorem 1.1(e) | dvdscmulr 11811 |
[ApostolNT] p.
14 | Theorem 1.1(f) | 1dvds 11796 |
[ApostolNT] p.
14 | Theorem 1.1(g) | dvds0 11797 |
[ApostolNT] p.
14 | Theorem 1.1(h) | 0dvds 11802 |
[ApostolNT] p.
14 | Theorem 1.1(i) | dvdsleabs 11834 |
[ApostolNT] p.
14 | Theorem 1.1(j) | dvdsabseq 11836 |
[ApostolNT] p.
14 | Theorem 1.1(k) | divconjdvds 11838 |
[ApostolNT] p.
15 | Definition | dfgcd2 11998 |
[ApostolNT] p.
16 | Definition | isprm2 12100 |
[ApostolNT] p.
16 | Theorem 1.5 | coprmdvds 12075 |
[ApostolNT] p.
16 | Theorem 1.7 | prminf 12439 |
[ApostolNT] p.
16 | Theorem 1.4(a) | gcdcom 11957 |
[ApostolNT] p.
16 | Theorem 1.4(b) | gcdass 11999 |
[ApostolNT] p.
16 | Theorem 1.4(c) | absmulgcd 12001 |
[ApostolNT] p.
16 | Theorem 1.4(d)1 | gcd1 11971 |
[ApostolNT] p.
16 | Theorem 1.4(d)2 | gcdid0 11964 |
[ApostolNT] p.
17 | Theorem 1.8 | coprm 12127 |
[ApostolNT] p.
17 | Theorem 1.9 | euclemma 12129 |
[ApostolNT] p.
17 | Theorem 1.10 | 1arith2 12349 |
[ApostolNT] p.
19 | Theorem 1.14 | divalg 11912 |
[ApostolNT] p.
20 | Theorem 1.15 | eucalg 12042 |
[ApostolNT] p.
25 | Definition | df-phi 12194 |
[ApostolNT] p.
26 | Theorem 2.2 | phisum 12223 |
[ApostolNT] p.
28 | Theorem 2.5(a) | phiprmpw 12205 |
[ApostolNT] p.
28 | Theorem 2.5(c) | phimul 12209 |
[ApostolNT] p.
104 | Definition | congr 12083 |
[ApostolNT] p.
106 | Remark | dvdsval3 11782 |
[ApostolNT] p.
106 | Definition | moddvds 11790 |
[ApostolNT] p.
107 | Example 2 | mod2eq0even 11866 |
[ApostolNT] p.
107 | Example 3 | mod2eq1n2dvds 11867 |
[ApostolNT] p.
107 | Example 4 | zmod1congr 10327 |
[ApostolNT] p.
107 | Theorem 5.2(b) | modqmul12d 10364 |
[ApostolNT] p.
107 | Theorem 5.2(c) | modqexp 10632 |
[ApostolNT] p.
108 | Theorem 5.3 | modmulconst 11814 |
[ApostolNT] p.
109 | Theorem 5.4 | cncongr1 12086 |
[ApostolNT] p.
109 | Theorem 5.4 "Cancellation law" | cncongr 12088 |
[ApostolNT] p.
113 | Theorem 5.17 | eulerth 12216 |
[ApostolNT] p.
113 | Theorem 5.18 | vfermltl 12234 |
[ApostolNT] p.
114 | Theorem 5.19 | fermltl 12217 |
[ApostolNT] p.
179 | Definition | df-lgs 14066 lgsprme0 14110 |
[ApostolNT] p.
180 | Example 1 | 1lgs 14111 |
[ApostolNT] p.
180 | Theorem 9.2 | lgsvalmod 14087 |
[ApostolNT] p.
180 | Theorem 9.3 | lgsdirprm 14102 |
[ApostolNT] p.
188 | Definition | df-lgs 14066 lgs1 14112 |
[ApostolNT] p.
188 | Theorem 9.9(a) | lgsdir 14103 |
[ApostolNT] p.
188 | Theorem 9.9(b) | lgsdi 14105 |
[ApostolNT] p.
188 | Theorem 9.9(c) | lgsmodeq 14113 |
[ApostolNT] p.
188 | Theorem 9.9(d) | lgsmulsqcoprm 14114 |
[Bauer] p. 482 | Section
1.2 | pm2.01 616 pm2.65 659 |
[Bauer] p. 483 | Theorem
1.3 | acexmid 5868 onsucelsucexmidlem 4525 |
[Bauer], p.
481 | Section 1.1 | pwtrufal 14403 |
[Bauer], p.
483 | Definition | n0rf 3435 |
[Bauer], p. 483 | Theorem
1.2 | 2irrexpq 14061 2irrexpqap 14063 |
[Bauer], p. 485 | Theorem
2.1 | ssfiexmid 6870 |
[Bauer], p. 494 | Theorem
5.5 | ivthinc 13788 |
[BauerHanson], p.
27 | Proposition 5.2 | cnstab 8592 |
[BauerSwan], p.
14 | Remark | 0ct 7100 ctm 7102 |
[BauerSwan],
p. 14 | Proposition 2.6 | subctctexmid 14406 |
[BauerSwan], p.
14 | Table" is defined as ` ` per | enumct 7108 |
[BauerTaylor], p.
32 | Lemma 6.16 | prarloclem 7491 |
[BauerTaylor], p.
50 | Lemma 11.4 | subhalfnqq 7404 |
[BauerTaylor], p.
52 | Proposition 11.15 | prarloc 7493 |
[BauerTaylor], p.
53 | Lemma 11.16 | addclpr 7527 addlocpr 7526 |
[BauerTaylor], p.
55 | Proposition 12.7 | appdivnq 7553 |
[BauerTaylor], p.
56 | Lemma 12.8 | prmuloc 7556 |
[BauerTaylor], p.
56 | Lemma 12.9 | mullocpr 7561 |
[BellMachover] p.
36 | Lemma 10.3 | idALT 20 |
[BellMachover] p.
97 | Definition 10.1 | df-eu 2029 |
[BellMachover] p.
460 | Notation | df-mo 2030 |
[BellMachover] p.
460 | Definition | mo3 2080 mo3h 2079 |
[BellMachover] p.
462 | Theorem 1.1 | bm1.1 2162 |
[BellMachover] p.
463 | Theorem 1.3ii | bm1.3ii 4121 |
[BellMachover] p.
466 | Axiom Pow | axpow3 4174 |
[BellMachover] p.
466 | Axiom Union | axun2 4432 |
[BellMachover] p.
469 | Theorem 2.2(i) | ordirr 4538 |
[BellMachover] p.
469 | Theorem 2.2(iii) | onelon 4381 |
[BellMachover] p.
469 | Theorem 2.2(vii) | ordn2lp 4541 |
[BellMachover] p.
471 | Problem 2.5(ii) | bm2.5ii 4492 |
[BellMachover] p.
471 | Definition of Lim | df-ilim 4366 |
[BellMachover] p.
472 | Axiom Inf | zfinf2 4585 |
[BellMachover] p.
473 | Theorem 2.8 | limom 4610 |
[Bobzien] p.
116 | Statement T3 | stoic3 1431 |
[Bobzien] p.
117 | Statement T2 | stoic2a 1429 |
[Bobzien] p.
117 | Statement T4 | stoic4a 1432 |
[Bobzien] p.
117 | Conclusion the contradictory | stoic1a 1427 |
[BourbakiAlg1] p.
1 | Definition 1 | df-mgm 12667 |
[BourbakiAlg1] p.
4 | Definition 5 | df-sgrp 12700 |
[BourbakiAlg1] p.
12 | Definition 2 | df-mnd 12710 |
[BourbakiAlg1] p.
92 | Definition 1 | df-ring 13007 |
[BourbakiEns] p.
| Proposition 8 | fcof1 5778 fcofo 5779 |
[BourbakiTop1] p.
| Remark | xnegmnf 9816 xnegpnf 9815 |
[BourbakiTop1] p.
| Remark | rexneg 9817 |
[BourbakiTop1] p.
| Proposition | ishmeo 13471 |
[BourbakiTop1] p.
| Property V_i | ssnei2 13324 |
[BourbakiTop1] p.
| Property V_ii | innei 13330 |
[BourbakiTop1] p.
| Property V_iv | neissex 13332 |
[BourbakiTop1] p.
| Proposition 1 | neipsm 13321 neiss 13317 |
[BourbakiTop1] p.
| Proposition 2 | cnptopco 13389 |
[BourbakiTop1] p.
| Proposition 4 | imasnopn 13466 |
[BourbakiTop1] p.
| Property V_iii | elnei 13319 |
[BourbakiTop1] p.
| Definition is due to Bourbaki (Def. 1 | df-top 13163 |
[Bruck] p. 1 | Section
I.1 | df-mgm 12667 |
[Bruck] p. 23 | Section
II.1 | df-sgrp 12700 |
[Bruck] p. 28 | Theorem
3.2 | dfgrp3m 12858 |
[ChoquetDD] p.
2 | Definition of mapping | df-mpt 4063 |
[Cohen] p.
301 | Remark | relogoprlem 13956 |
[Cohen] p. 301 | Property
2 | relogmul 13957 relogmuld 13972 |
[Cohen] p. 301 | Property
3 | relogdiv 13958 relogdivd 13973 |
[Cohen] p. 301 | Property
4 | relogexp 13960 |
[Cohen] p. 301 | Property
1a | log1 13954 |
[Cohen] p. 301 | Property
1b | loge 13955 |
[Cohen4] p.
348 | Observation | relogbcxpbap 14050 |
[Cohen4] p.
352 | Definition | rpelogb 14034 |
[Cohen4] p. 361 | Property
2 | rprelogbmul 14040 |
[Cohen4] p. 361 | Property
3 | logbrec 14045 rprelogbdiv 14042 |
[Cohen4] p. 361 | Property
4 | rplogbreexp 14038 |
[Cohen4] p. 361 | Property
6 | relogbexpap 14043 |
[Cohen4] p. 361 | Property
1(a) | rplogbid1 14032 |
[Cohen4] p. 361 | Property
1(b) | rplogb1 14033 |
[Cohen4] p.
367 | Property | rplogbchbase 14035 |
[Cohen4] p. 377 | Property
2 | logblt 14047 |
[Crosilla] p. | Axiom
1 | ax-ext 2159 |
[Crosilla] p. | Axiom
2 | ax-pr 4206 |
[Crosilla] p. | Axiom
3 | ax-un 4430 |
[Crosilla] p. | Axiom
4 | ax-nul 4126 |
[Crosilla] p. | Axiom
5 | ax-iinf 4584 |
[Crosilla] p. | Axiom
6 | ru 2961 |
[Crosilla] p. | Axiom
8 | ax-pow 4171 |
[Crosilla] p. | Axiom
9 | ax-setind 4533 |
[Crosilla], p. | Axiom
6 | ax-sep 4118 |
[Crosilla], p. | Axiom
7 | ax-coll 4115 |
[Crosilla], p. | Axiom
7' | repizf 4116 |
[Crosilla], p. | Theorem
is stated | ordtriexmid 4517 |
[Crosilla], p. | Axiom
of choice implies instances | acexmid 5868 |
[Crosilla], p.
| Definition of ordinal | df-iord 4363 |
[Crosilla], p. | Theorem
"Foundation implies instances of EM" | regexmid 4531 |
[Eisenberg] p.
67 | Definition 5.3 | df-dif 3131 |
[Eisenberg] p.
82 | Definition 6.3 | df-iom 4587 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 6644 |
[Enderton] p. 18 | Axiom
of Empty Set | axnul 4125 |
[Enderton] p.
19 | Definition | df-tp 3599 |
[Enderton] p.
26 | Exercise 5 | unissb 3837 |
[Enderton] p.
26 | Exercise 10 | pwel 4215 |
[Enderton] p.
28 | Exercise 7(b) | pwunim 4283 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1m 3953 iinin2m 3952 iunin1 3948 iunin2 3947 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2m 3951 iundif2ss 3949 |
[Enderton] p.
33 | Exercise 23 | iinuniss 3966 |
[Enderton] p.
33 | Exercise 25 | iununir 3967 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 3974 |
[Enderton] p.
33 | Exercise 24(b) | iunpw 4477 iunpwss 3975 |
[Enderton] p.
38 | Exercise 6(a) | unipw 4214 |
[Enderton] p.
38 | Exercise 6(b) | pwuni 4189 |
[Enderton] p. 41 | Lemma
3D | opeluu 4447 rnex 4890
rnexg 4888 |
[Enderton] p.
41 | Exercise 8 | dmuni 4833 rnuni 5036 |
[Enderton] p.
42 | Definition of a function | dffun7 5239 dffun8 5240 |
[Enderton] p.
43 | Definition of function value | funfvdm2 5576 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 5273 |
[Enderton] p.
44 | Definition (d) | dfima2 4968 dfima3 4969 |
[Enderton] p.
47 | Theorem 3H | fvco2 5581 |
[Enderton] p. 49 | Axiom
of Choice (first form) | df-ac 7199 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 5756 |
[Enderton] p.
52 | Definition | df-map 6644 |
[Enderton] p.
53 | Exercise 21 | coass 5143 |
[Enderton] p.
53 | Exercise 27 | dmco 5133 |
[Enderton] p.
53 | Exercise 14(a) | funin 5283 |
[Enderton] p.
53 | Exercise 22(a) | imass2 5000 |
[Enderton] p.
54 | Remark | ixpf 6714 ixpssmap 6726 |
[Enderton] p.
54 | Definition of infinite Cartesian product | df-ixp 6693 |
[Enderton] p.
56 | Theorem 3M | erref 6549 |
[Enderton] p. 57 | Lemma
3N | erthi 6575 |
[Enderton] p.
57 | Definition | df-ec 6531 |
[Enderton] p.
58 | Definition | df-qs 6535 |
[Enderton] p.
60 | Theorem 3Q | th3q 6634 th3qcor 6633 th3qlem1 6631 th3qlem2 6632 |
[Enderton] p.
61 | Exercise 35 | df-ec 6531 |
[Enderton] p.
65 | Exercise 56(a) | dmun 4830 |
[Enderton] p.
68 | Definition of successor | df-suc 4368 |
[Enderton] p.
71 | Definition | df-tr 4099 dftr4 4103 |
[Enderton] p.
72 | Theorem 4E | unisuc 4410 unisucg 4411 |
[Enderton] p.
73 | Exercise 6 | unisuc 4410 unisucg 4411 |
[Enderton] p.
73 | Exercise 5(a) | truni 4112 |
[Enderton] p.
73 | Exercise 5(b) | trint 4113 |
[Enderton] p.
79 | Theorem 4I(A1) | nna0 6469 |
[Enderton] p.
79 | Theorem 4I(A2) | nnasuc 6471 onasuc 6461 |
[Enderton] p.
79 | Definition of operation value | df-ov 5872 |
[Enderton] p.
80 | Theorem 4J(A1) | nnm0 6470 |
[Enderton] p.
80 | Theorem 4J(A2) | nnmsuc 6472 onmsuc 6468 |
[Enderton] p.
81 | Theorem 4K(1) | nnaass 6480 |
[Enderton] p.
81 | Theorem 4K(2) | nna0r 6473 nnacom 6479 |
[Enderton] p.
81 | Theorem 4K(3) | nndi 6481 |
[Enderton] p.
81 | Theorem 4K(4) | nnmass 6482 |
[Enderton] p.
81 | Theorem 4K(5) | nnmcom 6484 |
[Enderton] p.
82 | Exercise 16 | nnm0r 6474 nnmsucr 6483 |
[Enderton] p.
88 | Exercise 23 | nnaordex 6523 |
[Enderton] p.
129 | Definition | df-en 6735 |
[Enderton] p.
132 | Theorem 6B(b) | canth 5823 |
[Enderton] p.
133 | Exercise 1 | xpomen 12379 |
[Enderton] p.
134 | Theorem (Pigeonhole Principle) | phpm 6859 |
[Enderton] p.
136 | Corollary 6E | nneneq 6851 |
[Enderton] p.
139 | Theorem 6H(c) | mapen 6840 |
[Enderton] p.
142 | Theorem 6I(3) | xpdjuen 7211 |
[Enderton] p.
143 | Theorem 6J | dju0en 7207 dju1en 7206 |
[Enderton] p.
144 | Corollary 6K | undif2ss 3498 |
[Enderton] p.
145 | Figure 38 | ffoss 5489 |
[Enderton] p.
145 | Definition | df-dom 6736 |
[Enderton] p.
146 | Example 1 | domen 6745 domeng 6746 |
[Enderton] p.
146 | Example 3 | nndomo 6858 |
[Enderton] p.
149 | Theorem 6L(c) | xpdom1 6829 xpdom1g 6827 xpdom2g 6826 |
[Enderton] p.
168 | Definition | df-po 4293 |
[Enderton] p.
192 | Theorem 7M(a) | oneli 4425 |
[Enderton] p.
192 | Theorem 7M(b) | ontr1 4386 |
[Enderton] p.
192 | Theorem 7M(c) | onirri 4539 |
[Enderton] p.
193 | Corollary 7N(b) | 0elon 4389 |
[Enderton] p.
193 | Corollary 7N(c) | onsuci 4512 |
[Enderton] p.
193 | Corollary 7N(d) | ssonunii 4485 |
[Enderton] p.
194 | Remark | onprc 4548 |
[Enderton] p.
194 | Exercise 16 | suc11 4554 |
[Enderton] p.
197 | Definition | df-card 7173 |
[Enderton] p.
200 | Exercise 25 | tfis 4579 |
[Enderton] p.
206 | Theorem 7X(b) | en2lp 4550 |
[Enderton] p.
207 | Exercise 34 | opthreg 4552 |
[Enderton] p.
208 | Exercise 35 | suc11g 4553 |
[Geuvers], p.
1 | Remark | expap0 10536 |
[Geuvers], p. 6 | Lemma
2.13 | mulap0r 8562 |
[Geuvers], p. 6 | Lemma
2.15 | mulap0 8600 |
[Geuvers], p. 9 | Lemma
2.35 | msqge0 8563 |
[Geuvers], p.
9 | Definition 3.1(2) | ax-arch 7921 |
[Geuvers], p. 10 | Lemma
3.9 | maxcom 11196 |
[Geuvers], p. 10 | Lemma
3.10 | maxle1 11204 maxle2 11205 |
[Geuvers], p. 10 | Lemma
3.11 | maxleast 11206 |
[Geuvers], p. 10 | Lemma
3.12 | maxleb 11209 |
[Geuvers], p.
11 | Definition 3.13 | dfabsmax 11210 |
[Geuvers], p.
17 | Definition 6.1 | df-ap 8529 |
[Gleason] p.
117 | Proposition 9-2.1 | df-enq 7337 enqer 7348 |
[Gleason] p.
117 | Proposition 9-2.2 | df-1nqqs 7341 df-nqqs 7338 |
[Gleason] p.
117 | Proposition 9-2.3 | df-plpq 7334 df-plqqs 7339 |
[Gleason] p.
119 | Proposition 9-2.4 | df-mpq 7335 df-mqqs 7340 |
[Gleason] p.
119 | Proposition 9-2.5 | df-rq 7342 |
[Gleason] p.
119 | Proposition 9-2.6 | ltexnqq 7398 |
[Gleason] p.
120 | Proposition 9-2.6(i) | halfnq 7401 ltbtwnnq 7406 ltbtwnnqq 7405 |
[Gleason] p.
120 | Proposition 9-2.6(ii) | ltanqg 7390 |
[Gleason] p.
120 | Proposition 9-2.6(iii) | ltmnqg 7391 |
[Gleason] p.
123 | Proposition 9-3.5 | addclpr 7527 |
[Gleason] p.
123 | Proposition 9-3.5(i) | addassprg 7569 |
[Gleason] p.
123 | Proposition 9-3.5(ii) | addcomprg 7568 |
[Gleason] p.
123 | Proposition 9-3.5(iii) | ltaddpr 7587 |
[Gleason] p.
123 | Proposition 9-3.5(iv) | ltexpri 7603 |
[Gleason] p.
123 | Proposition 9-3.5(v) | ltaprg 7609 ltaprlem 7608 |
[Gleason] p.
123 | Proposition 9-3.5(vi) | addcanprg 7606 |
[Gleason] p.
124 | Proposition 9-3.7 | mulclpr 7562 |
[Gleason] p. 124 | Theorem
9-3.7(iv) | 1idpr 7582 |
[Gleason] p.
124 | Proposition 9-3.7(i) | mulassprg 7571 |
[Gleason] p.
124 | Proposition 9-3.7(ii) | mulcomprg 7570 |
[Gleason] p.
124 | Proposition 9-3.7(iii) | distrprg 7578 |
[Gleason] p.
124 | Proposition 9-3.7(v) | recexpr 7628 |
[Gleason] p.
126 | Proposition 9-4.1 | df-enr 7716 enrer 7725 |
[Gleason] p.
126 | Proposition 9-4.2 | df-0r 7721 df-1r 7722 df-nr 7717 |
[Gleason] p.
126 | Proposition 9-4.3 | df-mr 7719 df-plr 7718 negexsr 7762 recexsrlem 7764 |
[Gleason] p.
127 | Proposition 9-4.4 | df-ltr 7720 |
[Gleason] p.
130 | Proposition 10-1.3 | creui 8906 creur 8905 cru 8549 |
[Gleason] p.
130 | Definition 10-1.1(v) | ax-cnre 7913 axcnre 7871 |
[Gleason] p.
132 | Definition 10-3.1 | crim 10851 crimd 10970 crimi 10930 crre 10850 crred 10969 crrei 10929 |
[Gleason] p.
132 | Definition 10-3.2 | remim 10853 remimd 10935 |
[Gleason] p.
133 | Definition 10.36 | absval2 11050 absval2d 11178 absval2i 11137 |
[Gleason] p.
133 | Proposition 10-3.4(a) | cjadd 10877 cjaddd 10958 cjaddi 10925 |
[Gleason] p.
133 | Proposition 10-3.4(c) | cjmul 10878 cjmuld 10959 cjmuli 10926 |
[Gleason] p.
133 | Proposition 10-3.4(e) | cjcj 10876 cjcjd 10936 cjcji 10908 |
[Gleason] p.
133 | Proposition 10-3.4(f) | cjre 10875 cjreb 10859 cjrebd 10939 cjrebi 10911 cjred 10964 rere 10858 rereb 10856 rerebd 10938 rerebi 10910 rered 10962 |
[Gleason] p.
133 | Proposition 10-3.4(h) | addcj 10884 addcjd 10950 addcji 10920 |
[Gleason] p.
133 | Proposition 10-3.7(a) | absval 10994 |
[Gleason] p.
133 | Proposition 10-3.7(b) | abscj 11045 abscjd 11183 abscji 11141 |
[Gleason] p.
133 | Proposition 10-3.7(c) | abs00 11057 abs00d 11179 abs00i 11138 absne0d 11180 |
[Gleason] p.
133 | Proposition 10-3.7(d) | releabs 11089 releabsd 11184 releabsi 11142 |
[Gleason] p.
133 | Proposition 10-3.7(f) | absmul 11062 absmuld 11187 absmuli 11144 |
[Gleason] p.
133 | Proposition 10-3.7(g) | sqabsadd 11048 sqabsaddi 11145 |
[Gleason] p.
133 | Proposition 10-3.7(h) | abstri 11097 abstrid 11189 abstrii 11148 |
[Gleason] p.
134 | Definition 10-4.1 | df-exp 10506 exp0 10510 expp1 10513 expp1d 10640 |
[Gleason] p.
135 | Proposition 10-4.2(a) | expadd 10548 expaddd 10641 |
[Gleason] p.
135 | Proposition 10-4.2(b) | cxpmul 14000 cxpmuld 14023 expmul 10551 expmuld 10642 |
[Gleason] p.
135 | Proposition 10-4.2(c) | mulexp 10545 mulexpd 10654 rpmulcxp 13997 |
[Gleason] p.
141 | Definition 11-2.1 | fzval 9997 |
[Gleason] p.
168 | Proposition 12-2.1(a) | climadd 11318 |
[Gleason] p.
168 | Proposition 12-2.1(b) | climsub 11320 |
[Gleason] p.
168 | Proposition 12-2.1(c) | climmul 11319 |
[Gleason] p.
171 | Corollary 12-2.2 | climmulc2 11323 |
[Gleason] p.
172 | Corollary 12-2.5 | climrecl 11316 |
[Gleason] p.
172 | Proposition 12-2.4(c) | climabs 11312 climcj 11313 climim 11315 climre 11314 |
[Gleason] p.
173 | Definition 12-3.1 | df-ltxr 7987 df-xr 7986 ltxr 9762 |
[Gleason] p. 180 | Theorem
12-5.3 | climcau 11339 |
[Gleason] p. 217 | Lemma
13-4.1 | btwnzge0 10286 |
[Gleason] p.
223 | Definition 14-1.1 | df-met 13156 |
[Gleason] p.
223 | Definition 14-1.1(a) | met0 13531 xmet0 13530 |
[Gleason] p.
223 | Definition 14-1.1(c) | metsym 13538 |
[Gleason] p.
223 | Definition 14-1.1(d) | mettri 13540 mstri 13640 xmettri 13539 xmstri 13639 |
[Gleason] p.
230 | Proposition 14-2.6 | txlm 13446 |
[Gleason] p.
240 | Proposition 14-4.2 | metcnp3 13678 |
[Gleason] p.
243 | Proposition 14-4.16 | addcn2 11302 addcncntop 13719 mulcn2 11304 mulcncntop 13721 subcn2 11303 subcncntop 13720 |
[Gleason] p.
295 | Remark | bcval3 10715 bcval4 10716 |
[Gleason] p.
295 | Equation 2 | bcpasc 10730 |
[Gleason] p.
295 | Definition of binomial coefficient | bcval 10713 df-bc 10712 |
[Gleason] p.
296 | Remark | bcn0 10719 bcnn 10721 |
[Gleason] p. 296 | Theorem
15-2.8 | binom 11476 |
[Gleason] p.
308 | Equation 2 | ef0 11664 |
[Gleason] p.
308 | Equation 3 | efcj 11665 |
[Gleason] p.
309 | Corollary 15-4.3 | efne0 11670 |
[Gleason] p.
309 | Corollary 15-4.4 | efexp 11674 |
[Gleason] p.
310 | Equation 14 | sinadd 11728 |
[Gleason] p.
310 | Equation 15 | cosadd 11729 |
[Gleason] p.
311 | Equation 17 | sincossq 11740 |
[Gleason] p.
311 | Equation 18 | cosbnd 11745 sinbnd 11744 |
[Gleason] p.
311 | Definition of ` ` | df-pi 11645 |
[Golan] p.
1 | Remark | srgisid 12995 |
[Golan] p.
1 | Definition | df-srg 12973 |
[Hamilton] p.
31 | Example 2.7(a) | idALT 20 |
[Hamilton] p. 73 | Rule
1 | ax-mp 5 |
[Hamilton] p. 74 | Rule
2 | ax-gen 1449 |
[Herstein] p. 55 | Lemma
2.2.1(a) | grpideu 12778 mndideu 12719 |
[Herstein] p. 55 | Lemma
2.2.1(b) | grpinveu 12801 |
[Herstein] p. 55 | Lemma
2.2.1(c) | grpinvinv 12826 |
[Herstein] p. 55 | Lemma
2.2.1(d) | grpinvadd 12837 |
[Herstein] p.
57 | Exercise 1 | dfgrp3me 12859 |
[Heyting] p.
127 | Axiom #1 | ax1hfs 14475 |
[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 7218 |
[HoTT], p. | Theorem
7.2.6 | nndceq 6494 |
[HoTT], p.
| Exercise 11.10 | neapmkv 14471 |
[HoTT], p. | Exercise
11.11 | mulap0bd 8603 |
[HoTT], p. | Section
11.2.1 | df-iltp 7460 df-imp 7459 df-iplp 7458 df-reap 8522 |
[HoTT], p. | Theorem
11.2.4 | recapb 8617 rerecapb 8789 |
[HoTT], p. | Theorem
11.2.12 | cauappcvgpr 7652 |
[HoTT], p. | Corollary
11.4.3 | conventions 14129 |
[HoTT], p.
| Exercise 11.6(i) | dcapnconst 14464 dceqnconst 14463 |
[HoTT], p. | Corollary
11.2.13 | axcaucvg 7890 caucvgpr 7672 caucvgprpr 7702 caucvgsr 7792 |
[HoTT], p. | Definition
11.2.1 | df-inp 7456 |
[HoTT], p.
| Exercise 11.6(ii) | nconstwlpo 14469 |
[HoTT], p. | Proposition
11.2.3 | df-iso 4294 ltpopr 7585 ltsopr 7586 |
[HoTT], p. | Definition
11.2.7(v) | apsym 8553 reapcotr 8545 reapirr 8524 |
[HoTT], p. | Definition
11.2.7(vi) | 0lt1 8074 gt0add 8520 leadd1 8377 lelttr 8036 lemul1a 8804 lenlt 8023 ltadd1 8376 ltletr 8037 ltmul1 8539 reaplt 8535 |
[Jech] p. 4 | Definition of
class | cv 1352 cvjust 2172 |
[Jech] p.
78 | Note | opthprc 4674 |
[KalishMontague] p.
81 | Note 1 | ax-i9 1530 |
[Kreyszig] p.
3 | Property M1 | metcl 13520 xmetcl 13519 |
[Kreyszig] p.
4 | Property M2 | meteq0 13527 |
[Kreyszig] p.
12 | Equation 5 | muleqadd 8614 |
[Kreyszig] p.
18 | Definition 1.3-2 | mopnval 13609 |
[Kreyszig] p.
19 | Remark | mopntopon 13610 |
[Kreyszig] p.
19 | Theorem T1 | mopn0 13655 mopnm 13615 |
[Kreyszig] p.
19 | Theorem T2 | unimopn 13653 |
[Kreyszig] p.
19 | Definition of neighborhood | neibl 13658 |
[Kreyszig] p.
20 | Definition 1.3-3 | metcnp2 13680 |
[Kreyszig] p.
25 | Definition 1.4-1 | lmbr 13380 |
[Kunen] p. 10 | Axiom
0 | a9e 1696 |
[Kunen] p. 12 | Axiom
6 | zfrep6 4117 |
[Kunen] p. 24 | Definition
10.24 | mapval 6654 mapvalg 6652 |
[Kunen] p. 31 | Definition
10.24 | mapex 6648 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 3894 |
[Lang] p.
3 | Statement | lidrideqd 12692 mndbn0 12724 |
[Lang] p.
3 | Definition | df-mnd 12710 |
[Lang] p.
7 | Definition | dfgrp2e 12793 |
[Levy] p.
338 | Axiom | df-clab 2164 df-clel 2173 df-cleq 2170 |
[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 1598 |
[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 1502 |
[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 1638 r19.2m 3509 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 1554 19.3h 1553 rr19.3v 2876 |
[Margaris] p.
89 | Theorem 19.5 | alcom 1478 |
[Margaris] p.
89 | Theorem 19.6 | alexdc 1619 alexim 1645 |
[Margaris] p.
89 | Theorem 19.7 | alnex 1499 |
[Margaris] p.
89 | Theorem 19.8 | 19.8a 1590 spsbe 1842 |
[Margaris] p.
89 | Theorem 19.9 | 19.9 1644 19.9h 1643 19.9v 1871 exlimd 1597 |
[Margaris] p.
89 | Theorem 19.11 | excom 1664 excomim 1663 |
[Margaris] p.
89 | Theorem 19.12 | 19.12 1665 r19.12 2583 |
[Margaris] p.
90 | Theorem 19.14 | exnalim 1646 |
[Margaris] p.
90 | Theorem 19.15 | albi 1468 ralbi 2609 |
[Margaris] p.
90 | Theorem 19.16 | 19.16 1555 |
[Margaris] p.
90 | Theorem 19.17 | 19.17 1556 |
[Margaris] p.
90 | Theorem 19.18 | exbi 1604 rexbi 2610 |
[Margaris] p.
90 | Theorem 19.19 | 19.19 1666 |
[Margaris] p.
90 | Theorem 19.20 | alim 1457 alimd 1521 alimdh 1467 alimdv 1879 ralimdaa 2543 ralimdv 2545 ralimdva 2544 ralimdvva 2546 sbcimdv 3028 |
[Margaris] p.
90 | Theorem 19.21 | 19.21-2 1667 19.21 1583 19.21bi 1558 19.21h 1557 19.21ht 1581 19.21t 1582 19.21v 1873 alrimd 1610 alrimdd 1609 alrimdh 1479 alrimdv 1876 alrimi 1522 alrimih 1469 alrimiv 1874 alrimivv 1875 r19.21 2553 r19.21be 2568 r19.21bi 2565 r19.21t 2552 r19.21v 2554 ralrimd 2555 ralrimdv 2556 ralrimdva 2557 ralrimdvv 2561 ralrimdvva 2562 ralrimi 2548 ralrimiv 2549 ralrimiva 2550 ralrimivv 2558 ralrimivva 2559 ralrimivvva 2560 ralrimivw 2551 rexlimi 2587 |
[Margaris] p.
90 | Theorem 19.22 | 2alimdv 1881 2eximdv 1882 exim 1599
eximd 1612 eximdh 1611 eximdv 1880 rexim 2571 reximdai 2575 reximddv 2580 reximddv2 2582 reximdv 2578 reximdv2 2576 reximdva 2579 reximdvai 2577 reximi2 2573 |
[Margaris] p.
90 | Theorem 19.23 | 19.23 1678 19.23bi 1592 19.23h 1498 19.23ht 1497 19.23t 1677 19.23v 1883 19.23vv 1884 exlimd2 1595 exlimdh 1596 exlimdv 1819 exlimdvv 1897 exlimi 1594 exlimih 1593 exlimiv 1598 exlimivv 1896 r19.23 2585 r19.23v 2586 rexlimd 2591 rexlimdv 2593 rexlimdv3a 2596 rexlimdva 2594 rexlimdva2 2597 rexlimdvaa 2595 rexlimdvv 2601 rexlimdvva 2602 rexlimdvw 2598 rexlimiv 2588 rexlimiva 2589 rexlimivv 2600 |
[Margaris] p.
90 | Theorem 19.24 | i19.24 1639 |
[Margaris] p.
90 | Theorem 19.25 | 19.25 1626 |
[Margaris] p.
90 | Theorem 19.26 | 19.26-2 1482 19.26-3an 1483 19.26 1481 r19.26-2 2606 r19.26-3 2607 r19.26 2603 r19.26m 2608 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 1561 19.27h 1560 19.27v 1899 r19.27av 2612 r19.27m 3518 r19.27mv 3519 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 1563 19.28h 1562 19.28v 1900 r19.28av 2613 r19.28m 3512 r19.28mv 3515 rr19.28v 2877 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1620 19.29r 1621 19.29r2 1622 19.29x 1623 r19.29 2614 r19.29d2r 2621 r19.29r 2615 |
[Margaris] p.
90 | Theorem 19.30 | 19.30dc 1627 |
[Margaris] p.
90 | Theorem 19.31 | 19.31r 1681 |
[Margaris] p.
90 | Theorem 19.32 | 19.32dc 1679 19.32r 1680 r19.32r 2623 r19.32vdc 2626 r19.32vr 2625 |
[Margaris] p.
90 | Theorem 19.33 | 19.33 1484 19.33b2 1629 19.33bdc 1630 |
[Margaris] p.
90 | Theorem 19.34 | 19.34 1684 |
[Margaris] p.
90 | Theorem 19.35 | 19.35-1 1624 19.35i 1625 |
[Margaris] p.
90 | Theorem 19.36 | 19.36-1 1673 19.36aiv 1901 19.36i 1672 r19.36av 2628 |
[Margaris] p.
90 | Theorem 19.37 | 19.37-1 1674 19.37aiv 1675 r19.37 2629 r19.37av 2630 |
[Margaris] p.
90 | Theorem 19.38 | 19.38 1676 |
[Margaris] p.
90 | Theorem 19.39 | i19.39 1640 |
[Margaris] p.
90 | Theorem 19.40 | 19.40-2 1632 19.40 1631 r19.40 2631 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 1686 19.41h 1685 19.41v 1902 19.41vv 1903 19.41vvv 1904 19.41vvvv 1905 r19.41 2632 r19.41v 2633 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 1688 19.42h 1687 19.42v 1906 19.42vv 1911 19.42vvv 1912 19.42vvvv 1913 r19.42v 2634 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1628 r19.43 2635 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 1682 r19.44av 2636 r19.44mv 3517 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 1683 r19.45av 2637 r19.45mv 3516 |
[Margaris] p.
110 | Exercise 2(b) | eu1 2051 |
[Megill] p. 444 | Axiom
C5 | ax-17 1526 |
[Megill] p. 445 | Lemma
L12 | alequcom 1515 ax-10 1505 |
[Megill] p. 446 | Lemma
L17 | equtrr 1710 |
[Megill] p. 446 | Lemma
L19 | hbnae 1721 |
[Megill] p. 447 | Remark
9.1 | df-sb 1763 sbid 1774 |
[Megill] p. 448 | Scheme
C5' | ax-4 1510 |
[Megill] p. 448 | Scheme
C6' | ax-7 1448 |
[Megill] p. 448 | Scheme
C8' | ax-8 1504 |
[Megill] p. 448 | Scheme
C9' | ax-i12 1507 |
[Megill] p. 448 | Scheme
C11' | ax-10o 1716 |
[Megill] p. 448 | Scheme
C12' | ax-13 2150 |
[Megill] p. 448 | Scheme
C13' | ax-14 2151 |
[Megill] p. 448 | Scheme
C15' | ax-11o 1823 |
[Megill] p. 448 | Scheme
C16' | ax-16 1814 |
[Megill] p. 448 | Theorem
9.4 | dral1 1730 dral2 1731 drex1 1798 drex2 1732 drsb1 1799 drsb2 1841 |
[Megill] p. 449 | Theorem
9.7 | sbcom2 1987 sbequ 1840 sbid2v 1996 |
[Megill] p. 450 | Example
in Appendix | hba1 1540 |
[Mendelson] p.
36 | Lemma 1.8 | idALT 20 |
[Mendelson] p.
69 | Axiom 4 | rspsbc 3045 rspsbca 3046 stdpc4 1775 |
[Mendelson] p.
69 | Axiom 5 | ra5 3051 stdpc5 1584 |
[Mendelson] p. 81 | Rule
C | exlimiv 1598 |
[Mendelson] p.
95 | Axiom 6 | stdpc6 1703 |
[Mendelson] p.
95 | Axiom 7 | stdpc7 1770 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 3459 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 3460 |
[Mendelson] p.
231 | Exercise 4.10(n) | inssun 3375 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 3423 |
[Mendelson] p.
231 | Exercise 4.10(q) | inssddif 3376 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddifnel 3266 |
[Mendelson] p.
231 | Definition of union | unssin 3374 |
[Mendelson] p.
235 | Exercise 4.12(c) | univ 4473 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 3806 |
[Mendelson] p.
235 | Exercise 4.12(j) | pwin 4279 |
[Mendelson] p.
235 | Exercise 4.12(k) | pwunss 4280 |
[Mendelson] p.
235 | Exercise 4.12(l) | pwssunim 4281 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 3827 |
[Mendelson] p.
235 | Exercise 4.12(p) | reli 4752 |
[Mendelson] p.
235 | Exercise 4.12(t) | relssdmrn 5145 |
[Mendelson] p.
246 | Definition of successor | df-suc 4368 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 6839 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 6815 xpsneng 6816 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 6821 xpcomeng 6822 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 6824 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 6818 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 6646 |
[Mendelson] p.
255 | Exercise 4.43 | mapsnen 6805 |
[Mendelson] p.
255 | Exercise 4.47 | xpmapen 6844 |
[Mendelson] p.
255 | Exercise 4.42(a) | map0e 6680 |
[Mendelson] p.
255 | Exercise 4.42(b) | map1 6806 |
[Mendelson] p.
258 | Exercise 4.56(c) | djuassen 7210 djucomen 7209 |
[Mendelson] p.
258 | Exercise 4.56(g) | xp2dju 7208 |
[Mendelson] p.
266 | Proposition 4.34(a) | oa1suc 6462 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 3357 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 4711 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 4712 |
[Monk1] p. 34 | Definition
3.3 | df-opab 4062 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5140 coi2 5141 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 4837 rn0 4879 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 5029 |
[Monk1] p. 37 | Theorem
3.13(i) | relxp 4732 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxpm 4843 rnxpm 5054 |
[Monk1] p. 37 | Theorem
3.13(ii) | 0xp 4703 xp0 5044 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 4983 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 4980 |
[Monk1] p. 39 | Theorem
3.17 | imaex 4979 imaexg 4978 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 4977 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 5642 funfvop 5624 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 5555 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 5563 |
[Monk1] p. 43 | Theorem
4.6 | funun 5256 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 5763 dff13f 5765 |
[Monk1] p. 46 | Theorem
4.15(v) | funex 5735 funrnex 6109 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 5757 |
[Monk1] p. 52 | Theorem
5.12(ii) | op2ndb 5108 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 3858 |
[Monk1] p. 52 | Definition
5.13 (i) | 1stval2 6150 df-1st 6135 |
[Monk1] p. 52 | Definition
5.13 (ii) | 2ndval2 6151 df-2nd 6136 |
[Monk2] p. 105 | Axiom
C4 | ax-5 1447 |
[Monk2] p. 105 | Axiom
C7 | ax-8 1504 |
[Monk2] p. 105 | Axiom
C8 | ax-11 1506 ax-11o 1823 |
[Monk2] p. 105 | Axiom
(C8) | ax11v 1827 |
[Monk2] p. 109 | Lemma
12 | ax-7 1448 |
[Monk2] p. 109 | Lemma
15 | equvin 1863 equvini 1758 eqvinop 4240 |
[Monk2] p. 113 | Axiom
C5-1 | ax-17 1526 |
[Monk2] p. 113 | Axiom
C5-2 | ax6b 1651 |
[Monk2] p. 113 | Axiom
C5-3 | ax-7 1448 |
[Monk2] p. 114 | Lemma
22 | hba1 1540 |
[Monk2] p. 114 | Lemma
23 | hbia1 1552 nfia1 1580 |
[Monk2] p. 114 | Lemma
24 | hba2 1551 nfa2 1579 |
[Moschovakis] p.
2 | Chapter 2 | df-stab 831 dftest 14476 |
[Munkres] p. 77 | Example
2 | distop 13252 |
[Munkres] p.
78 | Definition of basis | df-bases 13208 isbasis3g 13211 |
[Munkres] p.
78 | Definition of a topology generated by a basis | df-topgen 12657 tgval2 13218 |
[Munkres] p.
79 | Remark | tgcl 13231 |
[Munkres] p. 80 | Lemma
2.1 | tgval3 13225 |
[Munkres] p. 80 | Lemma
2.2 | tgss2 13246 tgss3 13245 |
[Munkres] p. 81 | Lemma
2.3 | basgen 13247 basgen2 13248 |
[Munkres] p.
89 | Definition of subspace topology | resttop 13337 |
[Munkres] p. 93 | Theorem
6.1(1) | 0cld 13279 topcld 13276 |
[Munkres] p. 93 | Theorem
6.1(3) | uncld 13280 |
[Munkres] p.
94 | Definition of closure | clsval 13278 |
[Munkres] p.
94 | Definition of interior | ntrval 13277 |
[Munkres] p.
102 | Definition of continuous function | df-cn 13355 iscn 13364 iscn2 13367 |
[Munkres] p. 107 | Theorem
7.2(g) | cncnp 13397 cncnp2m 13398 cncnpi 13395 df-cnp 13356 iscnp 13366 |
[Munkres] p. 127 | Theorem
10.1 | metcn 13681 |
[Pierik], p. 8 | Section
2.2.1 | dfrex2fin 6897 |
[Pierik], p. 9 | Definition
2.4 | df-womni 7156 |
[Pierik], p. 9 | Definition
2.5 | df-markov 7144 omniwomnimkv 7159 |
[Pierik], p. 10 | Section
2.3 | dfdif3 3245 |
[Pierik], p.
14 | Definition 3.1 | df-omni 7127 exmidomniim 7133 finomni 7132 |
[Pierik], p. 15 | Section
3.1 | df-nninf 7113 |
[PradicBrown2022], p. 1 | Theorem
1 | exmidsbthr 14427 |
[PradicBrown2022], p.
2 | Remark | exmidpw 6902 |
[PradicBrown2022], p.
2 | Proposition 1.1 | exmidfodomrlemim 7194 |
[PradicBrown2022], p.
2 | Proposition 1.2 | exmidfodomrlemr 7195 exmidfodomrlemrALT 7196 |
[PradicBrown2022], p.
4 | Lemma 3.2 | fodjuomni 7141 |
[PradicBrown2022], p. 5 | Lemma
3.4 | peano3nninf 14412 peano4nninf 14411 |
[PradicBrown2022], p. 5 | Lemma
3.5 | nninfall 14414 |
[PradicBrown2022], p. 5 | Theorem
3.6 | nninfsel 14422 |
[PradicBrown2022], p. 5 | Corollary
3.7 | nninfomni 14424 |
[PradicBrown2022], p. 5 | Definition
3.3 | nnsf 14410 |
[Quine] p. 16 | Definition
2.1 | df-clab 2164 rabid 2652 |
[Quine] p. 17 | Definition
2.1'' | dfsb7 1991 |
[Quine] p. 18 | Definition
2.7 | df-cleq 2170 |
[Quine] p. 19 | Definition
2.9 | df-v 2739 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2286 |
[Quine] p. 35 | Theorem
5.2 | abid2 2298 abid2f 2345 |
[Quine] p. 40 | Theorem
6.1 | sb5 1887 |
[Quine] p. 40 | Theorem
6.2 | sb56 1885 sb6 1886 |
[Quine] p. 41 | Theorem
6.3 | df-clel 2173 |
[Quine] p. 41 | Theorem
6.4 | eqid 2177 |
[Quine] p. 41 | Theorem
6.5 | eqcom 2179 |
[Quine] p. 42 | Theorem
6.6 | df-sbc 2963 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 2964 dfsbcq2 2965 |
[Quine] p. 43 | Theorem
6.8 | vex 2740 |
[Quine] p. 43 | Theorem
6.9 | isset 2743 |
[Quine] p. 44 | Theorem
7.3 | spcgf 2819 spcgv 2824 spcimgf 2817 |
[Quine] p. 44 | Theorem
6.11 | spsbc 2974 spsbcd 2975 |
[Quine] p. 44 | Theorem
6.12 | elex 2748 |
[Quine] p. 44 | Theorem
6.13 | elab 2881 elabg 2883 elabgf 2879 |
[Quine] p. 44 | Theorem
6.14 | noel 3426 |
[Quine] p. 48 | Theorem
7.2 | snprc 3656 |
[Quine] p. 48 | Definition
7.1 | df-pr 3598 df-sn 3597 |
[Quine] p. 49 | Theorem
7.4 | snss 3726 snssg 3725 |
[Quine] p. 49 | Theorem
7.5 | prss 3747 prssg 3748 |
[Quine] p. 49 | Theorem
7.6 | prid1 3697 prid1g 3695 prid2 3698 prid2g 3696 snid 3622
snidg 3620 |
[Quine] p. 51 | Theorem
7.12 | snexg 4181 snexprc 4183 |
[Quine] p. 51 | Theorem
7.13 | prexg 4208 |
[Quine] p. 53 | Theorem
8.2 | unisn 3823 unisng 3824 |
[Quine] p. 53 | Theorem
8.3 | uniun 3826 |
[Quine] p. 54 | Theorem
8.6 | elssuni 3835 |
[Quine] p. 54 | Theorem
8.7 | uni0 3834 |
[Quine] p. 56 | Theorem
8.17 | uniabio 5184 |
[Quine] p. 56 | Definition
8.18 | dfiota2 5175 |
[Quine] p. 57 | Theorem
8.19 | iotaval 5185 |
[Quine] p. 57 | Theorem
8.22 | iotanul 5189 |
[Quine] p. 58 | Theorem
8.23 | euiotaex 5190 |
[Quine] p. 58 | Definition
9.1 | df-op 3600 |
[Quine] p. 61 | Theorem
9.5 | opabid 4254 opelopab 4268 opelopaba 4263 opelopabaf 4270 opelopabf 4271 opelopabg 4265 opelopabga 4260 oprabid 5901 |
[Quine] p. 64 | Definition
9.11 | df-xp 4629 |
[Quine] p. 64 | Definition
9.12 | df-cnv 4631 |
[Quine] p. 64 | Definition
9.15 | df-id 4290 |
[Quine] p. 65 | Theorem
10.3 | fun0 5270 |
[Quine] p. 65 | Theorem
10.4 | funi 5244 |
[Quine] p. 65 | Theorem
10.5 | funsn 5260 funsng 5258 |
[Quine] p. 65 | Definition
10.1 | df-fun 5214 |
[Quine] p. 65 | Definition
10.2 | args 4993 dffv4g 5508 |
[Quine] p. 68 | Definition
10.11 | df-fv 5220 fv2 5506 |
[Quine] p. 124 | Theorem
17.3 | nn0opth2 10688 nn0opth2d 10687 nn0opthd 10686 |
[Quine] p. 284 | Axiom
39(vi) | funimaex 5297 funimaexg 5296 |
[Roman] p. 19 | Part
Preliminaries | df-ring 13007 |
[Rudin] p. 164 | Equation
27 | efcan 11668 |
[Rudin] p. 164 | Equation
30 | efzval 11675 |
[Rudin] p. 167 | Equation
48 | absefi 11760 |
[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 5009 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 5011 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 5008 |
[Schechter] p.
51 | Definition of transitivity | cotr 5006 |
[Schechter] p.
187 | Definition of "ring with unit" | isring 13009 |
[Schechter] p.
428 | Definition 15.35 | bastop1 13250 |
[Stoll] p. 13 | Definition
of symmetric difference | symdif1 3400 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 3494 dif0 3493 |
[Stoll] p. 16 | Exercise
4.8 | difdifdirss 3507 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 3393 |
[Stoll] p. 19 | Theorem
5.2(13') | indmss 3394 |
[Stoll] p.
20 | Remark | invdif 3377 |
[Stoll] p. 25 | Definition
of ordered triple | df-ot 3601 |
[Stoll] p.
43 | Definition | uniiun 3937 |
[Stoll] p.
44 | Definition | intiin 3938 |
[Stoll] p.
45 | Definition | df-iin 3887 |
[Stoll] p. 45 | Definition
indexed union | df-iun 3886 |
[Stoll] p. 176 | Theorem
3.4(27) | imandc 889 imanst 888 |
[Stoll] p. 262 | Example
4.1 | symdif1 3400 |
[Suppes] p. 22 | Theorem
2 | eq0 3441 |
[Suppes] p. 22 | Theorem
4 | eqss 3170 eqssd 3172 eqssi 3171 |
[Suppes] p. 23 | Theorem
5 | ss0 3463 ss0b 3462 |
[Suppes] p. 23 | Theorem
6 | sstr 3163 |
[Suppes] p. 25 | Theorem
12 | elin 3318 elun 3276 |
[Suppes] p. 26 | Theorem
15 | inidm 3344 |
[Suppes] p. 26 | Theorem
16 | in0 3457 |
[Suppes] p. 27 | Theorem
23 | unidm 3278 |
[Suppes] p. 27 | Theorem
24 | un0 3456 |
[Suppes] p. 27 | Theorem
25 | ssun1 3298 |
[Suppes] p. 27 | Theorem
26 | ssequn1 3305 |
[Suppes] p. 27 | Theorem
27 | unss 3309 |
[Suppes] p. 27 | Theorem
28 | indir 3384 |
[Suppes] p. 27 | Theorem
29 | undir 3385 |
[Suppes] p. 28 | Theorem
32 | difid 3491 difidALT 3492 |
[Suppes] p. 29 | Theorem
33 | difin 3372 |
[Suppes] p. 29 | Theorem
34 | indif 3378 |
[Suppes] p. 29 | Theorem
35 | undif1ss 3497 |
[Suppes] p. 29 | Theorem
36 | difun2 3502 |
[Suppes] p. 29 | Theorem
37 | difin0 3496 |
[Suppes] p. 29 | Theorem
38 | disjdif 3495 |
[Suppes] p. 29 | Theorem
39 | difundi 3387 |
[Suppes] p. 29 | Theorem
40 | difindiss 3389 |
[Suppes] p. 30 | Theorem
41 | nalset 4130 |
[Suppes] p. 39 | Theorem
61 | uniss 3828 |
[Suppes] p. 39 | Theorem
65 | uniop 4252 |
[Suppes] p. 41 | Theorem
70 | intsn 3877 |
[Suppes] p. 42 | Theorem
71 | intpr 3874 intprg 3875 |
[Suppes] p. 42 | Theorem
73 | op1stb 4475 op1stbg 4476 |
[Suppes] p. 42 | Theorem
78 | intun 3873 |
[Suppes] p. 44 | Definition
15(a) | dfiun2 3918 dfiun2g 3916 |
[Suppes] p. 44 | Definition
15(b) | dfiin2 3919 |
[Suppes] p. 47 | Theorem
86 | elpw 3580 elpw2 4154 elpw2g 4153 elpwg 3582 |
[Suppes] p. 47 | Theorem
87 | pwid 3589 |
[Suppes] p. 47 | Theorem
89 | pw0 3738 |
[Suppes] p. 48 | Theorem
90 | pwpw0ss 3802 |
[Suppes] p. 52 | Theorem
101 | xpss12 4730 |
[Suppes] p. 52 | Theorem
102 | xpindi 4758 xpindir 4759 |
[Suppes] p. 52 | Theorem
103 | xpundi 4679 xpundir 4680 |
[Suppes] p. 54 | Theorem
105 | elirrv 4544 |
[Suppes] p. 58 | Theorem
2 | relss 4710 |
[Suppes] p. 59 | Theorem
4 | eldm 4820 eldm2 4821 eldm2g 4819 eldmg 4818 |
[Suppes] p. 59 | Definition
3 | df-dm 4633 |
[Suppes] p. 60 | Theorem
6 | dmin 4831 |
[Suppes] p. 60 | Theorem
8 | rnun 5033 |
[Suppes] p. 60 | Theorem
9 | rnin 5034 |
[Suppes] p. 60 | Definition
4 | dfrn2 4811 |
[Suppes] p. 61 | Theorem
11 | brcnv 4806 brcnvg 4804 |
[Suppes] p. 62 | Equation
5 | elcnv 4800 elcnv2 4801 |
[Suppes] p. 62 | Theorem
12 | relcnv 5002 |
[Suppes] p. 62 | Theorem
15 | cnvin 5032 |
[Suppes] p. 62 | Theorem
16 | cnvun 5030 |
[Suppes] p. 63 | Theorem
20 | co02 5138 |
[Suppes] p. 63 | Theorem
21 | dmcoss 4892 |
[Suppes] p. 63 | Definition
7 | df-co 4632 |
[Suppes] p. 64 | Theorem
26 | cnvco 4808 |
[Suppes] p. 64 | Theorem
27 | coass 5143 |
[Suppes] p. 65 | Theorem
31 | resundi 4916 |
[Suppes] p. 65 | Theorem
34 | elima 4971 elima2 4972 elima3 4973 elimag 4970 |
[Suppes] p. 65 | Theorem
35 | imaundi 5037 |
[Suppes] p. 66 | Theorem
40 | dminss 5039 |
[Suppes] p. 66 | Theorem
41 | imainss 5040 |
[Suppes] p. 67 | Exercise
11 | cnvxp 5043 |
[Suppes] p. 81 | Definition
34 | dfec2 6532 |
[Suppes] p. 82 | Theorem
72 | elec 6568 elecg 6567 |
[Suppes] p. 82 | Theorem
73 | erth 6573 erth2 6574 |
[Suppes] p. 89 | Theorem
96 | map0b 6681 |
[Suppes] p. 89 | Theorem
97 | map0 6683 map0g 6682 |
[Suppes] p. 89 | Theorem
98 | mapsn 6684 |
[Suppes] p. 89 | Theorem
99 | mapss 6685 |
[Suppes] p. 92 | Theorem
1 | enref 6759 enrefg 6758 |
[Suppes] p. 92 | Theorem
2 | ensym 6775 ensymb 6774 ensymi 6776 |
[Suppes] p. 92 | Theorem
3 | entr 6778 |
[Suppes] p. 92 | Theorem
4 | unen 6810 |
[Suppes] p. 94 | Theorem
15 | endom 6757 |
[Suppes] p. 94 | Theorem
16 | ssdomg 6772 |
[Suppes] p. 94 | Theorem
17 | domtr 6779 |
[Suppes] p. 95 | Theorem
18 | isbth 6960 |
[Suppes] p. 98 | Exercise
4 | fundmen 6800 fundmeng 6801 |
[Suppes] p. 98 | Exercise
6 | xpdom3m 6828 |
[Suppes] p.
130 | Definition 3 | df-tr 4099 |
[Suppes] p. 132 | Theorem
9 | ssonuni 4484 |
[Suppes] p.
134 | Definition 6 | df-suc 4368 |
[Suppes] p. 136 | Theorem
Schema 22 | findes 4599 finds 4596 finds1 4598 finds2 4597 |
[Suppes] p.
162 | Definition 5 | df-ltnqqs 7343 df-ltpq 7336 |
[Suppes] p. 228 | Theorem
Schema 61 | onintss 4387 |
[TakeutiZaring] p.
8 | Axiom 1 | ax-ext 2159 |
[TakeutiZaring] p.
13 | Definition 4.5 | df-cleq 2170 |
[TakeutiZaring] p.
13 | Proposition 4.6 | df-clel 2173 |
[TakeutiZaring] p.
13 | Proposition 4.9 | cvjust 2172 |
[TakeutiZaring] p.
13 | Proposition 4.7(3) | eqtr 2195 |
[TakeutiZaring] p.
14 | Definition 4.16 | df-oprab 5873 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 2961 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 3612 elpr2 3613 elprg 3611 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 3607 elsn2 3625 elsn2g 3624 elsng 3606 velsn 3608 |
[TakeutiZaring] p.
15 | Exercise 3 | elop 4228 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 3602 sneqr 3758 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 3610 dfsn2 3605 |
[TakeutiZaring] p.
16 | Axiom 3 | uniex 4434 |
[TakeutiZaring] p.
16 | Exercise 6 | opth 4234 |
[TakeutiZaring] p.
16 | Exercise 8 | rext 4212 |
[TakeutiZaring] p.
16 | Corollary 5.8 | unex 4438 unexg 4440 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 3640 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 3808 |
[TakeutiZaring] p.
16 | Definition 5.6 | df-in 3135 df-un 3133 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 3821 uniprg 3822 |
[TakeutiZaring] p.
17 | Axiom 4 | vpwex 4176 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 3639 |
[TakeutiZaring] p.
17 | Exercise 5 | elsuc 4403 elsucg 4401 sstr2 3162 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3279 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 3327 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3292 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 3345 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 3382 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 3383 |
[TakeutiZaring] p.
17 | Definition 5.9 | dfss2 3144 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 3576 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 3306 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3142 sseqin2 3354 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3175 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 3355 inss2 3356 |
[TakeutiZaring] p.
18 | Exercise 13 | nssr 3215 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 3816 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 4213 |
[TakeutiZaring] p.
18 | Exercise 19 | pweqb 4220 |
[TakeutiZaring] p.
20 | Definition | df-rab 2464 |
[TakeutiZaring] p.
20 | Corollary 5.16 | 0ex 4127 |
[TakeutiZaring] p.
20 | Definition 5.12 | df-dif 3131 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 3424 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 3491 difidALT 3492 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0rf 3435 |
[TakeutiZaring] p.
21 | Theorem 5.22 | setind 4535 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 2739 |
[TakeutiZaring] p.
21 | Proposition 5.21 | vprc 4132 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 3461 |
[TakeutiZaring] p.
22 | Exercise 3 | ssex 4137 ssexg 4139 |
[TakeutiZaring] p.
22 | Exercise 4 | inex1 4134 |
[TakeutiZaring] p.
22 | Exercise 5 | ruv 4546 |
[TakeutiZaring] p.
22 | Exercise 6 | elirr 4537 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0im 3487 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3260 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3ss 3396 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3261 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3269 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 2460 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 2461 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 4738 xpexg 4737 xpexgALT 6128 |
[TakeutiZaring] p.
23 | Definition 6.4(1) | df-rel 4630 |
[TakeutiZaring] p.
23 | Definition 6.4(2) | fun2cnv 5276 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1cnvcnv 5428 fun11 5279 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 5223 svrelfun 5277 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 4810 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 4812 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 4635 |
[TakeutiZaring] p.
24 | Definition 6.6(2) | df-ima 4636 |
[TakeutiZaring] p.
24 | Definition 6.6(3) | df-co 4632 |
[TakeutiZaring] p.
25 | Exercise 2 | cnvcnvss 5079 dfrel2 5075 |
[TakeutiZaring] p.
25 | Exercise 3 | xpss 4731 |
[TakeutiZaring] p.
25 | Exercise 5 | relun 4740 |
[TakeutiZaring] p.
25 | Exercise 6 | reluni 4746 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 4757 |
[TakeutiZaring] p.
25 | Exercise 12 | relres 4931 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 4908 opelresg 4910 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 4924 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 4927 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 4932 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 5253 |
[TakeutiZaring] p.
25 | Exercise 24 | relco 5123 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 5252 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 5429 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2070 |
[TakeutiZaring] p.
26 | Definition 6.11 | df-fv 5220 fv3 5534 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 5163 cnvexg 5162 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 4889 dmexg 4887 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 4890 rnexg 4888 |
[TakeutiZaring] p.
27 | Corollary 6.13 | funfvex 5528 |
[TakeutiZaring] p.
27 | Theorem 6.12(1) | tz6.12-1 5538 tz6.12 5539 tz6.12c 5541 |
[TakeutiZaring] p.
27 | Theorem 6.12(2) | tz6.12-2 5502 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 5215 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 5216 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 5218 wfo 5210 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 5217 wf1 5209 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 5219 wf1o 5211 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 5609 eqfnfv2 5610 eqfnfv2f 5613 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 5582 |
[TakeutiZaring] p.
28 | Theorem 6.16(1) | fnex 5734 fnexALT 6106 |
[TakeutiZaring] p.
28 | Proposition 6.17 | resfunexg 5733 resfunexgALT 6103 |
[TakeutiZaring] p.
29 | Exercise 9 | funimaex 5297 funimaexg 5296 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 4001 |
[TakeutiZaring] p.
30 | Definition 6.21 | eliniseg 4994 iniseg 4996 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 4286 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-isom 5221 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 5805 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 5806 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 5811 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 5813 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 5821 |
[TakeutiZaring] p.
35 | Notation | wtr 4098 |
[TakeutiZaring] p.
35 | Theorem 7.2 | tz7.2 4351 |
[TakeutiZaring] p.
35 | Definition 7.1 | dftr3 4102 |
[TakeutiZaring] p.
36 | Proposition 7.4 | ordwe 4572 |
[TakeutiZaring] p.
36 | Proposition 7.6 | ordelord 4378 |
[TakeutiZaring] p.
37 | Proposition 7.9 | ordin 4382 |
[TakeutiZaring] p.
38 | Corollary 7.15 | ordsson 4488 |
[TakeutiZaring] p.
38 | Definition 7.11 | df-on 4365 |
[TakeutiZaring] p.
38 | Proposition 7.12 | ordon 4482 |
[TakeutiZaring] p.
38 | Proposition 7.13 | onprc 4548 |
[TakeutiZaring] p.
39 | Theorem 7.17 | tfi 4578 |
[TakeutiZaring] p.
40 | Exercise 7 | dftr2 4100 |
[TakeutiZaring] p.
40 | Exercise 11 | unon 4507 |
[TakeutiZaring] p.
40 | Proposition 7.19 | ssorduni 4483 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 3835 |
[TakeutiZaring] p.
41 | Definition 7.22 | df-suc 4368 |
[TakeutiZaring] p.
41 | Proposition 7.23 | sssucid 4412 sucidg 4413 |
[TakeutiZaring] p.
41 | Proposition 7.24 | onsuc 4497 |
[TakeutiZaring] p.
42 | Exercise 1 | df-ilim 4366 |
[TakeutiZaring] p.
42 | Exercise 8 | onsucssi 4502 ordelsuc 4501 |
[TakeutiZaring] p.
42 | Proposition 7.30(1) | peano1 4590 |
[TakeutiZaring] p.
42 | Proposition 7.30(2) | peano2 4591 |
[TakeutiZaring] p.
42 | Proposition 7.30(3) | peano3 4592 |
[TakeutiZaring] p.
43 | Axiom 7 | omex 4589 |
[TakeutiZaring] p.
43 | Theorem 7.32 | ordom 4603 |
[TakeutiZaring] p.
43 | Corollary 7.31 | find 4595 |
[TakeutiZaring] p.
43 | Proposition 7.30(4) | peano4 4593 |
[TakeutiZaring] p.
43 | Proposition 7.30(5) | peano5 4594 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 3856 |
[TakeutiZaring] p.
44 | Exercise 3 | trintssm 4114 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 3857 |
[TakeutiZaring] p.
44 | Exercise 6 | onintonm 4513 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 3843 |
[TakeutiZaring] p.
47 | Lemma 1 | tfrlem1 6303 |
[TakeutiZaring] p.
47 | Theorem 7.41(1) | tfri1 6360 tfri1d 6330 |
[TakeutiZaring] p.
47 | Theorem 7.41(2) | tfri2 6361 tfri2d 6331 |
[TakeutiZaring] p.
47 | Theorem 7.41(3) | tfri3 6362 |
[TakeutiZaring] p.
50 | Exercise 3 | smoiso 6297 |
[TakeutiZaring] p.
50 | Definition 7.46 | df-smo 6281 |
[TakeutiZaring] p.
56 | Definition 8.1 | oasuc 6459 |
[TakeutiZaring] p.
57 | Proposition 8.2 | oacl 6455 |
[TakeutiZaring] p.
57 | Proposition 8.3 | oa0 6452 |
[TakeutiZaring] p.
57 | Proposition 8.16 | omcl 6456 |
[TakeutiZaring] p.
58 | Proposition 8.4 | nnaord 6504 nnaordi 6503 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 3929 uniss2 3838 |
[TakeutiZaring] p.
59 | Proposition 8.7 | oawordriexmid 6465 |
[TakeutiZaring] p.
59 | Proposition 8.9 | nnacl 6475 |
[TakeutiZaring] p.
62 | Exercise 5 | oaword1 6466 |
[TakeutiZaring] p.
62 | Definition 8.15 | om0 6453 omsuc 6467 |
[TakeutiZaring] p.
63 | Proposition 8.17 | nnmcl 6476 |
[TakeutiZaring] p.
63 | Proposition 8.19 | nnmord 6512 nnmordi 6511 |
[TakeutiZaring] p.
67 | Definition 8.30 | oei0 6454 |
[TakeutiZaring] p.
85 | Proposition 10.6(3) | cardonle 7180 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 6789 |
[TakeutiZaring] p.
90 | Proposition 10.20 | nneneq 6851 |
[TakeutiZaring] p.
90 | Corollary 10.21(1) | php5 6852 |
[TakeutiZaring] p.
91 | Definition 10.29 | df-fin 6737 isfi 6755 |
[TakeutiZaring] p.
92 | Proposition 10.33(2) | xpdom2 6825 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 6644 |
[TakeutiZaring] p.
96 | Proposition 10.45 | mapxpen 6842 |
[Tarski] p. 67 | Axiom
B5 | ax-4 1510 |
[Tarski] p. 68 | Lemma
6 | equid 1701 |
[Tarski] p. 69 | Lemma
7 | equcomi 1704 |
[Tarski] p. 70 | Lemma
14 | spim 1738 spime 1741 spimeh 1739 spimh 1737 |
[Tarski] p. 70 | Lemma
16 | ax-11 1506 ax-11o 1823 ax11i 1714 |
[Tarski] p. 70 | Lemmas 16
and 17 | sb6 1886 |
[Tarski] p. 77 | Axiom B6
(p. 75) of system S2 | ax-17 1526 |
[Tarski] p. 77 | Axiom B8
(p. 75) of system S2 | ax-13 2150 ax-14 2151 |
[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 2124 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 1481 |
[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 1635 |
[WhiteheadRussell] p.
160 | Theorem *11.21 | alrot3 1485 |
[WhiteheadRussell] p.
163 | Theorem *11.42 | 19.40-2 1632 |
[WhiteheadRussell] p.
164 | Theorem *11.53 | pm11.53 1895 |
[WhiteheadRussell] p.
175 | Definition *14.02 | df-eu 2029 |
[WhiteheadRussell] p.
178 | Theorem *13.18 | pm13.18 2428 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 2429 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 2875 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 3019 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 5192 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 5193 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2105 eupickbi 2108 |
[WhiteheadRussell] p.
235 | Definition *30.01 | df-fv 5220 |
[WhiteheadRussell] p.
360 | Theorem *54.43 | pm54.43 7183 |