Metamath Proof Explorer - mmtheorems23

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 - 2201-2300 - Page 23 of 58

Type	Label	Description
Statement
Syntax	csuc 2201	Extend class notation to include the successor function.
class suc A
Definition	df-ord 2202	Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the epsilon relation. Variant of definition of [BellMachover] p. 468.
|- (Ord A <-> (Tr A /\ E We A))
Definition	df-on 2203	Define the class of all ordinals. Definition 7.11 of [TakeutiZaring] p. 38.
|- On = {x | Ord x}
Definition	df-lim 2204	Define the limit ordinal predicate, which is true for a non-empty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 2280 and dflim3 2368 for alternate definitions.
|- (Lim A <-> (Ord A /\ -. A = (/) /\ A = U.A))
Definition	df-suc 2205	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 3132). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no affect on a proper class (sucprc 2297), so that the successor of any ordinal class is still an ordinal class (ordsuc 2318), simplifying certain proofs. Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript.
|- suc A = (A u. {A})
Theorem	ordeq 2206	Equality theorem for the ordinal predicate.
|- (A = B -> (Ord A <-> Ord B))
Theorem	elong 2207	An ordinal number is an ordinal set.
|- (A e. B -> (A e. On <-> Ord A))
Theorem	elon 2208	An ordinal number is an ordinal set.
|- A e. V   =>   |- (A e. On <-> Ord A)
Theorem	eloni 2209	An ordinal number has the ordinal property.
|- (A e. On -> Ord A)
Theorem	elon2 2210	An ordinal number is an ordinal set.
|- (A e. On <-> (Ord A /\ A e. V))
Theorem	limeq 2211	Equality theorem for the limit predicate.
|- (A = B -> (Lim A <-> Lim B))
Theorem	ordwe 2212	Epsilon well orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36.
|- (Ord A -> E We A)
Theorem	ordtr 2213	An ordinal class is transitive.
|- (Ord A -> Tr A)
Theorem	ordfr 2214	Epsilon is well-founded on an ordinal class.
|- (Ord A -> E Fr A)
Theorem	ordelss 2215	An element of an ordinal class is a subset of it.
|- ((Ord A /\ B e. A) -> B (_ A)
Theorem	trssord 2216	A transitive subclass of an ordinal class is ordinal.
|- ((Tr A /\ A (_ B /\ Ord B) -> Ord A)
Theorem	ordeirr 2217	Epsilon irreflexivity of ordinals: no ordinal is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. For ordinals, we can prove this without invoking the Axiom of Regularity.
|- (Ord A -> -. A e. A)
Theorem	nordeq 2218	A member of an ordinal class is not equal to it.
|- ((Ord A /\ B e. A) -> -. A = B)
Theorem	ordn2lp 2219	An ordinal class cannot an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469.
|- (Ord A -> -. (A e. B /\ B e. A))
Theorem	tz7.5 2220	A subclass (possibly proper) of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36.
|- ((Ord A /\ (B (_ A /\ -. B = (/))) -> E.x e. B (B i^i x) = (/))
Theorem	ordelord 2221	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36.
|- ((Ord A /\ B e. A) -> Ord B)
Theorem	ordelon 2222	An element of an ordinal class is an ordinal number.
|- ((Ord A /\ B e. A) -> B e. On)
Theorem	onelon 2223	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469.
|- ((A e. On /\ B e. A) -> B e. On)
Theorem	tz7.7 2224	Proposition 7.7 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Tr B) -> (B e. A <-> (B (_ A /\ -. B = A)))
Theorem	ordelssne 2225	Corollary 7.8 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Ord B) -> (A e. B <-> (A (_ B /\ -. A = B)))
Theorem	ordelpss 2226	Corollary 7.8 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Ord B) -> (A e. B <-> A (. B))
Theorem	ordsseleq 2227	For ordinals, subclass is equivalent to membership or equality.
|- ((Ord A /\ Ord B) -> (A (_ B <-> (A e. B \/ A = B)))
Theorem	ordin 2228	Proposition 7.9 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Ord B) -> Ord (A i^i B))
Theorem	onin 2229	The intersection of two ordinal numbers is an ordinal number.
|- ((A e. On /\ B e. On) -> (A i^i B) e. On)
Theorem	ordtri3or 2230	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38.
|- ((Ord A /\ Ord B) -> (A e. B \/ A = B \/ B e. A))
Theorem	ordtri1 2231	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A (_ B <-> -. B e. A))
Theorem	ontri1 2232	A trichotomy law for ordinal numbers.
|- ((A e. On /\ B e. On) -> (A (_ B <-> -. B e. A))
Theorem	ordtri2 2233	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A e. B <-> -. (A = B \/ B e. A)))
Theorem	ordtri3 2234	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A = B <-> -. (A e. B \/ B e. A)))
Theorem	ordtri4 2235	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A = B <-> (A (_ B /\ -. A e. B)))
Theorem	orddisj 2236	An ordinal class and its singleton are disjoint.
|- (Ord A -> (A i^i {A}) = (/))
Theorem	onfr 2237	The ordinal class is founded. This lemma is needed for ordon 2238 in order to eliminate the need for the Axiom of Regularity.
|- E Fr On
Theorem	ordon 2238	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity.
|- Ord On
Theorem	epweon 2239	The epsilon relation well-orders the class of ordinal numbers. Proposition 4.8(g) of [Mendelson] p. 244.
|- E We On
Theorem	onprc 2240	No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark of [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinals is ordinal (ordon 2238), it must be both an element of the set of all ordinals yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence.
|- -. On e. V
Theorem	ordeleqon 2241	A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse.
|- (Ord A <-> (A e. On \/ A = On))
Theorem	ordsson 2242	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38.
|- (Ord A -> A (_ On)
Theorem	onsst 2243	An ordinal number is a subset of the class of ordinal numbers.
|- (A e. On -> A (_ On)
Theorem	tfi 2244	The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring] p. 39. This principle states that if A is a class of ordinals with the property that every ordinal number that is a subset of A also belongs to A, then every ordinal is in A.
|- ((A (_ On /\ A.x e. On (x (_ A -> x e. A)) -> A = On)
Theorem	tfis 2245	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 2246	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 2247	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 2248	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)
Theorem	ssorduni 2249	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40.
|- (A (_ On -> Ord U.A)
Theorem	onunit 2250	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132.
|- (A e. B -> (A (_ On -> U.A e. On))
Theorem	onuni 2251	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193.
|- A e. V   =>   |- (A (_ On -> U.A e. On)
Theorem	uniord 2252	The union of an ordinal class is ordinal.
|- (Ord A -> Ord U.A)
Theorem	onelpsst 2253	Relationship between membership and proper subset of an ordinal number.
|- ((A e. On /\ B e. On) -> (A e. B <-> (A (_ B /\ -. A = B)))
Theorem	onsseleq 2254	Relationship between subset and membership of an ordinal number.
|- ((A e. On /\ B e. On) -> (A (_ B <-> (A e. B \/ A = B)))
Theorem	onelsst 2255	An element of an ordinal number is a subset of the number.
|- (A e. On -> (B e. A -> B (_ A))
Theorem	ordtr1 2256	Transitive law for ordinal classes.
|- (Ord C -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ordtr2 2257	Transitive law for ordinal classes.
|- ((Ord A /\ Ord C) -> ((A (_ B /\ B e. C) -> A e. C))
Theorem	ontr1 2258	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
|- (C e. On -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ontr2 2259	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40.
|- ((A e. On /\ C e. On) -> ((A (_ B /\ B e. C) -> A e. C))
Theorem	ordunidif 2260	The union of an ordinal stays the same if a subset equal to one of its elements is removed.
|- ((Ord A /\ B e. A) -> U.(A \ B) = U.A)
Theorem	onint 2261	The intersection (infimum) of a non-empty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45.
|- ((A (_ On /\ -. A = (/)) -> |^|A e. A)
Theorem	onint0 2262	The intersection of a class of ordinal numbers is zero iff the class contains zero.
|- (A (_ On -> (|^|A = (/) <-> (/) e. A))
Theorem	onssmin 2263	A non-empty class of ordinal numbers has a smallest member. Exercise 9 of [TakeutiZaring] p. 40.
|- ((A (_ On /\ -. A = (/)) -> E.x e. A A.y e. A x (_ y)
Theorem	onminsb 2264	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228.
|- (ps -> A.xps)   &   |- (x = |^|{x e. On | ph} -> (ph <-> ps))   =>   |- (E.x e. On ph -> ps)
Theorem	onminesb 2265	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228.
|- (E.x e. On ph -> [|^|{x e. On | ph} / x]ph)
Theorem	onintss 2266	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228.
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (ps -> |^|{x e. On | ph} (_ A))
Theorem	oninton 2267	The intersection of a non-empty collection of ordinals is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44.
|- ((A (_ On /\ -. A = (/)) -> |^|A e. On)
Theorem	onintrab 2268	The intersection of a non-empty class abstraction of ordinals exists iff it is an ordinal number.
|- (|^|{x e. On | ph} e. V <-> |^|{x e. On | ph} e. On)
Theorem	onintrab2 2269	An existence condition equivalent to an intersection's being an ordinal number.
|- (E.x e. On ph <-> |^|{x e. On | ph} e. On)
Theorem	onnmin 2270	No member of a set of ordinal numbers belongs to its minimum.
|- ((A (_ On /\ B e. A) -> -. B e. |^|A)
Theorem	onnminsb 2271	An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. ps is the wff resulting from the substitution of A for x in wff ph.
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (A e. |^|{x e. On | ph} -> -. ps))
Theorem	oneqmini 2272	A way to show that an ordinal number equals the minimum of a collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection.
|- (B (_ On -> ((A e. B /\ A.x e. A -. x e. B) -> A = |^|B))
Theorem	oneqmin 2273	A way to show that an ordinal number equals the minimum of a non-empty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection.
|- ((B (_ On /\ -. B = (/)) -> (A = |^|B <-> (A e. B /\ A.x e. A -. x e. B)))
Theorem	bm2.5ii 2274	Problem 2.5(ii) of [BellMachover] p. 471.
|- A e. V   =>   |- (A (_ On -> U.A = |^|{x e. On | A.y e. A y (_ x})
Theorem	onminex 2275	If a wff is true for an ordinal number, there is a smallest ordinal number for which it is true.
|- (x = y -> (ph <-> ps))   =>   |- (E.x e. On ph ->