Bibliographic Cross-Reference - Metamath Proof Explorer

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, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Metamath Proof Explorer

Bibliographic Reference	Description	Metamath Proof Explorer Page(s)
[Adamek] p. 21	Definition 3.1	df-cat 16688
[Adamek] p. 21	Condition 3.1(b)	df-cat 16688
[Adamek] p. 22	Example 3.3(1)	df-setc 17085
[Adamek] p. 24	Example 3.3(4.c)	0cat 16708
[Adamek] p. 25	Definition 3.5	df-oppc 16731
[Adamek] p. 28	Remark 3.9	oppciso 16800
[Adamek] p. 28	Remark 3.12	invf1o 16788  invisoinvl 16809
[Adamek] p. 28	Example 3.13	idinv 16808  idiso 16807
[Adamek] p. 28	Corollary 3.11	inveq 16793
[Adamek] p. 28	Definition 3.8	df-inv 16767  df-iso 16768  dfiso2 16791
[Adamek] p. 28	Proposition 3.10	sectcan 16774
[Adamek] p. 29	Remark 3.16	cicer 16825
[Adamek] p. 29	Definition 3.15	cic 16818  df-cic 16815
[Adamek] p. 29	Definition 3.17	df-func 16877
[Adamek] p. 29	Proposition 3.14(1)	invinv 16789
[Adamek] p. 29	Proposition 3.14(2)	invco 16790  isoco 16796
[Adamek] p. 30	Remark 3.19	df-func 16877
[Adamek] p. 30	Example 3.20(1)	idfucl 16900
[Adamek] p. 32	Proposition 3.21	funciso 16893
[Adamek] p. 33	Proposition 3.23	cofucl 16907
[Adamek] p. 34	Remark 3.28(2)	catciso 17116
[Adamek] p. 34	Remark 3.28 (1)	embedsetcestrc 17167
[Adamek] p. 34	Definition 3.27(2)	df-fth 16924
[Adamek] p. 34	Definition 3.27(3)	df-full 16923
[Adamek] p. 34	Definition 3.27 (1)	embedsetcestrc 17167
[Adamek] p. 35	Corollary 3.32	ffthiso 16948
[Adamek] p. 35	Proposition 3.30(c)	cofth 16954
[Adamek] p. 35	Proposition 3.30(d)	cofull 16953
[Adamek] p. 36	Definition 3.33 (1)	equivestrcsetc 17152
[Adamek] p. 36	Definition 3.33 (2)	equivestrcsetc 17152
[Adamek] p. 39	Definition 3.41	funcoppc 16894
[Adamek] p. 39	Definition 3.44.	df-catc 17104
[Adamek] p. 39	Proposition 3.43(c)	fthoppc 16942
[Adamek] p. 39	Proposition 3.43(d)	fulloppc 16941
[Adamek] p. 40	Remark 3.48	catccat 17113
[Adamek] p. 40	Definition 3.47	df-catc 17104
[Adamek] p. 48	Example 4.3(1.a)	0subcat 16857
[Adamek] p. 48	Example 4.3(1.b)	catsubcat 16858
[Adamek] p. 48	Definition 4.1(2)	fullsubc 16869
[Adamek] p. 48	Definition 4.1(a)	df-subc 16831
[Adamek] p. 49	Remark 4.4(2)	ressffth 16957
[Adamek] p. 83	Definition 6.1	df-nat 16962
[Adamek] p. 87	Remark 6.14(a)	fuccocl 16983
[Adamek] p. 87	Remark 6.14(b)	fucass 16987
[Adamek] p. 87	Definition 6.15	df-fuc 16963
[Adamek] p. 88	Remark 6.16	fuccat 16989
[Adamek] p. 101	Definition 7.1	df-inito 17000
[Adamek] p. 101	Example 7.2 (6)	irinitoringc 42930
[Adamek] p. 102	Definition 7.4	df-termo 17001
[Adamek] p. 102	Proposition 7.3 (1)	initoeu1w 17021
[Adamek] p. 102	Proposition 7.3 (2)	initoeu2 17025
[Adamek] p. 103	Definition 7.7	df-zeroo 17002
[Adamek] p. 103	Example 7.9 (3)	nzerooringczr 42933
[Adamek] p. 103	Proposition 7.6	termoeu1w 17028
[Adamek] p. 106	Definition 7.19	df-sect 16766
[Adamek] p. 478	Item Rng	df-ringc 42866
[AhoHopUll] p. 2	Section 1.1	df-bigo 43203
[AhoHopUll] p. 12	Section 1.3	df-blen 43225
[AhoHopUll] p. 318	Section 9.1	df-concat 13638  df-pfx 13757  df-substr 13708  df-word 13582  lencl 13600  wrd0 13606
[AkhiezerGlazman] p. 39	Linear operator norm	df-nmo 22889  df-nmoo 28151
[AkhiezerGlazman] p. 64	Theorem	hmopidmch 29563  hmopidmchi 29561
[AkhiezerGlazman] p. 65	Theorem 1	pjcmul1i 29611  pjcmul2i 29612
[AkhiezerGlazman] p. 72	Theorem	cnvunop 29328  unoplin 29330
[AkhiezerGlazman] p. 72	Equation 2	unopadj 29329  unopadj2 29348
[AkhiezerGlazman] p. 73	Theorem	elunop2 29423  lnopunii 29422
[AkhiezerGlazman] p. 80	Proposition 1	adjlnop 29496
[Apostol] p. 18	Theorem I.1	addcan 10546  addcan2d 10566  addcan2i 10556  addcand 10565  addcani 10555
[Apostol] p. 18	Theorem I.2	negeu 10598
[Apostol] p. 18	Theorem I.3	negsub 10657  negsubd 10726  negsubi 10687
[Apostol] p. 18	Theorem I.4	negneg 10659  negnegd 10711  negnegi 10679
[Apostol] p. 18	Theorem I.5	subdi 10794  subdid 10817  subdii 10810  subdir 10795  subdird 10818  subdiri 10811
[Apostol] p. 18	Theorem I.6	mul01 10541  mul01d 10561  mul01i 10552  mul02 10540  mul02d 10560  mul02i 10551
[Apostol] p. 18	Theorem I.7	mulcan 10996  mulcan2d 10993  mulcand 10992  mulcani 10998
[Apostol] p. 18	Theorem I.8	receu 11004  xreceu 30171
[Apostol] p. 18	Theorem I.9	divrec 11033  divrecd 11137  divreci 11103  divreczi 11096
[Apostol] p. 18	Theorem I.10	recrec 11055  recreci 11090
[Apostol] p. 18	Theorem I.11	mul0or 10999  mul0ord 11009  mul0ori 11007
[Apostol] p. 18	Theorem I.12	mul2neg 10800  mul2negd 10816  mul2negi 10809  mulneg1 10797  mulneg1d 10814  mulneg1i 10807
[Apostol] p. 18	Theorem I.13	divadddiv 11073  divadddivd 11178  divadddivi 11120
[Apostol] p. 18	Theorem I.14	divmuldiv 11058  divmuldivd 11175  divmuldivi 11118  rdivmuldivd 30332
[Apostol] p. 18	Theorem I.15	divdivdiv 11059  divdivdivd 11181  divdivdivi 11121
[Apostol] p. 20	Axiom 7	rpaddcl 12143  rpaddcld 12178  rpmulcl 12144  rpmulcld 12179
[Apostol] p. 20	Axiom 8	rpneg 12153
[Apostol] p. 20	Axiom 9	0nrp 12156
[Apostol] p. 20	Theorem I.17	lttri 10489
[Apostol] p. 20	Theorem I.18	ltadd1d 10952  ltadd1dd 10970  ltadd1i 10913
[Apostol] p. 20	Theorem I.19	ltmul1 11210  ltmul1a 11209  ltmul1i 11279  ltmul1ii 11289  ltmul2 11211  ltmul2d 12205  ltmul2dd 12219  ltmul2i 11282
[Apostol] p. 20	Theorem I.20	msqgt0 10879  msqgt0d 10926  msqgt0i 10896
[Apostol] p. 20	Theorem I.21	0lt1 10881
[Apostol] p. 20	Theorem I.23	lt0neg1 10865  lt0neg1d 10928  ltneg 10859  ltnegd 10937  ltnegi 10903
[Apostol] p. 20	Theorem I.25	lt2add 10844  lt2addd 10982  lt2addi 10921
[Apostol] p. 20	Definition of positive numbers	df-rp 12120
[Apostol] p. 21	Exercise 4	recgt0 11204  recgt0d 11295  recgt0i 11265  recgt0ii 11266
[Apostol] p. 22	Definition of integers	df-z 11712
[Apostol] p. 22	Definition of positive integers	dfnn3 11373
[Apostol] p. 22	Definition of rationals	df-q 12079
[Apostol] p. 24	Theorem I.26	supeu 8635
[Apostol] p. 26	Theorem I.28	nnunb 11621
[Apostol] p. 26	Theorem I.29	arch 11622
[Apostol] p. 28	Exercise 2	btwnz 11814
[Apostol] p. 28	Exercise 3	nnrecl 11623
[Apostol] p. 28	Exercise 4	rebtwnz 12077
[Apostol] p. 28	Exercise 5	zbtwnre 12076
[Apostol] p. 28	Exercise 6	qbtwnre 12325
[Apostol] p. 28	Exercise 10(a)	zeneo 15444  zneo 11795  zneoALTV 42424
[Apostol] p. 29	Theorem I.35	cxpsqrtth 24881  msqsqrtd 14563  resqrtth 14380  sqrtth 14488  sqrtthi 14494  sqsqrtd 14562
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 11360
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwo 12043
[Apostol] p. 361	Remark	crreczi 13290
[Apostol] p. 363	Remark	absgt0i 14522
[Apostol] p. 363	Example	abssubd 14576  abssubi 14526
[ApostolNT] p. 7	Remark	fmtno0 42296  fmtno1 42297  fmtno2 42306  fmtno3 42307  fmtno4 42308  fmtno5fac 42338  fmtnofz04prm 42333
[ApostolNT] p. 7	Definition	df-fmtno 42284
[ApostolNT] p. 8	Definition	df-ppi 25246
[ApostolNT] p. 14	Definition	df-dvds 15365
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 15379
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 15402
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 15398
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 15392
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 15394
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 15380
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 15381
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 15386
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 15417
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 15419
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 15421
[ApostolNT] p. 15	Definition	df-gcd 15597  dfgcd2 15643
[ApostolNT] p. 16	Definition	isprm2 15774
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 15746
[ApostolNT] p. 16	Theorem 1.7	prminf 15997
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 15615
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 15644
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 15646
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 15629
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 15621
[ApostolNT] p. 17	Theorem 1.8	coprm 15801
[ApostolNT] p. 17	Theorem 1.9	euclemma 15803
[ApostolNT] p. 17	Theorem 1.10	1arith2 16010
[ApostolNT] p. 18	Theorem 1.13	prmrec 16004
[ApostolNT] p. 19	Theorem 1.14	divalg 15507
[ApostolNT] p. 20	Theorem 1.15	eucalg 15680
[ApostolNT] p. 24	Definition	df-mu 25247
[ApostolNT] p. 25	Definition	df-phi 15849
[ApostolNT] p. 25	Theorem 2.1	musum 25337
[ApostolNT] p. 26	Theorem 2.2	phisum 15873
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 15859
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 15863
[ApostolNT] p. 32	Definition	df-vma 25244
[ApostolNT] p. 32	Theorem 2.9	muinv 25339
[ApostolNT] p. 32	Theorem 2.10	vmasum 25361
[ApostolNT] p. 38	Remark	df-sgm 25248
[ApostolNT] p. 38	Definition	df-sgm 25248
[ApostolNT] p. 75	Definition	df-chp 25245  df-cht 25243
[ApostolNT] p. 104	Definition	congr 15757
[ApostolNT] p. 106	Remark	dvdsval3 15368
[ApostolNT] p. 106	Definition	moddvds 15375
[ApostolNT] p. 107	Example 2	mod2eq0even 15451
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 15452
[ApostolNT] p. 107	Example 4	zmod1congr 12989
[ApostolNT] p. 107	Theorem 5.2(b)	modmul12d 13026
[ApostolNT] p. 107	Theorem 5.2(c)	modexp 13300
[ApostolNT] p. 108	Theorem 5.3	modmulconst 15397
[ApostolNT] p. 109	Theorem 5.4	cncongr1 15760
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 16156
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 15762
[ApostolNT] p. 113	Theorem 5.17	eulerth 15866
[ApostolNT] p. 113	Theorem 5.18	vfermltl 15884
[ApostolNT] p. 114	Theorem 5.19	fermltl 15867
[ApostolNT] p. 116	Theorem 5.24	wilthimp 25218
[ApostolNT] p. 179	Definition	df-lgs 25440  lgsprme0 25484
[ApostolNT] p. 180	Example 1	1lgs 25485
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 25461
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 25476
[ApostolNT] p. 181	Theorem 9.4	m1lgs 25533
[ApostolNT] p. 181	Theorem 9.5	2lgs 25552  2lgsoddprm 25561
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 25519
[ApostolNT] p. 185	Theorem 9.8	lgsquad 25528
[ApostolNT] p. 188	Definition	df-lgs 25440  lgs1 25486
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 25477
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 25479
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 25487
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 25488
[Baer] p. 40	Property (b)	mapdord 37708
[Baer] p. 40	Property (c)	mapd11 37709
[Baer] p. 40	Property (e)	mapdin 37732  mapdlsm 37734
[Baer] p. 40	Property (f)	mapd0 37735
[Baer] p. 40	Definition of projectivity	df-mapd 37695  mapd1o 37718
[Baer] p. 41	Property (g)	mapdat 37737
[Baer] p. 44	Part (1)	mapdpg 37776
[Baer] p. 45	Part (2)	hdmap1eq 37871  mapdheq 37798  mapdheq2 37799  mapdheq2biN 37800
[Baer] p. 45	Part (3)	baerlem3 37783
[Baer] p. 46	Part (4)	mapdheq4 37802  mapdheq4lem 37801
[Baer] p. 46	Part (5)	baerlem5a 37784  baerlem5abmN 37788  baerlem5amN 37786  baerlem5b 37785  baerlem5bmN 37787
[Baer] p. 47	Part (6)	hdmap1l6 37891  hdmap1l6a 37879  hdmap1l6e 37884  hdmap1l6f 37885  hdmap1l6g 37886  hdmap1l6lem1 37877  hdmap1l6lem2 37878  mapdh6N 37817  mapdh6aN 37805  mapdh6eN 37810  mapdh6fN 37811  mapdh6gN 37812  mapdh6lem1N 37803  mapdh6lem2N 37804
[Baer] p. 48	Part 9	hdmapval 37898
[Baer] p. 48	Part 10	hdmap10 37910
[Baer] p. 48	Part 11	hdmapadd 37913
[Baer] p. 48	Part (6)	hdmap1l6h 37887  mapdh6hN 37813
[Baer] p. 48	Part (7)	mapdh75cN 37823  mapdh75d 37824  mapdh75e 37822  mapdh75fN 37825  mapdh7cN 37819  mapdh7dN 37820  mapdh7eN 37818  mapdh7fN 37821
[Baer] p. 48	Part (8)	mapdh8 37858  mapdh8a 37845  mapdh8aa 37846  mapdh8ab 37847  mapdh8ac 37848  mapdh8ad 37849  mapdh8b 37850  mapdh8c 37851  mapdh8d 37853  mapdh8d0N 37852  mapdh8e 37854  mapdh8g 37855  mapdh8i 37856  mapdh8j 37857
[Baer] p. 48	Part (9)	mapdh9a 37859
[Baer] p. 48	Equation 10	mapdhvmap 37839
[Baer] p. 49	Part 12	hdmap11 37918  hdmapeq0 37914  hdmapf1oN 37935  hdmapneg 37916  hdmaprnN 37934  hdmaprnlem1N 37919  hdmaprnlem3N 37920  hdmaprnlem3uN 37921  hdmaprnlem4N 37923  hdmaprnlem6N 37924  hdmaprnlem7N 37925  hdmaprnlem8N 37926  hdmaprnlem9N 37927  hdmapsub 37917
[Baer] p. 49	Part 14	hdmap14lem1 37938  hdmap14lem10 37947  hdmap14lem1a 37936  hdmap14lem2N 37939  hdmap14lem2a 37937  hdmap14lem3 37940  hdmap14lem8 37945  hdmap14lem9 37946
[Baer] p. 50	Part 14	hdmap14lem11 37948  hdmap14lem12 37949  hdmap14lem13 37950  hdmap14lem14 37951  hdmap14lem15 37952  hgmapval 37957
[Baer] p. 50	Part 15	hgmapadd 37964  hgmapmul 37965  hgmaprnlem2N 37967  hgmapvs 37961
[Baer] p. 50	Part 16	hgmaprnN 37971
[Baer] p. 110	Lemma 1	hdmapip0com 37987
[Baer] p. 110	Line 27	hdmapinvlem1 37988
[Baer] p. 110	Line 28	hdmapinvlem2 37989
[Baer] p. 110	Line 30	hdmapinvlem3 37990
[Baer] p. 110	Part 1.2	hdmapglem5 37992  hgmapvv 37996
[Baer] p. 110	Proposition 1	hdmapinvlem4 37991
[Baer] p. 111	Line 10	hgmapvvlem1 37993
[Baer] p. 111	Line 15	hdmapg 38000  hdmapglem7 37999
[Bauer], p. 483	Theorem 1.2	2irrexpq 24882  2irrexpqALT 24947
[BellMachover] p. 36	Lemma 10.3	idALT 23
[BellMachover] p. 97	Definition 10.1	df-eu 2640
[BellMachover] p. 460	Notation	df-mo 2605
[BellMachover] p. 460	Definition	mo3 2633
[BellMachover] p. 461	Axiom Ext	ax-ext 2803
[BellMachover] p. 462	Theorem 1.1	axextmo 2808
[BellMachover] p. 463	Axiom Rep	axrep5 5002
[BellMachover] p. 463	Scheme Sep	axsep 5006
[BellMachover] p. 463	Theorem 1.3(ii)	bj-bm1.3ii 33541  bm1.3ii 5010
[BellMachover] p. 466	Problem	axpow2 5069
[BellMachover] p. 466	Axiom Pow	axpow3 5070
[BellMachover] p. 466	Axiom Union	axun2 7216
[BellMachover] p. 468	Definition	df-ord 5970
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 5985
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 5992
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 5987
[BellMachover] p. 471	Definition of N	df-om 7332
[BellMachover] p. 471	Problem 2.5(ii)	uniordint 7272
[BellMachover] p. 471	Definition of Lim	df-lim 5972
[BellMachover] p. 472	Axiom Inf	zfinf2 8823
[BellMachover] p. 473	Theorem 2.8	limom 7346
[BellMachover] p. 477	Equation 3.1	df-r1 8911
[BellMachover] p. 478	Definition	rankval2 8965
[BellMachover] p. 478	Theorem 3.3(i)	r1ord3 8929  r1ord3g 8926
[BellMachover] p. 480	Axiom Reg	zfreg 8776
[BellMachover] p. 488	Axiom AC	ac5 9621  dfac4 9265
[BellMachover] p. 490	Definition of aleph	alephval3 9253
[BeltramettiCassinelli] p. 98	Remark	atlatmstc 35389
[BeltramettiCassinelli] p. 107	Remark 10.3.5	atom1d 29763
[BeltramettiCassinelli] p. 166	Theorem 14.8.4	chirred 29805  chirredi 29804
[BeltramettiCassinelli1] p. 400	Proposition P8(ii)	atoml2i 29793
[Beran] p. 3	Definition of join	sshjval3 28764
[Beran] p. 39	Theorem 2.3(i)	cmcm2 29026  cmcm2i 29003  cmcm2ii 29008  cmt2N 35320
[Beran] p. 40	Theorem 2.3(iii)	lecm 29027  lecmi 29012  lecmii 29013
[Beran] p. 45	Theorem 3.4	cmcmlem 29001
[Beran] p. 49	Theorem 4.2	cm2j 29030  cm2ji 29035  cm2mi 29036
[Beran] p. 95	Definition	df-sh 28615  issh2 28617
[Beran] p. 95	Lemma 3.1(S5)	his5 28494
[Beran] p. 95	Lemma 3.1(S6)	his6 28507
[Beran] p. 95	Lemma 3.1(S7)	his7 28498
[Beran] p. 95	Lemma 3.2(S8)	ho01i 29238
[Beran] p. 95	Lemma 3.2(S9)	hoeq1 29240
[Beran] p. 95	Lemma 3.2(S10)	ho02i 29239
[Beran] p. 95	Lemma 3.2(S11)	hoeq2 29241
[Beran] p. 95	Postulate (S1)	ax-his1 28490  his1i 28508
[Beran] p. 95	Postulate (S2)	ax-his2 28491
[Beran] p. 95	Postulate (S3)	ax-his3 28492
[Beran] p. 95	Postulate (S4)	ax-his4 28493
[Beran] p. 96	Definition of norm	df-hnorm 28376  dfhnorm2 28530  normval 28532
[Beran] p. 96	Definition for Cauchy sequence	hcau 28592
[Beran] p. 96	Definition of Cauchy sequence	df-hcau 28381
[Beran] p. 96	Definition of complete subspace	isch3 28649
[Beran] p. 96	Definition of converge	df-hlim 28380  hlimi 28596
[Beran] p. 97	Theorem 3.3(i)	norm-i-i 28541  norm-i 28537
[Beran] p. 97	Theorem 3.3(ii)	norm-ii-i 28545  norm-ii 28546  normlem0 28517  normlem1 28518  normlem2 28519  normlem3 28520  normlem4 28521  normlem5 28522  normlem6 28523  normlem7 28524  normlem7tALT 28527
[Beran] p. 97	Theorem 3.3(iii)	norm-iii-i 28547  norm-iii 28548
[Beran] p. 98	Remark 3.4	bcs 28589  bcsiALT 28587  bcsiHIL 28588
[Beran] p. 98	Remark 3.4(B)	normlem9at 28529  normpar 28563  normpari 28562
[Beran] p. 98	Remark 3.4(C)	normpyc 28554  normpyth 28553  normpythi 28550
[Beran] p. 99	Remark	lnfn0 29457  lnfn0i 29452  lnop0 29376  lnop0i 29380
[Beran] p. 99	Theorem 3.5(i)	nmcexi 29436  nmcfnex 29463  nmcfnexi 29461  nmcopex 29439  nmcopexi 29437
[Beran] p. 99	Theorem 3.5(ii)	nmcfnlb 29464  nmcfnlbi 29462  nmcoplb 29440  nmcoplbi 29438
[Beran] p. 99	Theorem 3.5(iii)	lnfncon 29466  lnfnconi 29465  lnopcon 29445  lnopconi 29444
[Beran] p. 100	Lemma 3.6	normpar2i 28564
[Beran] p. 101	Lemma 3.6	norm3adifi 28561  norm3adifii 28556  norm3dif 28558  norm3difi 28555
[Beran] p. 102	Theorem 3.7(i)	chocunii 28711  pjhth 28803  pjhtheu 28804  pjpjhth 28835  pjpjhthi 28836  pjth 23614
[Beran] p. 102	Theorem 3.7(ii)	ococ 28816  ococi 28815
[Beran] p. 103	Remark 3.8	nlelchi 29471
[Beran] p. 104	Theorem 3.9	riesz3i 29472  riesz4 29474  riesz4i 29473
[Beran] p. 104	Theorem 3.10	cnlnadj 29489  cnlnadjeu 29488  cnlnadjeui 29487  cnlnadji 29486  cnlnadjlem1 29477  nmopadjlei 29498
[Beran] p. 106	Theorem 3.11(i)	adjeq0 29501
[Beran] p. 106	Theorem 3.11(v)	nmopadji 29500
[Beran] p. 106	Theorem 3.11(ii)	adjmul 29502
[Beran] p. 106	Theorem 3.11(iv)	adjadj 29346
[Beran] p. 106	Theorem 3.11(vi)	nmopcoadj2i 29512  nmopcoadji 29511
[Beran] p. 106	Theorem 3.11(iii)	adjadd 29503
[Beran] p. 106	Theorem 3.11(vii)	nmopcoadj0i 29513
[Beran] p. 106	Theorem 3.11(viii)	adjcoi 29510  pjadj2coi 29614  pjadjcoi 29571
[Beran] p. 107	Definition	df-ch 28629  isch2 28631
[Beran] p. 107	Remark 3.12	choccl 28716  isch3 28649  occl 28714  ocsh 28693  shoccl 28715  shocsh 28694
[Beran] p. 107	Remark 3.12(B)	ococin 28818
[Beran] p. 108	Theorem 3.13	chintcl 28742
[Beran] p. 109	Property (i)	pjadj2 29597  pjadj3 29598  pjadji 29095  pjadjii 29084
[Beran] p. 109	Property (ii)	pjidmco 29591  pjidmcoi 29587  pjidmi 29083
[Beran] p. 110	Definition of projector ordering	pjordi 29583
[Beran] p. 111	Remark	ho0val 29160  pjch1 29080
[Beran] p. 111	Definition	df-hfmul 29144  df-hfsum 29143  df-hodif 29142  df-homul 29141  df-hosum 29140
[Beran] p. 111	Lemma 4.4(i)	pjo 29081
[Beran] p. 111	Lemma 4.4(ii)	pjch 29104  pjchi 28842
[Beran] p. 111	Lemma 4.4(iii)	pjoc2 28849  pjoc2i 28848
[Beran] p. 112	Theorem 4.5(i)->(ii)	pjss2i 29090
[Beran] p. 112	Theorem 4.5(i)->(iv)	pjssmi 29575  pjssmii 29091
[Beran] p. 112	Theorem 4.5(i)<->(ii)	pjss2coi 29574
[Beran] p. 112	Theorem 4.5(i)<->(iii)	pjss1coi 29573
[Beran] p. 112	Theorem 4.5(i)<->(vi)	pjnormssi 29578
[Beran] p. 112	Theorem 4.5(iv)->(v)	pjssge0i 29576  pjssge0ii 29092
[Beran] p. 112	Theorem 4.5(v)<->(vi)	pjdifnormi 29577  pjdifnormii 29093
[Bobzien] p. 116	Statement T3	stoic3 1875
[Bobzien] p. 117	Statement T2	stoic2a 1873
[Bobzien] p. 117	Statement T4	stoic4a 1876
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1871
[Bogachev] p. 16	Definition 1.5	df-oms 30895
[Bogachev] p. 17	Lemma 1.5.4	omssubadd 30903
[Bogachev] p. 17	Example 1.5.2	omsmon 30901
[Bogachev] p. 41	Definition 1.11.2	df-carsg 30905
[Bogachev] p. 42	Theorem 1.11.4	carsgsiga 30925
[Bogachev] p. 116	Definition 2.3.1	df-itgm 30956  df-sitm 30934
[Bogachev] p. 118	Chapter 2.4.4	df-itgm 30956
[Bogachev] p. 118	Definition 2.4.1	df-sitg 30933
[Bollobas] p. 1	Section I.1	df-edg 26353  isuhgrop 26375  isusgrop 26468  isuspgrop 26467
[Bollobas] p. 2	Section I.1	df-subgr 26572  uhgrspan1 26607  uhgrspansubgr 26595
[Bollobas] p. 3	Definition	isomuspgr 42566
[Bollobas] p. 3	Section I.1	cusgrsize 26759  df-cusgr 26717  df-nbgr 26637  fusgrmaxsize 26769
[Bollobas] p. 4	Definition	df-upwlks 42576  df-wlks 26904
[Bollobas] p. 4	Section I.1	finsumvtxdg2size 26855  finsumvtxdgeven 26857  fusgr1th 26856  fusgrvtxdgonume 26859  vtxdgoddnumeven 26858
[Bollobas] p. 5	Notation	df-pths 27025
[Bollobas] p. 5	Definition	df-crcts 27095  df-cycls 27096  df-trls 27000  df-wlkson 26905
[Bollobas] p. 7	Section I.1	df-ushgr 26364
[BourbakiAlg1] p. 1	Definition 1	df-clintop 42697  df-cllaw 42683  df-mgm 17602  df-mgm2 42716
[BourbakiAlg1] p. 4	Definition 5	df-assintop 42698  df-asslaw 42685  df-sgrp 17644  df-sgrp2 42718
[BourbakiAlg1] p. 7	Definition 8	df-cmgm2 42717  df-comlaw 42684
[BourbakiAlg1] p. 12	Definition 2	df-mnd 17655
[BourbakiAlg1] p. 92	Definition 1	df-ring 18910
[BourbakiAlg1] p. 93	Section I.8.1	df-rng0 42736
[BourbakiEns] p.	Proposition 8	fcof1 6802  fcofo 6803
[BourbakiTop1] p.	Remark	xnegmnf 12336  xnegpnf 12335
[BourbakiTop1] p.	Remark	rexneg 12337
[BourbakiTop1] p.	Remark 3	ust0 22400  ustfilxp 22393
[BourbakiTop1] p.	Axiom GT'	tgpsubcn 22271
[BourbakiTop1] p.	Example 1	cstucnd 22465  iducn 22464  snfil 22045
[BourbakiTop1] p.	Example 2	neifil 22061
[BourbakiTop1] p.	Theorem 1	cnextcn 22248
[BourbakiTop1] p.	Theorem 2	ucnextcn 22485
[BourbakiTop1] p.	Theorem 3	df-hcmp 30544
[BourbakiTop1] p.	Paragraph 3	infil 22044
[BourbakiTop1] p.	Proposition	ishmeo 21940
[BourbakiTop1] p.	Definition 1	df-ucn 22457  df-ust 22381  filintn0 22042  filn0 22043  istgp 22258  ucnprima 22463
[BourbakiTop1] p.	Definition 2	df-cfilu 22468
[BourbakiTop1] p.	Definition 3	df-cusp 22479  df-usp 22438  df-utop 22412  trust 22410
[BourbakiTop1] p.	Definition 6	df-pcmp 30464
[BourbakiTop1] p.	Property V_i	ssnei2 21298
[BourbakiTop1] p.	Theorem 1(d)	iscncl 21451
[BourbakiTop1] p.	Condition F_I	ustssel 22386
[BourbakiTop1] p.	Condition U_I	ustdiag 22389
[BourbakiTop1] p.	Property V_ii	innei 21307
[BourbakiTop1] p.	Property V_iv	neiptopreu 21315  neissex 21309
[BourbakiTop1] p.	Proposition 1	neips 21295  neiss 21291  ucncn 22466  ustund 22402  ustuqtop 22427
[BourbakiTop1] p.	Proposition 2	cnpco 21449  neiptopreu 21315  utop2nei 22431  utop3cls 22432
[BourbakiTop1] p.	Proposition 3	fmucnd 22473  uspreg 22455  utopreg 22433
[BourbakiTop1] p.	Proposition 4	imasncld 21872  imasncls 21873  imasnopn 21871
[BourbakiTop1] p.	Proposition 9	cnpflf2 22181
[BourbakiTop1] p.	Condition F_II	ustincl 22388
[BourbakiTop1] p.	Condition U_II	ustinvel 22390
[BourbakiTop1] p.	Property V_iii	elnei 21293
[BourbakiTop1] p.	Proposition 11	cnextucn 22484
[BourbakiTop1] p.	Condition F_IIb	ustbasel 22387
[BourbakiTop1] p.	Condition U_III	ustexhalf 22391
[BourbakiTop1] p.	Definition C'''	df-cmp 21568
[BourbakiTop1] p.	Axioms FI, FIIa, FIIb, FIII)	df-fil 22027
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 21076
[BourbakiTop2] p. 195	Definition 1	df-ldlf 30461
[BrosowskiDeutsh] p. 89	Proof follows	stoweidlem62 41067
[BrosowskiDeutsh] p. 89	Lemmas are written following	stowei 41069  stoweid 41068
[BrosowskiDeutsh] p. 90	Lemma 1	stoweidlem1 41006  stoweidlem10 41015  stoweidlem14 41019  stoweidlem15 41020  stoweidlem35 41040  stoweidlem36 41041  stoweidlem37 41042  stoweidlem38 41043  stoweidlem40 41045  stoweidlem41 41046  stoweidlem43 41048  stoweidlem44 41049  stoweidlem46 41051  stoweidlem5 41010  stoweidlem50 41055  stoweidlem52 41057  stoweidlem53 41058  stoweidlem55 41060  stoweidlem56 41061
[BrosowskiDeutsh] p. 90	Lemma 1	stoweidlem23 41028  stoweidlem24 41029  stoweidlem27 41032  stoweidlem28 41033  stoweidlem30 41035
[BrosowskiDeutsh] p. 91	Proof	stoweidlem34 41039  stoweidlem59 41064  stoweidlem60 41065
[BrosowskiDeutsh] p. 91	Lemma 1	stoweidlem45 41050  stoweidlem49 41054  stoweidlem7 41012
[BrosowskiDeutsh] p. 91	Lemma 2	stoweidlem31 41036  stoweidlem39 41044  stoweidlem42 41047  stoweidlem48 41053  stoweidlem51 41056  stoweidlem54 41059  stoweidlem57 41062  stoweidlem58 41063
[BrosowskiDeutsh] p. 91	Lemma 1	stoweidlem25 41030
[BrosowskiDeutsh] p. 91	Lemma proves that the function ` ` (as defined	stoweidlem17 41022
[BrosowskiDeutsh] p. 92	Proof	stoweidlem11 41016  stoweidlem13 41018  stoweidlem26 41031  stoweidlem61 41066
[BrosowskiDeutsh] p. 92	Lemma 2	stoweidlem18 41023
[Bruck] p. 1	Section I.1	df-clintop 42697  df-mgm 17602  df-mgm2 42716
[Bruck] p. 23	Section II.1	df-sgrp 17644  df-sgrp2 42718
[Bruck] p. 28	Theorem 3.2	dfgrp3 17875
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4955
[Church] p. 129	Section II.24	df-ifp 1090  dfifp2 1091
[Clemente] p. 10	Definition IT	natded 27814
[Clemente] p. 10	Definition I` `m,n	natded 27814
[Clemente] p. 11	Definition E=>m,n	natded 27814
[Clemente] p. 11	Definition I=>m,n	natded 27814
[Clemente] p. 11	Definition E` `(1)	natded 27814
[Clemente] p. 11	Definition E` `(2)	natded 27814
[Clemente] p. 12	Definition E` `m,n,p	natded 27814
[Clemente] p. 12	Definition I` `n(1)	natded 27814
[Clemente] p. 12	Definition I` `n(2)	natded 27814
[Clemente] p. 13	Definition I` `m,n,p	natded 27814
[Clemente] p. 14	Proof 5.11	natded 27814
[Clemente] p. 14	Definition E` `n	natded 27814
[Clemente] p. 15	Theorem 5.2	ex-natded5.2-2 27816  ex-natded5.2 27815
[Clemente] p. 16	Theorem 5.3	ex-natded5.3-2 27819  ex-natded5.3 27818
[Clemente] p. 18	Theorem 5.5	ex-natded5.5 27821
[Clemente] p. 19	Theorem 5.7	ex-natded5.7-2 27823  ex-natded5.7 27822
[Clemente] p. 20	Theorem 5.8	ex-natded5.8-2 27825  ex-natded5.8 27824
[Clemente] p. 20	Theorem 5.13	ex-natded5.13-2 27827  ex-natded5.13 27826
[Clemente] p. 32	Definition I` `n	natded 27814
[Clemente] p. 32	Definition E` `m,n,p,a	natded 27814
[Clemente] p. 32	Definition E` `n,t	natded 27814
[Clemente] p. 32	Definition I` `n,t	natded 27814
[Clemente] p. 43	Theorem 9.20	ex-natded9.20 27828
[Clemente] p. 45	Theorem 9.20	ex-natded9.20-2 27829
[Clemente] p. 45	Theorem 9.26	ex-natded9.26-2 27831  ex-natded9.26 27830
[Cohen] p. 301	Remark	relogoprlem 24743
[Cohen] p. 301	Property 2	relogmul 24744  relogmuld 24777
[Cohen] p. 301	Property 3	relogdiv 24745  relogdivd 24778
[Cohen] p. 301	Property 4	relogexp 24748
[Cohen] p. 301	Property 1a	log1 24738
[Cohen] p. 301	Property 1b	loge 24739
[Cohen4] p. 348	Observation	relogbcxpb 24934
[Cohen4] p. 349	Property	relogbf 24938
[Cohen4] p. 352	Definition	elogb 24917
[Cohen4] p. 361	Property 2	relogbmul 24924
[Cohen4] p. 361	Property 3	logbrec 24929  relogbdiv 24926
[Cohen4] p. 361	Property 4	relogbreexp 24922
[Cohen4] p. 361	Property 6	relogbexp 24927
[Cohen4] p. 361	Property 1(a)	logbid1 24915
[Cohen4] p. 361	Property 1(b)	logb1 24916
[Cohen4] p. 367	Property	logbchbase 24918
[Cohen4] p. 377	Property 2	logblt 24931
[Cohn] p. 4	Proposition 1.1.5	sxbrsigalem1 30888  sxbrsigalem4 30890
[Cohn] p. 81	Section II.5	acsdomd 17541  acsinfd 17540  acsinfdimd 17542  acsmap2d 17539  acsmapd 17538
[Cohn] p. 143	Example 5.1.1	sxbrsiga 30893
[Connell] p. 57	Definition	df-scmat 20672  df-scmatalt 43049
[CormenLeisersonRivest] p. 33	Equation 2.4	fldiv2 12962
[Crawley] p. 1	Definition of poset	df-poset 17306
[Crawley] p. 107	Theorem 13.2	hlsupr 35456
[Crawley] p. 110	Theorem 13.3	arglem1N 36260  dalaw 35956
[Crawley] p. 111	Theorem 13.4	hlathil 38031
[Crawley] p. 111	Definition of set W	df-watsN 36060
[Crawley] p. 111	Definition of dilation	df-dilN 36176  df-ldil 36174  isldil 36180
[Crawley] p. 111	Definition of translation	df-ltrn 36175  df-trnN 36177  isltrn 36189  ltrnu 36191
[Crawley] p. 112	Lemma A	cdlema1N 35861  cdlema2N 35862  exatleN 35474
[Crawley] p. 112	Lemma B	1cvrat 35546  cdlemb 35864  cdlemb2 36111  cdlemb3 36676  idltrn 36220  l1cvat 35125  lhpat 36113  lhpat2 36115  lshpat 35126  ltrnel 36209  ltrnmw 36221
[Crawley] p. 112	Lemma C	cdlemc1 36261  cdlemc2 36262  ltrnnidn 36244  trlat 36239  trljat1 36236  trljat2 36237  trljat3 36238  trlne 36255  trlnidat 36243  trlnle 36256
[Crawley] p. 112	Definition of automorphism	df-pautN 36061
[Crawley] p. 113	Lemma C	cdlemc 36267  cdlemc3 36263  cdlemc4 36264
[Crawley] p. 113	Lemma D	cdlemd 36277  cdlemd1 36268  cdlemd2 36269  cdlemd3 36270  cdlemd4 36271  cdlemd5 36272  cdlemd6 36273  cdlemd7 36274  cdlemd8 36275  cdlemd9 36276  cdleme31sde 36455  cdleme31se 36452  cdleme31se2 36453  cdleme31snd 36456  cdleme32a 36511  cdleme32b 36512  cdleme32c 36513  cdleme32d 36514  cdleme32e 36515  cdleme32f 36516  cdleme32fva 36507  cdleme32fva1 36508  cdleme32fvcl 36510  cdleme32le 36517  cdleme48fv 36569  cdleme4gfv 36577  cdleme50eq 36611  cdleme50f 36612  cdleme50f1 36613  cdleme50f1o 36616  cdleme50laut 36617  cdleme50ldil 36618  cdleme50lebi 36610  cdleme50rn 36615  cdleme50rnlem 36614  cdlemeg49le 36581  cdlemeg49lebilem 36609
[Crawley] p. 113	Lemma E	cdleme 36630  cdleme00a 36279  cdleme01N 36291  cdleme02N 36292  cdleme0a 36281  cdleme0aa 36280  cdleme0b 36282  cdleme0c 36283  cdleme0cp 36284  cdleme0cq 36285  cdleme0dN 36286  cdleme0e 36287  cdleme0ex1N 36293  cdleme0ex2N 36294  cdleme0fN 36288  cdleme0gN 36289  cdleme0moN 36295  cdleme1 36297  cdleme10 36324  cdleme10tN 36328  cdleme11 36340  cdleme11a 36330  cdleme11c 36331  cdleme11dN 36332  cdleme11e 36333  cdleme11fN 36334  cdleme11g 36335  cdleme11h 36336  cdleme11j 36337  cdleme11k 36338  cdleme11l 36339  cdleme12 36341  cdleme13 36342  cdleme14 36343  cdleme15 36348  cdleme15a 36344  cdleme15b 36345  cdleme15c 36346  cdleme15d 36347  cdleme16 36355  cdleme16aN 36329  cdleme16b 36349  cdleme16c 36350  cdleme16d 36351  cdleme16e 36352  cdleme16f 36353  cdleme16g 36354  cdleme19a 36373  cdleme19b 36374  cdleme19c 36375  cdleme19d 36376  cdleme19e 36377  cdleme19f 36378  cdleme1b 36296  cdleme2 36298  cdleme20aN 36379  cdleme20bN 36380  cdleme20c 36381  cdleme20d 36382  cdleme20e 36383  cdleme20f 36384  cdleme20g 36385  cdleme20h 36386  cdleme20i 36387  cdleme20j 36388  cdleme20k 36389  cdleme20l 36392  cdleme20l1 36390  cdleme20l2 36391  cdleme20m 36393  cdleme20y 36372  cdleme20zN 36371  cdleme21 36407  cdleme21d 36400  cdleme21e 36401  cdleme22a 36410  cdleme22aa 36409  cdleme22b 36411  cdleme22cN 36412  cdleme22d 36413  cdleme22e 36414  cdleme22eALTN 36415  cdleme22f 36416  cdleme22f2 36417  cdleme22g 36418  cdleme23a 36419  cdleme23b 36420  cdleme23c 36421  cdleme26e 36429  cdleme26eALTN 36431  cdleme26ee 36430  cdleme26f 36433  cdleme26f2 36435  cdleme26f2ALTN 36434  cdleme26fALTN 36432  cdleme27N 36439  cdleme27a 36437  cdleme27cl 36436  cdleme28c 36442  cdleme3 36307  cdleme30a 36448  cdleme31fv 36460  cdleme31fv1 36461  cdleme31fv1s 36462  cdleme31fv2 36463  cdleme31id 36464  cdleme31sc 36454  cdleme31sdnN 36457  cdleme31sn 36450  cdleme31sn1 36451  cdleme31sn1c 36458  cdleme31sn2 36459  cdleme31so 36449  cdleme35a 36518  cdleme35b 36520  cdleme35c 36521  cdleme35d 36522  cdleme35e 36523  cdleme35f 36524  cdleme35fnpq 36519  cdleme35g 36525  cdleme35h 36526  cdleme35h2 36527  cdleme35sn2aw 36528  cdleme35sn3a 36529  cdleme36a 36530  cdleme36m 36531  cdleme37m 36532  cdleme38m 36533  cdleme38n 36534  cdleme39a 36535  cdleme39n 36536  cdleme3b 36299  cdleme3c 36300  cdleme3d 36301  cdleme3e 36302  cdleme3fN 36303  cdleme3fa 36306  cdleme3g 36304  cdleme3h 36305  cdleme4 36308  cdleme40m 36537  cdleme40n 36538  cdleme40v 36539  cdleme40w 36540  cdleme41fva11 36547  cdleme41sn3aw 36544  cdleme41sn4aw 36545  cdleme41snaw 36546  cdleme42a 36541  cdleme42b 36548  cdleme42c 36542  cdleme42d 36543  cdleme42e 36549  cdleme42f 36550  cdleme42g 36551  cdleme42h 36552  cdleme42i 36553  cdleme42k 36554  cdleme42ke 36555  cdleme42keg 36556  cdleme42mN 36557  cdleme42mgN 36558  cdleme43aN 36559  cdleme43bN 36560  cdleme43cN 36561  cdleme43dN 36562  cdleme5 36310  cdleme50ex 36629  cdleme50ltrn 36627  cdleme51finvN 36626  cdleme51finvfvN 36625  cdleme51finvtrN 36628  cdleme6 36311  cdleme7 36319  cdleme7a 36313  cdleme7aa 36312  cdleme7b 36314  cdleme7c 36315  cdleme7d 36316  cdleme7e 36317  cdleme7ga 36318  cdleme8 36320  cdleme8tN 36325  cdleme9 36323  cdleme9a 36321  cdleme9b 36322  cdleme9tN 36327  cdleme9taN 36326  cdlemeda 36368  cdlemedb 36367  cdlemednpq 36369  cdlemednuN 36370  cdlemefr27cl 36473  cdlemefr32fva1 36480  cdlemefr32fvaN 36479  cdlemefrs32fva 36470  cdlemefrs32fva1 36471  cdlemefs27cl 36483  cdlemefs32fva1 36493  cdlemefs32fvaN 36492  cdlemesner 36366  cdlemeulpq 36290
[Crawley] p. 114	Lemma E	4atex 36146  4atexlem7 36145  cdleme0nex 36360  cdleme17a 36356  cdleme17c 36358  cdleme17d 36568  cdleme17d1 36359  cdleme17d2 36565  cdleme18a 36361  cdleme18b 36362  cdleme18c 36363  cdleme18d 36365  cdleme4a 36309
[Crawley] p. 115	Lemma E	cdleme21a 36395  cdleme21at 36398  cdleme21b 36396  cdleme21c 36397  cdleme21ct 36399  cdleme21f 36402  cdleme21g 36403  cdleme21h 36404  cdleme21i 36405  cdleme22gb 36364
[Crawley] p. 116	Lemma F	cdlemf 36633  cdlemf1 36631  cdlemf2 36632
[Crawley] p. 116	Lemma G	cdlemftr1 36637  cdlemg16 36727  cdlemg28 36774  cdlemg28a 36763  cdlemg28b 36773  cdlemg3a 36667  cdlemg42 36799  cdlemg43 36800  cdlemg44 36803  cdlemg44a 36801  cdlemg46 36805  cdlemg47 36806  cdlemg9 36704  ltrnco 36789  ltrncom 36808  tgrpabl 36821  trlco 36797
[Crawley] p. 116	Definition of G	df-tgrp 36813
[Crawley] p. 117	Lemma G	cdlemg17 36747  cdlemg17b 36732
[Crawley] p. 117	Definition of E	df-edring-rN 36826  df-edring 36827
[Crawley] p. 117	Definition of trace-preserving endomorphism	istendo 36830
[Crawley] p. 118	Remark	tendopltp 36850
[Crawley] p. 118	Lemma H	cdlemh 36887  cdlemh1 36885  cdlemh2 36886
[Crawley] p. 118	Lemma I	cdlemi 36890  cdlemi1 36888  cdlemi2 36889
[Crawley] p. 118	Lemma J	cdlemj1 36891  cdlemj2 36892  cdlemj3 36893  tendocan 36894
[Crawley] p. 118	Lemma K	cdlemk 37044  cdlemk1 36901  cdlemk10 36913  cdlemk11 36919  cdlemk11t 37016  cdlemk11ta 36999  cdlemk11tb 37001  cdlemk11tc 37015  cdlemk11u-2N 36959  cdlemk11u 36941  cdlemk12 36920  cdlemk12u-2N 36960  cdlemk12u 36942  cdlemk13-2N 36946  cdlemk13 36922  cdlemk14-2N 36948  cdlemk14 36924  cdlemk15-2N 36949  cdlemk15 36925  cdlemk16-2N 36950  cdlemk16 36927  cdlemk16a 36926  cdlemk17-2N 36951  cdlemk17 36928  cdlemk18-2N 36956  cdlemk18-3N 36970  cdlemk18 36938  cdlemk19-2N 36957  cdlemk19 36939  cdlemk19u 37040  cdlemk1u 36929  cdlemk2 36902  cdlemk20-2N 36962  cdlemk20 36944  cdlemk21-2N 36961  cdlemk21N 36943  cdlemk22-3 36971  cdlemk22 36963  cdlemk23-3 36972  cdlemk24-3 36973  cdlemk25-3 36974  cdlemk26-3 36976  cdlemk26b-3 36975  cdlemk27-3 36977  cdlemk28-3 36978  cdlemk29-3 36981  cdlemk3 36903  cdlemk30 36964  cdlemk31 36966  cdlemk32 36967  cdlemk33N 36979  cdlemk34 36980  cdlemk35 36982  cdlemk36 36983  cdlemk37 36984  cdlemk38 36985  cdlemk39 36986  cdlemk39u 37038  cdlemk4 36904  cdlemk41 36990  cdlemk42 37011  cdlemk42yN 37014  cdlemk43N 37033  cdlemk45 37017  cdlemk46 37018  cdlemk47 37019  cdlemk48 37020  cdlemk49 37021  cdlemk5 36906  cdlemk50 37022  cdlemk51 37023  cdlemk52 37024  cdlemk53 37027  cdlemk54 37028  cdlemk55 37031  cdlemk55u 37036  cdlemk56 37041  cdlemk5a 36905  cdlemk5auN 36930  cdlemk5u 36931  cdlemk6 36907  cdlemk6u 36932  cdlemk7 36918  cdlemk7u-2N 36958  cdlemk7u 36940  cdlemk8 36908  cdlemk9 36909  cdlemk9bN 36910  cdlemki 36911  cdlemkid 37006  cdlemkj-2N 36952  cdlemkj 36933  cdlemksat 36916  cdlemksel 36915  cdlemksv 36914  cdlemksv2 36917  cdlemkuat 36936  cdlemkuel-2N 36954  cdlemkuel-3 36968  cdlemkuel 36935  cdlemkuv-2N 36953  cdlemkuv2-2 36955  cdlemkuv2-3N 36969  cdlemkuv2 36937  cdlemkuvN 36934  cdlemkvcl 36912  cdlemky 36996  cdlemkyyN 37032  tendoex 37045
[Crawley] p. 120	Remark	dva1dim 37055
[Crawley] p. 120	Lemma L	cdleml1N 37046  cdleml2N 37047  cdleml3N 37048  cdleml4N 37049  cdleml5N 37050  cdleml6 37051  cdleml7 37052  cdleml8 37053  cdleml9 37054  dia1dim 37131
[Crawley] p. 120	Lemma M	dia11N 37118  diaf11N 37119  dialss 37116  diaord 37117  dibf11N 37231  djajN 37207
[Crawley] p. 120	Definition of isomorphism map	diaval 37102
[Crawley] p. 121	Lemma M	cdlemm10N 37188  dia2dimlem1 37134  dia2dimlem2 37135  dia2dimlem3 37136  dia2dimlem4 37137  dia2dimlem5 37138  diaf1oN 37200  diarnN 37199  dvheveccl 37182  dvhopN 37186
[Crawley] p. 121	Lemma N	cdlemn 37282  cdlemn10 37276  cdlemn11 37281  cdlemn11a 37277  cdlemn11b 37278  cdlemn11c 37279  cdlemn11pre 37280  cdlemn2 37265  cdlemn2a 37266  cdlemn3 37267  cdlemn4 37268  cdlemn4a 37269  cdlemn5 37271  cdlemn5pre 37270  cdlemn6 37272  cdlemn7 37273  cdlemn8 37274  cdlemn9 37275  diclspsn 37264
[Crawley] p. 121	Definition of phi(q)	df-dic 37243
[Crawley] p. 122	Lemma N	dih11 37335  dihf11 37337  dihjust 37287  dihjustlem 37286  dihord 37334  dihord1 37288  dihord10 37293  dihord11b 37292  dihord11c 37294  dihord2 37297  dihord2a 37289  dihord2b 37290  dihord2cN 37291  dihord2pre 37295  dihord2pre2 37296  dihordlem6 37283  dihordlem7 37284  dihordlem7b 37285
[Crawley] p. 122	Definition of isomorphism map	dihffval 37300  dihfval 37301  dihval 37302
[Diestel] p. 3	Section 1.1	df-cusgr 26717  df-nbgr 26637
[Diestel] p. 4	Section 1.1	df-subgr 26572  uhgrspan1 26607  uhgrspansubgr 26595
[Diestel] p. 5	Proposition 1.2.1	fusgrvtxdgonume 26859  vtxdgoddnumeven 26858
[Diestel] p. 27	Section 1.10	df-ushgr 26364
[Eisenberg] p. 67	Definition 5.3	df-dif 3801
[Eisenberg] p. 82	Definition 6.3	dfom3 8828
[Eisenberg] p. 125	Definition 8.21	df-map 8129
[Eisenberg] p. 216	Example 13.2(4)	omenps 8836
[Eisenberg] p. 310	Theorem 19.8	cardprc 9126
[Eisenberg] p. 310	Corollary 19.7(2)	cardsdom 9699
[Enderton] p. 18	Axiom of Empty Set	axnul 5014
[Enderton] p. 19	Definition	df-tp 4404
[Enderton] p. 26	Exercise 5	unissb 4693
[Enderton] p. 26	Exercise 10	pwel 5143
[Enderton] p. 28	Exercise 7(b)	pwun 5250
[Enderton] p. 30	Theorem "Distributive laws"	iinin1 4813  iinin2 4812  iinun2 4808  iunin1 4807  iunin1f 29918  iunin2 4806  uniin1 29911  uniin2 29912
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 4811  iundif2 4809
[Enderton] p. 32	Exercise 20	unineq 4109
[Enderton] p. 33	Exercise 23	iinuni 4832
[Enderton] p. 33	Exercise 25	iununi 4833
[Enderton] p. 33	Exercise 24(a)	iinpw 4840
[Enderton] p. 33	Exercise 24(b)	iunpw 7244  iunpwss 4841
[Enderton] p. 36	Definition	opthwiener 5202
[Enderton] p. 38	Exercise 6(a)	unipw 5141
[Enderton] p. 38	Exercise 6(b)	pwuni 4698
[Enderton] p. 41	Lemma 3D	opeluu 5161  rnex 7367  rnexg 7364
[Enderton] p. 41	Exercise 8	dmuni 5570  rnuni 5789
[Enderton] p. 42	Definition of a function	dffun7 6154  dffun8 6155
[Enderton] p. 43	Definition of function value	funfv2 6517
[Enderton] p. 43	Definition of single-rooted	funcnv 6195
[Enderton] p. 44	Definition (d)	dfima2 5713  dfima3 5714
[Enderton] p. 47	Theorem 3H	fvco2 6524
[Enderton] p. 49	Axiom of Choice (first form)	ac7 9617  ac7g 9618  df-ac 9259  dfac2 9274  dfac2a 9272  dfac2b 9273  dfac3 9264  dfac7 9276
[Enderton] p. 50	Theorem 3K(a)	imauni 6764
[Enderton] p. 52	Definition	df-map 8129
[Enderton] p. 53	Exercise 21	coass 5899
[Enderton] p. 53	Exercise 27	dmco 5888
[Enderton] p. 53	Exercise 14(a)	funin 6202
[Enderton] p. 53	Exercise 22(a)	imass2 5746
[Enderton] p. 54	Remark	ixpf 8203  ixpssmap 8215
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 8182
[Enderton] p. 55	Axiom of Choice (second form)	ac9 9627  ac9s 9637
[Enderton] p. 56	Theorem 3M	eqvrelref 34895  erref 8034
[Enderton] p. 57	Lemma 3N	eqvrelthi 34898  erthi 8063
[Enderton] p. 57	Definition	df-ec 8016
[Enderton] p. 58	Definition	df-qs 8020
[Enderton] p. 61	Exercise 35	df-ec 8016
[Enderton] p. 65	Exercise 56(a)	dmun 5567
[Enderton] p. 68	Definition of successor	df-suc 5973
[Enderton] p. 71	Definition	df-tr 4978  dftr4 4982
[Enderton] p. 72	Theorem 4E	unisuc 6043
[Enderton] p. 73	Exercise 6	unisuc 6043
[Enderton] p. 73	Exercise 5(a)	truni 4991
[Enderton] p. 73	Exercise 5(b)	trint 4993  trintALT 39930
[Enderton] p. 79	Theorem 4I(A1)	nna0 7956
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 7958  onasuc 7880
[Enderton] p. 79	Definition of operation value	df-ov 6913
[Enderton] p. 80	Theorem 4J(A1)	nnm0 7957
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 7959  onmsuc 7881
[Enderton] p. 81	Theorem 4K(1)	nnaass 7974
[Enderton] p. 81	Theorem 4K(2)	nna0r 7961  nnacom 7969
[Enderton] p. 81	Theorem 4K(3)	nndi 7975
[Enderton] p. 81	Theorem 4K(4)	nnmass 7976
[Enderton] p. 81	Theorem 4K(5)	nnmcom 7978
[Enderton] p. 82	Exercise 16	nnm0r 7962  nnmsucr 7977
[Enderton] p. 88	Exercise 23	nnaordex 7990
[Enderton] p. 129	Definition	df-en 8229
[Enderton] p. 132	Theorem 6B(b)	canth 6868
[Enderton] p. 133	Exercise 1	xpomen 9158
[Enderton] p. 133	Exercise 2	qnnen 15323
[Enderton] p. 134	Theorem (Pigeonhole Principle)	php 8419
[Enderton] p. 135	Corollary 6C	php3 8421
[Enderton] p. 136	Corollary 6E	nneneq 8418
[Enderton] p. 136	Corollary 6D(a)	pssinf 8445
[Enderton] p. 136	Corollary 6D(b)	ominf 8447
[Enderton] p. 137	Lemma 6F	pssnn 8453
[Enderton] p. 138	Corollary 6G	ssfi 8455
[Enderton] p. 139	Theorem 6H(c)	mapen 8399
[Enderton] p. 142	Theorem 6I(3)	xpcdaen 9327
[Enderton] p. 142	Theorem 6I(4)	mapcdaen 9328
[Enderton] p. 143	Theorem 6J	cda0en 9323  cda1en 9319
[Enderton] p. 144	Exercise 13	iunfi 8529  unifi 8530  unifi2 8531
[Enderton] p. 144	Corollary 6K	undif2 4269  unfi 8502  unfi2 8504
[Enderton] p. 145	Figure 38	ffoss 7394
[Enderton] p. 145	Definition	df-dom 8230
[Enderton] p. 146	Example 1	domen 8241  domeng 8242
[Enderton] p. 146	Example 3	nndomo 8429  nnsdom 8835  nnsdomg 8494
[Enderton] p. 149	Theorem 6L(a)	cdadom2 9331
[Enderton] p. 149	Theorem 6L(c)	mapdom1 8400  xpdom1 8334  xpdom1g 8332  xpdom2g 8331
[Enderton] p. 149	Theorem 6L(d)	mapdom2 8406
[Enderton] p. 151	Theorem 6M	zorn 9651  zorng 9648
[Enderton] p. 151	Theorem 6M(4)	ac8 9636  dfac5 9271
[Enderton] p. 159	Theorem 6Q	unictb 9719
[Enderton] p. 164	Example	infdif 9353
[Enderton] p. 168	Definition	df-po 5265
[Enderton] p. 192	Theorem 7M(a)	oneli 6074
[Enderton] p. 192	Theorem 7M(b)	ontr1 6013
[Enderton] p. 192	Theorem 7M(c)	onirri 6073
[Enderton] p. 193	Corollary 7N(b)	0elon 6020
[Enderton] p. 193	Corollary 7N(c)	onsuci 7304
[Enderton] p. 193	Corollary 7N(d)	ssonunii 7253
[Enderton] p. 194	Remark	onprc 7250
[Enderton] p. 194	Exercise 16	suc11 6070
[Enderton] p. 197	Definition	df-card 9085
[Enderton] p. 197	Theorem 7P	carden 9695
[Enderton] p. 200	Exercise 25	tfis 7320
[Enderton] p. 202	Lemma 7T	r1tr 8923
[Enderton] p. 202	Definition	df-r1 8911
[Enderton] p. 202	Theorem 7Q	r1val1 8933
[Enderton] p. 204	Theorem 7V(b)	rankval4 9014
[Enderton] p. 206	Theorem 7X(b)	en2lp 8786
[Enderton] p. 207	Exercise 30	rankpr 9004  rankprb 8998  rankpw 8990  rankpwi 8970  rankuniss 9013
[Enderton] p. 207	Exercise 34	opthreg 8797
[Enderton] p. 208	Exercise 35	suc11reg 8800
[Enderton] p. 212	Definition of aleph	alephval3 9253
[Enderton] p. 213	Theorem 8A(a)	alephord2 9219
[Enderton] p. 213	Theorem 8A(b)	cardalephex 9233
[Enderton] p. 218	Theorem Schema 8E	onfununi 7709
[Enderton] p. 222	Definition of kard	karden 9042  kardex 9041
[Enderton] p. 238	Theorem 8R	oeoa 7949
[Enderton] p. 238	Theorem 8S	oeoe 7951
[Enderton] p. 240	Exercise 25	oarec 7914
[Enderton] p. 257	Definition of cofinality	cflm 9394
[FaureFrolicher] p. 57	Definition 3.1.9	mreexd 16662
[FaureFrolicher] p. 83	Definition 4.1.1	df-mri 16608
[FaureFrolicher] p. 83	Proposition 4.1.3	acsfiindd 17537  mrieqv2d 16659  mrieqvd 16658
[FaureFrolicher] p. 84	Lemma 4.1.5	mreexmrid 16663
[FaureFrolicher] p. 86	Proposition 4.2.1	mreexexd 16668  mreexexlem2d 16665
[FaureFrolicher] p. 87	Theorem 4.2.2	acsexdimd 17543  mreexfidimd 16670
[Frege1879] p. 11	Statement	df3or2 38896
[Frege1879] p. 12	Statement	df3an2 38897  dfxor4 38894  dfxor5 38895
[Frege1879] p. 26	Axiom 1	ax-frege1 38919
[Frege1879] p. 26	Axiom 2	ax-frege2 38920
[Frege1879] p. 26	Proposition 1	ax-1 6
[Frege1879] p. 26	Proposition 2	ax-2 7
[Frege1879] p. 29	Proposition 3	frege3 38924
[Frege1879] p. 31	Proposition 4	frege4 38928
[Frege1879] p. 32	Proposition 5	frege5 38929
[Frege1879] p. 33	Proposition 6	frege6 38935
[Frege1879] p. 34	Proposition 7	frege7 38937
[Frege1879] p. 35	Axiom 8	ax-frege8 38938  axfrege8 38936
[Frege1879] p. 35	Proposition 8	pm2.04 90  wl-luk-pm2.04 33809
[Frege1879] p. 35	Proposition 9	frege9 38941
[Frege1879] p. 36	Proposition 10	frege10 38949
[Frege1879] p. 36	Proposition 11	frege11 38943
[Frege1879] p. 37	Proposition 12	frege12 38942
[Frege1879] p. 37	Proposition 13	frege13 38951
[Frege1879] p. 37	Proposition 14	frege14 38952
[Frege1879] p. 38	Proposition 15	frege15 38955
[Frege1879] p. 38	Proposition 16	frege16 38945
[Frege1879] p. 39	Proposition 17	frege17 38950
[Frege1879] p. 39	Proposition 18	frege18 38947
[Frege1879] p. 39	Proposition 19	frege19 38953
[Frege1879] p. 40	Proposition 20	frege20 38957
[Frege1879] p. 40	Proposition 21	frege21 38956
[Frege1879] p. 41	Proposition 22	frege22 38948
[Frege1879] p. 42	Proposition 23	frege23 38954
[Frege1879] p. 42	Proposition 24	frege24 38944
[Frege1879] p. 42	Proposition 25	frege25 38946  rp-frege25 38934
[Frege1879] p. 42	Proposition 26	frege26 38939
[Frege1879] p. 43	Axiom 28	ax-frege28 38959
[Frege1879] p. 43	Proposition 27	frege27 38940
[Frege1879] p. 43	Proposition 28	con3 151
[Frege1879] p. 43	Proposition 29	frege29 38960
[Frege1879] p. 44	Axiom 31	ax-frege31 38963  axfrege31 38962
[Frege1879] p. 44	Proposition 30	frege30 38961
[Frege1879] p. 44	Proposition 31	notnotr 128
[Frege1879] p. 44	Proposition 32	frege32 38964
[Frege1879] p. 44	Proposition 33	frege33 38965
[Frege1879] p. 45	Proposition 34	frege34 38966
[Frege1879] p. 45	Proposition 35	frege35 38967
[Frege1879] p. 45	Proposition 36	frege36 38968
[Frege1879] p. 46	Proposition 37	frege37 38969
[Frege1879] p. 46	Proposition 38	frege38 38970
[Frege1879] p. 46	Proposition 39	frege39 38971
[Frege1879] p. 46	Proposition 40	frege40 38972
[Frege1879] p. 47	Axiom 41	ax-frege41 38974  axfrege41 38973
[Frege1879] p. 47	Proposition 41	notnot 139
[Frege1879] p. 47	Proposition 42	frege42 38975
[Frege1879] p. 47	Proposition 43	frege43 38976
[Frege1879] p. 47	Proposition 44	frege44 38977
[Frege1879] p. 47	Proposition 45	frege45 38978
[Frege1879] p. 48	Proposition 46	frege46 38979
[Frege1879] p. 48	Proposition 47	frege47 38980
[Frege1879] p. 49	Proposition 48	frege48 38981
[Frege1879] p. 49	Proposition 49	frege49 38982
[Frege1879] p. 49	Proposition 50	frege50 38983
[Frege1879] p. 50	Axiom 52	ax-frege52a 38986  ax-frege52c 39017  frege52aid 38987  frege52b 39018
[Frege1879] p. 50	Axiom 54	ax-frege54a 38991  ax-frege54c 39021  frege54b 39022
[Frege1879] p. 50	Proposition 51	frege51 38984
[Frege1879] p. 50	Proposition 52	dfsbcq 3664
[Frege1879] p. 50	Proposition 53	frege53a 38989  frege53aid 38988  frege53b 39019  frege53c 39043
[Frege1879] p. 50	Proposition 54	biid 253  eqid 2825
[Frege1879] p. 50	Proposition 55	frege55a 38997  frege55aid 38994  frege55b 39026  frege55c 39047  frege55cor1a 38998  frege55lem2a 38996  frege55lem2b 39025  frege55lem2c 39046
[Frege1879] p. 50	Proposition 56	frege56a 39000  frege56aid 38999  frege56b 39027  frege56c 39048
[Frege1879] p. 51	Axiom 58	ax-frege58a 39004  ax-frege58b 39030  frege58bid 39031  frege58c 39050
[Frege1879] p. 51	Proposition 57	frege57a 39002  frege57aid 39001  frege57b 39028  frege57c 39049
[Frege1879] p. 51	Proposition 58	spsbc 3675
[Frege1879] p. 51	Proposition 59	frege59a 39006  frege59b 39033  frege59c 39051
[Frege1879] p. 52	Proposition 60	frege60a 39007  frege60b 39034  frege60c 39052
[Frege1879] p. 52	Proposition 61	frege61a 39008  frege61b 39035  frege61c 39053
[Frege1879] p. 52	Proposition 62	frege62a 39009  frege62b 39036  frege62c 39054
[Frege1879] p. 52	Proposition 63	frege63a 39010  frege63b 39037  frege63c 39055
[Frege1879] p. 53	Proposition 64	frege64a 39011  frege64b 39038  frege64c 39056
[Frege1879] p. 53	Proposition 65	frege65a 39012  frege65b 39039  frege65c 39057
[Frege1879] p. 54	Proposition 66	frege66a 39013  frege66b 39040  frege66c 39058
[Frege1879] p. 54	Proposition 67	frege67a 39014  frege67b 39041  frege67c 39059
[Frege1879] p. 54	Proposition 68	frege68a 39015  frege68b 39042  frege68c 39060
[Frege1879] p. 55	Definition 69	dffrege69 39061
[Frege1879] p. 58	Proposition 70	frege70 39062
[Frege1879] p. 59	Proposition 71	frege71 39063
[Frege1879] p. 59	Proposition 72	frege72 39064
[Frege1879] p. 59	Proposition 73	frege73 39065
[Frege1879] p. 60	Definition 76	dffrege76 39068
[Frege1879] p. 60	Proposition 74	frege74 39066
[Frege1879] p. 60	Proposition 75	frege75 39067
[Frege1879] p. 62	Proposition 77	frege77 39069  frege77d 38874
[Frege1879] p. 63	Proposition 78	frege78 39070
[Frege1879] p. 63	Proposition 79	frege79 39071
[Frege1879] p. 63	Proposition 80	frege80 39072
[Frege1879] p. 63	Proposition 81	frege81 39073  frege81d 38875
[Frege1879] p. 64	Proposition 82	frege82 39074
[Frege1879] p. 65	Proposition 83	frege83 39075  frege83d 38876
[Frege1879] p. 65	Proposition 84	frege84 39076
[Frege1879] p. 66	Proposition 85	frege85 39077
[Frege1879] p. 66	Proposition 86	frege86 39078
[Frege1879] p. 66	Proposition 87	frege87 39079  frege87d 38878
[Frege1879] p. 67	Proposition 88	frege88 39080
[Frege1879] p. 68	Proposition 89	frege89 39081
[Frege1879] p. 68	Proposition 90	frege90 39082
[Frege1879] p. 68	Proposition 91	frege91 39083  frege91d 38879
[Frege1879] p. 69	Proposition 92	frege92 39084
[Frege1879] p. 70	Proposition 93	frege93 39085
[Frege1879] p. 70	Proposition 94	frege94 39086
[Frege1879] p. 70	Proposition 95	frege95 39087
[Frege1879] p. 71	Definition 99	dffrege99 39091
[Frege1879] p. 71	Proposition 96	frege96 39088  frege96d 38877
[Frege1879] p. 71	Proposition 97	frege97 39089  frege97d 38880
[Frege1879] p. 71	Proposition 98	frege98 39090  frege98d 38881
[Frege1879] p. 72	Proposition 100	frege100 39092
[Frege1879] p. 72	Proposition 101	frege101 39093
[Frege1879] p. 72	Proposition 102	frege102 39094  frege102d 38882
[Frege1879] p. 73	Proposition 103	frege103 39095
[Frege1879] p. 73	Proposition 104	frege104 39096
[Frege1879] p. 73	Proposition 105	frege105 39097
[Frege1879] p. 73	Proposition 106	frege106 39098  frege106d 38883
[Frege1879] p. 74	Proposition 107	frege107 39099
[Frege1879] p. 74	Proposition 108	frege108 39100  frege108d 38884
[Frege1879] p. 74	Proposition 109	frege109 39101  frege109d 38885
[Frege1879] p. 75	Proposition 110	frege110 39102
[Frege1879] p. 75	Proposition 111	frege111 39103  frege111d 38887
[Frege1879] p. 76	Proposition 112	frege112 39104
[Frege1879] p. 76	Proposition 113	frege113 39105
[Frege1879] p. 76	Proposition 114	frege114 39106  frege114d 38886
[Frege1879] p. 77	Definition 115	dffrege115 39107
[Frege1879] p. 77	Proposition 116	frege116 39108
[Frege1879] p. 78	Proposition 117	frege117 39109
[Frege1879] p. 78	Proposition 118	frege118 39110
[Frege1879] p. 78	Proposition 119	frege119 39111
[Frege1879] p. 78	Proposition 120	frege120 39112
[Frege1879] p. 79	Proposition 121	frege121 39113
[Frege1879] p. 79	Proposition 122	frege122 39114  frege122d 38888
[Frege1879] p. 79	Proposition 123	frege123 39115
[Frege1879] p. 80	Proposition 124	frege124 39116  frege124d 38889
[Frege1879] p. 81	Proposition 125	frege125 39117
[Frege1879] p. 81	Proposition 126	frege126 39118  frege126d 38890
[Frege1879] p. 82	Proposition 127	frege127 39119
[Frege1879] p. 83	Proposition 128	frege128 39120
[Frege1879] p. 83	Proposition 129	frege129 39121  frege129d 38891
[Frege1879] p. 84	Proposition 130	frege130 39122
[Frege1879] p. 85	Proposition 131	frege131 39123  frege131d 38892
[Frege1879] p. 86	Proposition 132	frege132 39124
[Frege1879] p. 86	Proposition 133	frege133 39125  frege133d 38893
[Fremlin1] p. 13	Definition 111G (b)	df-salgen 41318
[Fremlin1] p. 13	Definition 111G (d)	borelmbl 41638
[Fremlin1] p. 13	Proposition 111G (b)	salgenss 41339
[Fremlin1] p. 14	Definition 112A	ismea 41453
[Fremlin1] p. 15	Remark 112B (d)	psmeasure 41473
[Fremlin1] p. 15	Property 112C (a)	meadjun 41464  meadjunre 41478
[Fremlin1] p. 15	Property 112C (b)	meassle 41465
[Fremlin1] p. 15	Property 112C (c)	meaunle 41466
[Fremlin1] p. 16	Property 112C (d)	iundjiun 41462  meaiunle 41471  meaiunlelem 41470
[Fremlin1] p. 16	Proposition 112C (e)	meaiuninc 41483  meaiuninc2 41484  meaiuninc3 41487  meaiuninc3v 41486  meaiunincf 41485  meaiuninclem 41482
[Fremlin1] p. 16	Proposition 112C (f)	meaiininc 41489  meaiininc2 41490  meaiininclem 41488
[Fremlin1] p. 19	Theorem 113C	caragen0 41508  caragendifcl 41516  caratheodory 41530  omelesplit 41520
[Fremlin1] p. 19	Definition 113A	isome 41496  isomennd 41533  isomenndlem 41532
[Fremlin1] p. 19	Remark 113B (c)	omeunle 41518
[Fremlin1] p. 19	Definition 112Df	caragencmpl 41537  voncmpl 41623
[Fremlin1] p. 19	Definition 113A (ii)	omessle 41500
[Fremlin1] p. 20	Theorem 113C	carageniuncl 41525  carageniuncllem1 41523  carageniuncllem2 41524  caragenuncl 41515  caragenuncllem 41514  caragenunicl 41526
[Fremlin1] p. 21	Remark 113D	caragenel2d 41534
[Fremlin1] p. 21	Theorem 113C	caratheodorylem1 41528  caratheodorylem2 41529
[Fremlin1] p. 21	Exercise 113Xa	caragencmpl 41537
[Fremlin1] p. 23	Lemma 114B	hoidmv1le 41596  hoidmv1lelem1 41593  hoidmv1lelem2 41594  hoidmv1lelem3 41595
[Fremlin1] p. 25	Definition 114E	isvonmbl 41640
[Fremlin1] p. 29	Lemma 115B	hoidmv1le 41596  hoidmvle 41602  hoidmvlelem1 41597  hoidmvlelem2 41598  hoidmvlelem3 41599  hoidmvlelem4 41600  hoidmvlelem5 41601  hsphoidmvle2 41587  hsphoif 41578  hsphoival 41581
[Fremlin1] p. 29	Definition 1135 (b)	hoicvr 41550
[Fremlin1] p. 29	Definition 115A (b)	hoicvrrex 41558
[Fremlin1] p. 29	Definition 115A (c)	hoidmv0val 41585  hoidmvn0val 41586  hoidmvval 41579  hoidmvval0 41589  hoidmvval0b 41592
[Fremlin1] p. 30	Lemma 115B	hoiprodp1 41590  hsphoidmvle 41588
[Fremlin1] p. 30	Definition 115C	df-ovoln 41539  df-voln 41541
[Fremlin1] p. 30	Proposition 115D (a)	dmovn 41606  ovn0 41568  ovn0lem 41567  ovnf 41565  ovnome 41575  ovnssle 41563  ovnsslelem 41562  ovnsupge0 41559
[Fremlin1] p. 30	Proposition 115D (b)	ovnhoi 41605  ovnhoilem1 41603  ovnhoilem2 41604  vonhoi 41669
[Fremlin1] p. 31	Lemma 115F	hoidifhspdmvle 41622  hoidifhspf 41620  hoidifhspval 41610  hoidifhspval2 41617  hoidifhspval3 41621  hspmbl 41631  hspmbllem1 41628  hspmbllem2 41629  hspmbllem3 41630
[Fremlin1] p. 31	Definition 115E	voncmpl 41623  vonmea 41576
[Fremlin1] p. 31	Proposition 115D (a)(iv)	ovnsubadd 41574  ovnsubadd2 41648  ovnsubadd2lem 41647  ovnsubaddlem1 41572  ovnsubaddlem2 41573
[Fremlin1] p. 32	Proposition 115G (a)	hoimbl 41633  hoimbl2 41667  hoimbllem 41632  hspdifhsp 41618  opnvonmbl 41636  opnvonmbllem2 41635
[Fremlin1] p. 32	Proposition 115G (b)	borelmbl 41638
[Fremlin1] p. 32	Proposition 115G (c)	iccvonmbl 41681  iccvonmbllem 41680  ioovonmbl 41679
[Fremlin1] p. 32	Proposition 115G (d)	vonicc 41687  vonicclem2 41686  vonioo 41684  vonioolem2 41683  vonn0icc 41690  vonn0icc2 41694  vonn0ioo 41689  vonn0ioo2 41692
[Fremlin1] p. 32	Proposition 115G (e)	ctvonmbl 41691  snvonmbl 41688  vonct 41695  vonsn 41693
[Fremlin1] p. 35	Lemma 121A	subsalsal 41362
[Fremlin1] p. 35	Lemma 121A (iii)	subsaliuncl 41361  subsaliuncllem 41360
[Fremlin1] p. 35	Proposition 121B	salpreimagtge 41722  salpreimalegt 41708  salpreimaltle 41723
[Fremlin1] p. 35	Proposition 121B (i)	issmf 41725  issmff 41731  issmflem 41724
[Fremlin1] p. 35	Proposition 121B (ii)	issmfle 41742  issmflelem 41741  smfpreimale 41751
[Fremlin1] p. 35	Proposition 121B (iii)	issmfgt 41753  issmfgtlem 41752
[Fremlin1] p. 36	Definition 121C	df-smblfn 41698  issmf 41725  issmff 41731  issmfge 41766  issmfgelem 41765  issmfgt 41753  issmfgtlem 41752  issmfle 41742  issmflelem 41741  issmflem 41724
[Fremlin1] p. 36	Proposition 121B	salpreimagelt 41706  salpreimagtlt 41727  salpreimalelt 41726
[Fremlin1] p. 36	Proposition 121B (iv)	issmfge 41766  issmfgelem 41765
[Fremlin1] p. 36	Proposition 121D (a)	bormflebmf 41750
[Fremlin1] p. 36	Proposition 121D (b)	cnfrrnsmf 41748  cnfsmf 41737
[Fremlin1] p. 36	Proposition 121D (c)	decsmf 41763  decsmflem 41762  incsmf 41739  incsmflem 41738
[Fremlin1] p. 37	Proposition 121E (a)	pimconstlt0 41702  pimconstlt1 41703  smfconst 41746
[Fremlin1] p. 37	Proposition 121E (b)	smfadd 41761  smfaddlem1 41759  smfaddlem2 41760
[Fremlin1] p. 37	Proposition 121E (c)	smfmulc1 41791
[Fremlin1] p. 37	Proposition 121E (d)	smfmul 41790  smfmullem1 41786  smfmullem2 41787  smfmullem3 41788  smfmullem4 41789
[Fremlin1] p. 37	Proposition 121E (e)	smfdiv 41792
[Fremlin1] p. 37	Proposition 121E (f)	smfpimbor1 41795  smfpimbor1lem2 41794
[Fremlin1] p. 37	Proposition 121E (g)	smfco 41797
[Fremlin1] p. 37	Proposition 121E (h)	smfres 41785
[Fremlin1] p. 38	Proposition 121E (e)	smfrec 41784
[Fremlin1] p. 38	Proposition 121E (f)	smfpimbor1lem1 41793  smfresal 41783
[Fremlin1] p. 38	Proposition 121F (a)	smflim 41773  smflim2 41800  smflimlem1 41767  smflimlem2 41768  smflimlem3 41769  smflimlem4 41770  smflimlem5 41771  smflimlem6 41772  smflimmpt 41804
[Fremlin1] p. 38	Proposition 121F (b)	smfsup 41808  smfsuplem1 41805  smfsuplem2 41806  smfsuplem3 41807  smfsupmpt 41809  smfsupxr 41810
[Fremlin1] p. 38	Proposition 121F (c)	smfinf 41812  smfinflem 41811  smfinfmpt 41813
[Fremlin1] p. 39	Remark 121G	smflim 41773  smflim2 41800  smflimmpt 41804
[Fremlin1] p. 39	Proposition 121F	smfpimcc 41802
[Fremlin1] p. 39	Proposition 121F (d)	smflimsup 41822  smflimsuplem2 41815  smflimsuplem6 41819  smflimsuplem7 41820  smflimsuplem8 41821  smflimsupmpt 41823
[Fremlin1] p. 39	Proposition 121F (e)	smfliminf 41825  smfliminflem 41824  smfliminfmpt 41826
[Fremlin1] p. 80	Definition 135E (b)	df-smblfn 41698
[Fremlin5] p. 193	Proposition 563Gb	nulmbl2 23709
[Fremlin5] p. 213	Lemma 565Ca	uniioovol 23752
[Fremlin5] p. 214	Lemma 565Ca	uniioombl 23762
[Fremlin5] p. 218	Lemma 565Ib	ftc1anclem6 34028
[Fremlin5] p. 220	Theorem 565Ma	ftc1anc 34031
[FreydScedrov] p. 283	Axiom of Infinity	ax-inf 8819  inf1 8803  inf2 8804
[Gleason] p. 117	Proposition 9-2.1	df-enq 10055  enqer 10065
[Gleason] p. 117	Proposition 9-2.2	df-1nq 10060  df-nq 10056
[Gleason] p. 117	Proposition 9-2.3	df-plpq 10052  df-plq 10058
[Gleason] p. 119	Proposition 9-2.4	caovmo 7136  df-mpq 10053  df-mq 10059
[Gleason] p. 119	Proposition 9-2.5	df-rq 10061
[Gleason] p. 119	Proposition 9-2.6	ltexnq 10119
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 10120  ltbtwnnq 10122
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanq 10115
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnq 10116
[Gleason] p. 120	Proposition 9-2.6(iv)	ltrnq 10123
[Gleason] p. 121	Definition 9-3.1	df-np 10125
[Gleason] p. 121	Definition 9-3.1 (ii)	prcdnq 10137
[Gleason] p. 121	Definition 9-3.1(iii)	prnmax 10139
[Gleason] p. 122	Definition	df-1p 10126
[Gleason] p. 122	Remark (1)	prub 10138
[Gleason] p. 122	Lemma 9-3.4	prlem934 10177
[Gleason] p. 122	Proposition 9-3.2	df-ltp 10129
[Gleason] p. 122	Proposition 9-3.3	ltsopr 10176  psslinpr 10175  supexpr 10198  suplem1pr 10196  suplem2pr 10197
[Gleason] p. 123	Proposition 9-3.5	addclpr 10162  addclprlem1 10160  addclprlem2 10161  df-plp 10127
[Gleason] p. 123	Proposition 9-3.5(i)	addasspr 10166
[Gleason] p. 123	Proposition 9-3.5(ii)	addcompr 10165
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 10178
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 10187  ltexprlem1 10180  ltexprlem2 10181  ltexprlem3 10182  ltexprlem4 10183  ltexprlem5 10184  ltexprlem6 10185  ltexprlem7 10186
[Gleason] p. 123	Proposition 9-3.5(v)	ltapr 10189  ltaprlem 10188
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanpr 10190
[Gleason] p. 124	Lemma 9-3.6	prlem936 10191
[Gleason] p. 124	Proposition 9-3.7	df-mp 10128  mulclpr 10164  mulclprlem 10163  reclem2pr 10192
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 10173
[Gleason] p. 124	Proposition 9-3.7(i)	mulasspr 10168
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcompr 10167
[Gleason] p. 124	Proposition 9-3.7(iii)	distrpr 10172
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 10195  reclem3pr 10193  reclem4pr 10194
[Gleason] p. 126	Proposition 9-4.1	df-enr 10199  enrer 10207
[Gleason] p. 126	Proposition 9-4.2	df-0r 10204  df-1r 10205  df-nr 10200
[Gleason] p. 126	Proposition 9-4.3	df-mr 10202  df-plr 10201  negexsr 10246  recexsr 10251  recexsrlem 10247
[Gleason] p. 127	Proposition 9-4.4	df-ltr 10203
[Gleason] p. 130	Proposition 10-1.3	creui 11352  creur 11351  cru 11349
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 10332  axcnre 10308
[Gleason] p. 132	Definition 10-3.1	crim 14239  crimd 14356  crimi 14317  crre 14238  crred 14355  crrei 14316
[Gleason] p. 132	Definition 10-3.2	remim 14241  remimd 14322
[Gleason] p. 133	Definition 10.36	absval2 14408  absval2d 14568  absval2i 14520
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 14265  cjaddd 14344  cjaddi 14312
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 14266  cjmuld 14345  cjmuli 14313
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 14264  cjcjd 14323  cjcji 14295
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 14263  cjreb 14247  cjrebd 14326  cjrebi 14298  cjred 14350  rere 14246  rereb 14244  rerebd 14325  rerebi 14297  rered 14348
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 14272  addcjd 14336  addcji 14307
[Gleason] p. 133	Proposition 10-3.7(a)	absval 14362
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 14403  abscjd 14573  abscji 14524
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 14413  abs00d 14569  abs00i 14521  absne0d 14570
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 14445  releabsd 14574  releabsi 14525
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 14418  absmuld 14577  absmuli 14527
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 14406  sqabsaddi 14528
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 14454  abstrid 14579  abstrii 14531
[Gleason] p. 134	Definition 10-4.1	0exp0e1 13166  df-exp 13162  exp0 13165  expp1 13168  expp1d 13310
[Gleason] p. 135	Proposition 10-4.2(a)	cxpadd 24831  cxpaddd 24869  expadd 13203  expaddd 13311  expaddz 13205
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 24840  cxpmuld 24888  expmul 13206  expmuld 13312  expmulz 13207
[Gleason] p. 135	Proposition 10-4.2(c)	mulcxp 24837  mulcxpd 24880  mulexp 13200  mulexpd 13324  mulexpz 13201
[Gleason] p. 140	Exercise 1	znnen 15322
[Gleason] p. 141	Definition 11-2.1	fzval 12628
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 14746  rlimadd 14757  rlimdiv 14760
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 14748  rlimsub 14758
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 14747  rlimmul 14759
[Gleason] p. 171	Corollary 12-2.2	climmulc2 14751
[Gleason] p. 172	Corollary 12-2.5	climrecl 14698
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 14718  climcj 14719  climim 14721  climre 14720  rlimabs 14723  rlimcj 14724  rlimim 14726  rlimre 14725
[Gleason] p. 173	Definition 12-3.1	df-ltxr 10403  df-xr 10402  ltxr 12242
[Gleason] p. 175	Definition 12-4.1	df-limsup 14586  limsupval 14589
[Gleason] p. 180	Theorem 12-5.1	climsup 14784
[Gleason] p. 180	Theorem 12-5.3	caucvg 14793  caucvgb 14794  caucvgr 14790  climcau 14785
[Gleason] p. 182	Exercise 3	cvgcmp 14929
[Gleason] p. 182	Exercise 4	cvgrat 14995
[Gleason] p. 195	Theorem 13-2.12	abs1m 14459
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 12931
[Gleason] p. 223	Definition 14-1.1	df-met 20107
[Gleason] p. 223	Definition 14-1.1(a)	met0 22525  xmet0 22524
[Gleason] p. 223	Definition 14-1.1(b)	metgt0 22541
[Gleason] p. 223	Definition 14-1.1(c)	metsym 22532
[Gleason] p. 223	Definition 14-1.1(d)	mettri 22534  mstri 22651  xmettri 22533  xmstri 22650
[Gleason] p. 225	Definition 14-1.5	xpsmet 22564
[Gleason] p. 230	Proposition 14-2.6	txlm 21829
[Gleason] p. 240	Theorem 14-4.3	metcnp4 23485
[Gleason] p. 240	Proposition 14-4.2	metcnp3 22722
[Gleason] p. 243	Proposition 14-4.16	addcn 23045  addcn2 14708  mulcn 23047  mulcn2 14710  subcn 23046  subcn2 14709
[Gleason] p. 295	Remark	bcval3 13393  bcval4 13394
[Gleason] p. 295	Equation 2	bcpasc 13408
[Gleason] p. 295	Definition of binomial coefficient	bcval 13391  df-bc 13390
[Gleason] p. 296	Remark	bcn0 13397  bcnn 13399
[Gleason] p. 296	Theorem 15-2.8	binom 14943
[Gleason] p. 308	Equation 2	ef0 15200
[Gleason] p. 308	Equation 3	efcj 15201
[Gleason] p. 309	Corollary 15-4.3	efne0 15206
[Gleason] p. 309	Corollary 15-4.4	efexp 15210
[Gleason] p. 310	Equation 14	sinadd 15273
[Gleason] p. 310	Equation 15	cosadd 15274
[Gleason] p. 311	Equation 17	sincossq 15285
[Gleason] p. 311	Equation 18	cosbnd 15290  sinbnd 15289
[Gleason] p. 311	Lemma 15-4.7	sqeqor 13279  sqeqori 13277
[Gleason] p. 311	Definition of ` `	df-pi 15182
[Godowski] p. 730	Equation SF	goeqi 29683
[GodowskiGreechie] p. 249	Equation IV	3oai 29078
[Golan] p. 1	Remark	srgisid 18889
[Golan] p. 1	Definition	df-srg 18867
[Golan] p. 149	Definition	df-slmd 30295
[GramKnuthPat], p. 47	Definition 2.42	df-fwddif 32800
[Gratzer] p. 23	Section 0.6	df-mre 16606
[Gratzer] p. 27	Section 0.6	df-mri 16608
[Hall] p. 1	Section 1.1	df-asslaw 42685  df-cllaw 42683  df-comlaw 42684
[Hall] p. 2	Section 1.2	df-clintop 42697
[Hall] p. 7	Section 1.3	df-sgrp2 42718
[Halmos] p. 31	Theorem 17.3	riesz1 29475  riesz2 29476
[Halmos] p. 41	Definition of Hermitian	hmopadj2 29351
[Halmos] p. 42	Definition of projector ordering	pjordi 29583
[Halmos] p. 43	Theorem 26.1	elpjhmop 29595  elpjidm 29594  pjnmopi 29558
[Halmos] p. 44	Remark	pjinormi 29097  pjinormii 29086
[Halmos] p. 44	Theorem 26.2	elpjch 29599  pjrn 29117  pjrni 29112  pjvec 29106
[Halmos] p. 44	Theorem 26.3	pjnorm2 29137
[Halmos] p. 44	Theorem 26.4	hmopidmpj 29564  hmopidmpji 29562
[Halmos] p. 45	Theorem 27.1	pjinvari 29601
[Halmos] p. 45	Theorem 27.3	pjoci 29590  pjocvec 29107
[Halmos] p. 45	Theorem 27.4	pjorthcoi 29579
[Halmos] p. 48	Theorem 29.2	pjssposi 29582
[Halmos] p. 48	Theorem 29.3	pjssdif1i 29585  pjssdif2i 29584
[Halmos] p. 50	Definition of spectrum	df-spec 29265
[Hamilton] p. 28	Definition 2.1	ax-1 6
[Hamilton] p. 31	Example 2.7(a)	idALT 23
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1894
[Hatcher] p. 25	Definition	df-phtpc 23168  df-phtpy 23147
[Hatcher] p. 26	Definition	df-pco 23181  df-pi1 23184
[Hatcher] p. 26	Proposition 1.2	phtpcer 23171
[Hatcher] p. 26	Proposition 1.3	pi1grp 23226
[Hefferon] p. 240	Definition 3.12	df-dmat 20671  df-dmatalt 43048
[Helfgott] p. 2	Theorem	tgoldbach 42549
[Helfgott] p. 4	Corollary 1.1	wtgoldbnnsum4prm 42534
[Helfgott] p. 4	Section 1.2.2	ax-hgprmladder 42546  bgoldbtbnd 42541  bgoldbtbnd 42541  tgblthelfgott 42547
[Helfgott] p. 5	Proposition 1.1	circlevma 31265
[Helfgott] p. 69	Statement 7.49	circlemethhgt 31266
[Helfgott] p. 69	Statement 7.50	hgt750lema 31280  hgt750lemb 31279  hgt750leme 31281  hgt750lemf 31276  hgt750lemg 31277
[Helfgott] p. 70	Section 7.4	ax-tgoldbachgt 42543  tgoldbachgt 31286  tgoldbachgtALTV 42544  tgoldbachgtd 31285
[Helfgott] p. 70	Statement 7.49	ax-hgt749 31267
[Herstein] p. 54	Exercise 28	df-grpo 27899
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 17794  grpoideu 27915  mndideu 17664
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 17817  grpoinveu 27925
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 17843  grpo2inv 27937
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 17854  grpoinvop 27939
[Herstein] p. 57	Exercise 1	dfgrp3e 17876
[Hitchcock] p. 5	Rule A3	mptnan 1867
[Hitchcock] p. 5	Rule A4	mptxor 1868
[Hitchcock] p. 5	Rule A5	mtpxor 1870
[Holland] p. 1519	Theorem 2	sumdmdi 29830
[Holland] p. 1520	Lemma 5	cdj1i 29843  cdj3i 29851  cdj3lem1 29844  cdjreui 29842
[Holland] p. 1524	Lemma 7	mddmdin0i 29841
[Holland95] p. 13	Theorem 3.6	hlathil 38031
[Holland95] p. 14	Line 15	hgmapvs 37961
[Holland95] p. 14	Line 16	hdmaplkr 37983
[Holland95] p. 14	Line 17	hdmapellkr 37984
[Holland95] p. 14	Line 19	hdmapglnm2 37981
[Holland95] p. 14	Line 20	hdmapip0com 37987
[Holland95] p. 14	Theorem 3.6	hdmapevec2 37906
[Holland95] p. 14	Lines 24 and 25	hdmapoc 38001
[Holland95] p. 204	Definition of involution	df-srng 19209
[Holland95] p. 212	Definition of subspace	df-psubsp 35573
[Holland95] p. 214	Lemma 3.3	lclkrlem2v 37598
[Holland95] p. 214	Definition 3.2	df-lpolN 37551
[Holland95] p. 214	Definition of nonsingular	pnonsingN 36003
[Holland95] p. 215	Lemma 3.3(1)	dihoml4 37447  poml4N 36023
[Holland95] p. 215	Lemma 3.3(2)	dochexmid 37538  pexmidALTN 36048  pexmidN 36039
[Holland95] p. 218	Theorem 3.6	lclkr 37603
[Holland95] p. 218	Definition of dual vector space	df-ldual 35194  ldualset 35195
[Holland95] p. 222	Item 1	df-lines 35571  df-pointsN 35572
[Holland95] p. 222	Item 2	df-polarityN 35973
[Holland95] p. 223	Remark	ispsubcl2N 36017  omllaw4 35316  pol1N 35980  polcon3N 35987
[Holland95] p. 223	Definition	df-psubclN 36005
[Holland95] p. 223	Equation for polarity	polval2N 35976
[Holmes] p. 40	Definition	df-xrn 34676
[Hughes] p. 44	Equation 1.21b	ax-his3 28492
[Hughes] p. 47	Definition of projection operator	dfpjop 29592
[Hughes] p. 49	Equation 1.30	eighmre 29373  eigre 29245  eigrei 29244
[Hughes] p. 49	Equation 1.31	eighmorth 29374  eigorth 29248  eigorthi 29247
[Hughes] p. 137	Remark (ii)	eigposi 29246
[Huneke] p. 1	Claim 1	frgrncvvdeq 27686
[Huneke] p. 1	Statement 1	frgrncvvdeqlem7 27682
[Huneke] p. 1	Statement 2	frgrncvvdeqlem8 27683
[Huneke] p. 1	Statement 3	frgrncvvdeqlem9 27684
[Huneke] p. 2	Claim 2	frgrregorufr 27702  frgrregorufr0 27701  frgrregorufrg 27703
[Huneke] p. 2	Claim 3	frgrhash2wsp 27709  frrusgrord 27718  frrusgrord0 27717
[Huneke] p. 2	Statement	df-clwwlknon 27459
[Huneke] p. 2	Statement 4	frgrwopreglem4 27692
[Huneke] p. 2	Statement 5	frgrwopreg1 27695  frgrwopreg2 27696  frgrwopregasn 27693  frgrwopregbsn 27694
[Huneke] p. 2	Statement 6	frgrwopreglem5 27698
[Huneke] p. 2	Statement 7	fusgreghash2wspv 27712
[Huneke] p. 2	Statement 8	fusgreghash2wsp 27715
[Huneke] p. 2	Statement 9	clwlksndivn 27457  numclwlk1 27770  numclwlk1lem1 27768  numclwlk1lem2 27769  numclwwlk1 27755  numclwwlk8 27803
[Huneke] p. 2	Definition 3	frgrwopreglem1 27689
[Huneke] p. 2	Definition 4	df-clwlks 27080
[Huneke] p. 2	Definition 6	2clwwlk 27727
[Huneke] p. 2	Definition 7	numclwwlkovh 27772  numclwwlkovh0 27771
[Huneke] p. 2	Statement 10	numclwwlk2 27784
[Huneke] p. 2	Statement 11	rusgrnumwlkg 27314
[Huneke] p. 2	Statement 12	numclwwlk3 27796
[Huneke] p. 2	Statement 13	numclwwlk5 27799
[Huneke] p. 2	Statement 14	numclwwlk7 27802
[Indrzejczak] p. 33	Definition ` `E	natded 27814  natded 27814
[Indrzejczak] p. 33	Definition ` `I	natded 27814
[Indrzejczak] p. 34	Definition ` `E	natded 27814  natded 27814
[Indrzejczak] p. 34	Definition ` `I	natded 27814
[Jech] p. 4	Definition of class	cv 1655  cvjust 2820
[Jech] p. 42	Lemma 6.1	alephexp1 9723
[Jech] p. 42	Equation 6.1	alephadd 9721  alephmul 9722
[Jech] p. 43	Lemma 6.2	infmap 9720  infmap2 9362
[Jech] p. 71	Lemma 9.3	jech9.3 8961
[Jech] p. 72	Equation 9.3	scott0 9033  scottex 9032
[Jech] p. 72	Exercise 9.1	rankval4 9014
[Jech] p. 72	Scheme "Collection Principle"	cp 9038
[Jech] p. 78	Note	opthprc 5404
[JonesMatijasevic] p. 694	Definition 2.3	rmxyval 38318
[JonesMatijasevic] p. 695	Lemma 2.15	jm2.15nn0 38408
[JonesMatijasevic] p. 695	Lemma 2.16	jm2.16nn0 38409
[JonesMatijasevic] p. 695	Equation 2.7	rmxadd 38330
[JonesMatijasevic] p. 695	Equation 2.8	rmyadd 38334
[JonesMatijasevic] p. 695	Equation 2.9	rmxp1 38335  rmyp1 38336
[JonesMatijasevic] p. 695	Equation 2.10	rmxm1 38337  rmym1 38338
[JonesMatijasevic] p. 695	Equation 2.11	rmx0 38328  rmx1 38329  rmxluc 38339
[JonesMatijasevic] p. 695	Equation 2.12	rmy0 38332  rmy1 38333  rmyluc 38340
[JonesMatijasevic] p. 695	Equation 2.13	rmxdbl 38342
[JonesMatijasevic] p. 695	Equation 2.14	rmydbl 38343
[JonesMatijasevic] p. 696	Lemma 2.17	jm2.17a 38365  jm2.17b 38366  jm2.17c 38367
[JonesMatijasevic] p. 696	Lemma 2.19	jm2.19 38398
[JonesMatijasevic] p. 696	Lemma 2.20	jm2.20nn 38402
[JonesMatijasevic] p. 696	Theorem 2.18	jm2.18 38393
[JonesMatijasevic] p. 697	Lemma 2.24	jm2.24 38368  jm2.24nn 38364
[JonesMatijasevic] p. 697	Lemma 2.26	jm2.26 38407
[JonesMatijasevic] p. 697	Lemma 2.27	jm2.27 38413  rmygeid 38369
[JonesMatijasevic] p. 698	Lemma 3.1	jm3.1 38425
[Juillerat] p. 11	Section *5	etransc 41288  etransclem47 41286  etransclem48 41287
[Juillerat] p. 12	Equation (7)	etransclem44 41283
[Juillerat] p. 12	Equation *(7)	etransclem46 41285
[Juillerat] p. 12	Proof of the derivative calculated	etransclem32 41271
[Juillerat] p. 13	Proof	etransclem35 41274
[Juillerat] p. 13	Part of case 2 proven in	etransclem38 41277
[Juillerat] p. 13	Part of case 2 proven	etransclem24 41263
[Juillerat] p. 13	Part of case 2: proven in	etransclem41 41280
[Juillerat] p. 14	Proof	etransclem23 41262
[KalishMontague] p. 81	Note 1	ax-6 2075
[KalishMontague] p. 85	Lemma 2	equid 2116
[KalishMontague] p. 85	Lemma 3	equcomi 2121
[KalishMontague] p. 86	Lemma 7	cbvalivw 2111  cbvaliw 2110  wl-cbvmotv 33836  wl-motae 33838  wl-moteq 33837
[KalishMontague] p. 87	Lemma 8	spimvw 2103  spimw 2102
[KalishMontague] p. 87	Lemma 9	spfw 2140  spw 2141
[Kalmbach] p. 14	Definition of lattice	chabs1 28926  chabs1i 28928  chabs2 28927  chabs2i 28929  chjass 28943  chjassi 28896  latabs1 17447  latabs2 17448
[Kalmbach] p. 15	Definition of atom	df-at 29748  ela 29749
[Kalmbach] p. 15	Definition of covers	cvbr2 29693  cvrval2 35344
[Kalmbach] p. 16	Definition	df-ol 35248  df-oml 35249
[Kalmbach] p. 20	Definition of commutes	cmbr 28994  cmbri 29000  cmtvalN 35281  df-cm 28993  df-cmtN 35247
[Kalmbach] p. 22	Remark	omllaw5N 35317  pjoml5 29023  pjoml5i 28998
[Kalmbach] p. 22	Definition	pjoml2 29021  pjoml2i 28995
[Kalmbach] p. 22	Theorem 2(v)	cmcm 29024  cmcmi 29002  cmcmii 29007  cmtcomN 35319
[Kalmbach] p. 22	Theorem 2(ii)	omllaw3 35315  omlsi 28814  pjoml 28846  pjomli 28845
[Kalmbach] p. 22	Definition of OML law	omllaw2N 35314
[Kalmbach] p. 23	Remark	cmbr2i 29006  cmcm3 29025  cmcm3i 29004  cmcm3ii 29009  cmcm4i 29005  cmt3N 35321  cmt4N 35322  cmtbr2N 35323
[Kalmbach] p. 23	Lemma 3	cmbr3 29018  cmbr3i 29010  cmtbr3N 35324
[Kalmbach] p. 25	Theorem 5	fh1 29028  fh1i 29031  fh2 29029  fh2i 29032  omlfh1N 35328
[Kalmbach] p. 65	Remark	chjatom 29767  chslej 28908  chsleji 28868  shslej 28790  shsleji 28780
[Kalmbach] p. 65	Proposition 1	chocin 28905  chocini 28864  chsupcl 28750  chsupval2 28820  h0elch 28663  helch 28651  hsupval2 28819  ocin 28706  ococss 28703  shococss 28704
[Kalmbach] p. 65	Definition of subspace sum	shsval 28722
[Kalmbach] p. 66	Remark	df-pjh 28805  pjssmi 29575  pjssmii 29091
[Kalmbach] p. 67	Lemma 3	osum 29055  osumi 29052
[Kalmbach] p. 67	Lemma 4	pjci 29610
[Kalmbach] p. 103	Exercise 6	atmd2 29810
[Kalmbach] p. 103	Exercise 12	mdsl0 29720
[Kalmbach] p. 140	Remark	hatomic 29770  hatomici 29769  hatomistici 29772
[Kalmbach] p. 140	Proposition 1	atlatmstc 35389
[Kalmbach] p. 140	Proposition 1(i)	atexch 29791  lsatexch 35113
[Kalmbach] p. 140	Proposition 1(ii)	chcv1 29765  cvlcvr1 35409  cvr1 35480
[Kalmbach] p. 140	Proposition 1(iii)	cvexch 29784  cvexchi 29779  cvrexch 35490
[Kalmbach] p. 149	Remark 2	chrelati 29774  hlrelat 35472  hlrelat5N 35471  lrelat 35084
[Kalmbach] p. 153	Exercise 5	lsmcv 19508  lsmsatcv 35080  spansncv 29063  spansncvi 29062
[Kalmbach] p. 153	Proposition 1(ii)	lsmcv2 35099  spansncv2 29703
[Kalmbach] p. 266	Definition	df-st 29621
[Kalmbach2] p. 8	Definition of adjoint	df-adjh 29259
[KanamoriPincus] p. 415	Theorem 1.1	fpwwe 9790  fpwwe2 9787
[KanamoriPincus] p. 416	Corollary 1.3	canth4 9791
[KanamoriPincus] p. 417	Corollary 1.6	canthp1 9798
[KanamoriPincus] p. 417	Corollary 1.4(a)	canthnum 9793
[KanamoriPincus] p. 417	Corollary 1.4(b)	canthwe 9795
[KanamoriPincus] p. 418	Proposition 1.7	pwfseq 9808
[KanamoriPincus] p. 419	Lemma 2.2	gchcdaidm 9812  gchxpidm 9813
[KanamoriPincus] p. 419	Theorem 2.1	gchacg 9824  gchhar 9823
[KanamoriPincus] p. 420	Lemma 2.3	pwcdadom 9360  unxpwdom 8770
[KanamoriPincus] p. 421	Proposition 3.1	gchpwdom 9814
[Kreyszig] p. 3	Property M1	metcl 22514  xmetcl 22513
[Kreyszig] p. 4	Property M2	meteq0 22521
[Kreyszig] p. 8	Definition 1.1-8	dscmet 22754
[Kreyszig] p. 12	Equation 5	conjmul 11075  muleqadd 11003
[Kreyszig] p. 18	Definition 1.3-2	mopnval 22620
[Kreyszig] p. 19	Remark	mopntopon 22621
[Kreyszig] p. 19	Theorem T1	mopn0 22680  mopnm 22626
[Kreyszig] p. 19	Theorem T2	unimopn 22678
[Kreyszig] p. 19	Definition of neighborhood	neibl 22683
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 22724
[Kreyszig] p. 25	Definition 1.4-1	lmbr 21440  lmmbr 23433  lmmbr2 23434
[Kreyszig] p. 26	Lemma 1.4-2(a)	lmmo 21562
[Kreyszig] p. 28	Theorem 1.4-5	lmcau 23488
[Kreyszig] p. 28	Definition 1.4-3	iscau 23451  iscmet2 23469
[Kreyszig] p. 30	Theorem 1.4-7	cmetss 23491
[Kreyszig] p. 30	Theorem 1.4-6(a)	1stcelcls 21642  metelcls 23480
[Kreyszig] p. 30	Theorem 1.4-6(b)	metcld 23481  metcld2 23482
[Kreyszig] p. 51	Equation 2	clmvneg1 23275  lmodvneg1 19269  nvinv 28045  vcm 27982
[Kreyszig] p. 51	Equation 1a	clm0vs 23271  lmod0vs 19259  slmd0vs 30318  vc0 27980
[Kreyszig] p. 51	Equation 1b	lmodvs0 19260  slmdvs0 30319  vcz 27981
[Kreyszig] p. 58	Definition 2.2-1	imsmet 28097  ngpmet 22784  nrmmetd 22756
[Kreyszig] p. 59	Equation 1	imsdval 28092  imsdval2 28093  ncvspds 23337  ngpds 22785
[Kreyszig] p. 63	Problem 1	nmval 22771  nvnd 28094
[Kreyszig] p. 64	Problem 2	nmeq0 22799  nmge0 22798  nvge0 28079  nvz 28075
[Kreyszig] p. 64	Problem 3	nmrtri 22805  nvabs 28078
[Kreyszig] p. 91	Definition 2.7-1	isblo3i 28207
[Kreyszig] p. 92	Equation 2	df-nmoo 28151
[Kreyszig] p. 97	Theorem 2.7-9(a)	blocn 28213  blocni 28211
[Kreyszig] p. 97	Theorem 2.7-9(b)	lnocni 28212
[Kreyszig] p. 129	Definition 3.1-1	cphipeq0 23380  ipeq0 20352  ipz 28125
[Kreyszig] p. 135	Problem 2	pythi 28256
[Kreyszig] p. 137	Lemma 3-2.1(a)	sii 28260
[Kreyszig] p. 144	Equation 4	supcvg 14969
[Kreyszig] p. 144	Theorem 3.3-1	minvec 23611  minveco 28291
[Kreyszig] p. 196	Definition 3.9-1	df-aj 28156
[Kreyszig] p. 247	Theorem 4.7-2	bcth 23504
[Kreyszig] p. 249	Theorem 4.7-3	ubth 28280
[Kreyszig] p. 470	Definition of positive operator ordering	leop 29533  leopg 29532
[Kreyszig] p. 476	Theorem 9.4-2	opsqrlem2 29551
[Kreyszig] p. 525	Theorem 10.1-1	htth 28326
[Kulpa] p. 547	Theorem	poimir 33981
[Kulpa] p. 547	Equation (1)	poimirlem32 33980
[Kulpa] p. 547	Equation (2)	poimirlem31 33979
[Kulpa] p. 548	Theorem	broucube 33982
[Kulpa] p. 548	Equation (6)	poimirlem26 33974
[Kulpa] p. 548	Equation (7)	poimirlem27 33975
[Kunen] p. 10	Axiom 0	ax6e 2402  axnul 5014
[Kunen] p. 11	Axiom 3	axnul 5014
[Kunen] p. 12	Axiom 6	zfrep6 7401
[Kunen] p. 24	Definition 10.24	mapval 8139  mapvalg 8137
[Kunen] p. 30	Lemma 10.20	fodom 9666
[Kunen] p. 31	Definition 10.24	mapex 8133
[Kunen] p. 95	Definition 2.1	df-r1 8911
[Kunen] p. 97	Lemma 2.10	r1elss 8953  r1elssi 8952
[Kunen] p. 107	Exercise 4	rankop 9005  rankopb 8999  rankuni 9010  rankxplim 9026  rankxpsuc 9029
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 4753
[Lang] p. 3	Definition	df-mnd 17655
[Lang] p. 7	Definition	dfgrp2e 17809
[Lang] p. 53	Definition	df-cat 16688
[Lang] p. 54	Definition	df-iso 16768
[Lang] p. 57	Definition	df-inito 17000  df-termo 17001
[Lang] p. 58	Example	irinitoringc 42930
[Lang] p. 58	Statement	initoeu1 17020  termoeu1 17027
[Lang] p. 62	Definition	df-func 16877
[Lang] p. 65	Definition	df-nat 16962
[Lang] p. 91	Note	df-ringc 42866
[Lang] p. 128	Remark	dsmmlmod 20459
[Lang] p. 129	Proof	lincscm 43080  lincscmcl 43082  lincsum 43079  lincsumcl 43081
[Lang] p. 129	Statement	lincolss 43084
[Lang] p. 129	Observation	dsmmfi 20452
[Lang] p. 147	Definition	snlindsntor 43121
[Lang] p. 504	Statement	mat1 20628  matring 20623
[Lang] p. 504	Definition	df-mamu 20564
[Lang] p. 505	Statement	mamuass 20582  mamutpos 20639  matassa 20624  mattposvs 20636  tposmap 20638
[Lang] p. 513	Definition	mdet1 20782  mdetf 20776
[Lang] p. 513	Theorem 4.4	cramer 20874
[Lang] p. 514	Proposition 4.6	mdetleib 20768
[Lang] p. 514	Proposition 4.8	mdettpos 20792
[Lang] p. 515	Definition	df-minmar1 20816  smadiadetr 20857
[Lang] p. 515	Corollary 4.9	mdetero 20791  mdetralt 20789
[Lang] p. 517	Proposition 4.15	mdetmul 20804
[Lang] p. 518	Definition	df-madu 20815
[Lang] p. 518	Proposition 4.16	madulid 20826  madurid 20825  matinv 20859
[Lang] p. 561	Theorem 3.1	cayleyhamilton 21072
[Lang], p. 561	Remark	chpmatply1 21014
[Lang], p. 561	Definition	df-chpmat 21009
[LarsonHostetlerEdwards] p. 278	Section 4.1	dvconstbi 39368
[LarsonHostetlerEdwards] p. 311	Example 1a	lhe4.4ex1a 39363
[LarsonHostetlerEdwards] p. 375	Theorem 5.1	expgrowth 39369
[LeBlanc] p. 277	Rule R2	axnul 5014
[Levy] p. 338	Axiom	df-clab 2812  df-clel 2821  df-cleq 2818
[Levy58] p. 2	Definition I	isfin1-3 9530
[Levy58] p. 2	Definition II	df-fin2 9430
[Levy58] p. 2	Definition Ia	df-fin1a 9429
[Levy58] p. 2	Definition III	df-fin3 9432
[Levy58] p. 3	Definition V	df-fin5 9433
[Levy58] p. 3	Definition IV	df-fin4 9431
[Levy58] p. 4	Definition VI	df-fin6 9434
[Levy58] p. 4	Definition VII	df-fin7 9435
[Levy58], p. 3	Theorem 1	fin1a2 9559
[Lipparini] p. 3	Lemma 2.1.1	nosepssdm 32370
[Lipparini] p. 3	Lemma 2.1.4	noresle 32380
[Lipparini] p. 6	Proposition 4.2	nosupbnd1 32394
[Lipparini] p. 6	Proposition 4.3	nosupbnd2 32396
[Lipparini] p. 7	Theorem 5.1	noetalem2 32398  noetalem3 32399
[Lopez-Astorga] p. 12	Rule 1	mptnan 1867
[Lopez-Astorga] p. 12	Rule 2	mptxor 1868
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1870
[Maeda] p. 167	Theorem 1(d) to (e)	mdsymlem6 29818
[Maeda] p. 168	Lemma 5	mdsym 29822  mdsymi 29821
[Maeda] p. 168	Lemma 4(i)	mdsymlem4 29816  mdsymlem6 29818  mdsymlem7 29819
[Maeda] p. 168	Lemma 4(ii)	mdsymlem8 29820
[MaedaMaeda] p. 1	Remark	ssdmd1 29723  ssdmd2 29724  ssmd1 29721  ssmd2 29722
[MaedaMaeda] p. 1	Lemma 1.2	mddmd2 29719
[MaedaMaeda] p. 1	Definition 1.1	df-dmd 29691  df-md 29690  mdbr 29704
[MaedaMaeda] p. 2	Lemma 1.3	mdsldmd1i 29741  mdslj1i 29729  mdslj2i 29730  mdslle1i 29727  mdslle2i 29728  mdslmd1i 29739  mdslmd2i 29740
[MaedaMaeda] p. 2	Lemma 1.4	mdsl1i 29731  mdsl2bi 29733  mdsl2i 29732
[MaedaMaeda] p. 2	Lemma 1.6	mdexchi 29745
[MaedaMaeda] p. 2	Lemma 1.5.1	mdslmd3i 29742
[MaedaMaeda] p. 2	Lemma 1.5.2	mdslmd4i 29743
[MaedaMaeda] p. 2	Lemma 1.5.3	mdsl0 29720
[MaedaMaeda] p. 2	Theorem 1.3	dmdsl3 29725  mdsl3 29726
[MaedaMaeda] p. 3	Theorem 1.9.1	csmdsymi 29744
[MaedaMaeda] p. 4	Theorem 1.14	mdcompli 29839
[MaedaMaeda] p. 30	Lemma 7.2	atlrelat1 35391  hlrelat1 35470
[MaedaMaeda] p. 31	Lemma 7.5	lcvexch 35109
[MaedaMaeda] p. 31	Lemma 7.5.1	cvmd 29746  cvmdi 29734  cvnbtwn4 29699  cvrnbtwn4 35349
[MaedaMaeda] p. 31	Lemma 7.5.2	cvdmd 29747
[MaedaMaeda] p. 31	Definition 7.4	cvlcvrp 35410  cvp 29785  cvrp 35486  lcvp 35110
[MaedaMaeda] p. 31	Theorem 7.6(b)	atmd 29809
[MaedaMaeda] p. 31	Theorem 7.6(c)	atdmd 29808
[MaedaMaeda] p. 32	Definition 7.8	cvlexch4N 35403  hlexch4N 35462
[MaedaMaeda] p. 34	Exercise 7.1	atabsi 29811
[MaedaMaeda] p. 41	Lemma 9.2(delta)	cvrat4 35513
[MaedaMaeda] p. 61	Definition 15.1	0psubN 35819  atpsubN 35823  df-pointsN 35572  pointpsubN 35821
[MaedaMaeda] p. 62	Theorem 15.5	df-pmap 35574  pmap11 35832  pmaple 35831  pmapsub 35838  pmapval 35827
[MaedaMaeda] p. 62	Theorem 15.5.1	pmap0 35835  pmap1N 35837
[MaedaMaeda] p. 62	Theorem 15.5.2	pmapglb 35840  pmapglb2N 35841  pmapglb2xN 35842  pmapglbx 35839
[MaedaMaeda] p. 63	Equation 15.5.3	pmapjoin 35922
[MaedaMaeda] p. 67	Postulate PS1	ps-1 35547
[MaedaMaeda] p. 68	Lemma 16.2	df-padd 35866  paddclN 35912  paddidm 35911
[MaedaMaeda] p. 68	Condition PS2	ps-2 35548
[MaedaMaeda] p. 68	Equation 16.2.1	paddass 35908
[MaedaMaeda] p. 69	Lemma 16.4	ps-1 35547
[MaedaMaeda] p. 69	Theorem 16.4	ps-2 35548
[MaedaMaeda] p. 70	Theorem 16.9	lsmmod 18446  lsmmod2 18447  lssats 35082  shatomici 29768  shatomistici 29771  shmodi 28800  shmodsi 28799
[MaedaMaeda] p. 130	Remark 29.6	dmdmd 29710  mdsymlem7 29819
[MaedaMaeda] p. 132	Theorem 29.13(e)	pjoml6i 28999
[MaedaMaeda] p. 136	Lemma 31.1.5	shjshseli 28903
[MaedaMaeda] p. 139	Remark	sumdmdii 29825
[Margaris] p. 40	Rule C	exlimiv 2029
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	ax-3 8
[Margaris] p. 49	Definition	df-an 387  df-ex 1879  df-or 879  dfbi2 468
[Margaris] p. 51	Theorem 1	idALT 23
[Margaris] p. 56	Theorem 3	conventions 27811
[Margaris] p. 59	Section 14	notnotrALTVD 39964
[Margaris] p. 60	Theorem 8	mth8 160
[Margaris] p. 60	Section 14	con3ALTVD 39965
[Margaris] p. 79	Rule C	exinst01 39673  exinst11 39674
[Margaris] p. 89	Theorem 19.2	19.2 2080  19.2g 2229  r19.2z 4284
[Margaris] p. 89	Theorem 19.3	19.3 2243  rr19.3v 3564
[Margaris] p. 89	Theorem 19.5	alcom 2209
[Margaris] p. 89	Theorem 19.6	alex 1924
[Margaris] p. 89	Theorem 19.7	alnex 1880
[Margaris] p. 89	Theorem 19.8	19.8a 2223
[Margaris] p. 89	Theorem 19.9	19.9 2247  19.9h 2317  exlimd 2261  exlimdh 2321
[Margaris] p. 89	Theorem 19.11	excom 2212  excomim 2213
[Margaris] p. 89	Theorem 19.12	19.12 2359
[Margaris] p. 90	Section 19	conventions-labels 27812  conventions-labels 27812  conventions-labels 27812  conventions-labels 27812
[Margaris] p. 90	Theorem 19.14	exnal 1925
[Margaris] p. 90	Theorem 19.15	2albi 39412  albi 1917
[Margaris] p. 90	Theorem 19.16	19.16 2268
[Margaris] p. 90	Theorem 19.17	19.17 2269
[Margaris] p. 90	Theorem 19.18	2exbi 39414  exbi 1946
[Margaris] p. 90	Theorem 19.19	19.19 2272
[Margaris] p. 90	Theorem 19.20	2alim 39411  2alimdv 2017  alimd 2255  alimdh 1916  alimdv 2015  ax-4 1908  ralimdaa 3167  ralimdv 3172  ralimdva 3171  ralimdvva 3173  sbcimdv 3724
[Margaris] p. 90	Theorem 19.21	19.21 2249  19.21h 2318  19.21t 2248  19.21vv 39410  alrimd 2258  alrimdd 2257  alrimdh 1964  alrimdv 2028  alrimi 2256  alrimih 1922  alrimiv 2026  alrimivv 2027  hbralrimi 3163  r19.21be 3142  r19.21bi 3141  ralrimd 3168  ralrimdv 3177  ralrimdva 3178  ralrimdvv 3182  ralrimdvva 3183  ralrimi 3166  ralrimia 40124  ralrimiv 3174  ralrimiva 3175  ralrimivv 3179  ralrimivva 3180  ralrimivvva 3181  ralrimivw 3176
[Margaris] p. 90	Theorem 19.22	2exim 39413  2eximdv 2018  exim 1932  eximd 2259  eximdh 1965  eximdv 2016  rexim 3216  reximd2a 3221  reximdai 3220  reximdd 40148  reximddv 3226  reximddv2 3229  reximddv3 40147  reximdv 3224  reximdv2 3222  reximdva 3225  reximdvai 3223  reximdvva 3228  reximi2 3218
[Margaris] p. 90	Theorem 19.23	19.23 2254  19.23bi 2232  19.23h 2319  19.23t 2252  exlimdv 2032  exlimdvv 2033  exlimexi 39563  exlimiv 2029  exlimivv 2031  rexlimd3 40140  rexlimdv 3239  rexlimdv3a 3242  rexlimdva 3240  rexlimdva2 3243  rexlimdvaa 3241  rexlimdvv 3247  rexlimdvva 3248  rexlimdvw 3244  rexlimiv 3236  rexlimiva 3237  rexlimivv 3246
[Margaris] p. 90	Theorem 19.24	19.24 2088
[Margaris] p. 90	Theorem 19.25	19.25 1983
[Margaris] p. 90	Theorem 19.26	19.26 1972
[Margaris] p. 90	Theorem 19.27	19.27 2270  r19.27z 4294  r19.27zv 4295
[Margaris] p. 90	Theorem 19.28	19.28 2271  19.28vv 39420  r19.28z 4287  r19.28zv 4290  rr19.28v 3565
[Margaris] p. 90	Theorem 19.29	19.29 1976  r19.29d2r 3290  r19.29imd 3284
[Margaris] p. 90	Theorem 19.30	19.30 1984
[Margaris] p. 90	Theorem 19.31	19.31 2277  19.31vv 39418
[Margaris] p. 90	Theorem 19.32	19.32 2276  r19.32 41987
[Margaris] p. 90	Theorem 19.33	19.33-2 39416  19.33 1987
[Margaris] p. 90	Theorem 19.34	19.34 2089
[Margaris] p. 90	Theorem 19.35	19.35 1980
[Margaris] p. 90	Theorem 19.36	19.36 2273  19.36vv 39417  r19.36zv 4296
[Margaris] p. 90	Theorem 19.37	19.37 2275  19.37vv 39419  r19.37zv 4291
[Margaris] p. 90	Theorem 19.38	19.38 1937
[Margaris] p. 90	Theorem 19.39	19.39 2087
[Margaris] p. 90	Theorem 19.40	19.40-2 1989  19.40 1971  r19.40 3298
[Margaris] p. 90	Theorem 19.41	19.41 2278  19.41rg 39589
[Margaris] p. 90	Theorem 19.42	19.42 2280
[Margaris] p. 90	Theorem 19.43	19.43 1985
[Margaris] p. 90	Theorem 19.44	19.44 2281  r19.44zv 4293
[Margaris] p. 90	Theorem 19.45	19.45 2282  r19.45zv 4292
[Margaris] p. 110	Exercise 2(b)	eu1 2695
[Mayet] p. 370	Remark	jpi 29680  largei 29677  stri 29667
[Mayet3] p. 9	Definition of CH-states	df-hst 29622  ishst 29624
[Mayet3] p. 10	Theorem	hstrbi 29676  hstri 29675
[Mayet3] p. 1223	Theorem 4.1	mayete3i 29138
[Mayet3] p. 1240	Theorem 7.1	mayetes3i 29139
[MegPav2000] p. 2344	Theorem 3.3	stcltrthi 29688
[MegPav2000] p. 2345	Definition 3.4-1	chintcl 28742  chsupcl 28750
[MegPav2000] p. 2345	Definition 3.4-2	hatomic 29770
[MegPav2000] p. 2345	Definition 3.4-3(a)	superpos 29764
[MegPav2000] p. 2345	Definition 3.4-3(b)	atexch 29791
[MegPav2000] p. 2366	Figure 7	pl42N 36053
[MegPav2002] p. 362	Lemma 2.2	latj31 17459  latj32 17457  latjass 17455
[Megill] p. 444	Axiom C5	ax-5 2009  ax5ALT 34977
[Megill] p. 444	Section 7	conventions 27811
[Megill] p. 445	Lemma L12	aecom-o 34971  ax-c11n 34958  axc11n 2447
[Megill] p. 446	Lemma L17	equtrr 2126
[Megill] p. 446	Lemma L18	ax6fromc10 34966
[Megill] p. 446	Lemma L19	hbnae-o 34998  hbnae 2454
[Megill] p. 447	Remark 9.1	df-sb 2068  sbid 2289  sbidd-misc 43368  sbidd 43367
[Megill] p. 448	Remark 9.6	axc14 2503
[Megill] p. 448	Scheme C4'	ax-c4 34954
[Megill] p. 448	Scheme C5'	ax-c5 34953  sp 2224
[Megill] p. 448	Scheme C6'	ax-11 2207
[Megill] p. 448	Scheme C7'	ax-c7 34955
[Megill] p. 448	Scheme C8'	ax-7 2112
[Megill] p. 448	Scheme C9'	ax-c9 34960
[Megill] p. 448	Scheme C10'	ax-6 2075  ax-c10 34956
[Megill] p. 448	Scheme C11'	ax-c11 34957
[Megill] p. 448	Scheme C12'	ax-8 2166
[Megill] p. 448	Scheme C13'	ax-9 2173
[Megill] p. 448	Scheme C14'	ax-c14 34961
[Megill] p. 448	Scheme C15'	ax-c15 34959
[Megill] p. 448	Scheme C16'	ax-c16 34962
[Megill] p. 448	Theorem 9.4	dral1-o 34974  dral1 2460  dral2-o 35000  dral2 2459  drex1 2462  drex2 2463  drsb1 2508  drsb2 2509
[Megill] p. 449	Theorem 9.7	sbcom2 2578  sbequ 2507  sbid2v 2545
[Megill] p. 450	Example in Appendix	hba1-o 34967  hba1 2325
[Mendelson] p. 35	Axiom A3	hirstL-ax3 41847
[Mendelson] p. 36	Lemma 1.8	idALT 23
[Mendelson] p. 69	Axiom 4	rspsbc 3742  rspsbca 3743  stdpc4 2483
[Mendelson] p. 69	Axiom 5	ax-c4 34954  ra4 3749  stdpc5 2250
[Mendelson] p. 81	Rule C	exlimiv 2029
[Mendelson] p. 95	Axiom 6	stdpc6 2132
[Mendelson] p. 95	Axiom 7	stdpc7 2133
[Mendelson] p. 225	Axiom system NBG	ru 3661
[Mendelson] p. 230	Exercise 4.8(b)	opthwiener 5202
[Mendelson] p. 231	Exercise 4.10(k)	inv1 4197
[Mendelson] p. 231	Exercise 4.10(l)	unv 4198
[Mendelson] p. 231	Exercise 4.10(n)	dfin3 4098
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 4147
[Mendelson] p. 231	Exercise 4.10(q)	dfin4 4099
[Mendelson] p. 231	Exercise 4.10(s)	ddif 3971
[Mendelson] p. 231	Definition of union	dfun3 4097
[Mendelson] p. 235	Exercise 4.12(c)	univ 5142
[Mendelson] p. 235	Exercise 4.12(d)	pwv 4657
[Mendelson] p. 235	Exercise 4.12(j)	pwin 5246
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 5247
[Mendelson] p. 235	Exercise 4.12(l)	pwssun 5248
[Mendelson] p. 235	Exercise 4.12(n)	uniin 4682
[Mendelson] p. 235	Exercise 4.12(p)	reli 5486
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5901
[Mendelson] p. 244	Proposition 4.8(g)	epweon 7248
[Mendelson] p. 246	Definition of successor	df-suc 5973
[Mendelson] p. 250	Exercise 4.36	oelim2 7947
[Mendelson] p. 254	Proposition 4.22(b)	xpen 8398
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 8319  xpsneng 8320
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 8326  xpcomeng 8327
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 8329
[Mendelson] p. 255	Definition	brsdom 8251
[Mendelson] p. 255	Exercise 4.39	endisj 8322
[Mendelson] p. 255	Exercise 4.41	mapprc 8131
[Mendelson] p. 255	Exercise 4.43	mapsnen 8308  mapsnend 8307
[Mendelson] p. 255	Exercise 4.45	mapunen 8404
[Mendelson] p. 255	Exercise 4.47	xpmapen 8403
[Mendelson] p. 255	Exercise 4.42(a)	map0e 8166
[Mendelson] p. 255	Exercise 4.42(b)	map1 8311
[Mendelson] p. 257	Proposition 4.24(a)	undom 8323
[Mendelson] p. 258	Exercise 4.56(b)	cdaen 9317
[Mendelson] p. 258	Exercise 4.56(c)	cdaassen 9326  cdacomen 9325
[Mendelson] p. 258	Exercise 4.56(f)	cdadom1 9330
[Mendelson] p. 258	Exercise 4.56(g)	xp2cda 9324
[Mendelson] p. 258	Definition of cardinal sum	cdaval 9314  df-cda 9312
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 7883
[Mendelson] p. 266	Proposition 4.34(f)	oaordex 7910
[Mendelson] p. 275	Proposition 4.42(d)	entri3 9703
[Mendelson] p. 281	Definition	df-r1 8911
[Mendelson] p. 281	Proposition 4.45 (b) to (a)	unir1 8960
[Mendelson] p. 287	Axiom system MK	ru 3661
[MertziosUnger] p. 152	Definition	df-frgr 27634
[MertziosUnger] p. 153	Remark 1	frgrconngr 27671
[MertziosUnger] p. 153	Remark 2	vdgn1frgrv2 27673  vdgn1frgrv3 27674
[MertziosUnger] p. 153	Remark 3	vdgfrgrgt2 27675
[MertziosUnger] p. 153	Proposition 1(a)	n4cyclfrgr 27668
[MertziosUnger] p. 153	Proposition 1(b)	2pthfrgr 27661  2pthfrgrrn 27659  2pthfrgrrn2 27660
[Mittelstaedt] p. 9	Definition	df-oc 28660
[Monk1] p. 22	Remark	conventions 27811
[Monk1] p. 22	Theorem 3.1	conventions 27811
[Monk1] p. 26	Theorem 2.8(vii)	ssin 4061
[Monk1] p. 33	Theorem 3.2(i)	ssrel 5446  ssrelf 29970
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 5447
[Monk1] p. 34	Definition 3.3	df-opab 4938
[Monk1] p. 36	Theorem 3.7(i)	coi1 5896  coi2 5897
[Monk1] p. 36	Theorem 3.8(v)	dm0 5575  rn0 5614
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5782
[Monk1] p. 37	Theorem 3.13(i)	relxp 5364
[Monk1] p. 37	Theorem 3.13(x)	dmxp 5580  rnxp 5809
[Monk1] p. 37	Theorem 3.13(ii)	0xp 5438  xp0 5797
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5726
[Monk1] p. 38	Theorem 3.16(viii)	imai 5723
[Monk1] p. 39	Theorem 3.17	imaex 7371  imaexg 7370
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5722
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 6605  funfvop 6583
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 6489
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 6499
[Monk1] p. 43	Theorem 4.6	funun 6172
[Monk1] p. 43	Theorem 4.8(iv)	dff13 6772  dff13f 6773
[Monk1] p. 46	Theorem 4.15(v)	funex 6743  funrnex 7400
[Monk1] p. 50	Definition 5.4	fniunfv 6765
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5865
[Monk1] p. 52	Theorem 5.11(viii)	ssint 4715
[Monk1] p. 52	Definition 5.13 (i)	1stval2 7450  df-1st 7433
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 7451  df-2nd 7434
[Monk1] p. 112	Theorem 15.17(v)	ranksn 9001  ranksnb 8974
[Monk1] p. 112	Theorem 15.17(iv)	rankuni2 9002
[Monk1] p. 112	Theorem 15.17(iii)	rankun 9003  rankunb 8997
[Monk1] p. 113	Theorem 15.18	r1val3 8985
[Monk1] p. 113	Definition 15.19	df-r1 8911  r1val2 8984
[Monk1] p. 117	Lemma	zorn2 9650  zorn2g 9647
[Monk1] p. 133	Theorem 18.11	cardom 9132
[Monk1] p. 133	Theorem 18.12	canth3 9705
[Monk1] p. 133	Theorem 18.14	carduni 9127
[Monk2] p. 105	Axiom C4	ax-4 1908
[Monk2] p. 105	Axiom C7	ax-7 2112
[Monk2] p. 105	Axiom C8	ax-12 2220  ax-c15 34959  ax12v2 2222
[Monk2] p. 108	Lemma 5	ax-c4 34954
[Monk2] p. 109	Lemma 12	ax-11 2207
[Monk2] p. 109	Lemma 15	equvini 2476  equvinv 2134  eqvinop 5177
[Monk2] p. 113	Axiom C5-1	ax-5 2009  ax5ALT 34977
[Monk2] p. 113	Axiom C5-2	ax-10 2192
[Monk2] p. 113	Axiom C5-3	ax-11 2207
[Monk2] p. 114	Lemma 21	sp 2224
[Monk2] p. 114	Lemma 22	axc4 2352  hba1-o 34967  hba1 2325
[Monk2] p. 114	Lemma 23	nfia1 2204
[Monk2] p. 114	Lemma 24	nfa2 2219  nfra2 3155
[Moore] p. 53	Part I	df-mre 16606
[Munkres] p. 77	Example 2	distop 21177  indistop 21184  indistopon 21183
[Munkres] p. 77	Example 3	fctop 21186  fctop2 21187
[Munkres] p. 77	Example 4	cctop 21188
[Munkres] p. 78	Definition of basis	df-bases 21128  isbasis3g 21131
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 16464  tgval2 21138
[Munkres] p. 79	Remark	tgcl 21151
[Munkres] p. 80	Lemma 2.1	tgval3 21145
[Munkres] p. 80	Lemma 2.2	tgss2 21169  tgss3 21168
[Munkres] p. 81	Lemma 2.3	basgen 21170  basgen2 21171
[Munkres] p. 83	Exercise 3	topdifinf 33737  topdifinfeq 33738  topdifinffin 33736  topdifinfindis 33734
[Munkres] p. 89	Definition of subspace topology	resttop 21342
[Munkres] p. 93	Theorem 6.1(1)	0cld 21220  topcld 21217
[Munkres] p. 93	Theorem 6.1(2)	iincld 21221
[Munkres] p. 93	Theorem 6.1(3)	uncld 21223
[Munkres] p. 94	Definition of closure	clsval 21219
[Munkres] p. 94	Definition of interior	ntrval 21218
[Munkres] p. 95	Theorem 6.5(a)	clsndisj 21257  elcls 21255
[Munkres] p. 95	Theorem 6.5(b)	elcls3 21265
[Munkres] p. 97	Theorem 6.6	clslp 21330  neindisj 21299
[Munkres] p. 97	Corollary 6.7	cldlp 21332
[Munkres] p. 97	Definition of limit point	islp2 21327  lpval 21321
[Munkres] p. 98	Definition of Hausdorff space	df-haus 21497
[Munkres] p. 102	Definition of continuous function	df-cn 21409  iscn 21417  iscn2 21420
[Munkres] p. 107	Theorem 7.2(g)	cncnp 21462  cncnp2 21463  cncnpi 21460  df-cnp 21410  iscnp 21419  iscnp2 21421
[Munkres] p. 127	Theorem 10.1	metcn 22725
[Munkres] p. 128	Theorem 10.3	metcn4 23486
[Nathanson] p. 123	Remark	reprgt 31244  reprinfz1 31245  reprlt 31242
[Nathanson] p. 123	Definition	df-repr 31232
[Nathanson] p. 123	Chapter 5.1	circlemethnat 31264
[Nathanson] p. 123	Proposition	breprexp 31256  breprexpnat 31257  itgexpif 31229
[NielsenChuang] p. 195	Equation 4.73	unierri 29514
[OeSilva] p. 2042	Section 2	ax-bgbltosilva 42542
[Pfenning] p. 17	Definition XM	natded 27814
[Pfenning] p. 17	Definition NNC	natded 27814  notnotrd 131
[Pfenning] p. 17	Definition ` `C	natded 27814
[Pfenning] p. 18	Rule"	natded 27814
[Pfenning] p. 18	Definition /\I	natded 27814
[Pfenning] p. 18	Definition ` `E	natded 27814  natded 27814  natded 27814  natded 27814  natded 27814
[Pfenning] p. 18	Definition ` `I	natded 27814  natded 27814  natded 27814  natded 27814  natded 27814
[Pfenning] p. 18	Definition ` `EL	natded 27814
[Pfenning] p. 18	Definition ` `ER	natded 27814
[Pfenning] p. 18	Definition ` `Ea,u	natded 27814
[Pfenning] p. 18	Definition ` `IR	natded 27814
[Pfenning] p. 18	Definition ` `Ia	natded 27814
[Pfenning] p. 127	Definition =E	natded 27814
[Pfenning] p. 127	Definition =I	natded 27814
[Ponnusamy] p. 361	Theorem 6.44	cphip0l 23378  df-dip 28107  dip0l 28124  ip0l 20350
[Ponnusamy] p. 361	Equation 6.45	cphipval 23418  ipval 28109
[Ponnusamy] p. 362	Equation I1	dipcj 28120  ipcj 20348
[Ponnusamy] p. 362	Equation I3	cphdir 23381  dipdir 28248  ipdir 20353  ipdiri 28236
[Ponnusamy] p. 362	Equation I4	ipidsq 28116  nmsq 23370
[Ponnusamy] p. 362	Equation 6.46	ip0i 28231
[Ponnusamy] p. 362	Equation 6.47	ip1i 28233
[Ponnusamy] p. 362	Equation 6.48	ip2i 28234
[Ponnusamy] p. 363	Equation I2	cphass 23387  dipass 28251  ipass 20359  ipassi 28247
[Prugovecki] p. 186	Definition of bra	braval 29354  df-bra 29260
[Prugovecki] p. 376	Equation 8.1	df-kb 29261  kbval 29364
[PtakPulmannova] p. 66	Proposition 3.2.17	atomli 29792
[PtakPulmannova] p. 68	Lemma 3.1.4	df-pclN 35958
[PtakPulmannova] p. 68	Lemma 3.2.20	atcvat3i 29806  atcvat4i 29807  cvrat3 35512  cvrat4 35513  lsatcvat3 35122
[PtakPulmannova] p. 68	Definition 3.2.18	cvbr 29692  cvrval 35339  df-cv 29689  df-lcv 35089  lspsncv0 19513
[PtakPulmannova] p. 72	Lemma 3.3.6	pclfinN 35970
[PtakPulmannova] p. 74	Lemma 3.3.10	pclcmpatN 35971
[Quine] p. 16	Definition 2.1	df-clab 2812  rabid 3326
[Quine] p. 17	Definition 2.1''	dfsb7 2589
[Quine] p. 18	Definition 2.7	df-cleq 2818
[Quine] p. 19	Definition 2.9	conventions 27811  df-v 3416
[Quine] p. 34	Theorem 5.1	abeq2 2937
[Quine] p. 35	Theorem 5.2	abid1 2949  abid2f 2996
[Quine] p. 40	Theorem 6.1	sb5 2308
[Quine] p. 40	Theorem 6.2	sb56 2305  sb6 2307
[Quine] p. 41	Theorem 6.3	df-clel 2821
[Quine] p. 41	Theorem 6.4	eqid 2825  eqid1 27877
[Quine] p. 41	Theorem 6.5	eqcom 2832
[Quine] p. 42	Theorem 6.6	df-sbc 3663
[Quine] p. 42	Theorem 6.7	dfsbcq 3664  dfsbcq2 3665
[Quine] p. 43	Theorem 6.8	vex 3417
[Quine] p. 43	Theorem 6.9	isset 3424
[Quine] p. 44	Theorem 7.3	spcgf 3505  spcgv 3510  spcimgf 3503
[Quine] p. 44	Theorem 6.11	spsbc 3675  spsbcd 3676
[Quine] p. 44	Theorem 6.12	elex 3429
[Quine] p. 44	Theorem 6.13	elab 3571  elabg 3569  elabgf 3567
[Quine] p. 44	Theorem 6.14	noel 4150
[Quine] p. 48	Theorem 7.2	snprc 4473
[Quine] p. 48	Definition 7.1	df-pr 4402  df-sn 4400
[Quine] p. 49	Theorem 7.4	snss 4537  snssg 4536
[Quine] p. 49	Theorem 7.5	prss 4571  prssg 4570
[Quine] p. 49	Theorem 7.6	prid1 4517  prid1g 4515  prid2 4518  prid2g 4516  snid 4431  snidg 4429
[Quine] p. 51	Theorem 7.12	snex 5131
[Quine] p. 51	Theorem 7.13	prex 5132
[Quine] p. 53	Theorem 8.2	unisn 4676  unisnALT 39975  unisng 4675
[Quine] p. 53	Theorem 8.3	uniun 4681
[Quine] p. 54	Theorem 8.6	elssuni 4691
[Quine] p. 54	Theorem 8.7	uni0 4689
[Quine] p. 56	Theorem 8.17	uniabio 6100
[Quine] p. 56	Definition 8.18	dfaiota2 41977  dfiota2 6091
[Quine] p. 57	Theorem 8.19	aiotaval 41984  iotaval 6101
[Quine] p. 57	Theorem 8.22	iotanul 6105
[Quine] p. 58	Theorem 8.23	iotaex 6107
[Quine] p. 58	Definition 9.1	df-op 4406
[Quine] p. 61	Theorem 9.5	opabid 5210  opelopab 5225  opelopaba 5219  opelopabaf 5227  opelopabf 5228  opelopabg 5221  opelopabga 5216  opelopabgf 5223  oprabid 6941
[Quine] p. 64	Definition 9.11	df-xp 5352
[Quine] p. 64	Definition 9.12	df-cnv 5354
[Quine] p. 64	Definition 9.15	df-id 5252
[Quine] p. 65	Theorem 10.3	fun0 6191
[Quine] p. 65	Theorem 10.4	funi 6159
[Quine] p. 65	Theorem 10.5	funsn 6179  funsng 6177
[Quine] p. 65	Definition 10.1	df-fun 6129
[Quine] p. 65	Definition 10.2	args 5738  dffv4 6434
[Quine] p. 68	Definition 10.11	conventions 27811  df-fv 6135  fv2 6432
[Quine] p. 124	Theorem 17.3	nn0opth2 13359  nn0opth2i 13358  nn0opthi 13357  omopthi 8009
[Quine] p. 177	Definition 25.2	df-rdg 7777
[Quine] p. 232	Equation i	carddom 9698
[Quine] p. 284	Axiom 39(vi)	funimaex 6213  funimaexg 6212
[Quine] p. 331	Axiom system NF	ru 3661
[ReedSimon] p. 36	Definition (iii)	ax-his3 28492
[ReedSimon] p. 63	Exercise 4(a)	df-dip 28107  polid 28567  polid2i 28565  polidi 28566
[ReedSimon] p. 63	Exercise 4(b)	df-ph 28219
[ReedSimon] p. 195	Remark	lnophm 29429  lnophmi 29428
[Retherford] p. 49	Exercise 1(i)	leopadd 29542
[Retherford] p. 49	Exercise 1(ii)	leopmul 29544  leopmuli 29543
[Retherford] p. 49	Exercise 1(iv)	leoptr 29547
[Retherford] p. 49	Definition VI.1	df-leop 29262  leoppos 29536
[Retherford] p. 49	Exercise 1(iii)	leoptri 29546
[Retherford] p. 49	Definition of operator ordering	leop3 29535
[Roman] p. 4	Definition	df-dmat 20671  df-dmatalt 43048
[Roman] p. 18	Part Preliminaries	df-rng0 42736
[Roman] p. 19	Part Preliminaries	df-ring 18910
[Roman] p. 46	Theorem 1.6	isldepslvec2 43135
[Roman] p. 112	Note	isldepslvec2 43135  ldepsnlinc 43158  zlmodzxznm 43147
[Roman] p. 112	Example	zlmodzxzequa 43146  zlmodzxzequap 43149  zlmodzxzldep 43154
[Roman] p. 170	Theorem 7.8	cayleyhamilton 21072
[Rosenlicht] p. 80	Theorem	heicant 33983
[Rosser] p. 281	Definition	df-op 4406
[RosserSchoenfeld] p. 71	Theorem 12.	ax-ros335 31268
[RosserSchoenfeld] p. 71	Theorem 13.	ax-ros336 31269
[Rotman] p. 28	Remark	pgrpgt2nabl 43008  pmtr3ncom 18252
[Rotman] p. 31	Theorem 3.4	symggen2 18248
[Rotman] p. 42	Theorem 3.15	cayley 18191  cayleyth 18192
[Rudin] p. 164	Equation 27	efcan 15205
[Rudin] p. 164	Equation 30	efzval 15211
[Rudin] p. 167	Equation 48	absefi 15305
[Sanford] p. 39	Remark	ax-mp 5  mto 189
[Sanford] p. 39	Rule 3	mtpxor 1870
[Sanford] p. 39	Rule 4	mptxor 1868
[Sanford] p. 40	Rule 1	mptnan 1867
[Schechter] p. 51	Definition of antisymmetry	intasym 5757
[Schechter] p. 51	Definition of irreflexivity	intirr 5760
[Schechter] p. 51	Definition of symmetry	cnvsym 5756
[Schechter] p. 51	Definition of transitivity	cotr 5753
[Schechter] p. 78	Definition of Moore collection of sets	df-mre 16606
[Schechter] p. 79	Definition of Moore closure	df-mrc 16607
[Schechter] p. 82	Section 4.5	df-mrc 16607
[Schechter] p. 84	Definition (A) of an algebraic closure system	df-acs 16609
[Schechter] p. 139	Definition AC3	dfac9 9280
[Schechter] p. 141	Definition (MC)	dfac11 38470
[Schechter] p. 149	Axiom DC1	ax-dc 9590  axdc3 9598
[Schechter] p. 187	Definition of ring with unit	isring 18912  isrngo 34233
[Schechter] p. 276	Remark 11.6.e	span0 28952
[Schechter] p. 276	Definition of span	df-span 28719  spanval 28743
[Schechter] p. 428	Definition 15.35	bastop1 21175
[Schwabhauser] p. 10	Axiom A1	axcgrrflx 26220  axtgcgrrflx 25781
[Schwabhauser] p. 10	Axiom A2	axcgrtr 26221
[Schwabhauser] p. 10	Axiom A3	axcgrid 26222  axtgcgrid 25782
[Schwabhauser] p. 10	Axioms A1 to A3	df-trkgc 25767
[Schwabhauser] p. 11	Axiom A4	axsegcon 26233  axtgsegcon 25783  df-trkgcb 25769
[Schwabhauser] p. 11	Axiom A5	ax5seg 26244  axtg5seg 25784  df-trkgcb 25769
[Schwabhauser] p. 11	Axiom A6	axbtwnid 26245  axtgbtwnid 25785  df-trkgb 25768
[Schwabhauser] p. 12	Axiom A7	axpasch 26247  axtgpasch 25786  df-trkgb 25768
[Schwabhauser] p. 12	Axiom A8	axlowdim2 26266  df-trkg2d 31288
[Schwabhauser] p. 13	Axiom A8	axtglowdim2 25789
[Schwabhauser] p. 13	Axiom A9	axtgupdim2 25790  df-trkg2d 31288
[Schwabhauser] p. 13	Axiom A10	axeuclid 26269  axtgeucl 25791  df-trkge 25770
[Schwabhauser] p. 13	Axiom A11	axcont 26282  axtgcont 25788  axtgcont1 25787  df-trkgb 25768
[Schwabhauser] p. 27	Theorem 2.1	cgrrflx 32628
[Schwabhauser] p. 27	Theorem 2.2	cgrcomim 32630
[Schwabhauser] p. 27	Theorem 2.3	cgrtr 32633
[Schwabhauser] p. 27	Theorem 2.4	cgrcoml 32637
[Schwabhauser] p. 27	Theorem 2.5	cgrcomr 32638  tgcgrcomimp 25796  tgcgrcoml 25798  tgcgrcomr 25797
[Schwabhauser] p. 28	Theorem 2.8	cgrtriv 32643  tgcgrtriv 25803
[Schwabhauser] p. 28	Theorem 2.10	5segofs 32647  tg5segofs 31296
[Schwabhauser] p. 28	Definition 2.10	df-afs 31293  df-ofs 32624
[Schwabhauser] p. 29	Theorem 2.11	cgrextend 32649  tgcgrextend 25804
[Schwabhauser] p. 29	Theorem 2.12	segconeq 32651  tgsegconeq 25805
[Schwabhauser] p. 30	Theorem 3.1	btwnouttr2 32663  btwntriv2 32653  tgbtwntriv2 25806
[Schwabhauser] p. 30	Theorem 3.2	btwncomim 32654  tgbtwncom 25807
[Schwabhauser] p. 30	Theorem 3.3	btwntriv1 32657  tgbtwntriv1 25810
[Schwabhauser] p. 30	Theorem 3.4	btwnswapid 32658  tgbtwnswapid 25811
[Schwabhauser] p. 30	Theorem 3.5	btwnexch2 32664  btwnintr 32660  tgbtwnexch2 25815  tgbtwnintr 25812
[Schwabhauser] p. 30	Theorem 3.6	btwnexch 32666  btwnexch3 32661  tgbtwnexch 25817  tgbtwnexch3 25813
[Schwabhauser] p. 30	Theorem 3.7	btwnouttr 32665  tgbtwnouttr 25816  tgbtwnouttr2 25814
[Schwabhauser] p. 32	Theorem 3.13	axlowdim1 26265
[Schwabhauser] p. 32	Theorem 3.14	btwndiff 32668  tgbtwndiff 25825
[Schwabhauser] p. 33	Theorem 3.17	tgtrisegint 25818  trisegint 32669
[Schwabhauser] p. 34	Theorem 4.2	ifscgr 32685  tgifscgr 25827
[Schwabhauser] p. 34	Theorem 4.11	colcom 25877  colrot1 25878  colrot2 25879  lncom 25941  lnrot1 25942  lnrot2 25943
[Schwabhauser] p. 34	Definition 4.1	df-ifs 32681
[Schwabhauser] p. 35	Theorem 4.3	cgrsub 32686  tgcgrsub 25828
[Schwabhauser] p. 35	Theorem 4.5	cgrxfr 32696  tgcgrxfr 25837
[Schwabhauser] p. 35	Statement 4.4	ercgrg 25836
[Schwabhauser] p. 35	Definition 4.4	df-cgr3 32682  df-cgrg 25830
[Schwabhauser] p. 35	Definition instead (given	df-cgrg 25830
[Schwabhauser] p. 36	Theorem 4.6	btwnxfr 32697  tgbtwnxfr 25849
[Schwabhauser] p. 36	Theorem 4.11	colinearperm1 32703  colinearperm2 32705  colinearperm3 32704  colinearperm4 32706  colinearperm5 32707
[Schwabhauser] p. 36	Definition 4.8	df-ismt 25852
[Schwabhauser] p. 36	Definition 4.10	df-colinear 32680  tgellng 25872  tglng 25865
[Schwabhauser] p. 37	Theorem 4.12	colineartriv1 32708
[Schwabhauser] p. 37	Theorem 4.13	colinearxfr 32716  lnxfr 25885
[Schwabhauser] p. 37	Theorem 4.14	lineext 32717  lnext 25886
[Schwabhauser] p. 37	Theorem 4.16	fscgr 32721  tgfscgr 25887
[Schwabhauser] p. 37	Theorem 4.17	linecgr 32722  lncgr 25888
[Schwabhauser] p. 37	Definition 4.15	df-fs 32683
[Schwabhauser] p. 38	Theorem 4.18	lineid 32724  lnid 25889
[Schwabhauser] p. 38	Theorem 4.19	idinside 32725  tgidinside 25890
[Schwabhauser] p. 39	Theorem 5.1	btwnconn1 32742  tgbtwnconn1 25894
[Schwabhauser] p. 41	Theorem 5.2	btwnconn2 32743  tgbtwnconn2 25895
[Schwabhauser] p. 41	Theorem 5.3	btwnconn3 32744  tgbtwnconn3 25896
[Schwabhauser] p. 41	Theorem 5.5	brsegle2 32750
[Schwabhauser] p. 41	Definition 5.4	df-segle 32748  legov 25904
[Schwabhauser] p. 41	Definition 5.5	legov2 25905
[Schwabhauser] p. 42	Remark 5.13	legso 25918
[Schwabhauser] p. 42	Theorem 5.6	seglecgr12im 32751
[Schwabhauser] p. 42	Theorem 5.7	seglerflx 32753
[Schwabhauser] p. 42	Theorem 5.8	segletr 32755
[Schwabhauser] p. 42	Theorem 5.9	segleantisym 32756
[Schwabhauser] p. 42	Theorem 5.10	seglelin 32757
[Schwabhauser] p. 42	Theorem 5.11	seglemin 32754
[Schwabhauser] p. 42	Theorem 5.12	colinbtwnle 32759
[Schwabhauser] p. 42	Proposition 5.7	legid 25906
[Schwabhauser] p. 42	Proposition 5.8	legtrd 25908
[Schwabhauser] p. 42	Proposition 5.9	legtri3 25909
[Schwabhauser] p. 42	Proposition 5.10	legtrid 25910
[Schwabhauser] p. 42	Proposition 5.11	leg0 25911
[Schwabhauser] p. 43	Theorem 6.2	btwnoutside 32766
[Schwabhauser] p. 43	Theorem 6.3	broutsideof3 32767
[Schwabhauser] p. 43	Theorem 6.4	broutsideof 32762  df-outsideof 32761
[Schwabhauser] p. 43	Definition 6.1	broutsideof2 32763  ishlg 25921
[Schwabhauser] p. 44	Theorem 6.4	hlln 25926
[Schwabhauser] p. 44	Theorem 6.5	hlid 25928  outsideofrflx 32768
[Schwabhauser] p. 44	Theorem 6.6	hlcomb 25922  hlcomd 25923  outsideofcom 32769
[Schwabhauser] p. 44	Theorem 6.7	hltr 25929  outsideoftr 32770
[Schwabhauser] p. 44	Theorem 6.11	hlcgreu 25937  outsideofeu 32772
[Schwabhauser] p. 44	Definition 6.8	df-ray 32779
[Schwabhauser] p. 45	Part 2	df-lines2 32780
[Schwabhauser] p. 45	Theorem 6.13	outsidele 32773
[Schwabhauser] p. 45	Theorem 6.15	lineunray 32788
[Schwabhauser] p. 45	Theorem 6.16	lineelsb2 32789  tglineelsb2 25951
[Schwabhauser] p. 45	Theorem 6.17	linecom 32791  linerflx1 32790  linerflx2 32792  tglinecom 25954  tglinerflx1 25952  tglinerflx2 25953
[Schwabhauser] p. 45	Theorem 6.18	linethru 32794  tglinethru 25955
[Schwabhauser] p. 45	Definition 6.14	df-line2 32778  tglng 25865
[Schwabhauser] p. 45	Proposition 6.13	legbtwn 25913
[Schwabhauser] p. 46	Theorem 6.19	linethrueu 32797  tglinethrueu 25958
[Schwabhauser] p. 46	Theorem 6.21	lineintmo 32798  tglineineq 25962  tglineinteq 25964  tglineintmo 25961
[Schwabhauser] p. 46	Theorem 6.23	colline 25968
[Schwabhauser] p. 46	Theorem 6.24	tglowdim2l 25969
[Schwabhauser] p. 46	Theorem 6.25	tglowdim2ln 25970
[Schwabhauser] p. 49	Theorem 7.3	mirinv 25985
[Schwabhauser] p. 49	Theorem 7.7	mirmir 25981
[Schwabhauser] p. 49	Theorem 7.8	mirreu3 25973
[Schwabhauser] p. 49	Definition 7.5	df-mir 25972  ismir 25978  mirbtwn 25977  mircgr 25976  mirfv 25975  mirval 25974
[Schwabhauser] p. 50	Theorem 7.8	mirreu 25983
[Schwabhauser] p. 50	Theorem 7.9	mireq 25984
[Schwabhauser] p. 50	Theorem 7.10	mirinv 25985
[Schwabhauser] p. 50	Theorem 7.11	mirf1o 25988
[Schwabhauser] p. 50	Theorem 7.13	miriso 25989
[Schwabhauser] p. 51	Theorem 7.14	mirmot 25994
[Schwabhauser] p. 51	Theorem 7.15	mirbtwnb 25991  mirbtwni 25990
[Schwabhauser] p. 51	Theorem 7.16	mircgrs 25992
[Schwabhauser] p. 51	Theorem 7.17	miduniq 26004
[Schwabhauser] p. 52	Lemma 7.21	symquadlem 26008
[Schwabhauser] p. 52	Theorem 7.18	miduniq1 26005
[Schwabhauser] p. 52	Theorem 7.19	miduniq2 26006
[Schwabhauser] p. 52	Theorem 7.20	colmid 26007
[Schwabhauser] p. 53	Lemma 7.22	krippen 26010
[Schwabhauser] p. 55	Lemma 7.25	midexlem 26011
[Schwabhauser] p. 57	Theorem 8.2	ragcom 26017
[Schwabhauser] p. 57	Definition 8.1	df-rag 26013  israg 26016
[Schwabhauser] p. 58	Theorem 8.3	ragcol 26018
[Schwabhauser] p. 58	Theorem 8.4	ragmir 26019
[Schwabhauser] p. 58	Theorem 8.5	ragtrivb 26021
[Schwabhauser] p. 58	Theorem 8.6	ragflat2 26022
[Schwabhauser] p. 58	Theorem 8.7	ragflat 26023
[Schwabhauser] p. 58	Theorem 8.8	ragtriva 26024
[Schwabhauser] p. 58	Theorem 8.9	ragflat3 26025  ragncol 26028
[Schwabhauser] p. 58	Theorem 8.10	ragcgr 26026
[Schwabhauser] p. 59	Theorem 8.12	perpcom 26032
[Schwabhauser] p. 59	Theorem 8.13	ragperp 26036
[Schwabhauser] p. 59	Theorem 8.14	perpneq 26033
[Schwabhauser] p. 59	Definition 8.11	df-perpg 26015  isperp 26031
[Schwabhauser] p. 59	Definition 8.13	isperp2 26034
[Schwabhauser] p. 60	Theorem 8.18	foot 26038
[Schwabhauser] p. 62	Lemma 8.20	colperpexlem1 26046  colperpexlem2 26047
[Schwabhauser] p. 63	Theorem 8.21	colperpex 26049  colperpexlem3 26048
[Schwabhauser] p. 64	Theorem 8.22	mideu 26054  midex 26053
[Schwabhauser] p. 66	Lemma 8.24	opphllem 26051
[Schwabhauser] p. 67	Theorem 9.2	oppcom 26060
[Schwabhauser] p. 67	Definition 9.1	islnopp 26055
[Schwabhauser] p. 68	Lemma 9.3	opphllem2 26064
[Schwabhauser] p. 68	Lemma 9.4	opphllem5 26067  opphllem6 26068
[Schwabhauser] p. 69	Theorem 9.5	opphl 26070
[Schwabhauser] p. 69	Theorem 9.6	axtgpasch 25786
[Schwabhauser] p. 70	Theorem 9.6	outpasch 26071
[Schwabhauser] p. 71	Theorem 9.8	lnopp2hpgb 26079
[Schwabhauser] p. 71	Definition 9.7	df-hpg 26074  hpgbr 26076
[Schwabhauser] p. 72	Lemma 9.10	hpgerlem 26081
[Schwabhauser] p. 72	Theorem 9.9	lnoppnhpg 26080
[Schwabhauser] p. 72	Theorem 9.11	hpgid 26082
[Schwabhauser] p. 72	Theorem 9.12	hpgcom 26083
[Schwabhauser] p. 72	Theorem 9.13	hpgtr 26084
[Schwabhauser] p. 73	Theorem 9.18	colopp 26085
[Schwabhauser] p. 73	Theorem 9.19	colhp 26086
[Schwabhauser] p. 88	Theorem 10.2	lmieu 26100
[Schwabhauser] p. 88	Definition 10.1	df-mid 26090
[Schwabhauser] p. 89	Theorem 10.4	lmicom 26104
[Schwabhauser] p. 89	Theorem 10.5	lmilmi 26105
[Schwabhauser] p. 89	Theorem 10.6	lmireu 26106
[Schwabhauser] p. 89	Theorem 10.7	lmieq 26107
[Schwabhauser] p. 89	Theorem 10.8	lmiinv 26108
[Schwabhauser] p. 89	Theorem 10.9	lmif1o 26111
[Schwabhauser] p. 89	Theorem 10.10	lmiiso 26113
[Schwabhauser] p. 89	Definition 10.3	df-lmi 26091
[Schwabhauser] p. 90	Theorem 10.11	lmimot 26114
[Schwabhauser] p. 91	Theorem 10.12	hypcgr 26117
[Schwabhauser] p. 92	Theorem 10.14	lmiopp 26118
[Schwabhauser] p. 92	Theorem 10.15	lnperpex 26119
[Schwabhauser] p. 92	Theorem 10.16	trgcopy 26120  trgcopyeu 26122
[Schwabhauser] p. 95	Definition 11.2	dfcgra2 26145
[Schwabhauser] p. 95	Definition 11.3	iscgra 26125
[Schwabhauser] p. 95	Proposition 11.4	cgracgr 26134
[Schwabhauser] p. 95	Proposition 11.10	cgrahl1 26132  cgrahl2 26133
[Schwabhauser] p. 96	Theorem 11.6	cgraid 26135
[Schwabhauser] p. 96	Theorem 11.9	cgraswap 26136
[Schwabhauser] p. 97	Theorem 11.7	cgracom 26138
[Schwabhauser] p. 97	Theorem 11.8	cgratr 26139
[Schwabhauser] p. 97	Theorem 11.21	cgrabtwn 26141  cgrahl 26142
[Schwabhauser] p. 98	Theorem 11.13	sacgr 26146
[Schwabhauser] p. 98	Theorem 11.14	oacgr 26148
[Schwabhauser] p. 98	Theorem 11.15	acopy 26149  acopyeu 26150
[Schwabhauser] p. 101	Theorem 11.24	inagswap 26155
[Schwabhauser] p. 101	Theorem 11.25	inaghl 26156
[Schwabhauser] p. 101	Property for point ` ` to lie in the angle ` ` Defnition 11.23	isinag 26154
[Schwabhauser] p. 102	Lemma 11.28	cgrg3col4 26159
[Schwabhauser] p. 102	Definition 11.27	df-leag 26157  isleag 26158
[Schwabhauser] p. 107	Theorem 11.49	tgsas 26161  tgsas1 26160  tgsas2 26162  tgsas3 26163
[Schwabhauser] p. 108	Theorem 11.50	tgasa 26165  tgasa1 26164
[Schwabhauser] p. 109	Theorem 11.51	tgsss1 26166  tgsss2 26167  tgsss3 26168
[Shapiro] p. 230	Theorem 6.5.1	dchrhash 25416  dchrsum 25414  dchrsum2 25413  sumdchr 25417
[Shapiro] p. 232	Theorem 6.5.2	dchr2sum 25418  sum2dchr 25419
[Shapiro], p. 199	Lemma 6.1C.2	ablfacrp 18826  ablfacrp2 18827
[Shapiro], p. 328	Equation 9.2.4	vmasum 25361
[Shapiro], p. 329	Equation 9.2.7	logfac2 25362
[Shapiro], p. 329	Equation 9.2.9	logfacrlim 25369
[Shapiro], p. 331	Equation 9.2.13	vmadivsum 25591
[Shapiro], p. 331	Equation 9.2.14	rplogsumlem2 25594
[Shapiro], p. 336	Exercise 9.1.7	vmalogdivsum 25648  vmalogdivsum2 25647
[Shapiro], p. 375	Theorem 9.4.1	dirith 25638  dirith2 25637
[Shapiro], p. 375	Equation 9.4.3	rplogsum 25636  rpvmasum 25635  rpvmasum2 25621
[Shapiro], p. 376	Equation 9.4.7	rpvmasumlem 25596
[Shapiro], p. 376	Equation 9.4.8	dchrvmasum 25634
[Shapiro], p. 377	Lemma 9.4.1	dchrisum 25601  dchrisumlem1 25598  dchrisumlem2 25599  dchrisumlem3 25600  dchrisumlema 25597
[Shapiro], p. 377	Equation 9.4.11	dchrvmasumlem1 25604
[Shapiro], p. 379	Equation 9.4.16	dchrmusum 25633  dchrmusumlem 25631  dchrvmasumlem 25632
[Shapiro], p. 380	Lemma 9.4.2	dchrmusum2 25603
[Shapiro], p. 380	Lemma 9.4.3	dchrvmasum2lem 25605
[Shapiro], p. 382	Lemma 9.4.4	dchrisum0 25629  dchrisum0re 25622  dchrisumn0 25630
[Shapiro], p. 382	Equation 9.4.27	dchrisum0fmul 25615
[Shapiro], p. 382	Equation 9.4.29	dchrisum0flb 25619
[Shapiro], p. 383	Equation 9.4.30	dchrisum0fno1 25620
[Shapiro], p. 403	Equation 10.1.16	pntrsumbnd 25675  pntrsumbnd2 25676  pntrsumo1 25674
[Shapiro], p. 405	Equation 10.2.1	mudivsum 25639
[Shapiro], p. 406	Equation 10.2.6	mulogsum 25641
[Shapiro], p. 407	Equation 10.2.7	mulog2sumlem1 25643
[Shapiro], p. 407	Equation 10.2.8	mulog2sum 25646
[Shapiro], p. 418	Equation 10.4.6	logsqvma 25651
[Shapiro], p. 418	Equation 10.4.8	logsqvma2 25652
[Shapiro], p. 419	Equation 10.4.10	selberg 25657
[Shapiro], p. 420	Equation 10.4.12	selberg2lem 25659
[Shapiro], p. 420	Equation 10.4.14	selberg2 25660
[Shapiro], p. 422	Equation 10.6.7	selberg3 25668
[Shapiro], p. 422	Equation 10.4.20	selberg4lem1 25669
[Shapiro], p. 422	Equation 10.4.21	selberg3lem1 25666  selberg3lem2 25667
[Shapiro], p. 422	Equation 10.4.23	selberg4 25670
[Shapiro], p. 427	Theorem 10.5.2	chpdifbnd 25664
[Shapiro], p. 428	Equation 10.6.2	selbergr 25677
[Shapiro], p. 429	Equation 10.6.8	selberg3r 25678
[Shapiro], p. 430	Equation 10.6.11	selberg4r 25679
[Shapiro], p. 431	Equation 10.6.15	pntrlog2bnd 25693
[Shapiro], p. 434	Equation 10.6.27	pntlema 25705  pntlemb 25706  pntlemc 25704  pntlemd 25703  pntlemg 25707
[Shapiro], p. 435	Equation 10.6.29	pntlema 25705
[Shapiro], p. 436	Lemma 10.6.1	pntpbnd 25697
[Shapiro], p. 436	Lemma 10.6.2	pntibnd 25702
[Shapiro], p. 436	Equation 10.6.34	pntlema 25705
[Shapiro], p. 436	Equation 10.6.35	pntlem3 25718  pntleml 25720
[Stoll] p. 13	Definition corresponds to	dfsymdif3 4124
[Stoll] p. 16	Exercise 4.4	0dif 4204  dif0 4182
[Stoll] p. 16	Exercise 4.8	difdifdir 4281
[Stoll] p. 17	Theorem 5.1(5)	unvdif 4267
[Stoll] p. 19	Theorem 5.2(13)	undm 4117
[Stoll] p. 19	Theorem 5.2(13')	indm 4118
[Stoll] p. 20	Remark	invdif 4100
[Stoll] p. 25	Definition of ordered triple	df-ot 4408
[Stoll] p. 43	Definition	uniiun 4795
[Stoll] p. 44	Definition	intiin 4796
[Stoll] p. 45	Definition	df-iin 4745
[Stoll] p. 45	Definition indexed union	df-iun 4744
[Stoll] p. 176	Theorem 3.4(27)	iman 392
[Stoll] p. 262	Example 4.1	dfsymdif3 4124
[Strang] p. 242	Section 6.3	expgrowth 39369
[Suppes] p. 22	Theorem 2	eq0 4160  eq0f 4157
[Suppes] p. 22	Theorem 4	eqss 3842  eqssd 3844  eqssi 3843
[Suppes] p. 23	Theorem 5	ss0 4201  ss0b 4200
[Suppes] p. 23	Theorem 6	sstr 3835  sstrALT2 39884
[Suppes] p. 23	Theorem 7	pssirr 3935
[Suppes] p. 23	Theorem 8	pssn2lp 3936
[Suppes] p. 23	Theorem 9	psstr 3939
[Suppes] p. 23	Theorem 10	pssss 3930
[Suppes] p. 25	Theorem 12	elin 4025  elun 3982
[Suppes] p. 26	Theorem 15	inidm 4049
[Suppes] p. 26	Theorem 16	in0 4195
[Suppes] p. 27	Theorem 23	unidm 3985
[Suppes] p. 27	Theorem 24	un0 4194
[Suppes] p. 27	Theorem 25	ssun1 4005
[Suppes] p. 27	Theorem 26	ssequn1 4012
[Suppes] p. 27	Theorem 27	unss 4016
[Suppes] p. 27	Theorem 28	indir 4107
[Suppes] p. 27	Theorem 29	undir 4108
[Suppes] p. 28	Theorem 32	difid 4180
[Suppes] p. 29	Theorem 33	difin 4093
[Suppes] p. 29	Theorem 34	indif 4101
[Suppes] p. 29	Theorem 35	undif1 4268
[Suppes] p. 29	Theorem 36	difun2 4273
[Suppes] p. 29	Theorem 37	difin0 4266
[Suppes] p. 29	Theorem 38	disjdif 4265
[Suppes] p. 29	Theorem 39	difundi 4111
[Suppes] p. 29	Theorem 40	difindi 4113
[Suppes] p. 30	Theorem 41	nalset 5022
[Suppes] p. 39	Theorem 61	uniss 4683
[Suppes] p. 39	Theorem 65	uniop 5203
[Suppes] p. 41	Theorem 70	intsn 4735
[Suppes] p. 42	Theorem 71	intpr 4732  intprg 4733
[Suppes] p. 42	Theorem 73	op1stb 5162
[Suppes] p. 42	Theorem 78	intun 4731
[Suppes] p. 44	Definition 15(a)	dfiun2 4776  dfiun2g 4774
[Suppes] p. 44	Definition 15(b)	dfiin2 4777
[Suppes] p. 47	Theorem 86	elpw 4386  elpw2 5052  elpw2g 5051  elpwg 4388  elpwgdedVD 39966
[Suppes] p. 47	Theorem 87	pwid 4396
[Suppes] p. 47	Theorem 89	pw0 4563
[Suppes] p. 48	Theorem 90	pwpw0 4564
[Suppes] p. 52	Theorem 101	xpss12 5361
[Suppes] p. 52	Theorem 102	xpindi 5492  xpindir 5493
[Suppes] p. 52	Theorem 103	xpundi 5408  xpundir 5409
[Suppes] p. 54	Theorem 105	elirrv 8777
[Suppes] p. 58	Theorem 2	relss 5445
[Suppes] p. 59	Theorem 4	eldm 5557  eldm2 5558  eldm2g 5556  eldmg 5555
[Suppes] p. 59	Definition 3	df-dm 5356
[Suppes] p. 60	Theorem 6	dmin 5568
[Suppes] p. 60	Theorem 8	rnun 5786
[Suppes] p. 60	Theorem 9	rnin 5787
[Suppes] p. 60	Definition 4	dfrn2 5547
[Suppes] p. 61	Theorem 11	brcnv 5541  brcnvg 5538
[Suppes] p. 62	Equation 5	elcnv 5535  elcnv2 5536
[Suppes] p. 62	Theorem 12	relcnv 5748
[Suppes] p. 62	Theorem 15	cnvin 5785
[Suppes] p. 62	Theorem 16	cnvun 5783
[Suppes] p. 63	Definition	dftrrels2 34864
[Suppes] p. 63	Theorem 20	co02 5894
[Suppes] p. 63	Theorem 21	dmcoss 5622
[Suppes] p. 63	Definition 7	df-co 5355
[Suppes] p. 64	Theorem 26	cnvco 5544
[Suppes] p. 64	Theorem 27	coass 5899
[Suppes] p. 65	Theorem 31	resundi 5651
[Suppes] p. 65	Theorem 34	elima 5716  elima2 5717  elima3 5718  elimag 5715
[Suppes] p. 65	Theorem 35	imaundi 5790
[Suppes] p. 66	Theorem 40	dminss 5792
[Suppes] p. 66	Theorem 41	imainss 5793
[Suppes] p. 67	Exercise 11	cnvxp 5796
[Suppes] p. 81	Definition 34	dfec2 8017
[Suppes] p. 82	Theorem 72	elec 8056  elecALTV 34579  elecg 8055
[Suppes] p. 82	Theorem 73	eqvrelth 34896  erth 8061  erth2 8062
[Suppes] p. 83	Theorem 74	eqvreldisj 34899  erdisj 8064
[Suppes] p. 89	Theorem 96	map0b 8168
[Suppes] p. 89	Theorem 97	map0 8171  map0g 8169
[Suppes] p. 89	Theorem 98	mapsn 8172  mapsnd 8170
[Suppes] p. 89	Theorem 99	mapss 8173
[Suppes] p. 91	Definition 12(ii)	alephsuc 9211
[Suppes] p. 91	Definition 12(iii)	alephlim 9210
[Suppes] p. 92	Theorem 1	enref 8261  enrefg 8260
[Suppes] p. 92	Theorem 2	ensym 8277  ensymb 8276  ensymi 8278
[Suppes] p. 92	Theorem 3	entr 8280
[Suppes] p. 92	Theorem 4	unen 8315
[Suppes] p. 94	Theorem 15	endom 8255
[Suppes] p. 94	Theorem 16	ssdomg 8274
[Suppes] p. 94	Theorem 17	domtr 8281
[Suppes] p. 95	Theorem 18	sbth 8355
[Suppes] p. 97	Theorem 23	canth2 8388  canth2g 8389
[Suppes] p. 97	Definition 3	brsdom2 8359  df-sdom 8231  dfsdom2 8358
[Suppes] p. 97	Theorem 21(i)	sdomirr 8372
[Suppes] p. 97	Theorem 22(i)	domnsym 8361
[Suppes] p. 97	Theorem 21(ii)	sdomnsym 8360
[Suppes] p. 97	Theorem 22(ii)	domsdomtr 8370
[Suppes] p. 97	Theorem 22(iv)	brdom2 8258
[Suppes] p. 97	Theorem 21(iii)	sdomtr 8373
[Suppes] p. 97	Theorem 22(iii)	sdomdomtr 8368
[Suppes] p. 98	Exercise 4	fundmen 8302  fundmeng 8303
[Suppes] p. 98	Exercise 6	xpdom3 8333
[Suppes] p. 98	Exercise 11	sdomentr 8369
[Suppes] p. 104	Theorem 37	fofi 8527
[Suppes] p. 104	Theorem 38	pwfi 8536
[Suppes] p. 105	Theorem 40	pwfi 8536
[Suppes] p. 111	Axiom for cardinal numbers	carden 9695
[Suppes] p. 130	Definition 3	df-tr 4978
[Suppes] p. 132	Theorem 9	ssonuni 7252
[Suppes] p. 134	Definition 6	df-suc 5973
[Suppes] p. 136	Theorem Schema 22	findes 7362  finds 7358  finds1 7361  finds2 7360
[Suppes] p. 151	Theorem 42	isfinite 8833  isfinite2 8493  isfiniteg 8495  unbnn 8491
[Suppes] p. 162	Definition 5	df-ltnq 10062  df-ltpq 10054
[Suppes] p. 197	Theorem Schema 4	tfindes 7328  tfinds 7325  tfinds2 7329
[Suppes] p. 209	Theorem 18	oaord1 7903
[Suppes] p. 209	Theorem 21	oaword2 7905
[Suppes] p. 211	Theorem 25	oaass 7913
[Suppes] p. 225	Definition 8	iscard2 9122
[Suppes] p. 227	Theorem 56	ondomon 9707
[Suppes] p. 228	Theorem 59	harcard 9124
[Suppes] p. 228	Definition 12(i)	aleph0 9209
[Suppes] p. 228	Theorem Schema 61	onintss 6017
[Suppes] p. 228	Theorem Schema 62	onminesb 7264  onminsb 7265
[Suppes] p. 229	Theorem 64	alephval2 9716
[Suppes] p. 229	Theorem 65	alephcard 9213
[Suppes] p. 229	Theorem 66	alephord2i 9220
[Suppes] p. 229	Theorem 67	alephnbtwn 9214
[Suppes] p. 229	Definition 12	df-aleph 9086
[Suppes] p. 242	Theorem 6	weth 9639
[Suppes] p. 242	Theorem 8	entric 9701
[Suppes] p. 242	Theorem 9	carden 9695
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2803
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2818
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2821
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2820
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2846
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 6914
[TakeutiZaring] p. 14	Proposition 4.14	ru 3661
[TakeutiZaring] p. 15	Axiom 2	zfpair 5127
[TakeutiZaring] p. 15	Exercise 1	elpr 4422  elpr2 4423  elprg 4420
[TakeutiZaring] p. 15	Exercise 2	elsn 4414  elsn2 4434  elsn2g 4433  elsng 4413  velsn 4415
[TakeutiZaring] p. 15	Exercise 3	elop 5158
[TakeutiZaring] p. 15	Exercise 4	sneq 4409  sneqr 4589
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 4418  dfsn2 4412  dfsn2ALT 4419
[TakeutiZaring] p. 16	Axiom 3	uniex 7218
[TakeutiZaring] p. 16	Exercise 6	opth 5167
[TakeutiZaring] p. 16	Exercise 7	opex 5155
[TakeutiZaring] p. 16	Exercise 8	rext 5139
[TakeutiZaring] p. 16	Corollary 5.8	unex 7221  unexg 7224
[TakeutiZaring] p. 16	Definition 5.3	dftp2 4452
[TakeutiZaring] p. 16	Definition 5.5	df-uni 4661
[TakeutiZaring] p. 16	Definition 5.6	df-in 3805  df-un 3803
[TakeutiZaring] p. 16	Proposition 5.7	unipr 4673  uniprg 4674
[TakeutiZaring] p. 17	Axiom 4	vpwex 5079
[TakeutiZaring] p. 17	Exercise 1	eltp 4451
[TakeutiZaring] p. 17	Exercise 5	elsuc 6036  elsucg 6034  sstr2 3834
[TakeutiZaring] p. 17	Exercise 6	uncom 3986
[TakeutiZaring] p. 17	Exercise 7	incom 4034
[TakeutiZaring] p. 17	Exercise 8	unass 3999
[TakeutiZaring] p. 17	Exercise 9	inass 4050
[TakeutiZaring] p. 17	Exercise 10	indi 4105
[TakeutiZaring] p. 17	Exercise 11	undi 4106
[TakeutiZaring] p. 17	Definition 5.9	df-pss 3814  dfss2 3815
[TakeutiZaring] p. 17	Definition 5.10	df-pw 4382
[TakeutiZaring] p. 18	Exercise 7	unss2 4013
[TakeutiZaring] p. 18	Exercise 9	df-ss 3812  sseqin2 4046
[TakeutiZaring] p. 18	Exercise 10	ssid 3848
[TakeutiZaring] p. 18	Exercise 12	inss1 4059  inss2 4060
[TakeutiZaring] p. 18	Exercise 13	nss 3888
[TakeutiZaring] p. 18	Exercise 15	unieq 4668
[TakeutiZaring] p. 18	Exercise 18	sspwb 5140  sspwimp 39967  sspwimpALT 39974  sspwimpALT2 39977  sspwimpcf 39969
[TakeutiZaring] p. 18	Exercise 19	pweqb 5148
[TakeutiZaring] p. 19	Axiom 5	ax-rep 4996
[TakeutiZaring] p. 20	Definition	df-rab 3126
[TakeutiZaring] p. 20	Corollary 5.16	0ex 5016
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3801
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 4148
[TakeutiZaring] p. 20	Proposition 5.15	difid 4180
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0 4162  n0f 4159  neq0 4161  neq0f 4158
[TakeutiZaring] p. 21	Axiom 6	zfreg 8776
[TakeutiZaring] p. 21	Axiom 6'	zfregs 8892
[TakeutiZaring] p. 21	Theorem 5.22	setind 8894
[TakeutiZaring] p. 21	Definition 5.20	df-v 3416
[TakeutiZaring] p. 21	Proposition 5.21	vprc 5024
[TakeutiZaring] p. 22	Exercise 1	0ss 4199
[TakeutiZaring] p. 22	Exercise 3	ssex 5029  ssexg 5031
[TakeutiZaring] p. 22	Exercise 4	inex1 5026
[TakeutiZaring] p. 22	Exercise 5	ruv 8783
[TakeutiZaring] p. 22	Exercise 6	elirr 8778
[TakeutiZaring] p. 22	Exercise 7	ssdif0 4173
[TakeutiZaring] p. 22	Exercise 11	difdif 3965
[TakeutiZaring] p. 22	Exercise 13	undif3 4120  undif3VD 39931
[TakeutiZaring] p. 22	Exercise 14	difss 3966
[TakeutiZaring] p. 22	Exercise 15	sscon 3973
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 3122
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 3123
[TakeutiZaring] p. 23	Proposition 6.2	xpex 7228  xpexg 7225
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 5353
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 6197
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 6351  fun11 6200
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 6139  svrelfun 6198
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 5546
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 5548
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 5358
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 5359
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 5355
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5833  dfrel2 5828
[TakeutiZaring] p. 25	Exercise 3	xpss 5362
[TakeutiZaring] p. 25	Exercise 5	relun 5473
[TakeutiZaring] p. 25	Exercise 6	reluni 5480
[TakeutiZaring] p. 25	Exercise 9	inxp 5491
[TakeutiZaring] p. 25	Exercise 12	relres 5666
[TakeutiZaring] p. 25	Exercise 13	opelres 5639  opelresi 5641
[TakeutiZaring] p. 25	Exercise 14	dmres 5659
[TakeutiZaring] p. 25	Exercise 15	resss 5662
[TakeutiZaring] p. 25	Exercise 17	resabs1 5667
[TakeutiZaring] p. 25	Exercise 18	funres 6169
[TakeutiZaring] p. 25	Exercise 24	relco 5878
[TakeutiZaring] p. 25	Exercise 29	funco 6167
[TakeutiZaring] p. 25	Exercise 30	f1co 6352
[TakeutiZaring] p. 26	Definition 6.10	eu2 2694
[TakeutiZaring] p. 26	Definition 6.11	conventions 27811  df-fv 6135  fv3 6455
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 7380  cnvexg 7379
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 7366  dmexg 7363
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 7367  rnexg 7364
[TakeutiZaring] p. 26	Corollary 6.9(1)	xpexb 39491
[TakeutiZaring] p. 26	Corollary 6.9(2)	xpexcnv 7375
[TakeutiZaring] p. 27	Corollary 6.13	fvex 6450
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1-afv 42070  tz6.12-1-afv2 42137  tz6.12-1 6459  tz6.12-afv 42069  tz6.12-afv2 42136  tz6.12 6460  tz6.12c-afv2 42138  tz6.12c 6462
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2-afv2 42133  tz6.12-2 6427  tz6.12i-afv2 42139  tz6.12i 6463
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 6130
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 6131
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 6133  wfo 6125
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 6132  wf1 6124
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 6134  wf1o 6126
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 6565  eqfnfv2 6566  eqfnfv2f 6569
[TakeutiZaring] p. 28	Exercise 5	fvco 6525
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 6742
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 6740
[TakeutiZaring] p. 29	Exercise 9	funimaex 6213  funimaexg 6212
[TakeutiZaring] p. 29	Definition 6.18	df-br 4876
[TakeutiZaring] p. 29	Definition 6.19(1)	df-so 5266
[TakeutiZaring] p. 30	Definition 6.21	dffr2 5311  dffr3 5743  eliniseg 5739  iniseg 5741
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 5257
[TakeutiZaring] p. 30	Proposition 6.23	fr2nr 5324  fr3nr 7245  frirr 5323
[TakeutiZaring] p. 30	Definition 6.24(1)	df-fr 5305
[TakeutiZaring] p. 30	Definition 6.24(2)	dfwe2 7247
[TakeutiZaring] p. 31	Exercise 1	frss 5313
[TakeutiZaring] p. 31	Exercise 4	wess 5333
[TakeutiZaring] p. 31	Proposition 6.26	tz6.26 5955  tz6.26i 5956  wefrc 5340  wereu2 5343
[TakeutiZaring] p. 32	Theorem 6.27	wfi 5957  wfii 5958
[TakeutiZaring] p. 32	Definition 6.28	df-isom 6136
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 6839
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 6840
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 6846
[TakeutiZaring] p. 33	Proposition 6.31(1)	isomin 6847
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 6848
[TakeutiZaring] p. 33	Proposition 6.32(1)	isofr 6852
[TakeutiZaring] p. 33	Proposition 6.32(3)	isowe 6859
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 6861
[TakeutiZaring] p. 35	Notation	wtr 4977
[TakeutiZaring] p. 35	Theorem 7.2	trelpss 39492  tz7.2 5330
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4981
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 5980
[TakeutiZaring] p. 36	Proposition 7.5	tz7.5 5988
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 5989  ordelordALT 39576  ordelordALTVD 39916
[TakeutiZaring] p. 37	Corollary 7.8	ordelpss 5995  ordelssne 5994
[TakeutiZaring] p. 37	Proposition 7.7	tz7.7 5993
[TakeutiZaring] p. 37	Proposition 7.9	ordin 5997
[TakeutiZaring] p. 38	Corollary 7.14	ordeleqon 7254
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 7255
[TakeutiZaring] p. 38	Definition 7.11	df-on 5971
[TakeutiZaring] p. 38	Proposition 7.10	ordtri3or 5999
[TakeutiZaring] p. 38	Proposition 7.12	onfrALT 39588  ordon 7249
[TakeutiZaring] p. 38	Proposition 7.13	onprc 7250
[TakeutiZaring] p. 39	Theorem 7.17	tfi 7319
[TakeutiZaring] p. 40	Exercise 3	ontr2 6014
[TakeutiZaring] p. 40	Exercise 7	dftr2 4979
[TakeutiZaring] p. 40	Exercise 9	onssmin 7263
[TakeutiZaring] p. 40	Exercise 11	unon 7297
[TakeutiZaring] p. 40	Exercise 12	ordun 6068
[TakeutiZaring] p. 40	Exercise 14	ordequn 6067
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 7251
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 4691
[TakeutiZaring] p. 41	Definition 7.22	df-suc 5973
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 6044  sucidg 6045
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 7279
[TakeutiZaring] p. 41	Proposition 7.25	onnbtwn 6058  ordnbtwn 6057
[TakeutiZaring] p. 41	Proposition 7.26	onsucuni 7294
[TakeutiZaring] p. 42	Exercise 1	df-lim 5972
[TakeutiZaring] p. 42	Exercise 4	omssnlim 7345
[TakeutiZaring] p. 42	Exercise 7	ssnlim 7349
[TakeutiZaring] p. 42	Exercise 8	onsucssi 7307  ordelsuc 7286
[TakeutiZaring] p. 42	Exercise 9	ordsucelsuc 7288
[TakeutiZaring] p. 42	Definition 7.27	nlimon 7317
[TakeutiZaring] p. 42	Definition 7.28	dfom2 7333
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 7351
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 7352
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 7353
[TakeutiZaring] p. 43	Remark	omon 7342
[TakeutiZaring] p. 43	Axiom 7	inf3 8816  omex 8824
[TakeutiZaring] p. 43	Theorem 7.32	ordom 7340
[TakeutiZaring] p. 43	Corollary 7.31	find 7357
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 7354
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 7355
[TakeutiZaring] p. 44	Exercise 1	limomss 7336
[TakeutiZaring] p. 44	Exercise 2	int0 4713
[TakeutiZaring] p. 44	Exercise 3	trintss 4995
[TakeutiZaring] p. 44	Exercise 4	intss1 4714
[TakeutiZaring] p. 44	Exercise 5	intex 5044
[TakeutiZaring] p. 44	Exercise 6	oninton 7266
[TakeutiZaring] p. 44	Exercise 11	ordintdif 6016
[TakeutiZaring] p. 44	Definition 7.35	df-int 4700
[TakeutiZaring] p. 44	Proposition 7.34	noinfep 8841
[TakeutiZaring] p. 45	Exercise 4	onint 7261
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 7743
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfr1 7764
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfr2 7765
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfr3 7766
[TakeutiZaring] p. 49	Theorem 7.44	tz7.44-1 7773  tz7.44-2 7774  tz7.44-3 7775
[TakeutiZaring] p. 50	Exercise 1	smogt 7735
[TakeutiZaring] p. 50	Exercise 3	smoiso 7730
[TakeutiZaring] p. 50	Definition 7.46	df-smo 7714
[TakeutiZaring] p. 51	Proposition 7.49	tz7.49 7811  tz7.49c 7812
[TakeutiZaring] p. 51	Proposition 7.48(1)	tz7.48-1 7809
[TakeutiZaring] p. 51	Proposition 7.48(2)	tz7.48-2 7808
[TakeutiZaring] p. 51	Proposition 7.48(3)	tz7.48-3 7810
[TakeutiZaring] p. 53	Proposition 7.53	2eu5 2737
[TakeutiZaring] p. 54	Proposition 7.56(1)	leweon 9154
[TakeutiZaring] p. 54	Proposition 7.58(1)	r0weon 9155
[TakeutiZaring] p. 56	Definition 8.1	oalim 7884  oasuc 7876
[TakeutiZaring] p. 57	Remark	tfindsg 7326
[TakeutiZaring] p. 57	Proposition 8.2	oacl 7887
[TakeutiZaring] p. 57	Proposition 8.3	oa0 7868  oa0r 7890
[TakeutiZaring] p. 57	Proposition 8.16	omcl 7888
[TakeutiZaring] p. 58	Corollary 8.5	oacan 7900
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 7971  nnaordi 7970  oaord 7899  oaordi 7898
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 4787  uniss2 4694
[TakeutiZaring] p. 59	Proposition 8.7	oawordri 7902
[TakeutiZaring] p. 59	Proposition 8.8	oawordeu 7907  oawordex 7909
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 7963
[TakeutiZaring] p. 59	Proposition 8.10	oaabs 7996
[TakeutiZaring] p. 60	Remark	oancom 8832
[TakeutiZaring] p. 60	Proposition 8.11	oalimcl 7912
[TakeutiZaring] p. 62	Exercise 1	nnarcl 7968
[TakeutiZaring] p. 62	Exercise 5	oaword1 7904
[TakeutiZaring] p. 62	Definition 8.15	om0x 7871  omlim 7885  omsuc 7878
[TakeutiZaring] p. 62	Definition 8.15(a)	om0 7869
[TakeutiZaring] p. 63	Proposition 8.17	nnecl 7965  nnmcl 7964
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 7984  nnmordi 7983  omord 7920  omordi 7918
[TakeutiZaring] p. 63	Proposition 8.20	omcan 7921
[TakeutiZaring] p. 63	Proposition 8.21	nnmwordri 7988  omwordri 7924
[TakeutiZaring] p. 63	Proposition 8.18(1)	om0r 7891
[TakeutiZaring] p. 63	Proposition 8.18(2)	om1 7894  om1r 7895
[TakeutiZaring] p. 64	Proposition 8.22	om00 7927
[TakeutiZaring] p. 64	Proposition 8.23	omordlim 7929
[TakeutiZaring] p. 64	Proposition 8.24	omlimcl 7930
[TakeutiZaring] p. 64	Proposition 8.25	odi 7931
[TakeutiZaring] p. 65	Theorem 8.26	omass 7932
[TakeutiZaring] p. 67	Definition 8.30	nnesuc 7960  oe0 7874  oelim 7886  oesuc 7879  onesuc 7882
[TakeutiZaring] p. 67	Proposition 8.31	oe0m0 7872
[TakeutiZaring] p. 67	Proposition 8.32	oen0 7938
[TakeutiZaring] p. 67	Proposition 8.33	oeordi 7939
[TakeutiZaring] p. 67	Proposition 8.31(2)	oe0m1 7873
[TakeutiZaring] p. 67	Proposition 8.31(3)	oe1m 7897
[TakeutiZaring] p. 68	Corollary 8.34	oeord 7940
[TakeutiZaring] p. 68	Corollary 8.36	oeordsuc 7946
[TakeutiZaring] p. 68	Proposition 8.35	oewordri 7944
[TakeutiZaring] p. 68	Proposition 8.37	oeworde 7945
[TakeutiZaring] p. 69	Proposition 8.41	oeoa 7949
[TakeutiZaring] p. 70	Proposition 8.42	oeoe 7951
[TakeutiZaring] p. 73	Theorem 9.1	trcl 8888  tz9.1 8889
[TakeutiZaring] p. 76	Definition 9.9	df-r1 8911  r10 8915  r1lim 8919  r1limg 8918  r1suc 8917  r1sucg 8916
[TakeutiZaring] p. 77	Proposition 9.10(2)	r1ord 8927  r1ord2 8928  r1ordg 8925
[TakeutiZaring] p. 78	Proposition 9.12	tz9.12 8937
[TakeutiZaring] p. 78	Proposition 9.13	rankwflem 8962  tz9.13 8938  tz9.13g 8939
[TakeutiZaring] p. 79	Definition 9.14	df-rank 8912  rankval 8963  rankvalb 8944  rankvalg 8964
[TakeutiZaring] p. 79	Proposition 9.16	rankel 8986  rankelb 8971
[TakeutiZaring] p. 79	Proposition 9.17	rankuni2b 9000  rankval3 8987  rankval3b 8973
[TakeutiZaring] p. 79	Proposition 9.18	rankonid 8976
[TakeutiZaring] p. 79	Proposition 9.15(1)	rankon 8942
[TakeutiZaring] p. 79	Proposition 9.15(2)	rankr1 8981  rankr1c 8968  rankr1g 8979
[TakeutiZaring] p. 79	Proposition 9.15(3)	ssrankr1 8982
[TakeutiZaring] p. 80	Exercise 1	rankss 8996  rankssb 8995
[TakeutiZaring] p. 80	Exercise 2	unbndrank 8989
[TakeutiZaring] p. 80	Proposition 9.19	bndrank 8988
[TakeutiZaring] p. 83	Axiom of Choice	ac4 9619  dfac3 9264
[TakeutiZaring] p. 84	Theorem 10.3	dfac8a 9173  numth 9616  numth2 9615
[TakeutiZaring] p. 85	Definition 10.4	cardval 9690
[TakeutiZaring] p. 85	Proposition 10.5	cardid 9691  cardid2 9099
[TakeutiZaring] p. 85	Proposition 10.9	oncard 9106
[TakeutiZaring] p. 85	Proposition 10.10	carden 9695
[TakeutiZaring] p. 85	Proposition 10.11	cardidm 9105
[TakeutiZaring] p. 85	Proposition 10.6(1)	cardon 9090
[TakeutiZaring] p. 85	Proposition 10.6(2)	cardne 9111
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 9103
[TakeutiZaring] p. 87	Proposition 10.15	pwen 8408
[TakeutiZaring] p. 88	Exercise 1	en0 8291
[TakeutiZaring] p. 88	Exercise 7	infensuc 8413
[TakeutiZaring] p. 89	Exercise 10	omxpen 8337
[TakeutiZaring] p. 90	Corollary 10.23	cardnn 9109
[TakeutiZaring] p. 90	Definition 10.27	alephiso 9241
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 8418
[TakeutiZaring] p. 90	Proposition 10.22	onomeneq 8425
[TakeutiZaring] p. 90	Proposition 10.26	alephprc 9242
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 8423
[TakeutiZaring] p. 91	Exercise 2	alephle 9231
[TakeutiZaring] p. 91	Exercise 3	aleph0 9209
[TakeutiZaring] p. 91	Exercise 4	cardlim 9118
[TakeutiZaring] p. 91	Exercise 7	infpss 9361
[TakeutiZaring] p. 91	Exercise 8	infcntss 8509
[TakeutiZaring] p. 91	Definition 10.29	df-fin 8232  isfi 8252
[TakeutiZaring] p. 92	Proposition 10.32	onfin 8426
[TakeutiZaring] p. 92	Proposition 10.34	imadomg 9678
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 8330
[TakeutiZaring] p. 93	Proposition 10.35	fodomb 9670
[TakeutiZaring] p. 93	Proposition 10.36	cdaxpdom 9333  unxpdom 8442
[TakeutiZaring] p. 93	Proposition 10.37	cardsdomel 9120  cardsdomelir 9119
[TakeutiZaring] p. 93	Proposition 10.38	sucxpdom 8444
[TakeutiZaring] p. 94	Proposition 10.39	infxpen 9157
[TakeutiZaring] p. 95	Definition 10.42	df-map 8129
[TakeutiZaring] p. 95	Proposition 10.40	infxpidm 9706  infxpidm2 9160
[TakeutiZaring] p. 95	Proposition 10.41	infcda 9352  infxp 9359
[TakeutiZaring] p. 96	Proposition 10.44	pw2en 8342  pw2f1o 8340
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 8401
[TakeutiZaring] p. 97	Theorem 10.46	ac6s3 9631
[TakeutiZaring] p. 98	Theorem 10.46	ac6c5 9626  ac6s5 9635
[TakeutiZaring] p. 98	Theorem 10.47	unidom 9687
[TakeutiZaring] p. 99	Theorem 10.48	uniimadom 9688  uniimadomf 9689
[TakeutiZaring] p. 100	Definition 11.1	cfcof 9418
[TakeutiZaring] p. 101	Proposition 11.7	cofsmo 9413
[TakeutiZaring] p. 102	Exercise 1	cfle 9398
[TakeutiZaring] p. 102	Exercise 2	cf0 9395
[TakeutiZaring] p. 102	Exercise 3	cfsuc 9401
[TakeutiZaring] p. 102	Exercise 4	cfom 9408
[TakeutiZaring] p. 102	Proposition 11.9	coftr 9417
[TakeutiZaring] p. 103	Theorem 11.15	alephreg 9726
[TakeutiZaring] p. 103	Proposition 11.11	cardcf 9396
[TakeutiZaring] p. 103	Proposition 11.13	alephsing 9420
[TakeutiZaring] p. 104	Corollary 11.17	cardinfima 9240
[TakeutiZaring] p. 104	Proposition 11.16	carduniima 9239
[TakeutiZaring] p. 104	Proposition 11.18	alephfp 9251  alephfp2 9252
[TakeutiZaring] p. 106	Theorem 11.20	gchina 9843
[TakeutiZaring] p. 106	Theorem 11.21	mappwen 9255
[TakeutiZaring] p. 107	Theorem 11.26	konigth 9713
[TakeutiZaring] p. 108	Theorem 11.28	pwcfsdom 9727
[TakeutiZaring] p. 108	Theorem 11.29	cfpwsdom 9728
[Tarski] p. 67	Axiom B5	ax-c5 34953
[Tarski] p. 67	Scheme B5	sp 2224
[Tarski] p. 68	Lemma 6	avril1 27873  equid 2116
[Tarski] p. 69	Lemma 7	equcomi 2121
[Tarski] p. 70	Lemma 14	spim 2407  spime 2409  spimeh 2101
[Tarski] p. 70	Lemma 16	ax-12 2220  ax-c15 34959  ax12i 2066
[Tarski] p. 70	Lemmas 16 and 17	sb6 2307
[Tarski] p. 75	Axiom B7	ax6v 2076
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-5 2009  ax5ALT 34977
[Tarski], p. 75	Scheme B8 of system S2	ax-7 2112  ax-8 2166  ax-9 2173
[Tarski1999] p. 178	Axiom 4	axtgsegcon 25783
[Tarski1999] p. 178	Axiom 5	axtg5seg 25784
[Tarski1999] p. 179	Axiom 7	axtgpasch 25786
[Tarski1999] p. 180	Axiom 7.1	axtgpasch 25786
[Tarski1999] p. 185	Axiom 11	axtgcont1 25787
[Truss] p. 114	Theorem 5.18	ruc 15353
[Viaclovsky7] p. 3	Corollary 0.3	mblfinlem3 33987
[Viaclovsky8] p. 3	Proposition 7	ismblfin 33989
[Weierstrass] p. 272	Definition	df-mdet 20766  mdetuni 20803
[WhiteheadRussell] p. 96	Axiom *1.2	pm1.2 932
[WhiteheadRussell] p. 96	Axiom *1.3	olc 899
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 900
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 948
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 995
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 181
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 133
[WhiteheadRussell] p. 100	Theorem *2.04	pm2.04 90  wl-luk-pm2.04 33809
[WhiteheadRussell] p. 100	Theorem *2.05	frege5 38929  imim2 58  wl-luk-imim2 33804
[WhiteheadRussell] p. 100	Theorem *2.06	imim1 83
[WhiteheadRussell] p. 101	Theorem *2.1	pm2.1 925
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2746  syl 17
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 931
[WhiteheadRussell] p. 101	Theorem *2.08	id 22  wl-luk-id 33807
[WhiteheadRussell] p. 101	Theorem *2.11	exmid 923
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 139
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13 926
[WhiteheadRussell] p. 102	Theorem *2.14	notnotr 128  notnotrALT2 39976  wl-luk-notnotr 33808
[WhiteheadRussell] p. 102	Theorem *2.15	con1 146
[WhiteheadRussell] p. 103	Theorem *2.16	ax-frege28 38959  axfrege28 38958  con3 151
[WhiteheadRussell] p. 103	Theorem *2.17	ax-3 8
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18 125
[WhiteheadRussell] p. 104	Theorem *2.2	orc 898
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 953
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 121  wl-luk-pm2.21 33801
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 122
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25 918
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26 968
[WhiteheadRussell] p. 104	Theorem *2.27	conventions-labels 27812  pm2.27 42  wl-luk-pm2.27 33799
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 951
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 952
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 997
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 998
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 996
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 1112
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 935
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 936
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 971
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 56
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 910
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 911
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5 166
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6 183
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 912
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 913
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 914
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 167
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 169
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 882
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54 883
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 917
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 919
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61 184
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 928
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 969
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 970
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 185
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 920  pm2.67 921
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521 168
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 927
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 1000
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68 929
[WhiteheadRussell] p. 108	Theorem *2.69	looinv 195
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 1001
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 1002
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 962
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 960
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 999
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 1003
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 84
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85 961
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 109
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 1019
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 463  pm3.2im 159
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11 1020
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12 1021
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13 1022
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 1023
[WhiteheadRussell] p. 111	Theorem *3.21	pm3.21 465
[WhiteheadRussell] p. 111	Theorem *3.22	pm3.22 453
[WhiteheadRussell] p. 111	Theorem *3.24	pm3.24 393
[WhiteheadRussell] p. 112	Theorem *3.35	pm3.35 837
[WhiteheadRussell] p. 112	Theorem *3.3 (Exp)	pm3.3 441
[WhiteheadRussell] p. 112	Theorem *3.31 (Imp)	pm3.31 442
[WhiteheadRussell] p. 112	Theorem *3.26 (Simp)	simpl 476  simplim 165
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 479  simprim 164
[WhiteheadRussell] p. 112	Theorem *3.33 (Syll)	pm3.33 781
[WhiteheadRussell] p. 112	Theorem *3.34 (Syll)	pm3.34 782
[WhiteheadRussell] p. 112	Theorem *3.37 (Transp)	pm3.37 842
[WhiteheadRussell] p. 113	Fact)	pm3.45 615
[WhiteheadRussell] p. 113	Theorem *3.4	pm3.4 844
[WhiteheadRussell] p. 113	Theorem *3.41	pm3.41 488
[WhiteheadRussell] p. 113	Theorem *3.42	pm3.42 489
[WhiteheadRussell] p. 113	Theorem *3.44	jao 988  pm3.44 987
[WhiteheadRussell] p. 113	Theorem *3.47	prth 843
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 467
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 991
[WhiteheadRussell] p. 116	Theorem *4.1	con34b 308
[WhiteheadRussell] p. 117	Theorem *4.2	biid 253
[WhiteheadRussell] p. 117	Theorem *4.11	notbi 311
[WhiteheadRussell] p. 117	Theorem *4.12	con2bi 345
[WhiteheadRussell] p. 117	Theorem *4.13	notnotb 307
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14 841
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 866
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 214
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 840  bitr 839
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 559
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 933  pm4.25 934
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 454
[WhiteheadRussell] p. 118	Theorem *4.4	andi 1035
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 901
[WhiteheadRussell] p. 118	Theorem *4.32	anass 462
[WhiteheadRussell] p. 118	Theorem *4.33	orass 950
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 625
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 946
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 628
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 1004
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 1113
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 1033
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42 1080
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 1051
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 1024
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 1026  pm4.45 1025  pm4.45im 863
[WhiteheadRussell] p. 120	Theorem *4.5	anor 1010
[WhiteheadRussell] p. 120	Theorem *4.6	imor 884
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 541
[WhiteheadRussell] p. 120	Theorem *4.51	ianor 1009
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52 1012
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53 1013
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54 1014
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55 1015
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 1011  pm4.56 1016
[WhiteheadRussell] p. 120	Theorem *4.57	oran 1017  pm4.57 1018
[WhiteheadRussell] p. 120	Theorem *4.61	pm4.61 395
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62 887
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63 388
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64 880
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65 396
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66 881
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67 389
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 553  pm4.71d 557  pm4.71i 555  pm4.71r 554  pm4.71rd 558  pm4.71ri 556
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 977
[WhiteheadRussell] p. 121	Theorem *4.73	iba 523
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 965
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 513  pm4.76 514
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 989  pm4.77 990
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78 963
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79 1031
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 383
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81 384
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 1052
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83 1053
[WhiteheadRussell] p. 122	Theorem *4.84	imbi1 339
[WhiteheadRussell] p. 122	Theorem *4.85	imbi2 340
[WhiteheadRussell] p. 122	Theorem *4.86	bibi1 343
[WhiteheadRussell] p. 122	Theorem *4.87	bi2.04 379  impexp 443  pm4.87 874
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 859
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11 972
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12 973
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13 975
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14 974
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15 1041
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 1042
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17 1040
[WhiteheadRussell] p. 124	Theorem *5.18	nbbn 375  pm5.18 373
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 378
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 860
[WhiteheadRussell] p. 124	Theorem *5.22	xor 1043
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3 1076
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24 1077
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2 930
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 568
[WhiteheadRussell] p. 125	Theorem *5.4	pm5.4 380
[WhiteheadRussell] p. 125	Theorem *5.5	pm5.5 353
[WhiteheadRussell] p. 125	Theorem *5.6	pm5.6 1029
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7 981
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 865
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 569
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 869
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 861
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 867
[WhiteheadRussell] p. 125	Theorem *5.41	imdi 381  pm5.41 382
[WhiteheadRussell] p. 125	Theorem *5.42	pm5.42 539
[WhiteheadRussell] p. 125	Theorem *5.44	pm5.44 538
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 1032
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54 1046
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55 976
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 1028
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62 1047
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63 1048
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71 1056
[WhiteheadRussell] p. 125	Theorem *5.501	pm5.501 358
[WhiteheadRussell] p. 126	Theorem *5.74	pm5.74 262
[WhiteheadRussell] p. 126	Theorem *5.75	pm5.75 1057
[WhiteheadRussell] p. 146	Theorem *10.12	pm10.12 39392
[WhiteheadRussell] p. 146	Theorem *10.14	pm10.14 39393
[WhiteheadRussell] p. 147	Theorem *10.22	19.26 1972
[WhiteheadRussell] p. 149	Theorem *10.251	pm10.251 39394
[WhiteheadRussell] p. 149	Theorem *10.252	pm10.252 39395
[WhiteheadRussell] p. 149	Theorem *10.253	pm10.253 39396
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1995
[WhiteheadRussell] p. 151	Theorem *10.301	albitr 39397
[WhiteheadRussell] p. 155	Theorem *10.42	pm10.42 39398
[WhiteheadRussell] p. 155	Theorem *10.52	pm10.52 39399
[WhiteheadRussell] p. 155	Theorem *10.53	pm10.53 39400
[WhiteheadRussell] p. 155	Theorem *10.541	pm10.541 39401
[WhiteheadRussell] p. 156	Theorem *10.55	pm10.55 39403
[WhiteheadRussell] p. 156	Theorem *10.56	pm10.56 39404
[WhiteheadRussell] p. 156	Theorem *10.57	pm10.57 39405
[WhiteheadRussell] p. 156	Theorem *10.542	pm10.542 39402
[WhiteheadRussell] p. 159	Axiom *11.07	pm11.07 2581
[WhiteheadRussell] p. 159	Theorem *11.11	pm11.11 39408
[WhiteheadRussell] p. 159	Theorem *11.12	pm11.12 39409
[WhiteheadRussell] p. 159	Theorem PM*11.1	2stdpc4 2484
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 2210
[WhiteheadRussell] p. 160	Theorem *11.22	2exnaln 1927
[WhiteheadRussell] p. 160	Theorem *11.25	2nexaln 1928
[WhiteheadRussell] p. 161	Theorem *11.3	19.21vv 39410
[WhiteheadRussell] p. 162	Theorem *11.32	2alim 39411
[WhiteheadRussell] p. 162	Theorem *11.33	2albi 39412
[WhiteheadRussell] p. 162	Theorem *11.34	2exim 39413
[WhiteheadRussell] p. 162	Theorem *11.36	spsbce-2 39415
[WhiteheadRussell] p. 162	Theorem *11.341	2exbi 39414
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1989
[WhiteheadRussell] p. 163	Theorem *11.43	19.36vv 39417
[WhiteheadRussell] p. 163	Theorem *11.44	19.31vv 39418
[WhiteheadRussell] p. 163	Theorem *11.421	19.33-2 39416
[WhiteheadRussell] p. 164	Theorem *11.5	2nalexn 1926
[WhiteheadRussell] p. 164	Theorem *11.46	19.37vv 39419
[WhiteheadRussell] p. 164	Theorem *11.47	19.28vv 39420
[WhiteheadRussell] p. 164	Theorem *11.51	2exnexn 1945
[WhiteheadRussell] p. 164	Theorem *11.52	pm11.52 39421
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 2370
[WhiteheadRussell] p. 164	Theorem *11.521	2exanali 39422
[WhiteheadRussell] p. 165	Theorem *11.6	pm11.6 39427
[WhiteheadRussell] p. 165	Theorem *11.56	aaanv 39423
[WhiteheadRussell] p. 165	Theorem *11.57	pm11.57 39424
[WhiteheadRussell] p. 165	Theorem *11.58	pm11.58 39425
[WhiteheadRussell] p. 165	Theorem *11.59	pm11.59 39426
[WhiteheadRussell] p. 166	Theorem *11.7	pm11.7 39431
[WhiteheadRussell] p. 166	Theorem *11.61	pm11.61 39428
[WhiteheadRussell] p. 166	Theorem *11.62	pm11.62 39429
[WhiteheadRussell] p. 166	Theorem *11.63	pm11.63 39430
[WhiteheadRussell] p. 166	Theorem *11.71	pm11.71 39432
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2640
[WhiteheadRussell] p. 178	Theorem *13.13	pm13.13a 39442  pm13.13b 39443
[WhiteheadRussell] p. 178	Theorem *13.14	pm13.14 39444
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 3080
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 3081
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 3563
[WhiteheadRussell] p. 179	Theorem *13.21	2sbc6g 39450
[WhiteheadRussell] p. 179	Theorem *13.22	2sbc5g 39451
[WhiteheadRussell] p. 179	Theorem *13.192	pm13.192 39445
[WhiteheadRussell] p. 179	Theorem *13.193	2pm13.193 39591  pm13.193 39446
[WhiteheadRussell] p. 179	Theorem *13.194	pm13.194 39447
[WhiteheadRussell] p. 179	Theorem *13.195	pm13.195 39448
[WhiteheadRussell] p. 179	Theorem *13.196	pm13.196a 39449
[WhiteheadRussell] p. 184	Theorem *14.12	pm14.12 39456
[WhiteheadRussell] p. 184	Theorem *14.111	iotasbc2 39455
[WhiteheadRussell] p. 184	Definition *14.01	iotasbc 39454
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3715
[WhiteheadRussell] p. 185	Theorem *14.122	pm14.122a 39457  pm14.122b 39458  pm14.122c 39459
[WhiteheadRussell] p. 185	Theorem *14.123	pm14.123a 39460  pm14.123b 39461  pm14.123c 39462
[WhiteheadRussell] p. 189	Theorem *14.2	iotaequ 39464
[WhiteheadRussell] p. 189	Theorem *14.18	pm14.18 39463
[WhiteheadRussell] p. 189	Theorem *14.202	iotavalb 39465
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 6108
[WhiteheadRussell] p. 190	Theorem *14.205	iotasbc5 39466
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 6109
[WhiteheadRussell] p. 191	Theorem *14.24	pm14.24 39467
[WhiteheadRussell] p. 192	Theorem *14.25	sbiota1 39469
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2716  eupickbi 2719  sbaniota 39470
[WhiteheadRussell] p. 192	Theorem *14.242	iotavalsb 39468
[WhiteheadRussell] p. 192	Theorem *14.271	eubi 2657
[WhiteheadRussell] p. 193	Theorem *14.272	iotasbcq 39472
[WhiteheadRussell] p. 235	Definition *30.01	conventions 27811  df-fv 6135
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 9146  pm54.43lem 9145
[Young] p. 141	Definition of operator ordering	leop2 29534
[Young] p. 142	Example 12.2(i)	0leop 29540  idleop 29541
[vandenDries] p. 42	Lemma 61	irrapx1 38231
[vandenDries] p. 43	Theorem 62	pellex 38238  pellexlem1 38232

This page was last updated on 1-Apr-2023.

Copyright terms: Public domain