Bibliographic Cross-Reference for the Intuitionistic Logic
Explorer
Bibliographic Reference |
Description | Intuitionistic Logic Explorer Page(s)
|
---|
[AczelRathjen], p.
71 | Definition 8.1.4 | enumct 7071 fidcenum 6912 |
[AczelRathjen], p.
72 | Proposition 8.1.11 | fidcenum 6912 |
[AczelRathjen], p.
73 | Lemma 8.1.14 | enumct 7071 |
[AczelRathjen], p.
73 | Corollary 8.1.13 | ennnfone 12295 |
[AczelRathjen], p.
74 | Lemma 8.1.16 | xpfi 6886 |
[AczelRathjen], p.
74 | Remark 8.1.17 | unfiexmid 6874 |
[AczelRathjen], p.
74 | Theorem 8.1.19 | ctiunct 12310 |
[AczelRathjen], p.
75 | Corollary 8.1.20 | unct 12312 |
[AczelRathjen], p.
75 | Corollary 8.1.23 | qnnen 12301 znnen 12268 |
[AczelRathjen], p.
77 | Lemma 8.1.27 | omctfn 12313 |
[AczelRathjen], p.
78 | Theorem 8.1.28 | omiunct 12314 |
[AczelRathjen], p.
80 | Corollary 8.2.4 | df-ihash 10678 |
[AczelRathjen], p.
183 | Chapter 20 | ax-setind 4508 |
[Apostol] p. 18 | Theorem
I.1 | addcan 8069 addcan2d 8074 addcan2i 8072 addcand 8073 addcani 8071 |
[Apostol] p. 18 | Theorem
I.2 | negeu 8080 |
[Apostol] p. 18 | Theorem
I.3 | negsub 8137 negsubd 8206 negsubi 8167 |
[Apostol] p. 18 | Theorem
I.4 | negneg 8139 negnegd 8191 negnegi 8159 |
[Apostol] p. 18 | Theorem
I.5 | subdi 8274 subdid 8303 subdii 8296 subdir 8275 subdird 8304 subdiri 8297 |
[Apostol] p. 18 | Theorem
I.6 | mul01 8278 mul01d 8282 mul01i 8280 mul02 8276 mul02d 8281 mul02i 8279 |
[Apostol] p. 18 | Theorem
I.9 | divrecapd 8680 |
[Apostol] p. 18 | Theorem
I.10 | recrecapi 8631 |
[Apostol] p. 18 | Theorem
I.12 | mul2neg 8287 mul2negd 8302 mul2negi 8295 mulneg1 8284 mulneg1d 8300 mulneg1i 8293 |
[Apostol] p. 18 | Theorem
I.15 | divdivdivap 8600 |
[Apostol] p. 20 | Axiom
7 | rpaddcl 9604 rpaddcld 9639 rpmulcl 9605 rpmulcld 9640 |
[Apostol] p. 20 | Axiom
9 | 0nrp 9616 |
[Apostol] p. 20 | Theorem
I.17 | lttri 7994 |
[Apostol] p. 20 | Theorem
I.18 | ltadd1d 8427 ltadd1dd 8445 ltadd1i 8391 |
[Apostol] p. 20 | Theorem
I.19 | ltmul1 8481 ltmul1a 8480 ltmul1i 8806 ltmul1ii 8814 ltmul2 8742 ltmul2d 9666 ltmul2dd 9680 ltmul2i 8809 |
[Apostol] p. 20 | Theorem
I.21 | 0lt1 8016 |
[Apostol] p. 20 | Theorem
I.23 | lt0neg1 8357 lt0neg1d 8404 ltneg 8351 ltnegd 8412 ltnegi 8382 |
[Apostol] p. 20 | Theorem
I.25 | lt2add 8334 lt2addd 8456 lt2addi 8399 |
[Apostol] p.
20 | Definition of positive numbers | df-rp 9581 |
[Apostol] p. 21 | Exercise
4 | recgt0 8736 recgt0d 8820 recgt0i 8792 recgt0ii 8793 |
[Apostol] p.
22 | Definition of integers | df-z 9183 |
[Apostol] p.
22 | Definition of rationals | df-q 9549 |
[Apostol] p. 24 | Theorem
I.26 | supeuti 6950 |
[Apostol] p. 26 | Theorem
I.29 | arch 9102 |
[Apostol] p. 28 | Exercise
2 | btwnz 9301 |
[Apostol] p. 28 | Exercise
3 | nnrecl 9103 |
[Apostol] p. 28 | Exercise
6 | qbtwnre 10182 |
[Apostol] p. 28 | Exercise
10(a) | zeneo 11793 zneo 9283 |
[Apostol] p. 29 | Theorem
I.35 | resqrtth 10959 sqrtthi 11047 |
[Apostol] p. 34 | Theorem
I.36 (principle of mathematical induction) | peano5nni 8851 |
[Apostol] p.
363 | Remark | absgt0api 11074 |
[Apostol] p.
363 | Example | abssubd 11121 abssubi 11078 |
[ApostolNT] p.
14 | Definition | df-dvds 11714 |
[ApostolNT] p.
14 | Theorem 1.1(a) | iddvds 11730 |
[ApostolNT] p.
14 | Theorem 1.1(b) | dvdstr 11754 |
[ApostolNT] p.
14 | Theorem 1.1(c) | dvds2ln 11750 |
[ApostolNT] p.
14 | Theorem 1.1(d) | dvdscmul 11744 |
[ApostolNT] p.
14 | Theorem 1.1(e) | dvdscmulr 11746 |
[ApostolNT] p.
14 | Theorem 1.1(f) | 1dvds 11731 |
[ApostolNT] p.
14 | Theorem 1.1(g) | dvds0 11732 |
[ApostolNT] p.
14 | Theorem 1.1(h) | 0dvds 11737 |
[ApostolNT] p.
14 | Theorem 1.1(i) | dvdsleabs 11768 |
[ApostolNT] p.
14 | Theorem 1.1(j) | dvdsabseq 11770 |
[ApostolNT] p.
14 | Theorem 1.1(k) | divconjdvds 11772 |
[ApostolNT] p.
15 | Definition | dfgcd2 11932 |
[ApostolNT] p.
16 | Definition | isprm2 12028 |
[ApostolNT] p.
16 | Theorem 1.5 | coprmdvds 12003 |
[ApostolNT] p.
16 | Theorem 1.4(a) | gcdcom 11891 |
[ApostolNT] p.
16 | Theorem 1.4(b) | gcdass 11933 |
[ApostolNT] p.
16 | Theorem 1.4(c) | absmulgcd 11935 |
[ApostolNT] p.
16 | Theorem 1.4(d)1 | gcd1 11905 |
[ApostolNT] p.
16 | Theorem 1.4(d)2 | gcdid0 11898 |
[ApostolNT] p.
17 | Theorem 1.8 | coprm 12053 |
[ApostolNT] p.
17 | Theorem 1.9 | euclemma 12055 |
[ApostolNT] p.
19 | Theorem 1.14 | divalg 11846 |
[ApostolNT] p.
20 | Theorem 1.15 | eucalg 11970 |
[ApostolNT] p.
25 | Definition | df-phi 12120 |
[ApostolNT] p.
26 | Theorem 2.2 | phisum 12149 |
[ApostolNT] p.
28 | Theorem 2.5(a) | phiprmpw 12131 |
[ApostolNT] p.
28 | Theorem 2.5(c) | phimul 12135 |
[ApostolNT] p.
104 | Definition | congr 12011 |
[ApostolNT] p.
106 | Remark | dvdsval3 11717 |
[ApostolNT] p.
106 | Definition | moddvds 11725 |
[ApostolNT] p.
107 | Example 2 | mod2eq0even 11800 |
[ApostolNT] p.
107 | Example 3 | mod2eq1n2dvds 11801 |
[ApostolNT] p.
107 | Example 4 | zmod1congr 10266 |
[ApostolNT] p.
107 | Theorem 5.2(b) | modqmul12d 10303 |
[ApostolNT] p.
107 | Theorem 5.2(c) | modqexp 10570 |
[ApostolNT] p.
108 | Theorem 5.3 | modmulconst 11749 |
[ApostolNT] p.
109 | Theorem 5.4 | cncongr1 12014 |
[ApostolNT] p.
109 | Theorem 5.4 "Cancellation law" | cncongr 12016 |
[ApostolNT] p.
113 | Theorem 5.17 | eulerth 12142 |
[ApostolNT] p.
113 | Theorem 5.18 | vfermltl 12160 |
[ApostolNT] p.
114 | Theorem 5.19 | fermltl 12143 |
[Bauer] p. 482 | Section
1.2 | pm2.01 606 pm2.65 649 |
[Bauer] p. 483 | Theorem
1.3 | acexmid 5835 onsucelsucexmidlem 4500 |
[Bauer], p.
481 | Section 1.1 | pwtrufal 13711 |
[Bauer], p.
483 | Definition | n0rf 3416 |
[Bauer], p. 483 | Theorem
1.2 | 2irrexpq 13435 2irrexpqap 13437 |
[Bauer], p. 485 | Theorem
2.1 | ssfiexmid 6833 |
[Bauer], p. 494 | Theorem
5.5 | ivthinc 13162 |
[BauerHanson], p.
27 | Proposition 5.2 | cnstab 8534 |
[BauerSwan], p.
14 | Remark | 0ct 7063 ctm 7065 |
[BauerSwan],
p. 14 | Proposition 2.6 | subctctexmid 13715 |
[BauerSwan], p.
14 | Table" is defined as ` ` per | enumct 7071 |
[BauerTaylor], p.
32 | Lemma 6.16 | prarloclem 7433 |
[BauerTaylor], p.
50 | Lemma 11.4 | subhalfnqq 7346 |
[BauerTaylor], p.
52 | Proposition 11.15 | prarloc 7435 |
[BauerTaylor], p.
53 | Lemma 11.16 | addclpr 7469 addlocpr 7468 |
[BauerTaylor], p.
55 | Proposition 12.7 | appdivnq 7495 |
[BauerTaylor], p.
56 | Lemma 12.8 | prmuloc 7498 |
[BauerTaylor], p.
56 | Lemma 12.9 | mullocpr 7503 |
[BellMachover] p.
36 | Lemma 10.3 | idALT 20 |
[BellMachover] p.
97 | Definition 10.1 | df-eu 2016 |
[BellMachover] p.
460 | Notation | df-mo 2017 |
[BellMachover] p.
460 | Definition | mo3 2067 mo3h 2066 |
[BellMachover] p.
462 | Theorem 1.1 | bm1.1 2149 |
[BellMachover] p.
463 | Theorem 1.3ii | bm1.3ii 4097 |
[BellMachover] p.
466 | Axiom Pow | axpow3 4150 |
[BellMachover] p.
466 | Axiom Union | axun2 4407 |
[BellMachover] p.
469 | Theorem 2.2(i) | ordirr 4513 |
[BellMachover] p.
469 | Theorem 2.2(iii) | onelon 4356 |
[BellMachover] p.
469 | Theorem 2.2(vii) | ordn2lp 4516 |
[BellMachover] p.
471 | Problem 2.5(ii) | bm2.5ii 4467 |
[BellMachover] p.
471 | Definition of Lim | df-ilim 4341 |
[BellMachover] p.
472 | Axiom Inf | zfinf2 4560 |
[BellMachover] p.
473 | Theorem 2.8 | limom 4585 |
[Bobzien] p.
116 | Statement T3 | stoic3 1418 |
[Bobzien] p.
117 | Statement T2 | stoic2a 1416 |
[Bobzien] p.
117 | Statement T4 | stoic4a 1419 |
[BourbakiEns] p.
| Proposition 8 | fcof1 5745 fcofo 5746 |
[BourbakiTop1] p.
| Remark | xnegmnf 9756 xnegpnf 9755 |
[BourbakiTop1] p.
| Remark | rexneg 9757 |
[BourbakiTop1] p.
| Proposition | ishmeo 12845 |
[BourbakiTop1] p.
| Property V_i | ssnei2 12698 |
[BourbakiTop1] p.
| Property V_ii | innei 12704 |
[BourbakiTop1] p.
| Property V_iv | neissex 12706 |
[BourbakiTop1] p.
| Proposition 1 | neipsm 12695 neiss 12691 |
[BourbakiTop1] p.
| Proposition 2 | cnptopco 12763 |
[BourbakiTop1] p.
| Proposition 4 | imasnopn 12840 |
[BourbakiTop1] p.
| Property V_iii | elnei 12693 |
[BourbakiTop1] p.
| Definition is due to Bourbaki (Def. 1 | df-top 12537 |
[ChoquetDD] p.
2 | Definition of mapping | df-mpt 4039 |
[Cohen] p.
301 | Remark | relogoprlem 13330 |
[Cohen] p. 301 | Property
2 | relogmul 13331 relogmuld 13346 |
[Cohen] p. 301 | Property
3 | relogdiv 13332 relogdivd 13347 |
[Cohen] p. 301 | Property
4 | relogexp 13334 |
[Cohen] p. 301 | Property
1a | log1 13328 |
[Cohen] p. 301 | Property
1b | loge 13329 |
[Cohen4] p.
348 | Observation | relogbcxpbap 13424 |
[Cohen4] p.
352 | Definition | rpelogb 13408 |
[Cohen4] p. 361 | Property
2 | rprelogbmul 13414 |
[Cohen4] p. 361 | Property
3 | logbrec 13419 rprelogbdiv 13416 |
[Cohen4] p. 361 | Property
4 | rplogbreexp 13412 |
[Cohen4] p. 361 | Property
6 | relogbexpap 13417 |
[Cohen4] p. 361 | Property
1(a) | rplogbid1 13406 |
[Cohen4] p. 361 | Property
1(b) | rplogb1 13407 |
[Cohen4] p.
367 | Property | rplogbchbase 13409 |
[Cohen4] p. 377 | Property
2 | logblt 13421 |
[Crosilla] p. | Axiom
1 | ax-ext 2146 |
[Crosilla] p. | Axiom
2 | ax-pr 4181 |
[Crosilla] p. | Axiom
3 | ax-un 4405 |
[Crosilla] p. | Axiom
4 | ax-nul 4102 |
[Crosilla] p. | Axiom
5 | ax-iinf 4559 |
[Crosilla] p. | Axiom
6 | ru 2945 |
[Crosilla] p. | Axiom
8 | ax-pow 4147 |
[Crosilla] p. | Axiom
9 | ax-setind 4508 |
[Crosilla], p. | Axiom
6 | ax-sep 4094 |
[Crosilla], p. | Axiom
7 | ax-coll 4091 |
[Crosilla], p. | Axiom
7' | repizf 4092 |
[Crosilla], p. | Theorem
is stated | ordtriexmid 4492 |
[Crosilla], p. | Axiom
of choice implies instances | acexmid 5835 |
[Crosilla], p.
| Definition of ordinal | df-iord 4338 |
[Crosilla], p. | Theorem
"Foundation implies instances of EM" | regexmid 4506 |
[Eisenberg] p.
67 | Definition 5.3 | df-dif 3113 |
[Eisenberg] p.
82 | Definition 6.3 | df-iom 4562 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 6607 |
[Enderton] p. 18 | Axiom
of Empty Set | axnul 4101 |
[Enderton] p.
19 | Definition | df-tp 3578 |
[Enderton] p.
26 | Exercise 5 | unissb 3813 |
[Enderton] p.
26 | Exercise 10 | pwel 4190 |
[Enderton] p.
28 | Exercise 7(b) | pwunim 4258 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1m 3929 iinin2m 3928 iunin1 3924 iunin2 3923 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2m 3927 iundif2ss 3925 |
[Enderton] p.
33 | Exercise 23 | iinuniss 3942 |
[Enderton] p.
33 | Exercise 25 | iununir 3943 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 3950 |
[Enderton] p.
33 | Exercise 24(b) | iunpw 4452 iunpwss 3951 |
[Enderton] p.
38 | Exercise 6(a) | unipw 4189 |
[Enderton] p.
38 | Exercise 6(b) | pwuni 4165 |
[Enderton] p. 41 | Lemma
3D | opeluu 4422 rnex 4865
rnexg 4863 |
[Enderton] p.
41 | Exercise 8 | dmuni 4808 rnuni 5009 |
[Enderton] p.
42 | Definition of a function | dffun7 5209 dffun8 5210 |
[Enderton] p.
43 | Definition of function value | funfvdm2 5544 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 5243 |
[Enderton] p.
44 | Definition (d) | dfima2 4942 dfima3 4943 |
[Enderton] p.
47 | Theorem 3H | fvco2 5549 |
[Enderton] p. 49 | Axiom
of Choice (first form) | df-ac 7153 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 5723 |
[Enderton] p.
52 | Definition | df-map 6607 |
[Enderton] p.
53 | Exercise 21 | coass 5116 |
[Enderton] p.
53 | Exercise 27 | dmco 5106 |
[Enderton] p.
53 | Exercise 14(a) | funin 5253 |
[Enderton] p.
53 | Exercise 22(a) | imass2 4974 |
[Enderton] p.
54 | Remark | ixpf 6677 ixpssmap 6689 |
[Enderton] p.
54 | Definition of infinite Cartesian product | df-ixp 6656 |
[Enderton] p.
56 | Theorem 3M | erref 6512 |
[Enderton] p. 57 | Lemma
3N | erthi 6538 |
[Enderton] p.
57 | Definition | df-ec 6494 |
[Enderton] p.
58 | Definition | df-qs 6498 |
[Enderton] p.
60 | Theorem 3Q | th3q 6597 th3qcor 6596 th3qlem1 6594 th3qlem2 6595 |
[Enderton] p.
61 | Exercise 35 | df-ec 6494 |
[Enderton] p.
65 | Exercise 56(a) | dmun 4805 |
[Enderton] p.
68 | Definition of successor | df-suc 4343 |
[Enderton] p.
71 | Definition | df-tr 4075 dftr4 4079 |
[Enderton] p.
72 | Theorem 4E | unisuc 4385 unisucg 4386 |
[Enderton] p.
73 | Exercise 6 | unisuc 4385 unisucg 4386 |
[Enderton] p.
73 | Exercise 5(a) | truni 4088 |
[Enderton] p.
73 | Exercise 5(b) | trint 4089 |
[Enderton] p.
79 | Theorem 4I(A1) | nna0 6433 |
[Enderton] p.
79 | Theorem 4I(A2) | nnasuc 6435 onasuc 6425 |
[Enderton] p.
79 | Definition of operation value | df-ov 5839 |
[Enderton] p.
80 | Theorem 4J(A1) | nnm0 6434 |
[Enderton] p.
80 | Theorem 4J(A2) | nnmsuc 6436 onmsuc 6432 |
[Enderton] p.
81 | Theorem 4K(1) | nnaass 6444 |
[Enderton] p.
81 | Theorem 4K(2) | nna0r 6437 nnacom 6443 |
[Enderton] p.
81 | Theorem 4K(3) | nndi 6445 |
[Enderton] p.
81 | Theorem 4K(4) | nnmass 6446 |
[Enderton] p.
81 | Theorem 4K(5) | nnmcom 6448 |
[Enderton] p.
82 | Exercise 16 | nnm0r 6438 nnmsucr 6447 |
[Enderton] p.
88 | Exercise 23 | nnaordex 6486 |
[Enderton] p.
129 | Definition | df-en 6698 |
[Enderton] p.
132 | Theorem 6B(b) | canth 5790 |
[Enderton] p.
133 | Exercise 1 | xpomen 12265 |
[Enderton] p.
134 | Theorem (Pigeonhole Principle) | phpm 6822 |
[Enderton] p.
136 | Corollary 6E | nneneq 6814 |
[Enderton] p.
139 | Theorem 6H(c) | mapen 6803 |
[Enderton] p.
142 | Theorem 6I(3) | xpdjuen 7165 |
[Enderton] p.
143 | Theorem 6J | dju0en 7161 dju1en 7160 |
[Enderton] p.
144 | Corollary 6K | undif2ss 3479 |
[Enderton] p.
145 | Figure 38 | ffoss 5458 |
[Enderton] p.
145 | Definition | df-dom 6699 |
[Enderton] p.
146 | Example 1 | domen 6708 domeng 6709 |
[Enderton] p.
146 | Example 3 | nndomo 6821 |
[Enderton] p.
149 | Theorem 6L(c) | xpdom1 6792 xpdom1g 6790 xpdom2g 6789 |
[Enderton] p.
168 | Definition | df-po 4268 |
[Enderton] p.
192 | Theorem 7M(a) | oneli 4400 |
[Enderton] p.
192 | Theorem 7M(b) | ontr1 4361 |
[Enderton] p.
192 | Theorem 7M(c) | onirri 4514 |
[Enderton] p.
193 | Corollary 7N(b) | 0elon 4364 |
[Enderton] p.
193 | Corollary 7N(c) | onsuci 4487 |
[Enderton] p.
193 | Corollary 7N(d) | ssonunii 4460 |
[Enderton] p.
194 | Remark | onprc 4523 |
[Enderton] p.
194 | Exercise 16 | suc11 4529 |
[Enderton] p.
197 | Definition | df-card 7127 |
[Enderton] p.
200 | Exercise 25 | tfis 4554 |
[Enderton] p.
206 | Theorem 7X(b) | en2lp 4525 |
[Enderton] p.
207 | Exercise 34 | opthreg 4527 |
[Enderton] p.
208 | Exercise 35 | suc11g 4528 |
[Geuvers], p.
1 | Remark | expap0 10475 |
[Geuvers], p. 6 | Lemma
2.13 | mulap0r 8504 |
[Geuvers], p. 6 | Lemma
2.15 | mulap0 8542 |
[Geuvers], p. 9 | Lemma
2.35 | msqge0 8505 |
[Geuvers], p.
9 | Definition 3.1(2) | ax-arch 7863 |
[Geuvers], p. 10 | Lemma
3.9 | maxcom 11131 |
[Geuvers], p. 10 | Lemma
3.10 | maxle1 11139 maxle2 11140 |
[Geuvers], p. 10 | Lemma
3.11 | maxleast 11141 |
[Geuvers], p. 10 | Lemma
3.12 | maxleb 11144 |
[Geuvers], p.
11 | Definition 3.13 | dfabsmax 11145 |
[Geuvers], p.
17 | Definition 6.1 | df-ap 8471 |
[Gleason] p.
117 | Proposition 9-2.1 | df-enq 7279 enqer 7290 |
[Gleason] p.
117 | Proposition 9-2.2 | df-1nqqs 7283 df-nqqs 7280 |
[Gleason] p.
117 | Proposition 9-2.3 | df-plpq 7276 df-plqqs 7281 |
[Gleason] p.
119 | Proposition 9-2.4 | df-mpq 7277 df-mqqs 7282 |
[Gleason] p.
119 | Proposition 9-2.5 | df-rq 7284 |
[Gleason] p.
119 | Proposition 9-2.6 | ltexnqq 7340 |
[Gleason] p.
120 | Proposition 9-2.6(i) | halfnq 7343 ltbtwnnq 7348 ltbtwnnqq 7347 |
[Gleason] p.
120 | Proposition 9-2.6(ii) | ltanqg 7332 |
[Gleason] p.
120 | Proposition 9-2.6(iii) | ltmnqg 7333 |
[Gleason] p.
123 | Proposition 9-3.5 | addclpr 7469 |
[Gleason] p.
123 | Proposition 9-3.5(i) | addassprg 7511 |
[Gleason] p.
123 | Proposition 9-3.5(ii) | addcomprg 7510 |
[Gleason] p.
123 | Proposition 9-3.5(iii) | ltaddpr 7529 |
[Gleason] p.
123 | Proposition 9-3.5(iv) | ltexpri 7545 |
[Gleason] p.
123 | Proposition 9-3.5(v) | ltaprg 7551 ltaprlem 7550 |
[Gleason] p.
123 | Proposition 9-3.5(vi) | addcanprg 7548 |
[Gleason] p.
124 | Proposition 9-3.7 | mulclpr 7504 |
[Gleason] p. 124 | Theorem
9-3.7(iv) | 1idpr 7524 |
[Gleason] p.
124 | Proposition 9-3.7(i) | mulassprg 7513 |
[Gleason] p.
124 | Proposition 9-3.7(ii) | mulcomprg 7512 |
[Gleason] p.
124 | Proposition 9-3.7(iii) | distrprg 7520 |
[Gleason] p.
124 | Proposition 9-3.7(v) | recexpr 7570 |
[Gleason] p.
126 | Proposition 9-4.1 | df-enr 7658 enrer 7667 |
[Gleason] p.
126 | Proposition 9-4.2 | df-0r 7663 df-1r 7664 df-nr 7659 |
[Gleason] p.
126 | Proposition 9-4.3 | df-mr 7661 df-plr 7660 negexsr 7704 recexsrlem 7706 |
[Gleason] p.
127 | Proposition 9-4.4 | df-ltr 7662 |
[Gleason] p.
130 | Proposition 10-1.3 | creui 8846 creur 8845 cru 8491 |
[Gleason] p.
130 | Definition 10-1.1(v) | ax-cnre 7855 axcnre 7813 |
[Gleason] p.
132 | Definition 10-3.1 | crim 10786 crimd 10905 crimi 10865 crre 10785 crred 10904 crrei 10864 |
[Gleason] p.
132 | Definition 10-3.2 | remim 10788 remimd 10870 |
[Gleason] p.
133 | Definition 10.36 | absval2 10985 absval2d 11113 absval2i 11072 |
[Gleason] p.
133 | Proposition 10-3.4(a) | cjadd 10812 cjaddd 10893 cjaddi 10860 |
[Gleason] p.
133 | Proposition 10-3.4(c) | cjmul 10813 cjmuld 10894 cjmuli 10861 |
[Gleason] p.
133 | Proposition 10-3.4(e) | cjcj 10811 cjcjd 10871 cjcji 10843 |
[Gleason] p.
133 | Proposition 10-3.4(f) | cjre 10810 cjreb 10794 cjrebd 10874 cjrebi 10846 cjred 10899 rere 10793 rereb 10791 rerebd 10873 rerebi 10845 rered 10897 |
[Gleason] p.
133 | Proposition 10-3.4(h) | addcj 10819 addcjd 10885 addcji 10855 |
[Gleason] p.
133 | Proposition 10-3.7(a) | absval 10929 |
[Gleason] p.
133 | Proposition 10-3.7(b) | abscj 10980 abscjd 11118 abscji 11076 |
[Gleason] p.
133 | Proposition 10-3.7(c) | abs00 10992 abs00d 11114 abs00i 11073 absne0d 11115 |
[Gleason] p.
133 | Proposition 10-3.7(d) | releabs 11024 releabsd 11119 releabsi 11077 |
[Gleason] p.
133 | Proposition 10-3.7(f) | absmul 10997 absmuld 11122 absmuli 11079 |
[Gleason] p.
133 | Proposition 10-3.7(g) | sqabsadd 10983 sqabsaddi 11080 |
[Gleason] p.
133 | Proposition 10-3.7(h) | abstri 11032 abstrid 11124 abstrii 11083 |
[Gleason] p.
134 | Definition 10-4.1 | df-exp 10445 exp0 10449 expp1 10452 expp1d 10578 |
[Gleason] p.
135 | Proposition 10-4.2(a) | expadd 10487 expaddd 10579 |
[Gleason] p.
135 | Proposition 10-4.2(b) | cxpmul 13374 cxpmuld 13397 expmul 10490 expmuld 10580 |
[Gleason] p.
135 | Proposition 10-4.2(c) | mulexp 10484 mulexpd 10592 rpmulcxp 13371 |
[Gleason] p.
141 | Definition 11-2.1 | fzval 9937 |
[Gleason] p.
168 | Proposition 12-2.1(a) | climadd 11253 |
[Gleason] p.
168 | Proposition 12-2.1(b) | climsub 11255 |
[Gleason] p.
168 | Proposition 12-2.1(c) | climmul 11254 |
[Gleason] p.
171 | Corollary 12-2.2 | climmulc2 11258 |
[Gleason] p.
172 | Corollary 12-2.5 | climrecl 11251 |
[Gleason] p.
172 | Proposition 12-2.4(c) | climabs 11247 climcj 11248 climim 11250 climre 11249 |
[Gleason] p.
173 | Definition 12-3.1 | df-ltxr 7929 df-xr 7928 ltxr 9702 |
[Gleason] p. 180 | Theorem
12-5.3 | climcau 11274 |
[Gleason] p. 217 | Lemma
13-4.1 | btwnzge0 10225 |
[Gleason] p.
223 | Definition 14-1.1 | df-met 12530 |
[Gleason] p.
223 | Definition 14-1.1(a) | met0 12905 xmet0 12904 |
[Gleason] p.
223 | Definition 14-1.1(c) | metsym 12912 |
[Gleason] p.
223 | Definition 14-1.1(d) | mettri 12914 mstri 13014 xmettri 12913 xmstri 13013 |
[Gleason] p.
230 | Proposition 14-2.6 | txlm 12820 |
[Gleason] p.
240 | Proposition 14-4.2 | metcnp3 13052 |
[Gleason] p.
243 | Proposition 14-4.16 | addcn2 11237 addcncntop 13093 mulcn2 11239 mulcncntop 13095 subcn2 11238 subcncntop 13094 |
[Gleason] p.
295 | Remark | bcval3 10653 bcval4 10654 |
[Gleason] p.
295 | Equation 2 | bcpasc 10668 |
[Gleason] p.
295 | Definition of binomial coefficient | bcval 10651 df-bc 10650 |
[Gleason] p.
296 | Remark | bcn0 10657 bcnn 10659 |
[Gleason] p. 296 | Theorem
15-2.8 | binom 11411 |
[Gleason] p.
308 | Equation 2 | ef0 11599 |
[Gleason] p.
308 | Equation 3 | efcj 11600 |
[Gleason] p.
309 | Corollary 15-4.3 | efne0 11605 |
[Gleason] p.
309 | Corollary 15-4.4 | efexp 11609 |
[Gleason] p.
310 | Equation 14 | sinadd 11663 |
[Gleason] p.
310 | Equation 15 | cosadd 11664 |
[Gleason] p.
311 | Equation 17 | sincossq 11675 |
[Gleason] p.
311 | Equation 18 | cosbnd 11680 sinbnd 11679 |
[Gleason] p.
311 | Definition of ` ` | df-pi 11580 |
[Hamilton] p.
31 | Example 2.7(a) | idALT 20 |
[Hamilton] p. 73 | Rule
1 | ax-mp 5 |
[Hamilton] p. 74 | Rule
2 | ax-gen 1436 |
[Heyting] p.
127 | Axiom #1 | ax1hfs 13784 |
[Hitchcock] p. 5 | Rule
A3 | mptnan 1412 |
[Hitchcock] p. 5 | Rule
A4 | mptxor 1413 |
[Hitchcock] p. 5 | Rule
A5 | mtpxor 1415 |
[HoTT], p. | Lemma
10.4.1 | exmidontriim 7172 |
[HoTT], p. | Theorem
7.2.6 | nndceq 6458 |
[HoTT], p.
| Exercise 11.10 | neapmkv 13780 |
[HoTT], p. | Exercise
11.11 | mulap0bd 8545 |
[HoTT], p. | Section
11.2.1 | df-iltp 7402 df-imp 7401 df-iplp 7400 df-reap 8464 |
[HoTT], p. | Theorem
11.2.12 | cauappcvgpr 7594 |
[HoTT], p. | Corollary
11.4.3 | conventions 13439 |
[HoTT], p.
| Exercise 11.6(i) | dcapnconst 13773 dceqnconst 13772 |
[HoTT], p. | Corollary
11.2.13 | axcaucvg 7832 caucvgpr 7614 caucvgprpr 7644 caucvgsr 7734 |
[HoTT], p. | Definition
11.2.1 | df-inp 7398 |
[HoTT], p.
| Exercise 11.6(ii) | nconstwlpo 13778 |
[HoTT], p. | Proposition
11.2.3 | df-iso 4269 ltpopr 7527 ltsopr 7528 |
[HoTT], p. | Definition
11.2.7(v) | apsym 8495 reapcotr 8487 reapirr 8466 |
[HoTT], p. | Definition
11.2.7(vi) | 0lt1 8016 gt0add 8462 leadd1 8319 lelttr 7978 lemul1a 8744 lenlt 7965 ltadd1 8318 ltletr 7979 ltmul1 8481 reaplt 8477 |
[Jech] p. 4 | Definition of
class | cv 1341 cvjust 2159 |
[Jech] p.
78 | Note | opthprc 4649 |
[KalishMontague] p.
81 | Note 1 | ax-i9 1517 |
[Kreyszig] p.
3 | Property M1 | metcl 12894 xmetcl 12893 |
[Kreyszig] p.
4 | Property M2 | meteq0 12901 |
[Kreyszig] p.
12 | Equation 5 | muleqadd 8556 |
[Kreyszig] p.
18 | Definition 1.3-2 | mopnval 12983 |
[Kreyszig] p.
19 | Remark | mopntopon 12984 |
[Kreyszig] p.
19 | Theorem T1 | mopn0 13029 mopnm 12989 |
[Kreyszig] p.
19 | Theorem T2 | unimopn 13027 |
[Kreyszig] p.
19 | Definition of neighborhood | neibl 13032 |
[Kreyszig] p.
20 | Definition 1.3-3 | metcnp2 13054 |
[Kreyszig] p.
25 | Definition 1.4-1 | lmbr 12754 |
[Kunen] p. 10 | Axiom
0 | a9e 1683 |
[Kunen] p. 12 | Axiom
6 | zfrep6 4093 |
[Kunen] p. 24 | Definition
10.24 | mapval 6617 mapvalg 6615 |
[Kunen] p. 31 | Definition
10.24 | mapex 6611 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 3870 |
[Levy] p.
338 | Axiom | df-clab 2151 df-clel 2160 df-cleq 2157 |
[Lopez-Astorga] p.
12 | Rule 1 | mptnan 1412 |
[Lopez-Astorga] p.
12 | Rule 2 | mptxor 1413 |
[Lopez-Astorga] p.
12 | Rule 3 | mtpxor 1415 |
[Margaris] p. 40 | Rule
C | exlimiv 1585 |
[Margaris] p. 49 | Axiom
A1 | ax-1 6 |
[Margaris] p. 49 | Axiom
A2 | ax-2 7 |
[Margaris] p. 49 | Axiom
A3 | condc 843 |
[Margaris] p.
49 | Definition | dfbi2 386 dfordc 882 exalim 1489 |
[Margaris] p.
51 | Theorem 1 | idALT 20 |
[Margaris] p.
56 | Theorem 3 | syld 45 |
[Margaris] p.
60 | Theorem 8 | jcn 641 |
[Margaris] p.
89 | Theorem 19.2 | 19.2 1625 r19.2m 3490 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 1541 19.3h 1540 rr19.3v 2860 |
[Margaris] p.
89 | Theorem 19.5 | alcom 1465 |
[Margaris] p.
89 | Theorem 19.6 | alexdc 1606 alexim 1632 |
[Margaris] p.
89 | Theorem 19.7 | alnex 1486 |
[Margaris] p.
89 | Theorem 19.8 | 19.8a 1577 spsbe 1829 |
[Margaris] p.
89 | Theorem 19.9 | 19.9 1631 19.9h 1630 19.9v 1858 exlimd 1584 |
[Margaris] p.
89 | Theorem 19.11 | excom 1651 excomim 1650 |
[Margaris] p.
89 | Theorem 19.12 | 19.12 1652 r19.12 2570 |
[Margaris] p.
90 | Theorem 19.14 | exnalim 1633 |
[Margaris] p.
90 | Theorem 19.15 | albi 1455 ralbi 2596 |
[Margaris] p.
90 | Theorem 19.16 | 19.16 1542 |
[Margaris] p.
90 | Theorem 19.17 | 19.17 1543 |
[Margaris] p.
90 | Theorem 19.18 | exbi 1591 rexbi 2597 |
[Margaris] p.
90 | Theorem 19.19 | 19.19 1653 |
[Margaris] p.
90 | Theorem 19.20 | alim 1444 alimd 1508 alimdh 1454 alimdv 1866 ralimdaa 2530 ralimdv 2532 ralimdva 2531 ralimdvva 2533 sbcimdv 3011 |
[Margaris] p.
90 | Theorem 19.21 | 19.21-2 1654 19.21 1570 19.21bi 1545 19.21h 1544 19.21ht 1568 19.21t 1569 19.21v 1860 alrimd 1597 alrimdd 1596 alrimdh 1466 alrimdv 1863 alrimi 1509 alrimih 1456 alrimiv 1861 alrimivv 1862 r19.21 2540 r19.21be 2555 r19.21bi 2552 r19.21t 2539 r19.21v 2541 ralrimd 2542 ralrimdv 2543 ralrimdva 2544 ralrimdvv 2548 ralrimdvva 2549 ralrimi 2535 ralrimiv 2536 ralrimiva 2537 ralrimivv 2545 ralrimivva 2546 ralrimivvva 2547 ralrimivw 2538 rexlimi 2574 |
[Margaris] p.
90 | Theorem 19.22 | 2alimdv 1868 2eximdv 1869 exim 1586
eximd 1599 eximdh 1598 eximdv 1867 rexim 2558 reximdai 2562 reximddv 2567 reximddv2 2569 reximdv 2565 reximdv2 2563 reximdva 2566 reximdvai 2564 reximi2 2560 |
[Margaris] p.
90 | Theorem 19.23 | 19.23 1665 19.23bi 1579 19.23h 1485 19.23ht 1484 19.23t 1664 19.23v 1870 19.23vv 1871 exlimd2 1582 exlimdh 1583 exlimdv 1806 exlimdvv 1884 exlimi 1581 exlimih 1580 exlimiv 1585 exlimivv 1883 r19.23 2572 r19.23v 2573 rexlimd 2578 rexlimdv 2580 rexlimdv3a 2583 rexlimdva 2581 rexlimdva2 2584 rexlimdvaa 2582 rexlimdvv 2588 rexlimdvva 2589 rexlimdvw 2585 rexlimiv 2575 rexlimiva 2576 rexlimivv 2587 |
[Margaris] p.
90 | Theorem 19.24 | i19.24 1626 |
[Margaris] p.
90 | Theorem 19.25 | 19.25 1613 |
[Margaris] p.
90 | Theorem 19.26 | 19.26-2 1469 19.26-3an 1470 19.26 1468 r19.26-2 2593 r19.26-3 2594 r19.26 2590 r19.26m 2595 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 1548 19.27h 1547 19.27v 1886 r19.27av 2599 r19.27m 3499 r19.27mv 3500 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 1550 19.28h 1549 19.28v 1887 r19.28av 2600 r19.28m 3493 r19.28mv 3496 rr19.28v 2861 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1607 19.29r 1608 19.29r2 1609 19.29x 1610 r19.29 2601 r19.29d2r 2608 r19.29r 2602 |
[Margaris] p.
90 | Theorem 19.30 | 19.30dc 1614 |
[Margaris] p.
90 | Theorem 19.31 | 19.31r 1668 |
[Margaris] p.
90 | Theorem 19.32 | 19.32dc 1666 19.32r 1667 r19.32r 2610 r19.32vdc 2613 r19.32vr 2612 |
[Margaris] p.
90 | Theorem 19.33 | 19.33 1471 19.33b2 1616 19.33bdc 1617 |
[Margaris] p.
90 | Theorem 19.34 | 19.34 1671 |
[Margaris] p.
90 | Theorem 19.35 | 19.35-1 1611 19.35i 1612 |
[Margaris] p.
90 | Theorem 19.36 | 19.36-1 1660 19.36aiv 1888 19.36i 1659 r19.36av 2615 |
[Margaris] p.
90 | Theorem 19.37 | 19.37-1 1661 19.37aiv 1662 r19.37 2616 r19.37av 2617 |
[Margaris] p.
90 | Theorem 19.38 | 19.38 1663 |
[Margaris] p.
90 | Theorem 19.39 | i19.39 1627 |
[Margaris] p.
90 | Theorem 19.40 | 19.40-2 1619 19.40 1618 r19.40 2618 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 1673 19.41h 1672 19.41v 1889 19.41vv 1890 19.41vvv 1891 19.41vvvv 1892 r19.41 2619 r19.41v 2620 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 1675 19.42h 1674 19.42v 1893 19.42vv 1898 19.42vvv 1899 19.42vvvv 1900 r19.42v 2621 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1615 r19.43 2622 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 1669 r19.44av 2623 r19.44mv 3498 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 1670 r19.45av 2624 r19.45mv 3497 |
[Margaris] p.
110 | Exercise 2(b) | eu1 2038 |
[Megill] p. 444 | Axiom
C5 | ax-17 1513 |
[Megill] p. 445 | Lemma
L12 | alequcom 1502 ax-10 1492 |
[Megill] p. 446 | Lemma
L17 | equtrr 1697 |
[Megill] p. 446 | Lemma
L19 | hbnae 1708 |
[Megill] p. 447 | Remark
9.1 | df-sb 1750 sbid 1761 |
[Megill] p. 448 | Scheme
C5' | ax-4 1497 |
[Megill] p. 448 | Scheme
C6' | ax-7 1435 |
[Megill] p. 448 | Scheme
C8' | ax-8 1491 |
[Megill] p. 448 | Scheme
C9' | ax-i12 1494 |
[Megill] p. 448 | Scheme
C11' | ax-10o 1703 |
[Megill] p. 448 | Scheme
C12' | ax-13 2137 |
[Megill] p. 448 | Scheme
C13' | ax-14 2138 |
[Megill] p. 448 | Scheme
C15' | ax-11o 1810 |
[Megill] p. 448 | Scheme
C16' | ax-16 1801 |
[Megill] p. 448 | Theorem
9.4 | dral1 1717 dral2 1718 drex1 1785 drex2 1719 drsb1 1786 drsb2 1828 |
[Megill] p. 449 | Theorem
9.7 | sbcom2 1974 sbequ 1827 sbid2v 1983 |
[Megill] p. 450 | Example
in Appendix | hba1 1527 |
[Mendelson] p.
36 | Lemma 1.8 | idALT 20 |
[Mendelson] p.
69 | Axiom 4 | rspsbc 3028 rspsbca 3029 stdpc4 1762 |
[Mendelson] p.
69 | Axiom 5 | ra5 3034 stdpc5 1571 |
[Mendelson] p. 81 | Rule
C | exlimiv 1585 |
[Mendelson] p.
95 | Axiom 6 | stdpc6 1690 |
[Mendelson] p.
95 | Axiom 7 | stdpc7 1757 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 3440 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 3441 |
[Mendelson] p.
231 | Exercise 4.10(n) | inssun 3357 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 3405 |
[Mendelson] p.
231 | Exercise 4.10(q) | inssddif 3358 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddifnel 3248 |
[Mendelson] p.
231 | Definition of union | unssin 3356 |
[Mendelson] p.
235 | Exercise 4.12(c) | univ 4448 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 3782 |
[Mendelson] p.
235 | Exercise 4.12(j) | pwin 4254 |
[Mendelson] p.
235 | Exercise 4.12(k) | pwunss 4255 |
[Mendelson] p.
235 | Exercise 4.12(l) | pwssunim 4256 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 3803 |
[Mendelson] p.
235 | Exercise 4.12(p) | reli 4727 |
[Mendelson] p.
235 | Exercise 4.12(t) | relssdmrn 5118 |
[Mendelson] p.
246 | Definition of successor | df-suc 4343 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 6802 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 6778 xpsneng 6779 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 6784 xpcomeng 6785 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 6787 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 6781 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 6609 |
[Mendelson] p.
255 | Exercise 4.43 | mapsnen 6768 |
[Mendelson] p.
255 | Exercise 4.47 | xpmapen 6807 |
[Mendelson] p.
255 | Exercise 4.42(a) | map0e 6643 |
[Mendelson] p.
255 | Exercise 4.42(b) | map1 6769 |
[Mendelson] p.
258 | Exercise 4.56(c) | djuassen 7164 djucomen 7163 |
[Mendelson] p.
258 | Exercise 4.56(g) | xp2dju 7162 |
[Mendelson] p.
266 | Proposition 4.34(a) | oa1suc 6426 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 3339 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 4686 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 4687 |
[Monk1] p. 34 | Definition
3.3 | df-opab 4038 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5113 coi2 5114 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 4812 rn0 4854 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 5002 |
[Monk1] p. 37 | Theorem
3.13(i) | relxp 4707 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxpm 4818 rnxpm 5027 |
[Monk1] p. 37 | Theorem
3.13(ii) | 0xp 4678 xp0 5017 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 4957 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 4954 |
[Monk1] p. 39 | Theorem
3.17 | imaex 4953 imaexg 4952 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 4951 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 5609 funfvop 5591 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 5524 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 5532 |
[Monk1] p. 43 | Theorem
4.6 | funun 5226 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 5730 dff13f 5732 |
[Monk1] p. 46 | Theorem
4.15(v) | funex 5702 funrnex 6074 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 5724 |
[Monk1] p. 52 | Theorem
5.12(ii) | op2ndb 5081 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 3834 |
[Monk1] p. 52 | Definition
5.13 (i) | 1stval2 6115 df-1st 6100 |
[Monk1] p. 52 | Definition
5.13 (ii) | 2ndval2 6116 df-2nd 6101 |
[Monk2] p. 105 | Axiom
C4 | ax-5 1434 |
[Monk2] p. 105 | Axiom
C7 | ax-8 1491 |
[Monk2] p. 105 | Axiom
C8 | ax-11 1493 ax-11o 1810 |
[Monk2] p. 105 | Axiom
(C8) | ax11v 1814 |
[Monk2] p. 109 | Lemma
12 | ax-7 1435 |
[Monk2] p. 109 | Lemma
15 | equvin 1850 equvini 1745 eqvinop 4215 |
[Monk2] p. 113 | Axiom
C5-1 | ax-17 1513 |
[Monk2] p. 113 | Axiom
C5-2 | ax6b 1638 |
[Monk2] p. 113 | Axiom
C5-3 | ax-7 1435 |
[Monk2] p. 114 | Lemma
22 | hba1 1527 |
[Monk2] p. 114 | Lemma
23 | hbia1 1539 nfia1 1567 |
[Monk2] p. 114 | Lemma
24 | hba2 1538 nfa2 1566 |
[Moschovakis] p.
2 | Chapter 2 | df-stab 821 dftest 13785 |
[Munkres] p. 77 | Example
2 | distop 12626 |
[Munkres] p.
78 | Definition of basis | df-bases 12582 isbasis3g 12585 |
[Munkres] p.
78 | Definition of a topology generated by a basis | df-topgen 12513 tgval2 12592 |
[Munkres] p.
79 | Remark | tgcl 12605 |
[Munkres] p. 80 | Lemma
2.1 | tgval3 12599 |
[Munkres] p. 80 | Lemma
2.2 | tgss2 12620 tgss3 12619 |
[Munkres] p. 81 | Lemma
2.3 | basgen 12621 basgen2 12622 |
[Munkres] p.
89 | Definition of subspace topology | resttop 12711 |
[Munkres] p. 93 | Theorem
6.1(1) | 0cld 12653 topcld 12650 |
[Munkres] p. 93 | Theorem
6.1(3) | uncld 12654 |
[Munkres] p.
94 | Definition of closure | clsval 12652 |
[Munkres] p.
94 | Definition of interior | ntrval 12651 |
[Munkres] p.
102 | Definition of continuous function | df-cn 12729 iscn 12738 iscn2 12741 |
[Munkres] p. 107 | Theorem
7.2(g) | cncnp 12771 cncnp2m 12772 cncnpi 12769 df-cnp 12730 iscnp 12740 |
[Munkres] p. 127 | Theorem
10.1 | metcn 13055 |
[Pierik], p. 8 | Section
2.2.1 | dfrex2fin 6860 |
[Pierik], p. 9 | Definition
2.4 | df-womni 7119 |
[Pierik], p. 9 | Definition
2.5 | df-markov 7107 omniwomnimkv 7122 |
[Pierik], p. 10 | Section
2.3 | dfdif3 3227 |
[Pierik], p.
14 | Definition 3.1 | df-omni 7090 exmidomniim 7096 finomni 7095 |
[Pierik], p. 15 | Section
3.1 | df-nninf 7076 |
[PradicBrown2022], p. 1 | Theorem
1 | exmidsbthr 13736 |
[PradicBrown2022], p.
2 | Remark | exmidpw 6865 |
[PradicBrown2022], p.
2 | Proposition 1.1 | exmidfodomrlemim 7148 |
[PradicBrown2022], p.
2 | Proposition 1.2 | exmidfodomrlemr 7149 exmidfodomrlemrALT 7150 |
[PradicBrown2022], p.
4 | Lemma 3.2 | fodjuomni 7104 |
[PradicBrown2022], p. 5 | Lemma
3.4 | peano3nninf 13721 peano4nninf 13720 |
[PradicBrown2022], p. 5 | Lemma
3.5 | nninfall 13723 |
[PradicBrown2022], p. 5 | Theorem
3.6 | nninfsel 13731 |
[PradicBrown2022], p. 5 | Corollary
3.7 | nninfomni 13733 |
[PradicBrown2022], p. 5 | Definition
3.3 | nnsf 13719 |
[Quine] p. 16 | Definition
2.1 | df-clab 2151 rabid 2639 |
[Quine] p. 17 | Definition
2.1'' | dfsb7 1978 |
[Quine] p. 18 | Definition
2.7 | df-cleq 2157 |
[Quine] p. 19 | Definition
2.9 | df-v 2723 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2273 |
[Quine] p. 35 | Theorem
5.2 | abid2 2285 abid2f 2332 |
[Quine] p. 40 | Theorem
6.1 | sb5 1874 |
[Quine] p. 40 | Theorem
6.2 | sb56 1872 sb6 1873 |
[Quine] p. 41 | Theorem
6.3 | df-clel 2160 |
[Quine] p. 41 | Theorem
6.4 | eqid 2164 |
[Quine] p. 41 | Theorem
6.5 | eqcom 2166 |
[Quine] p. 42 | Theorem
6.6 | df-sbc 2947 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 2948 dfsbcq2 2949 |
[Quine] p. 43 | Theorem
6.8 | vex 2724 |
[Quine] p. 43 | Theorem
6.9 | isset 2727 |
[Quine] p. 44 | Theorem
7.3 | spcgf 2803 spcgv 2808 spcimgf 2801 |
[Quine] p. 44 | Theorem
6.11 | spsbc 2957 spsbcd 2958 |
[Quine] p. 44 | Theorem
6.12 | elex 2732 |
[Quine] p. 44 | Theorem
6.13 | elab 2865 elabg 2867 elabgf 2863 |
[Quine] p. 44 | Theorem
6.14 | noel 3408 |
[Quine] p. 48 | Theorem
7.2 | snprc 3635 |
[Quine] p. 48 | Definition
7.1 | df-pr 3577 df-sn 3576 |
[Quine] p. 49 | Theorem
7.4 | snss 3696 snssg 3703 |
[Quine] p. 49 | Theorem
7.5 | prss 3723 prssg 3724 |
[Quine] p. 49 | Theorem
7.6 | prid1 3676 prid1g 3674 prid2 3677 prid2g 3675 snid 3601
snidg 3599 |
[Quine] p. 51 | Theorem
7.12 | snexg 4157 snexprc 4159 |
[Quine] p. 51 | Theorem
7.13 | prexg 4183 |
[Quine] p. 53 | Theorem
8.2 | unisn 3799 unisng 3800 |
[Quine] p. 53 | Theorem
8.3 | uniun 3802 |
[Quine] p. 54 | Theorem
8.6 | elssuni 3811 |
[Quine] p. 54 | Theorem
8.7 | uni0 3810 |
[Quine] p. 56 | Theorem
8.17 | uniabio 5157 |
[Quine] p. 56 | Definition
8.18 | dfiota2 5148 |
[Quine] p. 57 | Theorem
8.19 | iotaval 5158 |
[Quine] p. 57 | Theorem
8.22 | iotanul 5162 |
[Quine] p. 58 | Theorem
8.23 | euiotaex 5163 |
[Quine] p. 58 | Definition
9.1 | df-op 3579 |
[Quine] p. 61 | Theorem
9.5 | opabid 4229 opelopab 4243 opelopaba 4238 opelopabaf 4245 opelopabf 4246 opelopabg 4240 opelopabga 4235 oprabid 5865 |
[Quine] p. 64 | Definition
9.11 | df-xp 4604 |
[Quine] p. 64 | Definition
9.12 | df-cnv 4606 |
[Quine] p. 64 | Definition
9.15 | df-id 4265 |
[Quine] p. 65 | Theorem
10.3 | fun0 5240 |
[Quine] p. 65 | Theorem
10.4 | funi 5214 |
[Quine] p. 65 | Theorem
10.5 | funsn 5230 funsng 5228 |
[Quine] p. 65 | Definition
10.1 | df-fun 5184 |
[Quine] p. 65 | Definition
10.2 | args 4967 dffv4g 5477 |
[Quine] p. 68 | Definition
10.11 | df-fv 5190 fv2 5475 |
[Quine] p. 124 | Theorem
17.3 | nn0opth2 10626 nn0opth2d 10625 nn0opthd 10624 |
[Quine] p. 284 | Axiom
39(vi) | funimaex 5267 funimaexg 5266 |
[Rudin] p. 164 | Equation
27 | efcan 11603 |
[Rudin] p. 164 | Equation
30 | efzval 11610 |
[Rudin] p. 167 | Equation
48 | absefi 11695 |
[Sanford] p.
39 | Remark | ax-mp 5 |
[Sanford] p. 39 | Rule
3 | mtpxor 1415 |
[Sanford] p. 39 | Rule
4 | mptxor 1413 |
[Sanford] p. 40 | Rule
1 | mptnan 1412 |
[Schechter] p.
51 | Definition of antisymmetry | intasym 4982 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 4984 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 4981 |
[Schechter] p.
51 | Definition of transitivity | cotr 4979 |
[Schechter] p.
428 | Definition 15.35 | bastop1 12624 |
[Stoll] p. 13 | Definition
of symmetric difference | symdif1 3382 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 3475 dif0 3474 |
[Stoll] p. 16 | Exercise
4.8 | difdifdirss 3488 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 3375 |
[Stoll] p. 19 | Theorem
5.2(13') | indmss 3376 |
[Stoll] p.
20 | Remark | invdif 3359 |
[Stoll] p. 25 | Definition
of ordered triple | df-ot 3580 |
[Stoll] p.
43 | Definition | uniiun 3913 |
[Stoll] p.
44 | Definition | intiin 3914 |
[Stoll] p.
45 | Definition | df-iin 3863 |
[Stoll] p. 45 | Definition
indexed union | df-iun 3862 |
[Stoll] p. 176 | Theorem
3.4(27) | imandc 879 imanst 878 |
[Stoll] p. 262 | Example
4.1 | symdif1 3382 |
[Suppes] p. 22 | Theorem
2 | eq0 3422 |
[Suppes] p. 22 | Theorem
4 | eqss 3152 eqssd 3154 eqssi 3153 |
[Suppes] p. 23 | Theorem
5 | ss0 3444 ss0b 3443 |
[Suppes] p. 23 | Theorem
6 | sstr 3145 |
[Suppes] p. 25 | Theorem
12 | elin 3300 elun 3258 |
[Suppes] p. 26 | Theorem
15 | inidm 3326 |
[Suppes] p. 26 | Theorem
16 | in0 3438 |
[Suppes] p. 27 | Theorem
23 | unidm 3260 |
[Suppes] p. 27 | Theorem
24 | un0 3437 |
[Suppes] p. 27 | Theorem
25 | ssun1 3280 |
[Suppes] p. 27 | Theorem
26 | ssequn1 3287 |
[Suppes] p. 27 | Theorem
27 | unss 3291 |
[Suppes] p. 27 | Theorem
28 | indir 3366 |
[Suppes] p. 27 | Theorem
29 | undir 3367 |
[Suppes] p. 28 | Theorem
32 | difid 3472 difidALT 3473 |
[Suppes] p. 29 | Theorem
33 | difin 3354 |
[Suppes] p. 29 | Theorem
34 | indif 3360 |
[Suppes] p. 29 | Theorem
35 | undif1ss 3478 |
[Suppes] p. 29 | Theorem
36 | difun2 3483 |
[Suppes] p. 29 | Theorem
37 | difin0 3477 |
[Suppes] p. 29 | Theorem
38 | disjdif 3476 |
[Suppes] p. 29 | Theorem
39 | difundi 3369 |
[Suppes] p. 29 | Theorem
40 | difindiss 3371 |
[Suppes] p. 30 | Theorem
41 | nalset 4106 |
[Suppes] p. 39 | Theorem
61 | uniss 3804 |
[Suppes] p. 39 | Theorem
65 | uniop 4227 |
[Suppes] p. 41 | Theorem
70 | intsn 3853 |
[Suppes] p. 42 | Theorem
71 | intpr 3850 intprg 3851 |
[Suppes] p. 42 | Theorem
73 | op1stb 4450 op1stbg 4451 |
[Suppes] p. 42 | Theorem
78 | intun 3849 |
[Suppes] p. 44 | Definition
15(a) | dfiun2 3894 dfiun2g 3892 |
[Suppes] p. 44 | Definition
15(b) | dfiin2 3895 |
[Suppes] p. 47 | Theorem
86 | elpw 3559 elpw2 4130 elpw2g 4129 elpwg 3561 |
[Suppes] p. 47 | Theorem
87 | pwid 3568 |
[Suppes] p. 47 | Theorem
89 | pw0 3714 |
[Suppes] p. 48 | Theorem
90 | pwpw0ss 3778 |
[Suppes] p. 52 | Theorem
101 | xpss12 4705 |
[Suppes] p. 52 | Theorem
102 | xpindi 4733 xpindir 4734 |
[Suppes] p. 52 | Theorem
103 | xpundi 4654 xpundir 4655 |
[Suppes] p. 54 | Theorem
105 | elirrv 4519 |
[Suppes] p. 58 | Theorem
2 | relss 4685 |
[Suppes] p. 59 | Theorem
4 | eldm 4795 eldm2 4796 eldm2g 4794 eldmg 4793 |
[Suppes] p. 59 | Definition
3 | df-dm 4608 |
[Suppes] p. 60 | Theorem
6 | dmin 4806 |
[Suppes] p. 60 | Theorem
8 | rnun 5006 |
[Suppes] p. 60 | Theorem
9 | rnin 5007 |
[Suppes] p. 60 | Definition
4 | dfrn2 4786 |
[Suppes] p. 61 | Theorem
11 | brcnv 4781 brcnvg 4779 |
[Suppes] p. 62 | Equation
5 | elcnv 4775 elcnv2 4776 |
[Suppes] p. 62 | Theorem
12 | relcnv 4976 |
[Suppes] p. 62 | Theorem
15 | cnvin 5005 |
[Suppes] p. 62 | Theorem
16 | cnvun 5003 |
[Suppes] p. 63 | Theorem
20 | co02 5111 |
[Suppes] p. 63 | Theorem
21 | dmcoss 4867 |
[Suppes] p. 63 | Definition
7 | df-co 4607 |
[Suppes] p. 64 | Theorem
26 | cnvco 4783 |
[Suppes] p. 64 | Theorem
27 | coass 5116 |
[Suppes] p. 65 | Theorem
31 | resundi 4891 |
[Suppes] p. 65 | Theorem
34 | elima 4945 elima2 4946 elima3 4947 elimag 4944 |
[Suppes] p. 65 | Theorem
35 | imaundi 5010 |
[Suppes] p. 66 | Theorem
40 | dminss 5012 |
[Suppes] p. 66 | Theorem
41 | imainss 5013 |
[Suppes] p. 67 | Exercise
11 | cnvxp 5016 |
[Suppes] p. 81 | Definition
34 | dfec2 6495 |
[Suppes] p. 82 | Theorem
72 | elec 6531 elecg 6530 |
[Suppes] p. 82 | Theorem
73 | erth 6536 erth2 6537 |
[Suppes] p. 89 | Theorem
96 | map0b 6644 |
[Suppes] p. 89 | Theorem
97 | map0 6646 map0g 6645 |
[Suppes] p. 89 | Theorem
98 | mapsn 6647 |
[Suppes] p. 89 | Theorem
99 | mapss 6648 |
[Suppes] p. 92 | Theorem
1 | enref 6722 enrefg 6721 |
[Suppes] p. 92 | Theorem
2 | ensym 6738 ensymb 6737 ensymi 6739 |
[Suppes] p. 92 | Theorem
3 | entr 6741 |
[Suppes] p. 92 | Theorem
4 | unen 6773 |
[Suppes] p. 94 | Theorem
15 | endom 6720 |
[Suppes] p. 94 | Theorem
16 | ssdomg 6735 |
[Suppes] p. 94 | Theorem
17 | domtr 6742 |
[Suppes] p. 95 | Theorem
18 | isbth 6923 |
[Suppes] p. 98 | Exercise
4 | fundmen 6763 fundmeng 6764 |
[Suppes] p. 98 | Exercise
6 | xpdom3m 6791 |
[Suppes] p.
130 | Definition 3 | df-tr 4075 |
[Suppes] p. 132 | Theorem
9 | ssonuni 4459 |
[Suppes] p.
134 | Definition 6 | df-suc 4343 |
[Suppes] p. 136 | Theorem
Schema 22 | findes 4574 finds 4571 finds1 4573 finds2 4572 |
[Suppes] p.
162 | Definition 5 | df-ltnqqs 7285 df-ltpq 7278 |
[Suppes] p. 228 | Theorem
Schema 61 | onintss 4362 |
[TakeutiZaring] p.
8 | Axiom 1 | ax-ext 2146 |
[TakeutiZaring] p.
13 | Definition 4.5 | df-cleq 2157 |
[TakeutiZaring] p.
13 | Proposition 4.6 | df-clel 2160 |
[TakeutiZaring] p.
13 | Proposition 4.9 | cvjust 2159 |
[TakeutiZaring] p.
13 | Proposition 4.7(3) | eqtr 2182 |
[TakeutiZaring] p.
14 | Definition 4.16 | df-oprab 5840 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 2945 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 3591 elpr2 3592 elprg 3590 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 3586 elsn2 3604 elsn2g 3603 elsng 3585 velsn 3587 |
[TakeutiZaring] p.
15 | Exercise 3 | elop 4203 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 3581 sneqr 3734 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 3589 dfsn2 3584 |
[TakeutiZaring] p.
16 | Axiom 3 | uniex 4409 |
[TakeutiZaring] p.
16 | Exercise 6 | opth 4209 |
[TakeutiZaring] p.
16 | Exercise 8 | rext 4187 |
[TakeutiZaring] p.
16 | Corollary 5.8 | unex 4413 unexg 4415 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 3619 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 3784 |
[TakeutiZaring] p.
16 | Definition 5.6 | df-in 3117 df-un 3115 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 3797 uniprg 3798 |
[TakeutiZaring] p.
17 | Axiom 4 | vpwex 4152 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 3618 |
[TakeutiZaring] p.
17 | Exercise 5 | elsuc 4378 elsucg 4376 sstr2 3144 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3261 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 3309 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3274 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 3327 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 3364 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 3365 |
[TakeutiZaring] p.
17 | Definition 5.9 | dfss2 3126 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 3555 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 3288 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3124 sseqin2 3336 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3157 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 3337 inss2 3338 |
[TakeutiZaring] p.
18 | Exercise 13 | nssr 3197 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 3792 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 4188 |
[TakeutiZaring] p.
18 | Exercise 19 | pweqb 4195 |
[TakeutiZaring] p.
20 | Definition | df-rab 2451 |
[TakeutiZaring] p.
20 | Corollary 5.16 | 0ex 4103 |
[TakeutiZaring] p.
20 | Definition 5.12 | df-dif 3113 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 3406 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 3472 difidALT 3473 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0rf 3416 |
[TakeutiZaring] p.
21 | Theorem 5.22 | setind 4510 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 2723 |
[TakeutiZaring] p.
21 | Proposition 5.21 | vprc 4108 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 3442 |
[TakeutiZaring] p.
22 | Exercise 3 | ssex 4113 ssexg 4115 |
[TakeutiZaring] p.
22 | Exercise 4 | inex1 4110 |
[TakeutiZaring] p.
22 | Exercise 5 | ruv 4521 |
[TakeutiZaring] p.
22 | Exercise 6 | elirr 4512 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0im 3468 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3242 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3ss 3378 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3243 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3251 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 2447 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 2448 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 4713 xpexg 4712 xpexgALT 6093 |
[TakeutiZaring] p.
23 | Definition 6.4(1) | df-rel 4605 |
[TakeutiZaring] p.
23 | Definition 6.4(2) | fun2cnv 5246 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1cnvcnv 5398 fun11 5249 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 5193 svrelfun 5247 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 4785 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 4787 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 4610 |
[TakeutiZaring] p.
24 | Definition 6.6(2) | df-ima 4611 |
[TakeutiZaring] p.
24 | Definition 6.6(3) | df-co 4607 |
[TakeutiZaring] p.
25 | Exercise 2 | cnvcnvss 5052 dfrel2 5048 |
[TakeutiZaring] p.
25 | Exercise 3 | xpss 4706 |
[TakeutiZaring] p.
25 | Exercise 5 | relun 4715 |
[TakeutiZaring] p.
25 | Exercise 6 | reluni 4721 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 4732 |
[TakeutiZaring] p.
25 | Exercise 12 | relres 4906 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 4883 opelresg 4885 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 4899 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 4902 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 4907 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 5223 |
[TakeutiZaring] p.
25 | Exercise 24 | relco 5096 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 5222 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 5399 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2057 |
[TakeutiZaring] p.
26 | Definition 6.11 | df-fv 5190 fv3 5503 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 5136 cnvexg 5135 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 4864 dmexg 4862 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 4865 rnexg 4863 |
[TakeutiZaring] p.
27 | Corollary 6.13 | funfvex 5497 |
[TakeutiZaring] p.
27 | Theorem 6.12(1) | tz6.12-1 5507 tz6.12 5508 tz6.12c 5510 |
[TakeutiZaring] p.
27 | Theorem 6.12(2) | tz6.12-2 5471 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 5185 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 5186 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 5188 wfo 5180 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 5187 wf1 5179 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 5189 wf1o 5181 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 5577 eqfnfv2 5578 eqfnfv2f 5581 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 5550 |
[TakeutiZaring] p.
28 | Theorem 6.16(1) | fnex 5701 fnexALT 6073 |
[TakeutiZaring] p.
28 | Proposition 6.17 | resfunexg 5700 resfunexgALT 6070 |
[TakeutiZaring] p.
29 | Exercise 9 | funimaex 5267 funimaexg 5266 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 3977 |
[TakeutiZaring] p.
30 | Definition 6.21 | eliniseg 4968 iniseg 4970 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 4261 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-isom 5191 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 5772 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 5773 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 5778 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 5780 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 5788 |
[TakeutiZaring] p.
35 | Notation | wtr 4074 |
[TakeutiZaring] p.
35 | Theorem 7.2 | tz7.2 4326 |
[TakeutiZaring] p.
35 | Definition 7.1 | dftr3 4078 |
[TakeutiZaring] p.
36 | Proposition 7.4 | ordwe 4547 |
[TakeutiZaring] p.
36 | Proposition 7.6 | ordelord 4353 |
[TakeutiZaring] p.
37 | Proposition 7.9 | ordin 4357 |
[TakeutiZaring] p.
38 | Corollary 7.15 | ordsson 4463 |
[TakeutiZaring] p.
38 | Definition 7.11 | df-on 4340 |
[TakeutiZaring] p.
38 | Proposition 7.12 | ordon 4457 |
[TakeutiZaring] p.
38 | Proposition 7.13 | onprc 4523 |
[TakeutiZaring] p.
39 | Theorem 7.17 | tfi 4553 |
[TakeutiZaring] p.
40 | Exercise 7 | dftr2 4076 |
[TakeutiZaring] p.
40 | Exercise 11 | unon 4482 |
[TakeutiZaring] p.
40 | Proposition 7.19 | ssorduni 4458 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 3811 |
[TakeutiZaring] p.
41 | Definition 7.22 | df-suc 4343 |
[TakeutiZaring] p.
41 | Proposition 7.23 | sssucid 4387 sucidg 4388 |
[TakeutiZaring] p.
41 | Proposition 7.24 | suceloni 4472 |
[TakeutiZaring] p.
42 | Exercise 1 | df-ilim 4341 |
[TakeutiZaring] p.
42 | Exercise 8 | onsucssi 4477 ordelsuc 4476 |
[TakeutiZaring] p.
42 | Proposition 7.30(1) | peano1 4565 |
[TakeutiZaring] p.
42 | Proposition 7.30(2) | peano2 4566 |
[TakeutiZaring] p.
42 | Proposition 7.30(3) | peano3 4567 |
[TakeutiZaring] p.
43 | Axiom 7 | omex 4564 |
[TakeutiZaring] p.
43 | Theorem 7.32 | ordom 4578 |
[TakeutiZaring] p.
43 | Corollary 7.31 | find 4570 |
[TakeutiZaring] p.
43 | Proposition 7.30(4) | peano4 4568 |
[TakeutiZaring] p.
43 | Proposition 7.30(5) | peano5 4569 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 3832 |
[TakeutiZaring] p.
44 | Exercise 3 | trintssm 4090 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 3833 |
[TakeutiZaring] p.
44 | Exercise 6 | onintonm 4488 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 3819 |
[TakeutiZaring] p.
47 | Lemma 1 | tfrlem1 6267 |
[TakeutiZaring] p.
47 | Theorem 7.41(1) | tfri1 6324 tfri1d 6294 |
[TakeutiZaring] p.
47 | Theorem 7.41(2) | tfri2 6325 tfri2d 6295 |
[TakeutiZaring] p.
47 | Theorem 7.41(3) | tfri3 6326 |
[TakeutiZaring] p.
50 | Exercise 3 | smoiso 6261 |
[TakeutiZaring] p.
50 | Definition 7.46 | df-smo 6245 |
[TakeutiZaring] p.
56 | Definition 8.1 | oasuc 6423 |
[TakeutiZaring] p.
57 | Proposition 8.2 | oacl 6419 |
[TakeutiZaring] p.
57 | Proposition 8.3 | oa0 6416 |
[TakeutiZaring] p.
57 | Proposition 8.16 | omcl 6420 |
[TakeutiZaring] p.
58 | Proposition 8.4 | nnaord 6468 nnaordi 6467 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 3905 uniss2 3814 |
[TakeutiZaring] p.
59 | Proposition 8.7 | oawordriexmid 6429 |
[TakeutiZaring] p.
59 | Proposition 8.9 | nnacl 6439 |
[TakeutiZaring] p.
62 | Exercise 5 | oaword1 6430 |
[TakeutiZaring] p.
62 | Definition 8.15 | om0 6417 omsuc 6431 |
[TakeutiZaring] p.
63 | Proposition 8.17 | nnmcl 6440 |
[TakeutiZaring] p.
63 | Proposition 8.19 | nnmord 6476 nnmordi 6475 |
[TakeutiZaring] p.
67 | Definition 8.30 | oei0 6418 |
[TakeutiZaring] p.
85 | Proposition 10.6(3) | cardonle 7134 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 6752 |
[TakeutiZaring] p.
90 | Proposition 10.20 | nneneq 6814 |
[TakeutiZaring] p.
90 | Corollary 10.21(1) | php5 6815 |
[TakeutiZaring] p.
91 | Definition 10.29 | df-fin 6700 isfi 6718 |
[TakeutiZaring] p.
92 | Proposition 10.33(2) | xpdom2 6788 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 6607 |
[TakeutiZaring] p.
96 | Proposition 10.45 | mapxpen 6805 |
[Tarski] p. 67 | Axiom
B5 | ax-4 1497 |
[Tarski] p. 68 | Lemma
6 | equid 1688 |
[Tarski] p. 69 | Lemma
7 | equcomi 1691 |
[Tarski] p. 70 | Lemma
14 | spim 1725 spime 1728 spimeh 1726 spimh 1724 |
[Tarski] p. 70 | Lemma
16 | ax-11 1493 ax-11o 1810 ax11i 1701 |
[Tarski] p. 70 | Lemmas 16
and 17 | sb6 1873 |
[Tarski] p. 77 | Axiom B6
(p. 75) of system S2 | ax-17 1513 |
[Tarski] p. 77 | Axiom B8
(p. 75) of system S2 | ax-13 2137 ax-14 2138 |
[WhiteheadRussell] p.
96 | Axiom *1.3 | olc 701 |
[WhiteheadRussell] p.
96 | Axiom *1.4 | pm1.4 717 |
[WhiteheadRussell] p.
96 | Axiom *1.2 (Taut) | pm1.2 746 |
[WhiteheadRussell] p.
96 | Axiom *1.5 (Assoc) | pm1.5 755 |
[WhiteheadRussell] p.
97 | Axiom *1.6 (Sum) | orim2 779 |
[WhiteheadRussell] p.
100 | Theorem *2.01 | pm2.01 606 |
[WhiteheadRussell] p.
100 | Theorem *2.02 | ax-1 6 |
[WhiteheadRussell] p.
100 | Theorem *2.03 | con2 633 |
[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 827 |
[WhiteheadRussell] p.
101 | Theorem *2.06 | barbara 2111 syl 14 |
[WhiteheadRussell] p.
101 | Theorem *2.07 | pm2.07 727 |
[WhiteheadRussell] p.
101 | Theorem *2.08 | id 19 idALT 20 |
[WhiteheadRussell] p.
101 | Theorem *2.11 | exmiddc 826 |
[WhiteheadRussell] p.
101 | Theorem *2.12 | notnot 619 |
[WhiteheadRussell] p.
101 | Theorem *2.13 | pm2.13dc 875 |
[WhiteheadRussell] p.
102 | Theorem *2.14 | notnotrdc 833 |
[WhiteheadRussell] p.
102 | Theorem *2.15 | con1dc 846 |
[WhiteheadRussell] p.
103 | Theorem *2.16 | con3 632 |
[WhiteheadRussell] p.
103 | Theorem *2.17 | condc 843 |
[WhiteheadRussell] p.
103 | Theorem *2.18 | pm2.18dc 845 |
[WhiteheadRussell] p.
104 | Theorem *2.2 | orc 702 |
[WhiteheadRussell] p.
104 | Theorem *2.3 | pm2.3 765 |
[WhiteheadRussell] p.
104 | Theorem *2.21 | pm2.21 607 |
[WhiteheadRussell] p.
104 | Theorem *2.24 | pm2.24 611 |
[WhiteheadRussell] p.
104 | Theorem *2.25 | pm2.25dc 883 |
[WhiteheadRussell] p.
104 | Theorem *2.26 | pm2.26dc 897 |
[WhiteheadRussell] p.
104 | Theorem *2.27 | pm2.27 40 |
[WhiteheadRussell] p.
104 | Theorem *2.31 | pm2.31 758 |
[WhiteheadRussell] p.
105 | Theorem *2.32 | pm2.32 759 |
[WhiteheadRussell] p.
105 | Theorem *2.36 | pm2.36 794 |
[WhiteheadRussell] p.
105 | Theorem *2.37 | pm2.37 795 |
[WhiteheadRussell] p.
105 | Theorem *2.38 | pm2.38 793 |
[WhiteheadRussell] p.
105 | Definition *2.33 | df-3or 968 |
[WhiteheadRussell] p.
106 | Theorem *2.4 | pm2.4 768 |
[WhiteheadRussell] p.
106 | Theorem *2.41 | pm2.41 766 |
[WhiteheadRussell] p.
106 | Theorem *2.42 | pm2.42 767 |
[WhiteheadRussell] p.
106 | Theorem *2.43 | pm2.43 53 |
[WhiteheadRussell] p.
106 | Theorem *2.45 | pm2.45 728 |
[WhiteheadRussell] p.
106 | Theorem *2.46 | pm2.46 729 |
[WhiteheadRussell] p.
107 | Theorem *2.5 | pm2.5dc 857 pm2.5gdc 856 |
[WhiteheadRussell] p.
107 | Theorem *2.6 | pm2.6dc 852 |
[WhiteheadRussell] p.
107 | Theorem *2.47 | pm2.47 730 |
[WhiteheadRussell] p.
107 | Theorem *2.48 | pm2.48 731 |
[WhiteheadRussell] p.
107 | Theorem *2.49 | pm2.49 732 |
[WhiteheadRussell] p.
107 | Theorem *2.51 | pm2.51 645 |
[WhiteheadRussell] p.
107 | Theorem *2.52 | pm2.52 646 |
[WhiteheadRussell] p.
107 | Theorem *2.53 | pm2.53 712 |
[WhiteheadRussell] p.
107 | Theorem *2.54 | pm2.54dc 881 |
[WhiteheadRussell] p.
107 | Theorem *2.55 | orel1 715 |
[WhiteheadRussell] p.
107 | Theorem *2.56 | orel2 716 |
[WhiteheadRussell] p.
107 | Theorem *2.61 | pm2.61dc 855 |
[WhiteheadRussell] p.
107 | Theorem *2.62 | pm2.62 738 |
[WhiteheadRussell] p.
107 | Theorem *2.63 | pm2.63 790 |
[WhiteheadRussell] p.
107 | Theorem *2.64 | pm2.64 791 |
[WhiteheadRussell] p.
107 | Theorem *2.65 | pm2.65 649 |
[WhiteheadRussell] p.
107 | Theorem *2.67 | pm2.67-2 703 pm2.67 733 |
[WhiteheadRussell] p.
107 | Theorem *2.521 | pm2.521dc 859 pm2.521gdc 858 |
[WhiteheadRussell] p.
107 | Theorem *2.621 | pm2.621 737 |
[WhiteheadRussell] p.
108 | Theorem *2.8 | pm2.8 800 |
[WhiteheadRussell] p.
108 | Theorem *2.68 | pm2.68dc 884 |
[WhiteheadRussell] p.
108 | Theorem *2.69 | looinvdc 905 |
[WhiteheadRussell] p.
108 | Theorem *2.73 | pm2.73 796 |
[WhiteheadRussell] p.
108 | Theorem *2.74 | pm2.74 797 |
[WhiteheadRussell] p.
108 | Theorem *2.75 | pm2.75 799 |
[WhiteheadRussell] p.
108 | Theorem *2.76 | pm2.76 798 |
[WhiteheadRussell] p.
108 | Theorem *2.77 | ax-2 7 |
[WhiteheadRussell] p.
108 | Theorem *2.81 | pm2.81 801 |
[WhiteheadRussell] p.
108 | Theorem *2.82 | pm2.82 802 |
[WhiteheadRussell] p.
108 | Theorem *2.83 | pm2.83 77 |
[WhiteheadRussell] p.
108 | Theorem *2.85 | pm2.85dc 895 |
[WhiteheadRussell] p.
108 | Theorem *2.86 | pm2.86 100 |
[WhiteheadRussell] p.
111 | Theorem *3.1 | pm3.1 744 |
[WhiteheadRussell] p.
111 | Theorem *3.2 | pm3.2 138 |
[WhiteheadRussell] p.
111 | Theorem *3.11 | pm3.11dc 946 |
[WhiteheadRussell] p.
111 | Theorem *3.12 | pm3.12dc 947 |
[WhiteheadRussell] p.
111 | Theorem *3.13 | pm3.13dc 948 |
[WhiteheadRussell] p.
111 | Theorem *3.14 | pm3.14 743 |
[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 683 |
[WhiteheadRussell] p.
112 | Theorem *3.35 | pm3.35 345 |
[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 850 |
[WhiteheadRussell] p.
112 | Theorem *3.27 (Simp) | simpr 109 simprimdc 849 |
[WhiteheadRussell] p.
112 | Theorem *3.33 (Syll) | pm3.33 343 |
[WhiteheadRussell] p.
112 | Theorem *3.34 (Syll) | pm3.34 344 |
[WhiteheadRussell] p.
112 | Theorem *3.37 (Transp) | pm3.37 679 |
[WhiteheadRussell] p.
113 | Fact) | pm3.45 587 |
[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 745 pm3.44 705 |
[WhiteheadRussell] p.
113 | Theorem *3.47 | anim12 342 |
[WhiteheadRussell] p.
113 | Theorem *3.43 (Comp) | pm3.43 592 |
[WhiteheadRussell] p.
114 | Theorem *3.48 | pm3.48 775 |
[WhiteheadRussell] p.
116 | Theorem *4.1 | con34bdc 861 |
[WhiteheadRussell] p.
117 | Theorem *4.2 | biid 170 |
[WhiteheadRussell] p.
117 | Theorem *4.13 | notnotbdc 862 |
[WhiteheadRussell] p.
117 | Theorem *4.14 | pm4.14dc 880 |
[WhiteheadRussell] p.
117 | Theorem *4.15 | pm4.15 684 |
[WhiteheadRussell] p.
117 | Theorem *4.21 | bicom 139 |
[WhiteheadRussell] p.
117 | Theorem *4.22 | biantr 941 bitr 464 |
[WhiteheadRussell] p.
117 | Theorem *4.24 | pm4.24 393 |
[WhiteheadRussell] p.
117 | Theorem *4.25 | oridm 747 pm4.25 748 |
[WhiteheadRussell] p.
118 | Theorem *4.3 | ancom 264 |
[WhiteheadRussell] p.
118 | Theorem *4.4 | andi 808 |
[WhiteheadRussell] p.
118 | Theorem *4.31 | orcom 718 |
[WhiteheadRussell] p.
118 | Theorem *4.32 | anass 399 |
[WhiteheadRussell] p.
118 | Theorem *4.33 | orass 757 |
[WhiteheadRussell] p.
118 | Theorem *4.36 | anbi1 462 |
[WhiteheadRussell] p.
118 | Theorem *4.37 | orbi1 782 |
[WhiteheadRussell] p.
118 | Theorem *4.38 | pm4.38 595 |
[WhiteheadRussell] p.
118 | Theorem *4.39 | pm4.39 812 |
[WhiteheadRussell] p.
118 | Definition *4.34 | df-3an 969 |
[WhiteheadRussell] p.
119 | Theorem *4.41 | ordi 806 |
[WhiteheadRussell] p.
119 | Theorem *4.42 | pm4.42r 960 |
[WhiteheadRussell] p.
119 | Theorem *4.43 | pm4.43 938 |
[WhiteheadRussell] p.
119 | Theorem *4.44 | pm4.44 769 |
[WhiteheadRussell] p.
119 | Theorem *4.45 | orabs 804 pm4.45 774 pm4.45im 332 |
[WhiteheadRussell] p.
119 | Theorem *10.22 | 19.26 1468 |
[WhiteheadRussell] p.
120 | Theorem *4.5 | anordc 945 |
[WhiteheadRussell] p.
120 | Theorem *4.6 | imordc 887 imorr 711 |
[WhiteheadRussell] p.
120 | Theorem *4.7 | anclb 317 |
[WhiteheadRussell] p.
120 | Theorem *4.51 | ianordc 889 |
[WhiteheadRussell] p.
120 | Theorem *4.52 | pm4.52im 740 |
[WhiteheadRussell] p.
120 | Theorem *4.53 | pm4.53r 741 |
[WhiteheadRussell] p.
120 | Theorem *4.54 | pm4.54dc 892 |
[WhiteheadRussell] p.
120 | Theorem *4.55 | pm4.55dc 927 |
[WhiteheadRussell] p.
120 | Theorem *4.56 | ioran 742 pm4.56 770 |
[WhiteheadRussell] p.
120 | Theorem *4.57 | orandc 928 oranim 771 |
[WhiteheadRussell] p.
120 | Theorem *4.61 | annimim 676 |
[WhiteheadRussell] p.
120 | Theorem *4.62 | pm4.62dc 888 |
[WhiteheadRussell] p.
120 | Theorem *4.63 | pm4.63dc 876 |
[WhiteheadRussell] p.
120 | Theorem *4.64 | pm4.64dc 890 |
[WhiteheadRussell] p.
120 | Theorem *4.65 | pm4.65r 677 |
[WhiteheadRussell] p.
120 | Theorem *4.66 | pm4.66dc 891 |
[WhiteheadRussell] p.
120 | Theorem *4.67 | pm4.67dc 877 |
[WhiteheadRussell] p.
120 | Theorem *4.71 | pm4.71 387 pm4.71d 391 pm4.71i 389 pm4.71r 388 pm4.71rd 392 pm4.71ri 390 |
[WhiteheadRussell] p.
121 | Theorem *4.72 | pm4.72 817 |
[WhiteheadRussell] p.
121 | Theorem *4.73 | iba 298 |
[WhiteheadRussell] p.
121 | Theorem *4.74 | biorf 734 |
[WhiteheadRussell] p.
121 | Theorem *4.76 | jcab 593 pm4.76 594 |
[WhiteheadRussell] p.
121 | Theorem *4.77 | jaob 700 pm4.77 789 |
[WhiteheadRussell] p.
121 | Theorem *4.78 | pm4.78i 772 |
[WhiteheadRussell] p.
121 | Theorem *4.79 | pm4.79dc 893 |
[WhiteheadRussell] p.
122 | Theorem *4.8 | pm4.8 697 |
[WhiteheadRussell] p.
122 | Theorem *4.81 | pm4.81dc 898 |
[WhiteheadRussell] p.
122 | Theorem *4.82 | pm4.82 939 |
[WhiteheadRussell] p.
122 | Theorem *4.83 | pm4.83dc 940 |
[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 547 |
[WhiteheadRussell] p.
123 | Theorem *5.1 | pm5.1 591 |
[WhiteheadRussell] p.
123 | Theorem *5.11 | pm5.11dc 899 |
[WhiteheadRussell] p.
123 | Theorem *5.12 | pm5.12dc 900 |
[WhiteheadRussell] p.
123 | Theorem *5.13 | pm5.13dc 902 |
[WhiteheadRussell] p.
123 | Theorem *5.14 | pm5.14dc 901 |
[WhiteheadRussell] p.
124 | Theorem *5.15 | pm5.15dc 1378 |
[WhiteheadRussell] p.
124 | Theorem *5.16 | pm5.16 818 |
[WhiteheadRussell] p.
124 | Theorem *5.17 | pm5.17dc 894 |
[WhiteheadRussell] p.
124 | Theorem *5.18 | nbbndc 1383 pm5.18dc 873 |
[WhiteheadRussell] p.
124 | Theorem *5.19 | pm5.19 696 |
[WhiteheadRussell] p.
124 | Theorem *5.21 | pm5.21 685 |
[WhiteheadRussell] p.
124 | Theorem *5.22 | xordc 1381 |
[WhiteheadRussell] p.
124 | Theorem *5.23 | dfbi3dc 1386 |
[WhiteheadRussell] p.
124 | Theorem *5.24 | pm5.24dc 1387 |
[WhiteheadRussell] p.
124 | Theorem *5.25 | dfor2dc 885 |
[WhiteheadRussell] p.
125 | Theorem *5.3 | pm5.3 467 |
[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 916 pm5.6r 917 |
[WhiteheadRussell] p.
125 | Theorem *5.7 | pm5.7dc 943 |
[WhiteheadRussell] p.
125 | Theorem *5.31 | pm5.31 346 |
[WhiteheadRussell] p.
125 | Theorem *5.32 | pm5.32 449 |
[WhiteheadRussell] p.
125 | Theorem *5.33 | pm5.33 599 |
[WhiteheadRussell] p.
125 | Theorem *5.35 | pm5.35 907 |
[WhiteheadRussell] p.
125 | Theorem *5.36 | pm5.36 600 |
[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 915 |
[WhiteheadRussell] p.
125 | Theorem *5.53 | pm5.53 792 |
[WhiteheadRussell] p.
125 | Theorem *5.54 | pm5.54dc 908 |
[WhiteheadRussell] p.
125 | Theorem *5.55 | pm5.55dc 903 |
[WhiteheadRussell] p.
125 | Theorem *5.61 | pm5.61 784 |
[WhiteheadRussell] p.
125 | Theorem *5.62 | pm5.62dc 934 |
[WhiteheadRussell] p.
125 | Theorem *5.63 | pm5.63dc 935 |
[WhiteheadRussell] p.
125 | Theorem *5.71 | pm5.71dc 950 |
[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 951 |
[WhiteheadRussell] p.
150 | Theorem *10.3 | alsyl 1622 |
[WhiteheadRussell] p.
160 | Theorem *11.21 | alrot3 1472 |
[WhiteheadRussell] p.
163 | Theorem *11.42 | 19.40-2 1619 |
[WhiteheadRussell] p.
164 | Theorem *11.53 | pm11.53 1882 |
[WhiteheadRussell] p.
175 | Definition *14.02 | df-eu 2016 |
[WhiteheadRussell] p.
178 | Theorem *13.18 | pm13.18 2415 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 2416 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 2859 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 3002 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 5165 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 5166 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2092 eupickbi 2095 |
[WhiteheadRussell] p.
235 | Definition *30.01 | df-fv 5190 |
[WhiteheadRussell] p.
360 | Theorem *54.43 | pm54.43 7137 |