mmtheorems32 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10682

Statement List for Metamath Proof Explorer - 3101-3200 - Page 32 of 107

Type	Label	Description
Statement
Theorem	onssneli2 3101	An ordering law for ordinal numbers.
|- A e. On   =>   |- (B (_ A -> -. A e. B)
Theorem	onelin 3102	An element of an ordinal number equals the intersection with it.
|- A e. On   =>   |- (B e. A -> B = (B i^i A))
Theorem	onelun 3103	An ordinal number equals its union with any element.
|- A e. On   =>   |- (B e. A -> (A u. B) = A)
Theorem	onsuc 3104	The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193.
|- A e. On   =>   |- suc A e. On
Theorem	onunisuc 3105	An ordinal number is equal to the union of its successor.
|- A e. On   =>   |- U.suc A = A
Theorem	onuniorsuc 3106	An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union.
|- A e. On   =>   |- (A = U.A \/ A = suc U.A)
Theorem	onuninsuc 3107	A limit ordinal is not a successor ordinal.
|- A e. On   =>   |- (A = U.A <-> -. E.x e. On A = suc x)
Theorem	onssel 3108	Subset is equivalent to membership or equality for ordinal numbers.
|- A e. On   &   |- B e. On   =>   |- (A (_ B <-> (A e. B \/ A = B))
Theorem	onun 3109	The union of two ordinal numbers is an ordinal number.
|- A e. On   &   |- B e. On   =>   |- (A u. B) e. On
Theorem	onsucss 3110	A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse.
|- A e. On   &   |- B e. On   =>   |- (A e. B <-> suc A (_ B)
Theorem	nlimsucg 3111	A successor is not a limit ordinal.
|- (A e. B -> -. Lim suc A)
Theorem	unizlim 3112	An ordinal equal to its own union is either zero or a limit ordinal.
|- (Ord A -> (A = U.A <-> (A = (/) \/ Lim A)))
Theorem	orduninsuc 3113	An ordinal equal to its union is not a successor.
|- (Ord A -> (A = U.A <-> -. E.x e. On A = suc x))
Theorem	ordunisuc2 3114	An ordinal equal to its union contains the successor of each of its members.
|- (Ord A -> (A = U.A <-> A.x e. A suc x e. A))
Theorem	ordzsl 3115	An ordinal is zero, a successor ordinal, or a limit ordinal.
|- (Ord A <-> (A = (/) \/ E.x e. On A = suc x \/ Lim A))
Theorem	onzsl 3116	An ordinal number is zero, a successor ordinal, or a limit ordinal number.
|- (A e. On <-> (A = (/) \/ E.x e. On A = suc x \/ (A e. V /\ Lim A)))
Theorem	dflim3 3117	An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor.
|- (Lim A <-> (Ord A /\ -. (A = (/) \/ E.x e. On A = suc x)))
Theorem	dflim4 3118	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A.x e. A suc x e. A))
Theorem	limsuc 3119	The successor of a member of a limit ordinal is also a member.
|- (Lim A -> (B e. A <-> suc B e. A))
Theorem	limsssuc 3120	A class includes a limit ordinal iff the successor of the class includes it.
|- (Lim A -> (A (_ B <-> A (_ suc B))
Theorem	nlimon 3121	Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of [TakeutiZaring] p. 42, who use the symbol KI for this class.
|- {x e. On | (x = (/) \/ E.y e. On x = suc y)} = {x e. On | -. Lim x}
Theorem	limuni3 3122	The union of a nonempty class of limit ordinals is a limit ordinal.
|- ((A =/= (/) /\ A.x e. A Lim x) -> Lim U.A)
Theorem	on0eqelt 3123	An ordinal number either equals zero or contains zero.
|- (A e. On -> (A = (/) \/ (/) e. A))
Theorem	snsn0non 3124	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 3135). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 3240.
|- -. {{(/)}} e. On
Transfinite induction
Theorem	tfi 3125	The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring] p. 39. This principle states that if A is a class of ordinal numbers with the property that every ordinal number included in A also belongs to A, then every ordinal number is in A.
|- ((A (_ On /\ A.x e. On (x (_ A -> x e. A)) -> A = On)
Theorem	tfis 3126	Transfinite Induction Schema. If all ordinal numbers less than a given number x have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200.
|- (x e. On -> (A.y e. x [y / x]ph -> ph))   =>   |- (x e. On -> ph)
Theorem	tfis2f 3127	Transfinite Induction Schema with implicit substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   &   |- (x e. On -> (A.y e. x ps -> ph))   =>   |- (x e. On -> ph)
Theorem	tfis2 3128	Transfinite Induction Schema with implicit substitution.
|- (x = y -> (ph <-> ps))   &   |- (x e. On -> (A.y e. x ps -> ph))   =>   |- (x e. On -> ph)
Theorem	tfis3 3129	Transfinite Induction Schema with implicit substitution.
|- (x = y -> (ph <-> ps))   &   |- (x = A -> (ph <-> ch))   &   |- (x e. On -> (A.y e. x ps -> ph))   =>   |- (A e. On -> ch)
The natural numbers (i.e. finite ordinals)
Syntax	com 3130	Extend class notation to include the class of natural numbers.
class om
Definition	df-om 3131	Define the class of natural numbers, which are all ordinal numbers that are less than every limit ordinal, i.e. all finite ordinals. Our definition is a variant of the Definition of N of [BellMachover] p. 471. See dfom2 3132 for an alternate definition. Later, when we assume the Axiom of Infinity, we show om is a set in omex 4617, and om can then be defined per dfom3 4620 (the smallest inductive set) and dfom4 4622. Note: the natural numbers om are a subset of the ordinal numbers df-on 2950. They are completely different from the natural numbers NN (df-n 5891) that are a subset of the complex numbers defined much later in our development, although the two sets have analogous properties and operations defined on them.
|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
Theorem	dfom2 3132	An alternate definition of the set of natural numbers om. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the inner class builder of non-limit ordinal numbers (see nlimon 3121).
|- om = {x e. On | suc x (_ {y e. On | -. Lim y}}
Theorem	elom 3133	Membership in omega. The hypothesis can be eliminated if we assume the Axiom of Infinity; see elom3 4621.
|- A e. V   =>   |- (A e. om <-> (Ord A /\ A.x(Lim x -> A e. x)))
Theorem	elomg 3134	Membership in omega. The antecedent can be eliminated if we assume the Axiom of Infinity; see elom3 4621.
|- (A e. B -> (A e. om <-> (Ord A /\ A.x(Lim x -> A e. x))))
Theorem	omsson 3135	Omega is a subset of On.
|- om (_ On
Theorem	limomss 3136	The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity.
|- (Lim A -> om (_ A)
Theorem	nnont 3137	A natural number is an ordinal number.
|- (A e. om -> A e. On)
Theorem	nnon 3138	A natural number is an ordinal number.
|- A e. om   =>   |- A e. On
Theorem	nnord 3139	A natural number is ordinal.
|- (A e. om -> Ord A)
Theorem	ordom 3140	Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43.
|- Ord om
Theorem	elnn 3141	A member of a natural number is a natural number.
|- ((A e. B /\ B e. om) -> A e. om)
Theorem	omon 3142	The class of natural numbers om is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43.
|- (om e. On \/ om = On)
Theorem	nnlim 3143	A natural number is not a limit ordinal.
|- (A e. om -> -. Lim A)
Theorem	omssnlim 3144	The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42.
|- om (_ {x e. On | -. Lim x}
Theorem	limom 3145	Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Our proof, however, does not require the Axiom of Infinity.
|- Lim om
Theorem	peano2b 3146	A class belongs to omega iff its successor does.
|- (A e. om <-> suc A e. om)
Theorem	nnsuc 3147	A non-zero natural number is a successor.
|- ((A e. om /\ A =/= (/)) -> E.x e. om A = suc x)
Peano's postulates
Theorem	peano1 3148	Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 3148 through peano5 3152 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity.
|- (/) e. om
Theorem	peano2 3149	The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42.
|- (A e. om -> suc A e. om)
Theorem	peano3 3150	The successor of any natural number is not zero. One of Peano's 5 postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42.
|- (A e. om -> suc A =/= (/))
Theorem	peano4 3151	Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's 5 postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43.
|- ((A e. om /\ B e. om) -> (suc A = suc B <-> A = B))
Theorem	peano5 3152	The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's 5 postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43.
|- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om (_ A)
Theorem	nn0suc 3153	A natural number is either 0 or a successor.
|- (A e. om -> (A = (/) \/ E.x e. om A = suc x))
Finite induction (for finite ordinals)
Theorem	find 3154	The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-01. The hypothesis states that A is a set of natural numbers, zero belongs to A, and given any member of A the member's successor also belongs to A. The conclusion is that every natural number is in A.
|- (A (_ om /\ (/) e. A /\ A.x e. A suc x e. A)   =>   |- A = om
Theorem	finds 3155	Principle of Finite Induction (inference schema) with implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- ps   &   |- (y e. om -> (ch -> th))   =>   |- (A e. om -> ta)
Theorem	findsg 3156	Principle of Finite Induction (inference schema) with implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. The basis of this version is an arbitrary natural number B instead of zero.
|- (x = B -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- (B e. om -> ps)   &   |- (((y e. om /\ B e. om) /\ B (_ y) -> (ch -> th))   =>   |- (((A e. om /\ B e. om) /\ B (_ A) -> ta)
Theorem	finds2 3157	Principle of Finite Induction (inference schema) with implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (ta -> ps)   &   |- (y e. om -> (ta -> (ch -> th)))   =>   |- (x e. om -> (ta -> ph))
Theorem	finds1 3158	Principle of Finite Induction (inference schema) with implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- ps   &   |- (y e. om -> (ch -> th))   =>   |- (x e. om -> ph)
Theorem	findes 3159	Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136. (Contributed by Raph Levien, 9-Jul-2003.)
|- [(/) / x]ph   &   |- (x e. om -> (ph -> [suc x / x]ph))   =>   |- (x e. om -> ph)
Theorem	tfinds 3160	Principle of Transfinite Induction (inference schema) with implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction hypothesis for successors, and the induction hypothesis for limit ordinals. Theorem Schema 4 of [Suppes] p. 197.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (