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 official, cleaned up set.mm database file in the Metamath program download is sometimes several days behind the preproduction set.mm (7MB) that corresponds to this page. Email: Norm Megill. Wikis: AsteroidMeta (Recent Changes); Ghestalt (Recent Changes). Mailing list: Google Groups. Syndication: RSS feed (web version) courtesy of Dan Getz (please note: the feed URL was changed on 22-Sep-2008).

The standard port 80 is not available for the development site, and some users have reported that the original port 8888 is sometimes blocked. Therefore I added two other ports, 88 and 443. You can discuss this problem here. — Norm 24 Jun 2008

Last updated on 25-Sep-2008 at 12:12 AM ET.

Recent Additions to the Metamath Proof Explorer   Notes (last updated 8-Sep-08 )   News (last updated 24-Aug-08 )

Date	Label	Description
Theorem
24-Sep-2008	eupicka 1437	Version of eupick 1436 with closed formulas.
|- ((E!xph /\ E.x(ph /\ ps)) -> A.x(ph -> ps))
23-Sep-2008	inposet 10477	Inclusion partially orders any set. (Part of FL's sandbox.)
|- C = {<.x, y>. | x (_ y}   =>   |- (A e. B -> (C i^i (A X. A)) e. Poset)
23-Sep-2008	inpc 10476	Inclusion is a proper class. (Part of FL's sandbox.)
|- C = {<.x, y>. | x (_ y}   =>   |- -. C e. V
23-Sep-2008	inposetlem 10475	Lemma for inposet 10477. Definition of inclusion of sets using a class. (Part of FL's sandbox.)
|- A e. V   &   |- B e. V   &   |- C = {<.x, y>. | x (_ y}   =>   |- (ACB <-> A (_ B)
23-Sep-2008	vxveqv 10467	A theorem about things which don't exist V and (V X. V). (Part of FL's sandbox.)
|- (V X. V) =/= V
22-Sep-2008	dominf 4915	A nonempty set that is a subset of its union is infinite.
|- A e. V   =>   |- ((A =/= (/) /\ A (_ U.A) -> om ~<_ A)
22-Sep-2008	isfinite 4643	A set is strictly dominated by the class of natural numbers iff it is finite. Theorem 42 of [Suppes] p. 151. This theorem provides two equivalent ways to express "A is finite." The Axiom of Infinity is used for the reverse implication.
|- (A ~< om <-> A e. Fin)
20-Sep-2008	pwfi 4579	The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105.
|- (A e. Fin <-> P~A e. Fin)
19-Sep-2008	pwfilem 4577	Lemma for pwfi 4579.
|- F = {<.c, y>. | (c e. P~b /\ y = (c u. {x}))}   =>   |- (P~b e. Fin -> P~(b u. {x}) e. Fin)
18-Sep-2008	domfi 4549	A set dominated by a finite set is finite.
|- ((A e. Fin /\ B ~<_ A) -> B e. Fin)
17-Sep-2008	fodomfi 4575	An onto function implies dominance of domain over range, for finite sets. Unlike fodom 4808 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.
|- ((A e. Fin /\ F:A-onto->B) -> B ~<_ A)
16-Sep-2008	unctb 7578	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.)
|- ((A ~<_ om /\ B ~<_ om) -> (A u. B) ~<_ om)
15-Sep-2008	unfi2 4565	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 4563 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 4559).
|- ((A ~< om /\ B ~< om) -> (A u. B) ~< om)
14-Sep-2008	isfinite1 4539	Omega strictly dominates a finite set. See comment in omsdomnn 4538.
|- (A e. Fin -> (A ~<_ om /\ -. om ~~ A))
13-Sep-2008	sucdom 4852	Strict dominance of a set over a natural number is the same as dominance over its successor. The proof uses AC and Infinity. It is unclear if a proof without using these is possible, unlike the weaker versions omsucdom 4528, sucdomi 4529, and finsucdom 4532.
|- ((A e. om /\ B e. C) -> (A ~< B <-> suc A ~<_ B))
12-Sep-2008	cos2tsint 7464	Double-angle formula for cosine in terms of sine.
|- (A e. CC -> (cos` (2 x. A)) = (1 - (2 x. ((sin` A)^2))))
11-Sep-2008	intv 2747	The intersection of the universal class is empty.
|- |^|V = (/)
11-Sep-2008	viin 2611	Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 1033 and abid2 1583. When A = x, this evaluates to (/) by intiin 2606 and intv 2747.
|- |^|_x e. V A = {y | A.x y e. A}
11-Sep-2008	vne0 2290	The universal class is not equal to the empty set.
|- V =/= (/)
10-Sep-2008	isfinite2 4557	Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does not require the Axiom of Infinity.
|- (A ~< om -> A e. Fin)
9-Sep-2008	finsucdom 4532	Strict dominance of a finite set over a natural number is the same as dominance over its successor.
|- ((A e. om /\ B e. Fin) -> (A ~< B <-> suc A ~<_ B))
8-Sep-2008	expimpd 375	Exportation followed by a deduction version of importation.
|- ((ph /\ ps) -> (ch -> th))   =>   |- (ph -> ((ps /\ ch) -> th))
7-Sep-2008	ominf 4536	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136.
|- -. om e. Fin
7-Sep-2008	expdimp 377	A deduction version of exportation, followed by importation.
|- (ph -> ((ps /\ ch) -> th))   =>   |- ((ph /\ ps) -> (ch -> th))
6-Sep-2008	setwoe 10532	Building a set with only one element.
|- ((A e. B /\ B ~~ 1o) -> B = {A})
6-Sep-2008	set2elt 10531	Building a set with two elements.
|- ((C ~~ 2o /\ A e. C /\ B e. C) -> (A =/= B -> C = {A, B}))
6-Sep-2008	sfseqeq 10529	A finite set is equal to its subset if they are equinumerous.
|- ((B e. Fin /\ A (_ B /\ A ~~ B) -> A = B)
6-Sep-2008	divsubdirt 5776	Distribution of division over subtraction.
|- ((A e. CC /\ B e. CC /\ (C e. CC /\ C =/= 0)) -> ((A - B) / C) = ((A / C) - (B / C)))
6-Sep-2008	enfi 4543	Equinmerous sets have the same finiteness.
|- ((B e. C /\ A ~~ B) -> (A e. Fin <-> B e. Fin))
6-Sep-2008	pssinf 4534	A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of [Enderton] p. 136.
|- ((A (. B /\ A ~~ B) -> -. B e. Fin)
5-Sep-2008	fldivt 6256	Cancellation of the floor of a real divided by an integer.
|- ((A e. RR /\ N e. NN) -> (|_` ((|_` A) / N)) = (|_` (A / N)))
4-Sep-2008	intfracq 6255	Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac 6254.
|- Z = (|_` (M / N))   &   |- F = ((M / N) - Z)   =>   |- ((M e. ZZ /\ N e. NN) -> (0 <_ F /\ F <_ ((N - 1) / N) /\ (M / N) = (Z + F)))
3-Sep-2008	php3 4521	Corollary of Pigeonhole Principle. If A is finite and B is a proper subset of A, the B is strictly less numerous than A. Stronger version of Corollary 6C of [Enderton] p. 135.
|- ((A e. Fin /\ B (. A) -> B ~< A)
2-Sep-2008	rcfpfil 10569	Relative complements of the finite parts of an infinite set is a filter. When A = NN the set of the relative complements is called Frechet's filter and is used to define the concept of limit of a sequence.
|- ((A e. B /\ -. A e. Fin) -> {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} e. Fil)
2-Sep-2008	rcfpfillem6 10568	Lemma for rcfpfil 10569.
|- ((u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ v (_ A /\ u (_ v) -> v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
2-Sep-2008	rcfpfillem5 10567	Lemma for rcfpfil 10569.
|- (A e. B -> A e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
2-Sep-2008	rcfpfillem4 10566	Lemma for rcfpfil 10569.
|- (A e. B -> A.u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}A.v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
2-Sep-2008	rcfpfillem3 10565	Lemma for rcfpfil 10569.
|- (A e. B -> U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} = A)
2-Sep-2008	rcfpfillem2 10564	Lemma for rcfpfil 10569.
|- (-. A e. Fin -> -. (/) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
2-Sep-2008	rcfpfillem1 10563	Lemma for rcfpfil 10569.
|- (B e. C -> (B e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} <-> E.b(b (_ A /\ b e. Fin /\ B = (A \ b))))
2-Sep-2008	cnfilca 10562	Condition to have a filter finer than a given filter and containing a set A. Bourbaki T.G. I.37 cor. 1
|- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F (_ g) <-> A.x e. F (x i^i A) =/= (/)))
2-Sep-2008	efilcp2 10561	A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1.
|- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) <-> E.x e. Fil A (_ x))
2-Sep-2008	infi 10559	The intersection of two finite intersections is a finite intersection.
|- (C e. D -> ((A e. (fi` C) /\ B e. (fi` C)) -> (A i^i B) e. (fi` C)))
2-Sep-2008	fisub 10558	If a set has the finite intersection property, its subsets have also this property.
|- B = {z | E.y(y (_ A /\ y e. Fin /\ z = |^|y)}   &   |- D = {z | E.y(y (_ C /\ y e. Fin /\ z = |^|y)}   =>   |- (C (_ A -> (-. (/) e. B -> -. (/) e. D))
2-Sep-2008	filint2 10557	A filter is closed under taking finite intersections.
|- (F e. Fil -> ((A (_ F /\ A =/= (/) /\ A e. Fin) -> |^|A e. F))
2-Sep-2008	efilcp 10556	A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1.
|- B = {z | E.y(y (_ A /\ y e. Fin /\ z = |^|y)}   =>   |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B <-> E.x e. Fil A (_ x))
2-Sep-2008	fgsb 10555	Filter generated by a subbasis A. Bourbaki TG I.37 paragraph above prop. 1. The theorem has been slightly modified because the definitions of the empty set are different in Bourbaki and Metamath.
|- B = {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)}   =>   |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B -> {x e. P~X | E.y e. B y (_ x} e. Fil))
2-Sep-2008	fipfil2 10550	A filter has the finite intersection property. Bourbaki TG I.36 note of def. 1.
|- (F e. Fil -> ((A (_ F /\ A =/= (/) /\ A e. Fin) -> |^|A =/= (/)))
2-Sep-2008	fiiu2 10473	If A is the intersection of a finite set of elements of B then A (_ U.B.
|- (B e. C -> (A e. (fi` B) -> A (_ U.B))
2-Sep-2008	sppfi 10472	Specific properties of an element of (fi` C).
|- ((A e. B /\ C e. D) -> (A e. (fi` C) <-> E.z(z (_ C /\ z e. Fin /\ A = |^|z)))
2-Sep-2008	fine2 10471	If A is not empty, the class of all the finite intersections of A is not empty either.
|- (A e. B -> (A =/= (/) -> (fi` A) =/= (/)))
2-Sep-2008	fiv 10470	The set of all the finite intersections of the elements of A.
|- (A e. B -> (fi` A) = {u | E.z(z (_ A /\ z e. Fin /\ u = |^|z)})
2-Sep-2008	emfin 10466	The empty set is finite.
|- (/) e. Fin
2-Sep-2008	ficli 10462	The class of finite intersections of a class L are closed under intersection.
|- F = {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)}   =>   |- ((A e. F /\ B e. F