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-10658

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

Type	Label	Description
Statement
Theorem	onunisuc 3101	An ordinal number is equal to the union of its successor.
|- A e. On   =>   |- U.suc A = A
Theorem	onuniorsuc 3102	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 3103	A limit ordinal is not a successor ordinal.
|- A e. On   =>   |- (A = U.A <-> -. E.x e. On A = suc x)
Theorem	onssel 3104	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 3105	The union of two ordinal numbers is an ordinal number.
|- A e. On   &   |- B e. On   =>   |- (A u. B) e. On
Theorem	onsucss 3106	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 3107	A successor is not a limit ordinal.
|- (A e. B -> -. Lim suc A)
Theorem	unizlim 3108	An ordinal equal to its own union is either zero or a limit ordinal.
|- (Ord A -> (A = U.A <-> (A = (/) \/ Lim A)))
Theorem	orduninsuc 3109	An ordinal equal to its union is not a successor.
|- (Ord A -> (A = U.A <-> -. E.x e. On A = suc x))
Theorem	ordunisuc2 3110	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 3111	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 3112	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 3113	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 3114	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A.x e. A suc x e. A))
Theorem	limsuc 3115	The successor of a member of a limit ordinal is also a member.
|- (Lim A -> (B e. A <-> suc B e. A))
Theorem	limsssuc 3116	A class includes a limit ordinal iff the successor of the class includes it.
|- (Lim A -> (A (_ B <-> A (_ suc B))
Theorem	nlimon 3117	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 3118	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 3119	An ordinal number either equals zero or contains zero.
|- (A e. On -> (A = (/) \/ (/) e. A))
Theorem	snsn0non 3120	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 3131). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 3236.
|- -. {{(/)}} e. On
Transfinite induction
Theorem	tfi 3121	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 3122	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 3123	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 3124	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 3125	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 3126	Extend class notation to include the class of natural numbers.
class om
Definition	df-om 3127	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 3128 for an alternate definition. Later, when we assume the Axiom of Infinity, we show om is a set in omex 4608, and om can then be defined per dfom3 4611 (the smallest inductive set) and dfom4 4613. Note: the natural numbers om are a subset of the ordinal numbers df-on 2947. They are completely different from the natural numbers NN (df-n 5882) 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 3128	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 3117).
|- om = {x e. On | suc x (_ {y e. On | -. Lim y}}
Theorem	elom 3129	Membership in omega. The hypothesis can be eliminated if we assume the Axiom of Infinity; see elom3 4612.
|- A e. V   =>   |- (A e. om <-> (Ord A /\ A.x(Lim x -> A e. x)))
Theorem	elomg 3130	Membership in omega. The antecedent can be eliminated if we assume the Axiom of Infinity; see elom3 4612.
|- (A e. B -> (A e. om <-> (Ord A /\ A.x(Lim x -> A e. x))))
Theorem	omsson 3131	Omega is a subset of On.
|- om (_ On
Theorem	limomss 3132	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 3133	A natural number is an ordinal number.
|- (A e. om -> A e. On)
Theorem	nnon 3134	A natural number is an ordinal number.
|- A e. om   =>   |- A e. On
Theorem	nnord 3135	A natural number is ordinal.
|- (A e. om -> Ord A)
Theorem	ordom 3136	Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43.
|- Ord om
Theorem	elnn 3137	A member of a natural number is a natural number.
|- ((A e. B /\ B e. om) -> A e. om)
Theorem	omon 3138	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 3139	A natural number is not a limit ordinal.
|- (A e. om -> -. Lim A)
Theorem	omssnlim 3140	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 3141	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 3142	A class belongs to omega iff its successor does.
|- (A e. om <-> suc A e. om)
Theorem	nnsuc 3143	A non-zero natural number is a successor.
|- ((A e. om /\ A =/= (/)) -> E.x e. om A = suc x)
Peano's postulates
Theorem	peano1 3144	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 3144 through peano5 3148 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity.
|- (/) e. om
Theorem	peano2 3145	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 3146	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 3147	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 3148	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 3149	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 3150	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-2001. 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 3151	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 3152	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 3153	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 3154	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 3155	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 3156	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 -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- ps   &   |- (y e. On -> (ch -> th))   &   |- (Lim x -> (A.y e. x ch -> ph))   =>   |- (A e. On -> ta)
Theorem	tfindsg 3157	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. The basis of this version is an arbitrary ordinal B instead of zero. Remark in [TakeutiZaring] p. 57.
|- (x = B -> (ph <-> ps))   &   |- (