Metamath Proof Explorer - mmtheorems35

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 3401-3500 - Page 35 of 58

Type	Label	Description
Statement
Theorem	limensuci 3401	A limit ordinal is equinumerous to its successor.
|- Lim A   =>   |- (A e. B -> A ~~ suc A)
Theorem	limensuc 3402	A limit ordinal is equinumerous to its successor.
|- ((A e. B /\ Lim A) -> A ~~ suc A)
Theorem	phplem1 3403	Lemma for Pigeonhole Principle. This just says that if we remove an element of a set then put it back in, we end up with the original set.
|- (B e. A -> ({B} u. (A \ {B})) = A)
Theorem	phplem2 3404	Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element.
|- ((A e. om /\ B e. A) -> ({A} u. (A \ {B})) = (suc A \ {B}))
Theorem	phplem3 3405	Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements.
|- A e. V   &   |- B e. V   =>   |- ((A e. om /\ B e. A) -> A ~~ (suc A \ {B}))
Theorem	phplem4 3406	Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor.
|- A e. V   &   |- B e. V   =>   |- ((A e. om /\ B e. suc A) -> A ~~ (suc A \ {B}))
Theorem	phplem5 3407	Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers.
|- A e. V   &   |- B e. V   =>   |- ((A e. om /\ B e. om) -> (suc A ~~ suc B -> A ~~ B))
Theorem	nneneq 3408	Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136.
|- ((A e. om /\ B e. om) -> (A ~~ B <-> A = B))
Theorem	php 3409	Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 3403 through phplem5 3407, nneneq 3408, and this final piece of the proof.
|- ((A e. om /\ B (. A) -> -. A ~~ B)
Theorem	php2 3410	Corollary of Pigeonhole Principle.
|- ((A e. om /\ B (. A) -> B ~< A)
Theorem	php3 3411	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. (The expression E.x e. omA ~~ x is the definition of "finite", and "infinite" is defined as "not finite".)
|- ((E.x e. om A ~~ x /\ B (. A) -> B ~< A)
Theorem	php4 3412	Corollary of the Pigeonhole Principle php 3409: a natural number is strictly dominated by its successor.
|- (A e. om -> A ~< suc A)
Theorem	php5 3413	Corollary of the Pigeonhole Principle php 3409: a natural number is not equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring] p. 90.
|- (A e. om -> -. A ~~ suc A)
Theorem	onomeneq 3414	An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of [TakeutiZaring] p. 90 and its converse.
|- ((A e. On /\ B e. om) -> (A ~~ B <-> A = B))
Theorem	onfin 3415	An ordinal number is finite iff it is a natural number. Proposition 10.32 of [TakeutiZaring] p. 92.
|- (A e. On -> (E.x e. om A ~~ x <-> A e. om))
Theorem	nndomo 3416	Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146.
|- ((A e. om /\ B e. om) -> (A ~<_ B <-> A (_ B))
Theorem	nnsdomo 3417	Cardinal ordering agrees with natural number ordering.
|- ((A e. om /\ B e. om) -> (A ~< B <-> A (. B))
Theorem	omsucdom 3418	Strict dominance of natural numbers is the same as dominance over the successor of the smaller.
|- ((A e. om /\ B e. om) -> (A ~< B <-> suc A ~<_ B))
Theorem	sucdomi 3419	Dominance of a set over a successor of a natural number implies strict dominance over the number. For the converse, see sucdom 3648.
|- ((A e. om /\ B e. C) -> (suc A ~<_ B -> A ~< B))
Theorem	0sdom1dom 3420	Strict dominance over zero is the same as dominance over one.
|- A e. V   =>   |- ((/) ~< A <-> 1o ~<_ A)
Theorem	finsucdom 3421	Strict dominance of a finite set over a natural number is the same as dominance over its successor.
|- ((A e. om /\ E.x e. om B ~~ x) -> (A ~< B <-> suc A ~<_ B))
Theorem	pssinf 3422	A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of [Enderton] p. 136.
|- ((A (. B /\ A ~~ B) -> -. E.x e. om B ~~ x)
Theorem	ominf 3423	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136.
|- -. E.x e. om om ~~ x
Theorem	omsdomnn 3424	Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. Here we use A ~<_ om /\ -. om ~~ A instead of A ~< om because, due to a peculiarity ultimately caused our ordered pair definition, we would need the axiom of infinity (which we have avoided up to now) in order to prove the latter.
|- (A e. om -> (A ~<_ om /\ -. om ~~ A))
Theorem	isfinite1 3425	Omega strictly dominates a finite set. See comment in omsdomnn 3424.
|- (E.x e. om A ~~ x -> (A ~<_ om /\ -. om ~~ A))
Theorem	infsdomnn 3426	An infinite set strictly dominates a natural number.
|- A e. V   =>   |- ((om ~<_ A /\ B e. om) -> B ~< A)
Theorem	infn0 3427	An infinite set is not empty.
|- A e. V   =>   |- (om ~<_ A -> -. A = (/))
Theorem	pssnn 3428	A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137.
|- ((A e. om /\ B (. A) -> E.x e. A B ~~ x)
Theorem	ssnn 3429	A subset of a natural number is finite.
|- ((A e. om /\ B (_ A) -> E.x e. om B ~~ x)
Theorem	ssfi 3430	A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138.
|- ((E.x e. om A ~~ x /\ B (_ A) -> E.x e. om B ~~ x)
Theorem	unblem1 3431	Lemma for unbnn 3435. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set.
|- (((B (_ om /\ A.x e. om E.y e. B x e. y) /\ A e. B) -> |^|(B \ suc A) e. B)
Theorem	unblem2 3432	Lemma for unbnn 3435. The value of the function F belongs to the unbounded set of natural numbers A.
|- (w e. F -> A.x w e. F)   &   |- F = (rec({<.x, y>. | y = |^|(A \ suc x)}, |^|A) |` om)   =>   |- ((A (_ om /\ A.w e. om E.v e. A w e. v) -> (z e. om -> (F` z) e. A))
Theorem	unblem3 3433	Lemma for unbnn 3435. The value of the function F is less than its value at a successor.
|- (w e. F -> A.x w e. F)   &   |- F = (rec({<.x, y>. | y = |^|(A \ suc x)}, |^|A) |` om)   =>   |- ((A (_ om /\ A.w e. om E.v e. A w e. v) -> (z e. om -> (F` z) e. (F` suc z)))
Theorem	unblem4 3434	Lemma for unbnn 3435. The function F maps the set of natural numbers one-to-one to set of unbounded natural numbers A.
|- (w e. F -> A.x w e. F)   &   |- F = (rec({<.x, y>. | y = |^|(A \ suc x)}, |^|A) |` om)   =>   |- ((A (_ om /\ A.w e. om E.v e. A w e. v) -> F:om-1-1->A)
Theorem	unbnn 3435	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of [Suppes] p. 151.
|- A e. V   =>   |- ((A (_ om /\ A.x e. om E.y e. A x e. y) -> A ~~ om)
Theorem	unbnn2 3436	Version of unbnn 3435 that does not require a strict upper bound.
|- A e. V   =>   |- ((A (_ om /\ A.x e. om E.y e. A x (_ y) -> A ~~ om)
Theorem	isfinite2 3437	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 -> E.x e. om A ~~ x)
Theorem	unfilem1 3438	Lemma for proving that the union of two finite sets is finite.
|- A e. om   &   |- B e. om   &   |- F = {<.x, y>. | (x e. B /\ y = (A +o x))}   =>   |- ran F = ((A +o B) \ A)
Theorem	unfilem2 3439	Lemma for proving that the union of two finite sets is finite.
|- A e. om   &   |- B e. om   &   |- F = {<.x, y>. | (x e. B /\ y = (A +o x))}   =>   |- F:B-1-1-onto->((A +o B) \ A)
Theorem	unfilem3 3440	Lemma for proving that the union of two finite sets is finite.
|- ((A e. om /\ B e. om) -> B ~~ ((A +o B) \ A))
Theorem	unfi 3441	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144.
|- ((E.x e. om A ~~ x /\ E.x e. om B ~~ x) -> E.x e. om (A u. B) ~~ x)
Theorem	unfi2 3442	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144.
|- ((A ~< om /\ B ~< om) -> (A u. B) ~< om)
Theorem	infcntss 3443	Every infinite set has a denumerable subset. Similar to Exercise 8 of [TakeutiZaring] p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.)
|- A e. V   =>   |- (om ~<_ A -> E.x(x (_ A /\ x ~~ om))
Theorem	prfi 3444	An unordered pair is finite.
|- E.x e. om {A, B} ~~ x
Theorem	fiint 3445	Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite non-empty subcollection of A is in A". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally.
|- (A.x e. A A.y e. A (x i^i y) e. A <-> A.x(((x (_ A /\ -. x = (/)) /\ E.y e. om x ~~ y) -> |^|x e. A))
Theorem	zfregcl 3446	The Axiom of Regularity with class variables.
|- A e. V   =>   |- (E.x x e. A -> E.x e. A A.y e. x -. y e. A)
Theorem	zfreg 3447	The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the 'weak form'; there is also a 'strong form', not requiring that A be a set, that can be proved with more difficulty (see zfregs 3491).
|- A e. V   =>   |- (-. A = (/) -> E.x e. A (x i^i A) = (/))
Theorem	zfreg2 3448	The Axiom of Regularity using abbreviations. This form with the intersection arguments commuted (compared to zfreg 3447) is formally more convenient for us in some cases. Axiom Reg of [BellMachover] p. 480.
|- A e. V   =>   |- (-. A = (/) -> E.x e. A (A i^i x) = (/))
Theorem	eirrv 3449	The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. (This is trivial to prove from zfregfr 3452 and efrirr 2180, but this proof is direct from the Axiom of Regularity.)
|- -. x e. x
Theorem	eirr 3450	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22.
|- -. A e. A
Theorem	sucprcreg 3451	A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity).
|- (-. A e. V <-> suc A = A)
Theorem	zfregfr 3452	The epsilon relation is founded on any class.
|- E Fr A
Theorem	en2lp 3453	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206.
|- -. (A e. B /\ B e. A)
Theorem	preleq 3454	Equality of two unordered pairs when one member of each pair contains the other member.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- (((A e. B /\ C e. D) /\ {A, B} = {C, D}) -> (A = C /\ B = D))
Theorem	opthreg 3455	Theorem for alternate representation of ordered pairs, requiring Regularity. Exercise 34 of [Enderton] p. 207.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- ({A, {A, B}} = {C, {C, D}} -> (A = C /\ B = D))
Theorem	suc11reg 3456	The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse.
|- (suc A = suc B <-> A = B)
Theorem	inf0 3457	Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class "ran (rec({<.w, v>. | v = suc w}, y) |` om)" exists, is a subset of its union, and contains a given set y (and thus is non-empty). Thus it provides an example demonstrating that a set x exists with the necessary properties demanded by ax-inf 1079.
|- om e. V   =>   |- E.x(y e. x /\ A.y(y e. x -> E.z(y e. z /\ z e. x)))
Theorem	inf1 3458	Variation of Axiom of Infinity (using axinf 1084 as a hypothesis). Axiom of Infinity of [FreydScedrov] p. 283.
|- E.x(y e. x /\ A.y(y e. x -> E.z(y e. z /\ z e. x)))   =>   |-