Most Recent Proofs - Metamath Proof Explorer

Most Recent Proofs    These are the 10 (GIF, Unicode) or 100 (GIF, Unicode) most recent proofs in the Metamath Proof Explorer and the Hilbert Space Explorer. The stable set.mm database file in the Metamath program download is sometimes several days behind the preproduction set.mm (7MB) or set.mm.bz2 (compressed, 2MB) that corresponds to this page. Email: Norm Megill. Wikis: AsteroidMeta (Recent Changes); Ghilbert site; Ghilbert Google Group. Mailing list: Metamath Google Group. Syndication: RSS feed (web version) courtesy of Dan Getz.

Last updated on 12-Mar-2010 at 7:40 AM ET.

Recent Additions to the Metamath Proof Explorer   Notes (last updated 24-Jun-09 )   News (last updated 28-Feb-10 )

Date	Label	Description
Theorem
11-Mar-2010	eujust 1421	A soundness justification theorem for df-eu 1422, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 1391.
|- (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z))
22-Feb-2010	sbcrexg 2046	Interchange class substitution and restricted existential quantifier.
|- (A e. C -> ([A / x]E.y e. B ph <-> E.y e. B [A / x]ph))
22-Feb-2010	sbcralg 2045	Interchange class substitution and restricted quantifier.
|- (A e. C -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))
22-Feb-2010	sbcrext 2042	Interchange class substitution and restricted existential quantifier. (Unnecessary distinct variable restrictions were removed by David Abernethy, 22-Feb-2010.)
|- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / x]E.y e. B ph <-> E.y e. B [A / x]ph))
22-Feb-2010	sbcralt 2041	Interchange class substitution and restricted quantifier. (Unnecessary distinct variable restrictions were removed by David Abernethy, 22-Feb-2010.)
|- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))
18-Feb-2010	dvrunz 10971	In a division ring the unit is different from the zero.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   &   |- Z = (Id` G)   &   |- U = (Id` H)   =>   |- (R e. DivRing -> U =/= Z)
18-Feb-2010	uznzr 10968	In a unital ring the zero equals the unity iff the ring is the zero ring.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- Z = (Id` G)   &   |- U = (Id` H)   &   |- X = ran G   =>   |- (R e. Ring -> (X ~~ 1o <-> U = Z))
18-Feb-2010	ring1cl 10967	The unit of a ring belongs to the base set.
|- X = ran (1st` R)   &   |- H = (2nd` R)   &   |- U = (Id` H)   =>   |- (R e. Ring -> U e. X)
18-Feb-2010	rngunval2 10966	The value of the unit of a ring.
|- X = ran (1st` R)   &   |- H = (2nd` R)   &   |- U = (Id` H)   =>   |- (R e. Ring -> U = U.{u e. X | A.x e. X ((uHx) = x /\ (xHu) = x)})
18-Feb-2010	on1el6 10965	The only unital ring with one element is the zero ring.
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (R e. Ring -> (X ~~ 1o <-> R = <.{<.<.Z, Z>., Z>.}, {<.<.Z, Z>., Z>.}>.))
18-Feb-2010	on1el4 10964	The only unital ring with one element is the zero ring.
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. X) -> (X ~~ 1o <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.))
18-Feb-2010	on1el3 10963	The only unital ring with a base set consisting in one element is the zero ring.
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. B) -> (X = {A} <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.))
18-Feb-2010	uridm 10957	The unit of a ring is an identity element for the multiplication.
|- H = (2nd` R)   &   |- X = ran (1st` R)   &   |- U = (Id` H)   =>   |- ((R e. Ring /\ A e. X) -> ((UHA) = A /\ (AHU) = A))
18-Feb-2010	rnplrnml3 10951	In a unital ring the domain of the first operand of the addition equals the domain of the second operand of the addition.
|- G = (1st` R)   =>   |- (R e. Ring -> dom dom G = ran dom G)
18-Feb-2010	com2i 10942	Property of a commutative structure with two operation.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Com2 -> A.a e. X A.b e. X (aHb) = (bHa))
18-Feb-2010	mndmgmid 10925	A monoid is a magma with an identity element.
|- (G e. Mnd -> G e. (Magma i^i ExId))
18-Feb-2010	bsmgrli 10904	The base set of an operation with a right and left identity element is not empty.
|- X = ran G   =>   |- (G e. (Magma i^i ExId) -> X =/= (/))
18-Feb-2010	unpde2eg22 10827	If an unordered pair has two elements they are different.
|- ((A e. C /\ B e. D) -> ({A, B} ~~ 2o <-> A =/= B))
15-Feb-2010	elsb1 12230	Substitution applied to an atomic membership wff in which x doesn't occur.
|- ([y / x]z e. w <-> z e. w)
15-Feb-2010	elsb2 12229	Substitution applied to the atomic membership wff that a set contains itself. This wff is false by the axiom of regularity.
|- ([y / x]x e. x <-> y e. y)
15-Feb-2010	elsb4 12228	Substitution applied to an atomic membership wff.
|- ([y / x]z e. x <-> z e. y)
15-Feb-2010	elsb3NEW 12227	Substituion applied to an atomic membership wff. elsb3NEW 12227 is elsb3 1370 with the additional distinct variable requirement that x and y are distinct.
|- ([y / x]x e. z <-> y e. z)
15-Feb-2010	elsb2lem 12226	Lemma for elsb2
|- (E.x(x = y /\ x e. x) <-> y e. y)
15-Feb-2010	elequ3 12225	If two sets are equal they are not ordinary.
|- (x = y -> (x e. x <-> y e. y))
15-Feb-2010	elsb4lem 12224	Lemma for elsb4.
|- (E.x(x = y /\ z e. x) <-> z e. y)
15-Feb-2010	elsb3NEWlem 12223	Lemma for elsb3NEW.
|- (E.x(x = y /\ x e. z) <-> y e. z)
15-Feb-2010	subdefbi1 12222	Apply the definition of substitution to a biconditional.
|- (E.x(x = y /\ ph) <-> ps)   =>   |- ([y / x]ph <-> ps)
15-Feb-2010	sbf4 12221	Substitution has no effect on a bound variable.
|- ([y / x]E.xph <-> E.xph)
15-Feb-2010	sbf5 12220	Substitution has no effect on a bound variable.
|- (ph -> A.xph)   =>   |- ([y / x]E.yph <-> E.yph)
15-Feb-2010	sbf3 12219	Substitution has no effect on a bound variable.
|- (ph -> A.xph)   =>   |- ([y / x]A.yph <-> A.yph)
15-Feb-2010	boe 10745	{A, A} has only one element.
|- (A e. B -> {A, A} ~~ 1o)
5-Feb-2010	0vfval 8473	Value of the function for the zero vector on a normed complex vector space.
|- G = (+v` U)   &   |- Z = (0v` U)   =>   |- Z = (Id` G)
5-Feb-2010	grpidval 8276	The value of the identity element of a group.
|- X = ran G   &   |- U = (Id` G)   =>   |- (G e. Grp -> U = U.{u e. X | A.x e. X (uGx) = x})
5-Feb-2010	grpidvallem 8275	The value of the identity element of a group.
|- X = ran G   &   |- U = (Id` G)   &   |- G e. Grp   =>   |- U = U.{u e. X | A.x e. X (uGx) = x}
5-Feb-2010	grpsn 8274	The group operation for the singleton group.
|- A e. V   =>   |- {<.<.A, A>., A>.} e. Grp
5-Feb-2010	fungid 8273	Id is a function. (Contributed by FL, 5-Feb-2010.)
|- Fun Id
5-Feb-2010	gid0 8272	The identity of the empty set is the empty set. (Contributed by FL, 5-Feb-2010.)
|- (Id` (/)) = (/)
5-Feb-2010	grprlidrid 8271	In a group a left and right identity element is a left identity element. (Contributed by FL, 5-Feb-2010.)
|- X = ran G   =>   |- (G e. Grp -> U.{u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. X (uGx) = x})
1-Feb-2010	nrmsep2 11617	In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other.
|- ((J e. Nrm /\ (C e. (Clsd` J) /\ D e. (Clsd` J) /\ (C i^i D) = (/))) -> E.o e. J (C (_ o /\ (((cls` J)` o) i^i D) = (/)))
1-Feb-2010	nrmsep 11616	In a normal space, disjoint closed sets are separated by open sets.
|- ((J e. Nrm /\ (C e. (Clsd` J) /\ D e. (Clsd` J) /\ (C i^i D) = (/))) -> E.o e. J E.p e. J (C (_ o /\ D (_ p /\ (o i^i p) = (/)))
1-Feb-2010	nrmtop 11615	A normal space is a topological space.
|- (J e. Nrm -> J e. Top)
1-Feb-2010	isnrm2 11614	An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma.
|- (J e. Top -> (J e. Nrm <-> A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J (c (_ o /\ (((cls` J)` o) i^i d) = (/)))))
1-Feb-2010	isnrm 11613	The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular.
|- (J e. Nrm <-> (J e. Top /\ A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J E.p e. J (c (_ o /\ d (_ p /\ (o i^i p) = (/)))))
1-Feb-2010	regsep 11612	In a regular space, a closed set is separated by open sets from a point not in it.
|- X = U.J   =>   |- ((J e. Reg /\ (C e. (Clsd` J) /\ A e. X /\ A e/ C)) -> E.o e. J E.p e. J (C (_ o /\ A e. p /\ (o i^i p) = (/)))
1-Feb-2010	regtop 11611	A regular space is a topological space.
|- (J e. Reg -> J e. Top)
1-Feb-2010	isreg 11610	The predicate "is a regular space." In a regular space, any closed set is separated from any point not in it by neighborhoods. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do.
|- X = U.J   =>   |- (J e. Reg <-> (J e. Top /\ A.c e. (Clsd` J)A.x e. X (x e/ c -> E.o e. J E.p e. J (c (_ o /\ x e. p /\ (o i^i p) = (/)))))
1-Feb-2010	t1t0 11609	A T1 space is a T0 space.
|- (J e. Fre -> J e. Kol2)
1-Feb-2010	t1sep 11608	Any two distinct points in a T1 space are separated by an open set.
|- X = U.J   =>   |- ((J e. Fre /\ (A e. X /\ B e. X /\ A =/= B)) -> E.o e. J (A e. o /\ -. B e. o))
1-Feb-2010	t1sncld 11607	In a T1 space, one-point sets are closed.
|- X = U.J   =>   |- ((J e. Fre /\ A e. X) -> {A} e. (Clsd` J))
1-Feb-2010	t1top 11606	A T1 space is a topological space.
|- (J e. Fre -> J e. Top)
1-Feb-2010	t0dist 11603	Any two distinct points in a T0 space are topologically distinguishable.
|- X = U.J   =>   |- ((J e. Kol2 /\ (A e. X /\ B e. X /\ A =/= B)) -> E.o e. J -. (A e. o <-> B e. o))
1-Feb-2010	t0top 11602	A T0 space is a topological space.
|- (J e. Kol2 -> J e. Top)
1-Feb-2010	ist0-2 11601	The predicate "is a T0 space," expressed in more familiar terms.
|- X = U.J   =>   |- (J e. Top -> (J e. Kol2 <-> A.x e. X A.y e. X (x =/= y -> E.o e. J ((x e. o /\ -. y e. o) \/ (-. x e. o /\ y e. o)))))
1-Feb-2010	ist0 11600	The predicate "is a T0 space." Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-2 11601.
|- X = U.J   =>   |- (J e. Kol2 <-> (J e. Top /\ A.x e. X A.y e. X (x =/= y -> E.o e. J -. (x e. o <-> y e. o))))
31-Jan-2010	ist1-3 11605	A space is T1 iff every point is the only point in the intersection of all open sets containing that point.
|- X = U.J   =>   |- (J e. Top -> (J e. Fre <-> A.x e. X |^|{o e. J | x e. o} = {x}))
31-Jan-2010	ist1-2 11604	An alternate characterization of T1 spaces.
|- X = U.J   =>   |- (J e. Top -> (J e. Fre <-> A.x e. X A.y e. X (x =/= y -> E.o e. J (x e. o /\ -. y e. o))))
30-Jan-2010	2ndcctbss 11540	If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard.
|- X = U.B   &   |- J = (topGen` B)   =>   |- ((B e. Bases /\ J e. 2ndc) -> E.b e. Bases (b ~<_ om /\ b (_ B /\ J = (topGen` b)))
30-Jan-2010	uncomp 11491	The union of two compact sets is compact.
|- X = U.J   =>   |- (((J e. Top /\ X = (S u. T)) /\ ((subSp` <.S, J>.) e. Comp /\ (subSp` <.T, J>.) e. Comp)) -> J e. Comp)
28-Jan-2010	alexsub 11501	The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover.
|- X = U.J   =>   |- (J e. Comp <-> E.x(J = (topGen` (fi` x)) /\ A.c e. P~ x(X = U.c -> E.d e. (P~c i^i Fin)X = U.d)))
28-Jan-2010	alexsublem4 11500	Lemma for alexsub 11501. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover.
|- X = U.J   =>   |- (J = (topGen` (fi` x)) -> (A.c e. P~ x(X = U.c -> E.d e. (P~c i^i Fin)X = U.d) -> A.a e. P~ (fi` x)(X = U.a -> E.b e. (P~a i^i Fin)X = U.b)))
28-Jan-2010	alexsublem3 11499	Lemma for alexsub 11501. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover.
|- X = U.J   =>   |- (((((J = (topGen` (fi` x)) /\ A.c e. P~ x(X = U.c -> E.d e. (P~c i^i Fin)X = U.d) /\ a e. P~(fi` x)) /\ (u e. P~(fi` x) /\ (a (_ u /\ A.b e. (P~u i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t (_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u)))) -> E.s e. t A.n e. (P~(u u. {s}) i^i Fin) -. X = U.n)
27-Jan-2010	alexsublem2 11498	Lemma for alexsub 11501. Every subset of a base which has no finite subcover is a subset of a maximal such collection.
|- X = U.J   =>   |- (((J = (topGen` (fi` x)) /\ A.c e. P~ x(X = U.c -> E.d e. (P~c i^i Fin)X = U.d) /\ a e. P~(fi` x)) /\ A.b e. (P~a i^i Fin) -. X = U.b) -> E.u e. ({z e. P~(fi` x) | (a (_ z /\ A.b e. (P~z i^i Fin) -. X = U.b)} u. {(/)})A.v e. ({z e. P~(fi` x) | (a (_ z /\ A.b e. (P~z i^i Fin) -. X = U.b)} u. {(/)}) -. u (. v)
27-Jan-2010	alexsublem1 11497	Lemma for alexsub 11501. A compact space has a subbase such that every cover taken from it has a finite subcover.
|- X = U.J   =>   |- (J e. Comp -> E.x(J = (topGen` (fi` x)) /\ A.c e. P~ x(X = U.c -> E.d e. (P~c i^i Fin)X = U.d)))
27-Jan-2010	exp512 11359	An exportation inference.
|- ((ph /\ ((ps /\ ch) /\ (th /\ ta))) -> et)   =>   |- (ph -> (ps -> (ch -> (th -> (ta -> et)))))
27-Jan-2010	exp5l 11353	An exportation inference.
|- (ph -> (((ps /\ ch) /\ (th /\ ta)) -> et))   =>   |- (ph -> (ps -> (ch -> (th -> (ta -> et)))))
25-Jan-2010	finsschain 11426	A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub 11501 and others.
|- (((A =/= (/) /\ A.x e. A A.y e. A (x (_ y \/ y (_ x)) /\ (B e. Fin /\ B (_ U.A)) -> E.z e. A B (_ z)
24-Jan-2010	extrid 11240	Extraction of the identity of a category.
|- (J e. A -> (id` <.<.D, C>., <.J, R>.>.) = J)
24-Jan-2010	extrcmp 11239	Extraction of the composition of a category.
|- ((J e. A /\ R e. B) -> (o` <.<.D, C>., <.J, R>.>.) = R)
24-Jan-2010	extrcod 11238	Extraction of the codomain of a category.
|- ((D e. A /\ C e. B) -> (cod` <.<.D, C>., <.J, R>.>.) = C)
24-Jan-2010	extrdom 11237	Extraction of the domain of a category.
|- (D e. A -> (dom` <.<.D, C>., <.J, R>.>.) = D)
24-Jan-2010	zrfld 10976	The zero ring is not a field.
|- A e. B   =>   |- -. <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Fld
24-Jan-2010	zrdivrng 10970	The zero ring is not a division ring.
|- A e. B   =>   |- -. <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. DivRing
24-Jan-2010	unmnd 10952	In a unital ring the multiplication is a monoid.
|- H = (2nd` R)   =>   |- (R e. Ring -> H e. Mnd)
24-Jan-2010	rngdmdmrn 10950	In a unital ring the range of the multiplication equals the domain of the first variable.
|- H = (2nd` R)   =>   |- (R e. Ring -> dom dom H = ran H)
24-Jan-2010	rnplrnml 10949	In a unital ring the range of the addition equals the range of the multiplication.
|- H = (2nd` R)   &   |- G = (1st` R)   =>   |- (R e. Ring -> ran G = ran H)
24-Jan-2010	rnplrnml2 10948	In a unital ring the range of the addition equals the domain of the first variable of the multiplication.
|- H = (2nd` R)   &   |- G = (1st` R)   =>   |- (R e. Ring -> ran G = dom dom H)
24-Jan-2010	rnplrnml0 10947	In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication.
|- H = (2nd` R)   &   |- G = (1st` R)   =>   |- (R e. Ring -> dom dom G = dom dom H)
24-Jan-2010	rngmgmbs4 10946	The range of an internal operation with a left and right identity element equals its base set.
|- ((G:(X X. X)-->X /\ E.u e. X A.x e. X ((xGu) = x /\ (uGx) = x)) -> ran G = X)
24-Jan-2010	rngmgmbs3 10945	The domain of the first variable of an internal operation with a left and right identity element equals its base set.
|- ((G:(X X. X)-->X /\ E.u e. X A.x e. X ((xGu) = x /\ (uGx) = x)) -> dom dom G = X)
24-Jan-2010	rngn0 10944	The base set of a ring is not empty.
|- G = (1st` R)   &   |- X = ran G   =>   |- (R e. Ring -> X =/= (/))
24-Jan-2010	seqzp2 10919	Value of the arbitrary-based recursive sequence builder at a successor value when the operation G is associative. Compare with seqzp1 6744.
|- X = dom dom G   &   |- G e. SemiGrp   &   |- F:(ZZ>=` M)-->X   =>   |- (N e. (ZZ>=` M) -> ((<.M, G>. seq F)` (N + 1)) = ((F` M)G((<.(M + 1), G>. seq F)` (N + 1))))
24-Jan-2010	isppm 10918	The sequence of partial products of elements of a magma is a sequence of elements of this magma.
|- X = dom dom G   =>   |- ((G e. Magma /\ F:NN-->X) -> (G seq1 F):NN-->X)
24-Jan-2010	tostos 10884	Any subset of a totally ordered set is totally ordered.
|- (R e. Toset -> (R i^i (A X. A)) e. Toset)
24-Jan-2010	pospos 10883	Any subset of a partially ordered set is partially ordered.
|- (R e. Poset -> (R i^i (A X. A)) e. Poset)
24-Jan-2010	cur1val 10847	The value of a curried operation.
|- ((F e. A /\ Fun F /\ Rel dom F) -> (cur1` F) = {<.x, y>. | (x e. dom dom F /\ y = (F o. `'(2nd |` ({x} X. V))))})
24-Jan-2010	uuniin 10824	The double union of an intersection is a part of the intersections of the unions.
|- U.U.(A i^i B) (_ (U.U.A i^i U.U.B)
24-Jan-2010	dmoprabsss 10728	The domain of an operation class abstraction. Compare dmoprabss 4064.
|- dom {<.<.x, y>., z>. | (<.x, y>. e. (A X. B) /\ ph)} (_ (A X. B)
24-Jan-2010	ssoprab2g 10727	Inference of operation class abstraction subclass from implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> {<.<.x, y>., z>. | ps} (_ {<.<.x, y>., z>. | ch})
24-Jan-2010	twsvbdop 10726	Two ways to state the domains of the variables of an operation.
|- {<.<.x, y>., z>. | (<.x, y>. e. (A X. B) /\ ph)} = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)}
23-Jan-2010	subntr 11483	An interior in a subspace topology. Willard in General Topology says that there is no analog of subcls 11482 for interiors. In some sense, that is true.
|- X = U.J   &   |- K = (subSp` <.Y, J>.)   =>   |- ((J e. Top /\ Y (_ X /\ S (_ Y) -> ((int` K)` S) = (((int` J)` (S u. (X \ Y))) i^i Y))
22-Jan-2010	locfincf 11578	A locally finite cover in a coarser topology is locally finite in a finer topology.
|- X = U.J   &   |- Y = U.K   =>   |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J (_ K /\ X = Y)) -> <.K, A>. e. LocFin)
22-Jan-2010	locfindsc 11577	The locally finite covers of a discrete space are precisely the point-finite covers.
|- Y = U.C   =>   |- (C e. B -> (<.P~X, C>. e. LocFin <-> (C e. PtFin /\ X = Y)))
22-Jan-2010	locfincomp 11576	For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces.
|- X = U.J   &   |- Y = U.C   =>   |- ((J e. Comp /\ C e. A) -> (<.J, C>. e. LocFin <-> (C e. Fin /\ X = Y)))
22-Jan-2010	subcls 11482	A closure in a subspace topology.
|- X = U.J   &   |- K = (subSp` <.Y, J>.)   =>   |- ((J e. Top /\ Y (_ X /\ S (_ Y) -> ((cls` K)` S) = (((cls` J)` S) i^i Y))
21-Jan-2010	comppfsc 11579	A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces.
|- X = U.J   =>   |- (J e. Top -> (J e. Comp <-> A.c e. P~ J(X = U.c -> E.d e. PtFin (d (_ c /\ X = U.d))))
21-Jan-2010	lfinpfin 11575	A locally finite cover is point-finite.
|- ((A e. B /\ <.J, A>. e. LocFin) -> A e. PtFin)
21-Jan-2010	locfinnei 11574	A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover.
|- X = U.J   =>   |- ((A e. B /\ <.J, A>. e. LocFin /\ P e. X) -> E.n e. ((nei` J)` {P}){s e. A | (s i^i n) =/= (/)} e. Fin)
21-Jan-2010	locfinbas 11573	A locally finite cover must cover the base set of its corresponding topological space.
|- X = U.J   &   |- Y = U.A   =>   |- ((A e. B /\ <.J, A>. e. LocFin) -> X = Y)
21-Jan-2010	locfintop 11572	A locally finite cover covers a topological space.
|- ((A e. B /\ <.J, A>. e. LocFin) -> J e. Top)
21-Jan-2010	finlocfin 11571	A finite cover of a topological space is a locally finite cover.
|- X = U.J   &   |- Y = U.A   =>   |- ((J e. Top /\ A e. Fin /\ X = Y) -> <.J, A>. e. LocFin)

Also new:

(28-Feb-2010) Raph Levien's Ghilbert project now has a new Ghilbert site and a Google Group.

(26-Jan-2010) Dmitri Vlasov writes, "I admire the simplicity and power of the metamath language, but still I see its great disadvantage - the proofs in metamath are completely non-manageable by humans without proof assistants. Therefore I decided to develop another language, which would be a higher-level superstructure language towards metamath, and which will support human-readable/writable proofs directly, without proof assistants. I call this language mdl (acronym for 'mathematics development language')." The latest version of Dmitri's translators from metamath to mdl and back can be downloaded from http://mathdevlanguage.sourceforge.net/. Currently only Linux is supported, but Dmitri says is should not be difficult to port it to other platforms that have a g++ compiler.

(27-Oct-2009) I uploaded searchable PDF scans of Whitehead and Russell's Principia Mathematica: Volume I (15MB), Volume II (15MB), and Volume III (11MB). I think these are the smallest searchable PDFs of these books available on the Internet. Volume I, of course, is the source of many of our propositional calculus theorems.

(11-Sep-2009) The metamath program (version 0.07.48) has been updated to enforce the whitespace requirement of the current spec.

(10-Sep-2009) Matthew Leitch has written an nice article, "How to write mathematics clearly", that briefly mentions Metamath. Overall it makes some excellent points. (I have written to him about a few things I disagree with.)

(28-May-2009) AsteroidMeta is back on-line. Note the URL change.

(12-May-2009) Charles Greathouse wrote a Greasemonkey script to reformat the axiom list on Metamath web site proof pages. This is a beta version; he will appreciate feedback.

(11-May-2009) Stefan Allan modified the metamath program to add the command "show statement xxx /mnemonics", which produces the output file Mnemosyne.txt for use with the Mnemosyne project. The current Metamath program download incorporates this command. Instructions: Create the file mnemosyne.txt with e.g. "show statement ax-* /mnemonics". In the Mnemosyne program, load the file by choosing File->Import then file format "Q and A on separate lines". Notes: (1) Don't try to load all of set.mm, it will crash the program due to a bug in Mnemosyne. (2) On my computer, the arrows in ax-1 don't display. Stefan reports that they do on his computer. (Both are Windows XP.)

(3-May-2009) Steven Baldasty wrote a Metamath syntax highlighting file for the gedit editor. Screenshot.

(1-May-2009) Users on a gaming forum discuss our 2+2=4 proof. Notable comments include "Ew math!" and "Whoever wrote this has absolutely no life."

(12-Mar-2009) Chris Capel has created a Javascript theorem viewer demo that (1) shows substitutions and (2) allows expanding and collapsing proof steps. You are invited to take a look and give him feedback at his Metablog.

(28-Feb-2009) Chris Capel has written a Metamath proof verifier in C#, available at http://pdf23ds.net/bzr/MathEditor/Verifier/Verifier.cs and weighing in at 550 lines. Also, that same URL without the file on it is a Bazaar repository.

(2-Dec-2008) A new section was added to the Deduction Theorem page, called Logic, Metalogic, Metametalogic, and Metametametalogic.

(24-Aug-2008) (From ocat): The 1-Aug-2008 version of mmj2 is ready (mmj2.zip), size = 1,534,041 bytes. This version contains the Theorem Loader enhancement which provides a "sandboxing" capability for user theorems and dynamic update of new theorems to the Metamath database already loaded in memory by mmj2. Also, the new "mmj2 Service" feature enables calling mmj2 as a subroutine, or having mmj2 call your program, and provides access to the mmj2 data structures and objects loaded in memory (i.e. get started writing those Jython programs!) See also mmj2 on AsteroidMeta.

(23-May-2008) Gérard Lang pointed me to Bob Solovay's note on AC and strongly inaccessible cardinals. One of the eventual goals for set.mm is to prove the Axiom of Choice from Grothendieck's axiom, like Mizar does, and this note may be helpful for anyone wanting to attempt that. Separately, I also came across a history of the size reduction of grothprim (viewable in Firefox and some versions of Internet Explorer).

(14-Apr-2008) A "/join" qualifier was added to the "search" command in the metamath program (version 0.07.37). This qualifier will join the $e hypotheses to the $a or $p for searching, so that math tokens in the $e's can be matched as well. For example, "search *com* +v" produces no results, but "search *com* +v /join" yields commutative laws involving vector addition. Thanks to Stefan Allan for suggesting this idea.

(8-Apr-2008) The 8,000th theorem, hlrel, was added to the Metamath Proof Explorer part of the database.

(2-Mar-2008) I added a small section to the end of the Deduction Theorem page.

(17-Feb-2008) ocat has uploaded the "1-Mar-2008" mmj2: mmj2.zip. See the description.

(16-Jan-2008) O'Cat has written mmj2 Proof Assistant Quick Tips.

(30-Dec-2007) "How to build a library of formalized mathematics".

(22-Dec-2007) The Metamath Proof Explorer was included in the top 30 science resources for 2007 by the University at Albany Science Library.

(17-Dec-2007) Metamath's Wikipedia entry says, "This article may require cleanup to meet Wikipedia's quality standards" (see its discussion page). Volunteers are welcome. :) (In the interest of objectivity, I don't edit this entry.)

(20-Nov-2007) Jeff Hoffman created nicod.mm and posted it to the Google Metamath Group.

(19-Nov-2007) Reinder Verlinde suggested adding tooltips to the hyperlinks on the proof pages, which I did for proof step hyperlinks. Discussion.

(5-Nov-2007) A Usenet challenge. :)

(4-Aug-2007) I added a "Request for comments on proposed 'maps to' notation" at the bottom of the AsteroidMeta set.mm discussion page.

(21-Jun-2007) A preprint (PDF file) describing Kurt Maes' axiom of choice with 5 quantifiers, proved in set.mm as ackm.

(20-Jun-2007) The 7,000th theorem, ifpr, was added to the Metamath Proof Explorer part of the database.

(29-Apr-2007) Blog mentions of Metamath: here and here.

(21-Mar-2007) Paul Chapman is working on a new proof browser, which has highlighting that allows you to see the referenced theorem before and after the substitution was made. Here is a screenshot of theorem 0nn0 and a screenshot of theorem 2p2e4.

(15-Mar-2007) A picture of Penny the cat guarding the us2.metamath.org:8888 server and making the rounds.

(16-Feb-2007) For convenience, the program "drule.c" (pronounced "D-rule", not "drool") mentioned in pmproofs.txt can now be downloaded (drule.c) without having to ask me for it. The same disclaimer applies: even though this program works and has no known bugs, it was not intended for general release. Read the comments at the top of the program for instructions.

(28-Jan-2007) Jason Orendorff set up a new mailing list for Metamath: http://groups.google.com/group/metamath.

(20-Jan-2007) Bob Solovay provided a revised version of his Metamath database for Peano arithmetic, peano.mm.

(2-Jan-2007) Raph Levien has set up a wiki called Barghest for the Ghilbert language and software.

(26-Dec-2006) I posted an explanation of theorem ecoprass on Usenet.

(2-Dec-2006) Berislav Žarnić translated the Metamath Solitaire applet to Croatian.

(26-Nov-2006) Dan Getz has created an RSS feed for new theorems as they appear on this page.

(6-Nov-2006) The first 3 paragraphs in Appendix 2: Note on the Axioms were rewritten to clarify the connection between Tarski's axiom system and Metamath.

(31-Oct-2006) ocat asked for a do-over due to a bug in mmj2 -- if you downloaded the mmj2.zip version dated 10/28/2006, then download the new version dated 10/30.

(29-Oct-2006) ocat has announced that the long-awaited 1-Nov-2006 release of mmj2 is available now.
     The new "Unify+Get Hints" is quite useful, and any proof can be generated as follows. With "?" in the Hyp field and Ref field blank, select "Unify+Get Hints". Select a hint from the list and put it in the Ref field. Edit any $n dummy variables to become the desired wffs. Rinse and repeat for the new proof steps generated, until the proof is done.
     The new tutorial, mmj2PATutorial.bat, explains this in detail. One way to reduce or avoid dummy $n's is to fill in the Hyp field with a comma-separated list of any known hypothesis matches to earlier proof steps, keeping a "?" in the list to indicate that the remaining hypotheses are unknown. Then "Unify+Get Hints" can be applied. The tutorial page \mmj2\data\mmp\PATutorial\Page405.mmp has an example.
     Don't forget that the eimm export/import program lets you go back and forth between the mmj2 and the metamath program proof assistants, without exiting from either one, to exploit the best features of each as required.

(21-Oct-2006) Martin Kiselkov has written a Metamath proof verifier in the Lua scripting language, called verify.lua. While it is not practical as an everyday verifier - he writes that it takes about 40 minutes to verify set.mm on a a Pentium 4 - it could be useful to someone learning Lua or Metamath, and importantly it provides another independent way of verifying the correctness of Metamath proofs. His code looks like it is nicely structured and very readable. He is currently working on a faster version in C++.

(19-Oct-2006) New AsteroidMeta page by Raph, Distinctors_vs_binders.

(13-Oct-2006) I put a simple Metamath browser on my PDA (Palm Tungsten E) so that I don't have to lug around my laptop. Here is a screenshot. It isn't polished, but I'll provide the file + instructions if anyone wants it.

(3-Oct-2006) A blog entry, Principia for Reverse Mathematics.

(28-Sep-2006) A blog entry, Metamath responds.

(26-Sep-2006) A blog entry, Metamath isn't hygienic.

(11-Aug-2006) A blog entry, Metamath and the Peano Induction Axiom.

(26-Jul-2006) A new open problem in predicate calculus was added.

(18-Jun-2006) The 6,000th theorem, mt4d, was added to the Metamath Proof Explorer part of the database.

(9-May-2006) Luca Ciciriello has upgraded the t2mf program, which is a C program used to create the MIDI files on the Metamath Music Page, so that it works on MacOS X. This is a nice accomplishment, since the original program was written before C was standardized by ANSI and will not compile on modern compilers.
      Unfortunately, the original program source states no copyright terms. The main author, Tim Thompson, has kindly agreed to release his code to public domain, but two other authors have also contributed to the code, and so far I have been unable to contact them for copyright clearance. Therefore I cannot offer the MacOS X version for public download on this site until this is resolved. Update 10-May-2006: Another author, M. Czeiszperger, has released his contribution to public domain.
      If you are interested in Luca's modified source code, please contact me directly.

(18-Apr-2006) Incomplete proofs in progress can now be interchanged between the Metamath program's CLI Proof Assistant and mmj2's GUI Proof Assistant, using a new export-import program called eimm. This can be done without exiting either proof assistant, so that the strengths of each approach can be exploited during proof development. See "Use Case 5a" and "Use Case 5b" at mmj2ProofAssistantFeedback.

(28-Mar-2006) Scott Fenton updated his second version of Metamath Solitaire (the one that uses external axioms). He writes: "I've switched to making it a standalone program, as it seems silly to have an applet that can't be run in a web browser. Check the README file for further info." The download is mmsol-0.5.tar.gz.

(27-Mar-2006) Scott Fenton has updated the Metamath Solitaire Java applet to Java 1.5: (1) QSort has been stripped out: its functionality is in the Collections class that Sun ships; (2) all Vectors have been replaced by ArrayLists; (3) generic types have been tossed in wherever they fit: this cuts back drastically on casting; and (4) any warnings Eclipse spouted out have been dealt with. I haven't yet updated it officially, because I don't know if it will work with Microsoft's JVM in older versions of Internet Explorer. The current official version is compiled with Java 1.3, because it won't work with Microsoft's JVM if it is compiled with Java 1.4. (As distasteful as that seems, I will get complaints from users if it doesn't work with Microsoft's JVM.) If anyone can verify that Scott's new version runs on Microsoft's JVM, I would be grateful. Scott's new version is mm.java-1.5.gz; after uncompressing it, rename it to mm.java, use it to replace the existing mm.java file in the Metamath Solitaire download, and recompile according to instructions in the mm.java comments.
      Scott has also created a second version, mmsol-0.2.tar.gz, that reads the axioms from ASCII files, instead of having the axioms hard-coded in the program. This can be very useful if you want to play with custom axioms, and you can also add a collection of starting theorems as "axioms" to work from. However, it must be run from the local directory with appletviewer, since the default Java security model doesn't allow reading files from a browser. It works with the JDK 5 Update 6 Java download.
To compile (from Windows Command Prompt): C:\Program Files\Java\jdk1.5.0_06\bin\javac.exe mm.java
To run (from Windows Command Prompt): C:\Program Files\Java\jdk1.5.0_06\bin\appletviewer.exe mms.html

(21-Jan-2006) Juha Arpiainen proved the independence of axiom ax-11 from the others. This was published as an open problem in my 1995 paper (Remark 9.5 on PDF page 17). See Item 9a on the Workshop Miscellany for his seven-line proof. See also the Asteroid Meta metamathMathQuestions page under the heading "Axiom of variable substitution: ax-11". Congratulations, Juha!

(20-Oct-2005) Juha Arpiainen is working on a proof verifier in Common Lisp called Bourbaki. Its proof language has its roots in Metamath, with the goal of providing a more powerful syntax and definitional soundness checking. See its documentation and related discussion.

(17-Oct-2005) Marnix Klooster has written a Metamath proof verifier in Haskell, called Hmm. Also see his Announcement. The complete program (Hmm.hs, HmmImpl.hs, and HmmVerify.hs) has only 444 lines of code, excluding comments and blank lines. It verifies compressed as well as regular proofs; moreover, it transparently verifies both per-spec compressed proofs and the flawed format he uncovered (see comment below of 16-Oct-05).

(16-Oct-2005) Marnix Klooster noticed that for large proofs, the compressed proof format did not match the spec in the book. His algorithm to correct the problem has been put into the Metamath program (version 0.07.6). The program still verifies older proofs with the incorrect format, but the user will be nagged to update them with 'save proof *'. In set.mm, 285 out of 6376 proofs are affected. (The incorrect format did not affect proof correctness or verification, since the compression and decompression algorithms matched each other.)

(13-Sep-2005) Scott Fenton found an interesting axiom, ax46, which could be used to replace both ax-4 and ax-6.

(29-Jul-2005) Metamath was selected as site of the week by American Scientist Online.

(8-Jul-2005) Roy Longton has contributed 53 new theorems to the Quantum Logic Explorer. You can see them in the Theorem List starting at lem3.3.3lem1. He writes, "If you want, you can post an open challenge to see if anyone can find shorter proofs of the theorems I submitted."

(10-May-2005) A Usenet post I posted about the infinite prime proof; another one about indexed unions.

(3-May-2005) The theorem divexpt is the 5,000th theorem added to the Metamath Proof Explorer database.

(12-Apr-2005) Raph Levien solved the open problem in item 16 on the Workshop Miscellany page and as a corollary proved that axiom ax-9 is independent from the other axioms of predicate calculus and equality. This is the first such independence proof so far; a goal is to prove all of them independent (or to derive any redundant ones from the others).

(8-Mar-2005) I added a paragraph above our complex number axioms table, summarizing the construction and indicating where Dedekind cuts are defined. Thanks to Andrew Buhr for comments on this.

(16-Feb-2005) The Metamath Music Page is mentioned as a reference or resource for a university course called Math, Mind, and Music. .

(28-Jan-2005) Steven Cullinane parodied the Metamath Music Page in his blog.

(18-Jan-2005) Waldek Hebisch upgraded the Metamath program to run on the AMD64 64-bit processor.

(17-Jan-2005) A symbol list summary was added to the beginning of the Hilbert Space Explorer Home Page. Thanks to Mladen Pavicic for suggesting this.

(6-Jan-2005) Someone assembled an amazon.com list of some of the books in the Metamath Proof Explorer Bibliography.

(4-Jan-2005) The definition of ordinal exponentiation was decided on after this Usenet discussion.

(19-Dec-2004) A bit of trivia: my Erdös number is 2, as you can see from this list.

(20-Oct-2004) I started this Usenet discussion about the "reals are uncountable" proof (127 comments; last one on Nov. 12).

(12-Oct-2004) gch-kn shows the equivalence of the Generalized Continuum Hypothesis and Prof. Nambiar's Axiom of Combinatorial Sets. This proof answers his Open Problem 2 (PDF file).

(5-Aug-2004) I gave a talk on "Hilbert Lattice Equations" at the Argonne workshop.

(25-Jul-2004) The theorem nthruz is the 4,000th theorem added to the Metamath Proof Explorer database.

(27-May-2004) Josiah Burroughs contributed the proofs u1lemn1b, u1lem3var1, oi3oa3lem1, and oi3oa3 to the Quantum Logic Explorer database ql.mm.

(23-May-2004) Some minor typos found by Josh Purinton were corrected in the Metamath book. In addition, Josh simplified the definition of the closure of a pre-statement of a formal system in Appendix C.

(5-May-2004) Gregory Bush has found shorter proofs for 67 of the 193 propositional calculus theorems listed in Principia Mathematica, thus establishing 67 new records. (This was challenge #4 on the open problems page.)