Metamath Proof Explorer - Bibliographic Cross-Reference

Bibliographic Cross-Reference

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Metamath Proof Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular set theory book, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books.

Bibliographic Cross-Reference for the Metamath Proof Explorer

Bibliographic Reference	Description	Metamath Proof Explorer Page(s)
[Apostol] p. 18	Theorem I.1	addcan 4120  addcant 4122
[Apostol] p. 18	Theorem I.2	negeu 4124
[Apostol] p. 18	Theorem I.3	subneg 4148  subnegt 4149
[Apostol] p. 18	Theorem I.4	negneg 4154  negnegt 4157
[Apostol] p. 18	Theorem I.5	subdi 4182  subdir 4183  subdit 4184
[Apostol] p. 18	Theorem I.6	mulzer1 4185  mulzer1t 4188  mulzer2 4186  mulzer2t 4189
[Apostol] p. 18	Theorem I.7	mulcan 4207  mulcant 4208  mulcant2 4209
[Apostol] p. 18	Theorem I.8	receu 4215
[Apostol] p. 18	Theorem I.9	divrec 4236  divrect 4238  divrecz 4237
[Apostol] p. 18	Theorem I.10	recrec 4253  recrect 4260
[Apostol] p. 18	Theorem I.11	mul0or 4210  mul0ort 4212
[Apostol] p. 18	Theorem I.12	mul2neg 4192  mul2negt 4199  mulneg1 4190  mulneg1t 4196
[Apostol] p. 18	Theorem I.13	divadddiv 4268  divadddivt 4264
[Apostol] p. 18	Theorem I.14	divmuldiv 4266  divmuldivt 4263
[Apostol] p. 18	Theorem I.15	divdivdiv 4269  divdivdivt 4265
[Apostol] p. 20	Theorem I.17	lttr 4307
[Apostol] p. 20	Theorem I.18	ltadd1 4313
[Apostol] p. 20	Theorem I.19	ltmul1 4394  ltmul1i 4393  ltmul2 4395  ltmullem 4337
[Apostol] p. 20	Theorem I.20	ltsqt 4376  sqgt0 4343
[Apostol] p. 20	Theorem I.21	lt01 4377
[Apostol] p. 20	Theorem I.23	lt0neg1t 4370  ltneg 4330  ltnegt 4366
[Apostol] p. 20	Theorem I.25	lt2add 4321  lt2addt 4361
[Apostol] p. 21	Exercise 4	recgt0 4386  recgt0i 4385  recgt0t 4401
[Apostol] p. 22	Definition of integers	df-z 4564
[Apostol] p. 22	Definition of positive integers	df-n 4423
[Apostol] p. 22	Definition of rational numbers	df-q 4628
[Apostol] p. 24	Theorem I.26	supeu 2158  supeui 2163
[Apostol] p. 26	Theorem I.28	nnunb 4520
[Apostol] p. 26	Theorem I.29	arch 4521
[Apostol] p. 28	Exercise 2	btwnz 4613
[Apostol] p. 28	Exercise 3	nnreclt 4522
[Apostol] p. 28	Exercise 4	rebtwnz 4620
[Apostol] p. 28	Exercise 5	zbtwnre 4619
[Apostol] p. 28	Exercise 6	qbtwnre 4650
[Apostol] p. 28	Exercise 10(a)	zneo 4601
[Apostol] p. 29	Theorem I.35	sqrth 4757
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nn 4424
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwo 4607  nnwoOLD 4608
[Apostol] p. 361	Remark	crmult 4530
[Apostol] p. 363	Remark	absgt0 4842
[Apostol] p. 363	Example	abssub 4845
[BellMachover] p. 97	Definition 10.1	df-eu 1009
[BellMachover] p. 460	Notation	df-mo 1010
[BellMachover] p. 460	Definition	mo3 1027
[BellMachover] p. 461	Axiom Ext	ax-ext 1074
[BellMachover] p. 462	Theorem 1.1	bm1.1 1088
[BellMachover] p. 463	Axiom Rep	zfrep3 1476
[BellMachover] p. 463	Scheme Sep	zfaus 1480
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 1481
[BellMachover] p. 466	Axiom Pow	ax-pow 1077
[BellMachover] p. 466	Axiom Union	ax-un 1076
[BellMachover] p. 468	Definition	df-ord 2202
[BellMachover] p. 469	Theorem 2.2(i)	ordeirr 2217
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 2223
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 2219
[BellMachover] p. 471	Definition of N	df-om 2373
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 2274
[BellMachover] p. 471	Definition of Lim	df-lim 2204
[BellMachover] p. 472	Axiom Inf	ax-inf 1079
[BellMachover] p. 473	Theorem 2.8	limom 2387
[BellMachover] p. 477	Equation 3.1	df-r1 3487
[BellMachover] p. 478	Definition	rankval2 3514
[BellMachover] p. 478	Theorem 3.3(i)	r1ord3 3501
[BellMachover] p. 480	Axiom Reg	zfreg2 3448
[BellMachover] p. 488	Axiom AC	ac5 3573  aceq4 3557  ax-ac 1080
[BeltramettiCassinelli] p. 107	Remark 10.3.5	atom1d 5750
[Beran] p. 3	Definition of join	dfchj3 5326  sshjval3t 5327
[Beran] p. 39	Theorem 2.3(i)	cmcm2 5502  cmcm2i 5507
[Beran] p. 40	Theorem 2.3(iii)	cmle 5511
[Beran] p. 45	Theorem 3.4	cmcmlem 5500
[Beran] p. 95	Definition	df-sh 5114  sh 5116
[Beran] p. 95	Lemma 3.1(S5)	his5 5050
[Beran] p. 95	Lemma 3.1(S6)	his6 5057
[Beran] p. 95	Lemma 3.1(S7)	his7 5051
[Beran] p. 95	Postulate (S1)	ax-his1 5045
[Beran] p. 95	Postulate (S2)	ax-his2 5046
[Beran] p. 95	Postulate (S3)	ax-his3 5047
[Beran] p. 95	Postulate (S4)	ax-his4 5048  axhis42 5049
[Beran] p. 96	Definition of norm	df-hnorm 5074  normvalt 5075
[Beran] p. 96	Definition for Cauchy sequence	hcauchy 5103
[Beran] p. 96	Definition of Cauchy sequence	df-cauchy 5102
[Beran] p. 96	Definition of complete subspace	chsscm 5147
[Beran] p. 96	Definition of converge	df-hlim 5107  hlim 5108
[Beran] p. 97	Theorem 3.3(i)	norm-i 5083  norm-it 5080
[Beran] p. 97	Theorem 3.3(ii)	norm-ii 5086  normlem0 5062  normlem1 5063  normlem2 5064  normlem3 5065  normlem4 5066  normlem5 5067  normlem6 5068  normlem7 5069  normlem7t 5072
[Beran] p. 97	Theorem 3.3(iii)	norm-iii 5087  norm-iiit 5088
[Beran] p. 98	Remark 3.4	bcs 5101
[Beran] p. 98	Remark 3.4(B)	normlem8 5071  normlem9 5070  normpar 5099
[Beran] p. 98	Remark 3.4(C)	normpyct 5093  normpyth 5090  normpytht 5092
[Beran] p. 100	Lemma 3.6	normpar2 5100  projlem1 5193  projlem10 5202  projlem11 5203  projlem12 5204  projlem13 5205  projlem14 5206  projlem15 5207  projlem16 5208  projlem17 5209  projlem17 5209  projlem2 5194  projlem21 5213  projlem22 5214  projlem3 5195  projlem5 5197  projlem8 5200  projlem8 5200  projlem9 5201
[Beran] p. 101	Lemma 3.6	norm3adif 5095  norm3adift 5098  norm3dif 5094  projlem 5224  projlem18 5210  projlem19 5211  projlem20 5212  projlem23 5215  projlem24 5216  projlem25 5217  projlem26 5218  projlem27 5219  projlem28 5220  projlem29 5221  projlem30 5222  projlem31 5223  projlem4 5196  projlem6 5198  projlem7 5199
[Beran] p. 102	Theorem 3.7(i)	chocuni 5179  pjpjth 5263  pjpjtht 5262  pjth 5239  pjthlem1 5225  pjthlem10 5234  pjthlem11 5235  pjthlem12 5236  pjthlem13 5237  pjthlem14 5238  pjthlem2 5226  pjthlem3 5227  pjthlem4 5228  pjthlem5 5229  pjthlem6 5230  pjthlem7 5231  pjthlem8 5232  pjthlem9 5233  pjtht 5240
[Beran] p. 102	Theorem 3.7(ii)	ococ 5252  ococt 5253
[Beran] p. 106	Theorem 3.11(viii)	pjadj2co 5656  pjadjco 5631
[Beran] p. 107	Definition	closedsub 5128  df-ch 5127
[Beran] p. 107	Remark 3.12	choclt 5191  chsscm 5147  occl 5188  occllem1 5180  occllem2 5181  occllem3 5182  occllem4 5183  occllem5 5184  occllem6 5185  occllem7 5186  occllem8 5187  occlt 5189  ocsh 5164  shocclt 5190  shocsh 5165
[Beran] p. 107	Remark 3.12(B)	ococint 5298
[Beran] p. 107	Remark 3.12(C)	ch2 5149  chcmh 5148
[Beran] p. 108	Theorem 3.13	chintclt 5297
[Beran] p. 109	Property (i)	pjadj 5564  pjadjt 5576
[Beran] p. 109	Property (ii)	pjidm 5563  pjidmco 5642
[Beran] p. 111	Remark	pjch0t 5562  pjch1t 5560
[Beran] p. 111	Definition	df-hosum 5485  df-pjdif 5486
[Beran] p. 111	Lemma 4.4(i)	pjot 5561
[Beran] p. 111	Lemma 4.4(ii)	pjch 5269  pjcht 5582
[Beran] p. 111	Lemma 4.4(iii)	pjoc2 5273  pjoc2t 5274
[Beran] p. 112	Theorem 4.5(i)->(ii)	pjss2 5571
[Beran] p. 112	Theorem 4.5(i)->(iv)	pjssm 5572  pjssmt 5635
[Beran] p. 112	Theorem 4.5(i)<->(ii)	pjss2co 5634
[Beran] p. 112	Theorem 4.5(i)<->(iii)	pjss1co 5633
[Beran] p. 112	Theorem 4.5(i)<->(vi)	pjnormss 5638
[Beran] p. 112	Theorem 4.5(iv)->(v)	pjssge0 5573  pjssge0t 5636
[Beran] p. 112	Theorem 4.5(v)<->(vi)	pjdifnorm 5574  pjdifnormt 5637
[Eisenberg] p. 67	Definition 5.3	df-dif 1489
[Eisenberg] p. 82	Definition 6.3	dfom3 3477
[Eisenberg] p. 125	Definition 8.21	df-map 3259
[Eisenberg] p. 216	Example 13.2(4)	omenps 3482
[Eisenberg] p. 310	Theorem 19.8	cardprc 3667
[Eisenberg] p. 310	Corollary 19.7(2)	cardsdom 3643
[Enderton] p. 18	Axiom of Empty Set	zfnul 1746
[Enderton] p. 19	Definition	df-tp 1814
[Enderton] p. 26	Exercise 5	unissb 1941
[Enderton] p. 28	Exercise 7(b)	pwun 1918
[Enderton] p. 30	Theorem "Distributive laws"	iinun2 2031  iunin2 2030
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 2033  iundif2 2032
[Enderton] p. 32	Exercise 20	unineq 1680
[Enderton] p. 33	Exercise 23	iinuni 2036
[Enderton] p. 33	Exercise 25	iununi 2037
[Enderton] p. 33	Exercise 24(a)	iinpw 2038
[Enderton] p. 33	Exercise 24(b)	iunpw 2040  iunpwss 2039
[Enderton] p. 36	Definition	opthwiener 1914
[Enderton] p. 38	Exercise 6(a)	unipw 1960
[Enderton] p. 38	Exercise 6(b)	pwuni 1961
[Enderton] p. 41	Lemma 3D	opeluu 1953  rnexg 2569
[Enderton] p. 41	Exercise 8	dmuni 2538  rnuni 2646
[Enderton] p. 42	Definition of a function	dffun6 2687  dffun7 2688
[Enderton] p. 43	Definition of function value	funfv2 2863
[Enderton] p. 43	Definition of single-rooted	funcnv 2703
[Enderton] p. 44	Definition (d)	dfima2 2604  dfima3 2605
[Enderton] p. 47	Theorem 3H	fvco2 2866
[Enderton] p. 49	Axiom of Choice (first form)	ac7 3569  ac7g 3570  aceq3 3556  aceq4 3557  aceq5 3563  aceq6a 3564  aceq6b 3565  aceq7 3566  aceqkm 3596
[Enderton] p. 50	Theorem 3K(a)	imaiun 2650
[Enderton] p. 52	Definition	df-map 3259
[Enderton] p. 53	Exercise 21	coass 2667
[Enderton] p. 53	Exercise 27	dmco2 2673
[Enderton] p. 53	Exercise 14(a)	funin 2708
[Enderton] p. 53	Exercise 22(a)	imass2 2622
[Enderton] p. 56	Theorem 3M	erref 3212
[Enderton] p. 57	Lemma 3N	erthi 3218
[Enderton] p. 57	Definition	df-ec 3202
[Enderton] p. 58	Definition	df-qs 3205
[Enderton] p. 60	Theorem 3Q	th3q 3253  th3qcor 3252  th3qlem1 3250  th3qlem2 3251
[Enderton] p. 61	Exercise 35	df-ec 3202
[Enderton] p. 65	Exercise 56(a)	dmun 2536
[Enderton] p. 68	Definition of successor	df-suc 2205
[Enderton] p. 71	Definition	df-tr 2042  dftr4 2046
[Enderton] p. 72	Theorem 4E	unisuc 2299
[Enderton] p. 73	Exercise 6	unisuc 2299
[Enderton] p. 79	Definition	df-opr 3003
[Enderton] p. 79	Theorem 4I(A1)	nna0 3166
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 3168
[Enderton] p. 80	Theorem 4J(A1)	nnm0 3167
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 3169
[Enderton] p. 81	Theorem 4K(1)	nnaass 3179
[Enderton] p. 81	Theorem 4K(2)	nna0r 3170  nnacom 3175
[Enderton] p. 81	Theorem 4K(3)	nndi 3180
[Enderton] p. 81	Theorem 4K(4)	nnmass 3181
[Enderton] p. 81	Theorem 4K(5)	nnmcom 3183
[Enderton] p. 82	Exercise 16	nnm0r 3171  nnmsucr 3182
[Enderton] p. 88	Exercise 23	nnaordex 3191
[Enderton] p. 129	Definition	bren 3282  df-en 3274
[Enderton] p. 132	Theorem 6B(b)	canth 2945
[Enderton] p. 133	Exercise 1	xpomen 4928
[Enderton] p. 133	Exercise 2	qnnen 4931
[Enderton] p. 134	Theorem (Pigeonhole Principle)	php 3409
[Enderton] p. 135	Corollary 6C	php3 3411
[Enderton] p. 136	Corollary 6E	nneneq 3408
[Enderton] p. 136	Corollary 6D(a)	pssinf 3422
[Enderton] p. 136	Corollary 6D(b)	ominf 3423
[Enderton] p. 137	Lemma 6F	pssnn 3428
[Enderton] p. 138	Corollary 6G	ssfi 3430
[Enderton] p. 139	Theorem 6H(c)	mapen 3386
[Enderton] p. 142	Theorem 6I(3)	xpcdaen 3726
[Enderton] p. 143	Theorem 6J	cda0en 3720  cda1en 3721
[Enderton] p. 144	Corollary 6K	undif2 1762  unfi 3441  unfi2 3442
[Enderton] p. 145	Figure 38	ffoss 2820
[Enderton] p. 145	Definition	df-dom 3275
[Enderton] p. 146	Example 1	domen 3284  domeng 3285
[Enderton] p. 146	Example 3	nndomo 3416  omsdomnn 3424
[Enderton] p. 149	Theorem 6L(a)	cdadom2 3728
[Enderton] p. 149	Theorem 6L(c)	mapdom1 3387  xpdom1 3346
[Enderton] p. 149	Theorem 6L(d)	mapdom2 3389
[Enderton] p. 151	Theorem 6M	zorn2 3612
[Enderton] p. 151	Theorem 6M(4)	ac8 3579  aceq5 3563
[Enderton] p. 162	Lemma 6R	infxpidm 4945
[Enderton] p. 164	Example	infdif 4948
[Enderton] p. 165	Exercise 34	infmap1 4950
[Enderton] p. 168	Definition	df-po 2128
[Enderton] p. 192	Theorem 7M(a)	onel 2346
[Enderton] p. 192	Theorem 7M(b)	ontr1 2258
[Enderton] p. 192	Theorem 7M(c)	oneirr 2345
[Enderton] p. 193	Corollary 7N(b)	0elon 2277
[Enderton] p. 193	Corollary 7N(c)	onsuc 2353
[Enderton] p. 193	Corollary 7N(d)	onuni 2251
[Enderton] p. 194	Remark	onprc 2240
[Enderton] p. 194	Exercise 16	suc11 2341
[Enderton] p. 197	Definition	df-card 3623
[Enderton] p. 197	Theorem 7P	carden 3638
[Enderton] p. 200	Exercise 25	tfis 2245
[Enderton] p. 202	Lemma 7T	r1tr 3498
[Enderton] p. 202	Definition	df-r1 3487
[Enderton] p. 202	Theorem 7Q	r1val1 3502
[Enderton] p. 204	Theorem 7V(b)	ranklon 3540
[Enderton] p. 206	Theorem 7X(b)	en2lp 3453
[Enderton] p. 207	Exercise 30	rankpr 3536  rankpw 3528  rankuniss 3534
[Enderton] p. 207	Exercise 34	opthreg 3455
[Enderton] p. 208	Exercise 35	suc11reg 3456
[Enderton] p. 213	Theorem 8A(a)	alephord2 3681
[Enderton] p. 213	Theorem 8A(b)	cardalephex 3691
[Enderton] p. 222	Definition of kard	karden 3551  kardex 3550
[Enderton] p. 257	Definition of cofinality	cflim 3704
[FreydScedrov] p. 283	Axiom of Infinity	ax-inf 1079  inf1 3458
[Gleason] p. 117	Proposition 9-2.1	df-enq 3831  enqer 3840
[Gleason] p. 117	Proposition 9-2.2	df-1q 3837  df-nq 3832
[Gleason] p. 117	Proposition 9-2.3	df-plpq 3829  df-plq 3833
[Gleason] p. 119	Proposition 9-2.4	caoprmo 3084  df-mpq 3830  df-mq 3834
[Gleason] p. 119	Proposition 9-2.5	df-rq 3835
[Gleason] p. 119	Proposition 9-2.6	ltexpq 3874  ltexpq2 3875
[Gleason] p. 120	Proposition 9-2.6(i)	halfpq 3876  ltbtwnpq 3878
[Gleason] p. 120	Proposition 9-2.6(ii)	ltapq 3870
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmpq 3871
[Gleason] p. 120	Proposition 9-2.6(iv)	ltrpq 3879
[Gleason] p. 121	Definition 9-3.1	df-np 3880
[Gleason] p. 121	Definition 9-3.1 (ii)	prcdpq 3891
[Gleason] p. 121	Definition 9-3.1(iii)	prnmax 3893
[Gleason] p. 122	Definition	df-1p 3881
[Gleason] p. 122	Remark (1)	prub 3892
[Gleason] p. 122	Lemma 9-3.4	prlem934 3933  prlem934a 3931  prlem934b 3932
[Gleason] p. 122	Proposition 9-3.2	df-ltp 3884
[Gleason] p. 122	Proposition 9-3.3	ltsopr 3930  psslinpr 3929  suplem1pr 3955  suplem2pr 3956  suppr 3957
[Gleason] p. 123	Proposition 9-3.5	addclpr 3914  addclprlem1 3912  addclprlem2 3913  df-plp 3882
[Gleason] p. 123	Proposition 9-3.5(i)	addasspr 3918
[Gleason] p. 123	Proposition 9-3.5(ii)	addcompr 3917
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 3934
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 3943  ltexprlem1 3936  ltexprlem2 3937  ltexprlem3 3938  ltexprlem4 3939  ltexprlem5 3940  ltexprlem6 3941  ltexprlem7 3942
[Gleason] p. 123	Proposition 9-3.5(v)	ltapr 3945  ltaprlem 3944
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanpr 3946
[Gleason] p. 124	Lemma 9-3.6	prlem936 3949  prlem936a 3947  prlem936b 3948
[Gleason] p. 124	Proposition 9-3.7	df-mp 3883  mulclpr 3916  mulclprlem 3915  reclem1pr 3950  reclem2pr 3951
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 3927
[Gleason] p. 124	Proposition 9-3.7(i)	mulasspr 3920
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcompr 3919
[Gleason] p. 124	Proposition 9-3.7(iii)	distrpr 3926
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 3954  reclem3pr 3952  reclem4pr 3953
[Gleason] p. 126	Proposition 9-4.1	df-enr 3960  df-mpr 3959  df-plpr 3958  enrer 3970
[Gleason] p. 126	Proposition 9-4.2	df-0r 3965  df-1r 3966  df-nr 3961
[Gleason] p. 126	Proposition 9-4.3	df-mr 3963  df-plr 3962  negexsr 4005  recexsr 4010  recexsrlem 4006
[Gleason] p. 127	Proposition 9-4.4	df-ltr 3964
[Gleason] p. 130	Proposition 10-1.3	creui 4533  creur 4532  cru 4529  crulem 4528  crut 4531
[Gleason] p. 130	Definition 10-1.1(v)	axcnre 4087
[Gleason] p. 132	Definition 10-3.1	crim 4807  crre 4806
[Gleason] p. 132	Definition 10-3.2	cjvalt 4799
[Gleason] p. 133	Definition 10.36	absval2 4836
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 4818  cjaddt 4831
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 4819  cjmult 4832
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 4808  cjcjt 4830
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 4811  cjret 4829  rere 4810
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 4828
[Gleason] p. 133	Proposition 10-3.7(a)	absvalt 4801
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 4844
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 4839
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 4858
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 4846  absmult 4849
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 4847
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 4859
[Godowski] p. 730	Equation (SF)	goeq 5706
[GodowskiGreechie] p. 249	Equation (IV)	3oa 5558
[Hamilton] p. 28	Definition 2.1	ax-1 3
[Hamilton] p. 31	Example 2.7(a)	id1 10
[Hamilton] p. 73	Rule 1	ax-mp 6
[Hamilton] p. 74	Rule 2	ax-gen 677
[Holland] p. 1519	Theorem 2	sumdmd 5787
[Jech] p. 42	Lemma 6.1	alephexp1 4954
[Jech] p. 43	Lemma 6.2	infmap2 4953
[Jech] p. 71	Lemma 9.3	jech9.3 3510
[Jech] p. 72	Equation 9.3	scott0 3542  scottex 3541
[Jech] p. 72	Exercise 9.1	ranklon 3540
[Jech] p. 72	Scheme "Collection Principle"	cp 3547
[Jech] p. 78	Definition implied by the footnote	opthprc 2457
[JustWeese] p. 174	Exercise 5(G)	df-cardn 3712
[KalishMontague] p. 81	Axiom B7' in footnote 1	ax-9 799
[Kalmbach] p. 14	Definition of lattice	chabs1 5434  chabs1t 5432  chabs2 5435  chabs2t 5433  chjass 5407  chjasst 5446
[Kalmbach] p. 15	Definition of atom	df-at 5737  elat 5738
[Kalmbach] p. 15	Definition of covers	cvbr2t 5715
[Kalmbach] p. 20	Definition of commutes	cmbr 5499  cmbrt 5494  df-cm 5493
[Kalmbach] p. 22	Definition	pjoml2 5495
[Kalmbach] p. 22	Theorem 2(v)	cmcm 5501  cmcmi 5506
[Kalmbach] p. 22	Theorem 2(ii)	omls 5251  pjoml 5271
[Kalmbach] p. 23	Remark	cmbr2 5505  cmcm3 5503  cmcm3i 5508  cmcm4 5504
[Kalmbach] p. 23	Lemma 3	cmbr3 5509
[Kalmbach] p. 25	Theorem 5	fh1 5518  fh2 5519
[Kalmbach] p. 65	Remark	chslej 5380  chslejt 5415  shslej 5339  shslejt 5351
[Kalmbach] p. 65	Proposition 1	chocin 5376  chsupclt 5309  chsupval2t 5303  dfchsup2 5299  h0elch 5159  helch 5151  hsupval2t 5301  ocin 5177  ococss 5174  shococss 5175
[Kalmbach] p. 65	Definition of subspace sum	shsumvalt 5279
[Kalmbach] p. 66	Remark	df-pj 5244  pjssm 5572  pjssmt 5635
[Kalmbach] p. 67	Lemma 3	osum 5538
[Kalmbach] p. 67	Lemma 4	pjc 5654
[Kalmbach] p. 140	Remark	hatomic 5754  hatomistic 5755
[Kalmbach] p. 140	Proposition 1(i)	atexch 5769
[Kalmbach] p. 140	Proposition 1(ii)	chcv1t 5751
[Kalmbach] p. 140	Proposition 1(iii)	cvexch 5760  cvexcht 5763
[Kalmbach] p. 149	Remark 2	chrelat 5757
[Kalmbach] p. 153	Exercise 5	spansncv 5542  spansncvt 5543
[Kalmbach] p. 153	Proposition 1(ii)	spansncv2t 5725
[Kalmbach] p. 266	Definition	df-st 5670
[Kunen] p. 12	Axiom 6	zfrep6 2744
[Kunen] p. 24	Definition 10.24	mapval 3264  mapvalg 3263
[Kunen] p. 30	Lemma 10.20	fodom 3613
[Kunen] p. 31	Definition 10.24	mapex 3261
[Maeda] p. 167	Theorem 1(d) to (e)	mdsymlem6 5781
[Maeda] p. 168	Lemma 5	mdsym 5784
[Maeda] p. 168	Lemma 4(i)	mdsymlem4 5779  mdsymlem6 5781  mdsymlem7 5782
[Maeda] p. 168	Lemma 4(ii)	mdsymlem8 5783
[MaedaMaeda] p. 1	Remark	ssdmd1 5736  ssmd1 5734  ssmd2 5735
[MaedaMaeda] p. 1	Definition 1.1	df-md 5713  mdbr 5726
[MaedaMaeda] p. 31	Lemma 7.5.1	cvnbtwn4t 5721
[MaedaMaeda] p. 31	Definition 7.4	cvp 5764
[MaedaMaeda] p. 70	Theorem 16.9	shatomic 5753  shmod 5364  shmods 5363
[MaedaMaeda] p. 130	Remark 29.6	dmdbr 5731
[MaedaMaeda] p. 132	Theorem 29.13(e)	pjoml5 5498
[MaedaMaeda] p. 136	Lemma 31.1.5	shjshsel 5413
[MaedaMaeda] p. 139	Remark	sumdmdi 5785
[Margaris] p. 49	Axiom A1	ax-1 3
[Margaris] p. 49	Axiom A2	ax-2 4
[Margaris] p. 49	Axiom A3	ax-3 5
[Margaris] p. 49	Definition	bi 396  df-an 198  df-ex 679  df-or 197
[Margaris] p. 51	Theorem 1	id1 10
[Margaris] p. 60	Theorem 8	mth8 108
[Margaris] p. 89	Theorem 19.2	19.2 713  r19.2z 1766
[Margaris] p. 89	Theorem 19.5	alcom 715
[Margaris] p. 89	Theorem 19.6	alex 717
[Margaris] p. 89	Theorem 19.7	alnex 716
[Margaris] p. 89	Theorem 19.9	19.9r 718  19.9rv 941
[Margaris] p. 89	Theorem 19.11	excom 728  excomim 727
[Margaris] p. 89	Theorem 19.12	19.12 729  r19.12 1281
[Margaris] p. 90	Theorem 19.14	exnal 721
[Margaris] p. 90	Theorem 19.15	19.15 694  r19.15 1292
[Margaris] p. 90	Theorem 19.16	19.16 730
[Margaris] p. 90	Theorem 19.17	19.17 731
[Margaris] p. 90	Theorem 19.18	19.18 732
[Margaris] p. 90	Theorem 19.19	19.19 737
[Margaris] p. 90	Theorem 19.20	19.20 690  19.20d 693  19.20dv 946  r19.20da 1255  r19.20dva 1256  r19.20sdv 1257
[Margaris] p. 90	Theorem 19.21	19.21 738  19.21ad 741  19.21adv 945  19.21ai 740  19.21aiv 943  19.21aivv 944  19.21bi 742  19.21g 792  19.21v 942  r19.21ad 1261  r19.21adv 1262  r19.21ai 1258  r19.21aiv 1259  r19.21aivv 1263  r19.21be 1269  r19.21bi 1266  r19.21v 1260  r19.23ai 1283
[Margaris] p. 90	Theorem 19.22	19.20dvv 948  19.22 722  19.22d 744  19.22dv 947  19.22dvv 949  r19.22 1272  r19.22d 1276  r19.22dv 1278  r19.22dv2 1277  r19.22dva 1280  r19.22i2 1274  r19.22sdv 1279
[Margaris] p. 90	Theorem 19.23	19.23 745  19.23ad 748  19.23adv 954  19.23advv 955  19.23ai 746  19.23aiv 952  19.23aivv 953  19.23bi 747  19.23v 950  19.23vv 951  r19.23ad 1285  r19.23adv 1286  r19.23advv 1288  r19.23aiv 1284  r19.23aivv 1287  r19.23v 1282
[Margaris] p. 90	Theorem 19.24	19.24 762
[Margaris] p. 90	Theorem 19.25	19.25 763
[Margaris] p. 90	Theorem 19.26	19.26 749  r19.26-2 1290  r19.26 1289  r19.26m 1291
[Margaris] p. 90	Theorem 19.27	19.27 750  19.27v 956  r19.27av 1293  r19.27zv 1771
[Margaris] p. 90	Theorem 19.28	19.28 751  19.28v 957  r19.28av 1294  r19.28zv 1769
[Margaris] p. 90	Theorem 19.29	19.29 752  19.29r 753  r19.29 1295  r19.29r 1296
[Margaris] p. 90	Theorem 19.30	19.30 764
[Margaris] p. 90	Theorem 19.31	19.31 766
[Margaris] p. 90	Theorem 19.32	19.32 765  r19.32v 1297
[Margaris] p. 90	Theorem 19.33	19.33 770  19.33b 771
[Margaris] p. 90	Theorem 19.34	19.34 772
[Margaris] p. 90	Theorem 19.35	19.35 754  19.35i 755  19.35ri 756  r19.35 1298
[Margaris] p. 90	Theorem 19.36	19.36 757  19.36aiv 959  19.36i 758  19.36v 958  r19.36av 1299  r19.36zv 1772
[Margaris] p. 90	Theorem 19.37	19.37 759  19.37aiv 962  19.37v 961  r19.37av 1300
[Margaris] p. 90	Theorem 19.38	19.38 760
[Margaris] p. 90	Theorem 19.39	19.39 761
[Margaris] p. 90	Theorem 19.40	19.40 773  r19.40 1301
[Margaris] p. 90	Theorem 19.41	19.41 774  19.41v 963  19.41vv 964  19.41vvv 965  r19.41v 1302
[Margaris] p. 90	Theorem 19.42	19.42 775  19.42v 966  19.42vv 968  r19.42v 1303
[Margaris] p. 90	Theorem 19.43	19.43 767  r19.43 1304
[Margaris] p. 90	Theorem 19.44	19.44 768  r19.44av 1305
[Margaris] p. 90	Theorem 19.45	19.45 769  r19.45av 1306  r19.45zv 1770
[Margaris] p. 110	Exercise 2(b)	eu1 1019
[Mayet] p. 370	Remark	jp 5703  large 5700  str 5698
[Megill] p. 444	Axiom C5	ax-17 925
[Megill] p. 446	Lemma L17	eqt2 815
[Megill] p. 446	Lemma L18	ax9a 808
[Megill] p. 446	Lemma L19	eq6 826
[Megill] p. 447	Remark 9.1	df-sb 853  sbid 868
[Megill] p. 448	Remark 9.6	ax15 1006
[Megill] p. 448	Scheme C4'	ax-5 674
[Megill] p. 448	Scheme C5'	ax-4 673
[Megill] p. 448	Scheme C6'	ax-7 676
[Megill] p. 448	Scheme C7'	ax-6 675
[Megill] p. 448	Scheme C8'	ax-8 798
[Megill] p. 448	Scheme C9'	ax-12 802
[Megill] p. 448	Scheme C10'	ax-9 799  ax9 807
[Megill] p. 448	Scheme C11'	ax-10 800
[Megill] p. 448	Scheme C12'	ax-13 804
[Megill] p. 448	Scheme C13'	ax-14 805
[Megill] p. 448	Scheme C14'	ax-15 806
[Megill] p. 448	Scheme C15'	ax-11 801
[Megill] p. 448	Scheme C16'	ax-16 922
[Megill] p. 449	Theorem 9.7	sbcom2 992  sbequ 877  sbid2v 993
[Megill] p. 450	Example	hba1 698
[MegillPavicic] p. 2344	Theorem 3.3	stcltrth 5711
[Mendelson] p. 59	Axiom 4	rax4 1471  stdpc4 869
[Mendelson] p. 59	Axiom 5	rax5 1472  stdpc5 739
[Mendelson] p. 225	Axiom system NBG	ru 1437
[Mendelson] p. 230	Exercise 4.8(b)	opthwiener 1914
[Mendelson] p. 231	Exercise 4.10(k)	inv 1723
[Mendelson] p. 231	Exercise 4.10(l)	unv 1724
[Mendelson] p. 231	Exercise 4.10(n)	dfin3 1672
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 1708
[Mendelson] p. 231	Exercise 4.10(q)	dfin4 1673
[Mendelson] p. 231	Exercise 4.10(s)	ddif 1597
[Mendelson] p. 231	Definition of union	dfun3 1671
[Mendelson] p. 235	Exercise 4.12(c)	univ 1964
[Mendelson] p. 235	Exercise 4.12(d)	pwv 1884
[Mendelson] p. 235	Exercise 4.12(j)	pwin 1915
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 1916
[Mendelson] p. 235	Exercise 4.12(l)	pwssun 1917
[Mendelson] p. 235	Exercise 4.12(n)	uniin 1935
[Mendelson] p. 235	Exercise 4.12(p)	reli 2500
[Mendelson] p. 235	Exercise 4.12(t)	relssdr 2668
[Mendelson] p. 244	Proposition 4.8(g)	epweon 2239
[Mendelson] p. 246	Definition of successor	df-suc 2205
[Mendelson] p. 254	Proposition 4.22(b)	xpen 3383
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 3339  xpsneng 3340
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 3343
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 3344
[Mendelson] p. 255	Definition	brsdom 3286
[Mendelson] p. 255	Exercise 4.39	endisj 3341
[Mendelson] p. 255	Exercise 4.41	mapprc 3260
[Mendelson] p. 255	Exercise 4.43	mapsnen 3334
[Mendelson] p. 255	Exercise 4.45	mapunen 3397
[Mendelson] p. 255	Exercise 4.47	xpmapen 3396
[Mendelson] p. 255	Exercise 4.42(a)	map0e 3266
[Mendelson] p. 255	Exercise 4.42(b)	map1 3335
[Mendelson] p. 257	Proposition 4.24(a)	undom 3342
[Mendelson] p. 258	Exercise 4.56(b)	cdaen 3719
[Mendelson] p. 258	Exercise 4.56(c)	cdaassen 3725  cdacomen 3724
[Mendelson] p. 258	Exercise 4.56(f)	cdadom1 3727
[Mendelson] p. 258	Exercise 4.56(g)	xp2cda 3723
[Mendelson] p. 258	Definition of cardinal sum	cdaval 3717  cdavalt 3716  df-cda 3715
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 3132
[Mendelson] p. 266	Proposition 4.34(f)	oaordex 3160
[Mendelson] p. 275	Proposition 4.42(d)	entri3 3647
[Mendelson] p. 281	Definition	df-r1 3487
[Mendelson] p. 281	Proposition 4.45 (b) to (a)	unir1 3511
[Mendelson] p. 287	Axiom system MK	ru 1437
[Mittelstaedt] p. 9	Definition	df-oc 5156
[Monk1] p. 26	Theorem 2.8(vii)	ssin 1659
[Monk1] p. 33	Theorem 3.2(i)	relss 2480
[Monk1] p. 33	Theorem 3.2(ii)	cleqrel 2483
[Monk1] p. 34	Definition 3.3	df-opab 2098
[Monk1] p. 36	Theorem 3.7(i)	coi1 2665  coi2 2666
[Monk1] p. 36	Theorem 3.8(v)	dm0 2542  rn0 2567
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 2634
[Monk1] p. 37	Theorem 3.13(i)	relxp 2486
[Monk1] p. 37	Theorem 3.13(x)	dmxp 2552  rnxp 2657
[Monk1] p. 37	Theorem 3.13(ii)	xp0 2652  xp0r 2474
[Monk1] p. 38	Theorem 3.16(ii)	ima0 2615
[Monk1] p. 38	Theorem 3.16(viii)	imai 2613
[Monk1] p. 39	Theorem 3.17	imaexg 2612
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 2611
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 2887  funopfv 2886
[Monk1] p. 42	Theorem 4.3(ii)	funfvop 2857
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 2859
[Monk1] p. 43	Theorem 4.6	funun 2700
[Monk1] p. 43	Theorem 4.8(iv)	f1fv 2916  f1fvf&nbs