Metamath Proof Explorer - mmtheorems24

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 - 2301-2400 - Page 24 of 58

Type	Label	Description
Statement
Theorem	sucexb 2301	A successor exists iff its class argument exists.
⊢ (A ∈ V ↔ suc A ∈ V)
Theorem	sucexg 2302	The successor of a set is a set (generalization).
⊢ (A ∈ B → suc A ∈ V)
Theorem	sucex 2303	The successor of a set is a set.
⊢ A ∈ V    ⇒   ⊢ suc A ∈ V
Theorem	sucid 2304	A set belongs to its successor.
⊢ A ∈ V    ⇒   ⊢ A ∈ suc A
Theorem	sucidg 2305	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized).
⊢ (A ∈ B → A ∈ suc A)
Theorem	nsuceq0 2306	No successor is empty.
⊢ ¬ suc A = ∅
Theorem	eqelsuc 2307	A set belongs to the successor of an equal set.
⊢ A ∈ V    ⇒   ⊢ (A = B → A ∈ suc B)
Theorem	trsuc 2308	A set whose successor belongs to a transitive class also belongs.
⊢ ((Tr A ∧ suc B ∈ A) → B ∈ A)
Theorem	trsucss 2309	A member of the successor of a transitive class is a subclass of it.
⊢ (Tr A → (B ∈ suc A → B ⊆ A))
Theorem	ordsssuc 2310	A subset of an ordinal is a member of its successor.
⊢ ((A ∈ On ∧ Ord B) → (A ⊆ B ↔ A ∈ suc B))
Theorem	onsssuc 2311	A subset of an ordinal number is a member of its successor.
⊢ ((A ∈ On ∧ B ∈ On) → (A ⊆ B ↔ A ∈ suc B))
Theorem	onmindif 2312	When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass.
⊢ ((A ⊆ On ∧ B ∈ On) → B ∈ ∩(A ∖ suc B))
Theorem	onmindif2 2313	The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed.
⊢ ((A ⊆ On ∧ ¬ A = ∅) → ∩A ∈ ∩ (A ∖ {∩A}))
Theorem	suceloni 2314	The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41.
⊢ (A ∈ On → suc A ∈ On)
Theorem	onpwsuc 2315	The collection of ordinal numbers in the power set of an ordinal number is its successor.
⊢ (A ∈ On → (℘A ∩ On) = suc A)
Theorem	ordnbtwn 2316	There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41.
⊢ (Ord A → ¬ (A ∈ B ∧ B ∈ suc A))
Theorem	onnbtwn 2317	There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41.
⊢ (A ∈ On → ¬ (A ∈ B ∧ B ∈ suc A))
Theorem	ordsuc 2318	The successor of an ordinal class is ordinal.
⊢ (Ord A ↔ Ord suc A)
Theorem	sucelon 2319	The successor of an ordinal number is an ordinal number.
⊢ (A ∈ On ↔ suc A ∈ On)
Theorem	ordsucss 2320	The successor of an element of an ordinal class is a subset of it.
⊢ (Ord B → (A ∈ B → suc A ⊆ B))
Theorem	sucssel 2321	A set whose successor is a subset of another class is a member of that class.
⊢ (A ∈ C → (suc A ⊆ B → A ∈ B))
Theorem	ordelsuc 2322	A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse.
⊢ ((A ∈ C ∧ Ord B) → (A ∈ B ↔ suc A ⊆ B))
Theorem	onsucmin 2323	The successor of an ordinal number is the smallest larger ordinal number.
⊢ (A ∈ On → suc A = ∩{x ∈ On∣A ∈ x})
Theorem	ordsucelsuc 2324	Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42.
⊢ (Ord B → (A ∈ B ↔ suc A ∈ suc B))
Theorem	ordsucsssuc 2325	The subclass relationship between two ordinal classes is inherited by their successors.
⊢ ((Ord A ∧ Ord B) → (A ⊆ B ↔ suc A ⊆ suc B))
Theorem	orddif 2326	Ordinal derived from its successor.
⊢ (Ord A → A = (suc A ∖ {A}))
Theorem	orduniss 2327	An ordinal class includes its union.
⊢ (Ord A → ∪A ⊆ A)
Theorem	ordtri2or 2328	A trichotomy law for ordinal classes.
⊢ ((Ord A ∧ Ord B) → (A ∈ B ∨ B ⊆ A))
Theorem	ordtri2or2 2329	A trichotomy law for ordinal classes.
⊢ ((Ord A ∧ Ord B) → (A ⊆ B ∨ B ⊆ A))
Theorem	ordssun 2330	Property of a subclass of the maximum (i.e. union) of two ordinals.
⊢ ((Ord B ∧ Ord C) → (A ⊆ (B ∪ C) ↔ (A ⊆ B ∨ A ⊆ C)))
Theorem	ordequn 2331	The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40.
⊢ ((Ord B ∧ Ord C) → (A = (B ∪ C) → (A = B ∨ A = C)))
Theorem	ordun 2332	The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40.
⊢ ((Ord A ∧ Ord B) → Ord (A ∪ B))
Theorem	ordsucun 2333	The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors.
⊢ ((Ord A ∧ Ord B) → suc (A ∪ B) = (suc A ∪ suc B))
Theorem	ordunisssuc 2334	A subclass relationship for union and successor of ordinal classes.
⊢ ((A ⊆ On ∧ Ord B) → (∪A ⊆ B ↔ A ⊆ suc B))
Theorem	onsucuni 2335	A class of ordinal numbers is a subclass of the successor of its union. Similar to Proposition 7.26 of [TakeutiZaring] p. 41.
⊢ (A ⊆ On → A ⊆ suc ∪A)
Theorem	ordsucuni 2336	An ordinal class is a subclass of the successor of its union.
⊢ (Ord A → A ⊆ suc ∪A)
Theorem	orduniorsuc 2337	An ordinal class is either its union or the successor of its union.
⊢ (Ord A → (A = ∪A ∨ A = suc ∪A))
Theorem	unon 2338	The class of all ordinals is its own union. Exercise 11 of [TakeutiZaring] p. 40.
⊢ ∪On = On
Theorem	ordunisuc 2339	An ordinal class is equal to the union of its successor.
⊢ (Ord A → ∪suc A = A)
Theorem	0elsuc 2340	The successor of an ordinal class contains the empty set.
⊢ (Ord A → ∅ ∈ suc A)
Theorem	suc11 2341	The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194.
⊢ ((A ∈ On ∧ B ∈ On) → (suc A = suc B ↔ A = B))
Theorem	limon 2342	The class of ordinal numbers is a limit ordinal.
⊢ Lim On
Theorem	onord 2343	An ordinal number is an ordinal class.
⊢ A ∈ On    ⇒   ⊢ Ord A
Theorem	ontrc 2344	An ordinal number is a transitive class.
⊢ A ∈ On    ⇒   ⊢ Tr A
Theorem	oneirr 2345	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192.
⊢ A ∈ On    ⇒   ⊢ ¬ A ∈ A
Theorem	onel 2346	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192.
⊢ A ∈ On    ⇒   ⊢ (B ∈ A → B ∈ On)
Theorem	onss 2347	An ordinal number is a subset of On.
⊢ A ∈ On    ⇒   ⊢ A ⊆ On
Theorem	onelss 2348	A member of an ordinal number is a subset of it.
⊢ A ∈ On    ⇒   ⊢ (B ∈ A → B ⊆ A)
Theorem	onssneli 2349	An ordering law for ordinals.
⊢ A ∈ On    ⇒   ⊢ (A ⊆ B → ¬ B ∈ A)
Theorem	onssneli2 2350	An ordering law for ordinals.
⊢ A ∈ On    ⇒   ⊢ (B ⊆ A → ¬ A ∈ B)
Theorem	onelin 2351	An element of an ordinal number equals the intersection with it.
⊢ A ∈ On    ⇒   ⊢ (B ∈ A → B = (B ∩ A))
Theorem	onelun 2352	An ordinal number equals its union with any element.
⊢ A ∈ On    ⇒   ⊢ (B ∈ A → (A ∪ B) = A)
Theorem	onsuc 2353	The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193.
⊢ A ∈ On    ⇒   ⊢ suc A ∈ On
Theorem	onunisuc 2354	An ordinal number is equal to the union of its successor.
⊢ A ∈ On    ⇒   ⊢ ∪suc A = A
Theorem	onuniorsuc 2355	An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union.
⊢ A ∈ On    ⇒   ⊢ (A = ∪A ∨ A = suc ∪A)
Theorem	onuninsuc 2356	A limit ordinal is not a successor ordinal.
⊢ A ∈ On    ⇒   ⊢ (A = ∪A ↔ ¬ ∃x ∈ On A = suc x)
Theorem	onssel 2357	Subset is equivalent to membership or equality for ordinal numbers.
⊢ A ∈ On    &   ⊢ B ∈ On    ⇒   ⊢ (A ⊆ B ↔ (A ∈ B ∨ A = B))
Theorem	onun 2358	The union of two ordinal numbers is an ordinal number.
⊢ A ∈ On    &   ⊢ B ∈ On    ⇒   ⊢ (A ∪ B) ∈ On
Theorem	onsucss 2359	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 ∈ On    &   ⊢ B ∈ On    ⇒   ⊢ (A ∈ B ↔ suc A ⊆ B)
Theorem	limsuclem 2360	Lemma for limsuc 2361.
⊢ A ∈ On    &   ⊢ B ∈ On    ⇒   ⊢ ((Lim A ∧ B ∈ A) → suc B ∈ A)
Theorem	limsuc 2361	The successor of a member of a limit ordinal is also a member.
⊢ (Lim A → (B ∈ A ↔ suc B ∈ A))
Theorem	limsssuc 2362	A class includes a limit ordinal iff the successor of the class includes it.
⊢ (Lim A → (A ⊆ B ↔ A ⊆ suc B))
Theorem	nlimsuc 2363	A successor is not a limit ordinal.
⊢ A ∈ V    ⇒   ⊢ ¬ Lim suc A
Theorem	unizlim 2364	An ordinal equal to its own union is either zero or a limit ordinal.
⊢ (Ord A → (A = ∪A ↔ (A = ∅ ∨ Lim A)))
Theorem	orduninsuc 2365	A limit ordinal is not a successor ordinal.
⊢ (Ord A → (A = ∪A ↔ ¬ ∃x ∈ On A = suc x))
Theorem	ordzsl 2366	An ordinal is zero, a successor ordinal, or a limit ordinal.
⊢ (Ord A ↔ (A = ∅ ∨ ∃x ∈ On A = suc x ∨ Lim A))
Theorem	onzsl 2367	An ordinal number is zero, a successor ordinal, or a limit ordinal number.
⊢ (A ∈ On ↔ (A = ∅ ∨ ∃x ∈ On A = suc x ∨ (A ∈ V ∧ Lim A)))
Theorem	dflim3 2368	An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor.
⊢ (Lim A ↔ (Ord A ∧ ¬ (A = ∅ ∨ ∃x ∈ On A = suc x)))
Theorem	nlimon 2369	Two ways of expressing 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 ∈ On∣(x = ∅ ∨ ∃y ∈ On x = suc y)} = {x ∈ On∣ ¬ Lim x}
Theorem	on0eqelt 2370	An ordinal number either equals zero or contains zero.
⊢ (A ∈ On → (A = ∅ ∨ ∅ ∈ A))
Theorem	snsn0non 2371	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 2377). It can be used to represent an "undefined" value for a partial operation on natural numbers or ordinals. See also onxpdisj 2476.
⊢ ¬ {{∅}} ∈ On
Syntax	com 2372	Extend class notation to include the class of natural numbers.
class ω
Definition	df-om 2373	Define the class of natural numbers. Our definition is a variant of the Definition of N of [BellMachover] p. 471. See dfom2 2374 for an alternate definition. Later, when we assume the Axiom of Infinity, we show ω is a set in omex 3475, and ω can then be defined per dfom3 3477 (the smallest inductive set) and dfom4 3479. Note: the natural numbers ω are a subset of the ordinal numbers df-on 2203. These are different from the natural number subset of complex numbers defined later (df-n 4423), although the two sets have analogous properties and operations defined on them.
⊢ ω = {x∣(Ord x ∧ ∀y(Lim y → x ∈ y))}
Theorem	dfom2 2374	An alternate definition of the set of natural numbers ω. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the inner class abstraction of non-limit ordinal numbers (see nlimon 2369).
⊢ ω = {x ∈ On∣suc x ⊆ {y ∈ On∣ ¬ Lim y}}
Theorem	elom 2375	Membership in omega. The hypothesis can be eliminated if we assume the Axiom of Infinity; see elom3 3478.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ω ↔ (Ord A ∧ ∀x(Lim x → A ∈ x)))
Theorem	elomg 2376	Membership in omega. The antecedent can be eliminated if we assume the Axiom of Infinity; see elom3 3478.
⊢ (A ∈ B → (A ∈ ω ↔ (Ord A ∧ ∀x(Lim x → A ∈ x))))
Theorem	omsson 2377	Omega is a subset of On.
⊢ ω ⊆ On
Theorem	limomss 2378	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 → ω ⊆ A)
Theorem	nnont 2379	A natural number is an ordinal number.
⊢ (A ∈ ω → A ∈ On)
Theorem	nnon 2380	A natural number is an ordinal number.
⊢ A ∈ ω    ⇒   ⊢ A ∈ On
Theorem	nnord 2381	A natural number is ordinal.
⊢ (A ∈ ω → Ord A)
Theorem	ordom 2382	Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43.
⊢ Ord ω
Theorem	elnn 2383	A member of a natural number is a natural number.
⊢ ((A ∈ B ∧ B ∈ ω) → A ∈ ω)
Theorem	omon 2384	The class of natural numbers ω is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinals (if we deny the Axiom of Infinity). Remark of [TakeutiZaring] p. 43.
⊢ (ω ∈ On ∨ ω = On)
Theorem	nnlim 2385	A natural number is not a limit ordinal.
⊢ (A ∈ ω → ¬ Lim A)
Theorem	omssnlim 2386	The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42.
⊢ ω ⊆ {x ∈ On∣ ¬ Lim x}
Theorem	limom 2387	Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Our proof, however, does not require the axiom of Infinity.
⊢ Lim ω
Theorem	peano2b 2388	A class belongs to omega iff its successor does.
⊢ (A ∈ ω ↔ suc A ∈ ω)
Theorem	nnsuc 2389	A non-zero natural number is a successor.
⊢ ((A ∈ ω ∧ ¬ A = ∅) → ∃x ∈ ω A = suc x)
Theorem	peano1 2390	Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: our proofs of peano1 2390 through peano5 2394 do not use the axiom of Infinity.
⊢ ∅ ∈ ω
Theorem	peano2 2391	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 ∈ ω → suc A ∈ ω)
Theorem	peano3 2392	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 ∈ ω → ¬ suc A = ∅)
Theorem	peano4 2393	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 ∈ ω ∧ B ∈ ω) → (suc A = suc B ↔ A = B))
Theorem	peano5 2394	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.
⊢ ((∅ ∈ A ∧ ∀x ∈ ω (x ∈ A → suc x ∈ A)) → ω ⊆ A)
Theorem	nn0suc 2395	A natural number is either 0 or a successor.
⊢ (A ∈ ω → (A = ∅ ∨ ∃x ∈ ω A = suc x))
Theorem	find 2396	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 ⊆ ω ∧ ∅ ∈ A ∧ ∀x ∈ A suc x ∈ A)    ⇒   ⊢ A = ω
Theorem	finds 2397	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 = ∅ → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = suc y → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ ω → (χ → θ))    ⇒   ⊢ (A ∈ ω → τ)
Theorem	findsg 2398	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 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = suc y → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ (B ∈ ω → ψ)    &   ⊢ (((y ∈ ω ∧ B ∈ ω) ∧ B ⊆ y) → (χ → θ))    ⇒   ⊢ (((A ∈ ω ∧ B ∈ ω) ∧ B ⊆ A) → τ)
Theorem	finds2 2399	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 = ∅ → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = suc y → (φ ↔ θ))    &   ⊢ (τ → ψ)    &   ⊢ (y ∈ ω → (τ → (χ → θ)))    ⇒   ⊢ (x ∈ ω → (τ → φ))
Theorem	findes 2400	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-03.)
⊢ [∅ / x]φ    &   ⊢ (x ∈ ω → (φ → [suc x / x]φ))    ⇒   ⊢ (x ∈ ω → φ)