P. 433 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43201-43300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iocmbl 43201	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol)
Theorem	cnioobibld 43202*	A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider 𝐹 = (𝑥 ∈ (0(,)1) ↦ (1 / 𝑥)). See cniccibl 25890 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	arearect 43203	The area of a rectangle whose sides are parallel to the coordinate axes in (ℝ × ℝ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝐶 ≤ 𝐷    &   ⊢ 𝑆 = ((𝐴[,]𝐵) × (𝐶[,]𝐷))    ⇒   ⊢ (area‘𝑆) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))
Theorem	areaquad 43204*	The area of a quadrilateral with two sides which are parallel to the y-axis in (ℝ × ℝ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    &   ⊢ 𝐸 ∈ ℝ    &   ⊢ 𝐹 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐶 ≤ 𝐸    &   ⊢ 𝐷 ≤ 𝐹    &   ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))    &   ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}    ⇒   ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
21.36  Mathbox for Richard Penner
21.36.1  Set Theory and Ordinal Numbers
Theorem	uniel 43205*	Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.)
⊢ (∪ 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦))
Theorem	unielss 43206*	Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ⊆ 𝐵 → (∪ 𝐵 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥))
Theorem	unielid 43207*	Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (∪ 𝐴 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥)
Theorem	ssunib 43208*	Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦)
Theorem	rp-intrabeq 43209*	Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥})
Theorem	rp-unirabeq 43210*	Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 = 𝐵 → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦})
Theorem	onmaxnelsup 43211*	Two ways to say the maximum element of a class of ordinals is also the supremum of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (¬ 𝐴 ⊆ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥))
Theorem	onsupneqmaxlim0 43212	If the supremum of a class of ordinals is not in that class, then the supremum is a limit ordinal or empty. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (𝐴 ⊆ ∪ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴))
Theorem	onsupcl2 43213	The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 ∈ On)
Theorem	onuniintrab 43214*	The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Closed form of uniordint 7820. (Contributed by RP, 28-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onintunirab 43215*	The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})
Theorem	onsupnmax 43216	If the union of a class of ordinals is not the maximum element of that class, then the union is a limit ordinal or empty. But this isn't a biconditional since 𝐴 could be a non-empty set where a limit ordinal or the empty set happens to be the largest element. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴))
Theorem	onsupuni 43217	The supremum of a set of ordinals is the union of that set. Lemma 2.10 of [Schloeder] p. 5. (Contributed by RP, 19-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → sup(𝐴, On, E ) = ∪ 𝐴)
Theorem	onsupuni2 43218	The supremum of a set of ordinals is the union of that set. (Contributed by RP, 22-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → sup(𝐴, On, E ) = ∪ 𝐴)
Theorem	onsupintrab 43219*	The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Definition 2.9 of [Schloeder] p. 5. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → sup(𝐴, On, E ) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onsupintrab2 43220*	The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → sup(𝐴, On, E ) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onsupcl3 43221*	The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ On)
Theorem	onsupex3 43222*	The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ V)
Theorem	onuniintrab2 43223*	The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	oninfint 43224	The infimum of a non-empty class of ordinals is the intersection of that class. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → inf(𝐴, On, E ) = ∩ 𝐴)
Theorem	oninfunirab 43225*	The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → inf(𝐴, On, E ) = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})
Theorem	oninfcl2 43226*	The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ On)
Theorem	onsupmaxb 43227	The union of a class of ordinals is an element is an element of that class if and only if there is a maximum element of that class under the epsilon relation, which is to say that the domain of the restricted epsilon relation is not the whole class. (Contributed by RP, 25-Jan-2025.)
⊢ (𝐴 ⊆ On → (dom ( E ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ¬ ∪ 𝐴 ∈ 𝐴))
Theorem	onexgt 43228*	For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ 𝑥)
Theorem	onexomgt 43229*	For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ·o 𝑥))
Theorem	omlimcl2 43230	The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐵 ·o 𝐴))
Theorem	onexlimgt 43231*	For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥))
Theorem	onexoegt 43232*	For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))
Theorem	oninfex2 43233*	The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V)
Theorem	onsupeqmax 43234*	Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∪ 𝐴 ∈ 𝐴))
Theorem	onsupeqnmax 43235*	Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ (∪ 𝐴 = ∪ ∪ 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴)))
Theorem	onsuplub 43236*	The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (𝐵 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝐵 ∈ 𝑧))
Theorem	onsupnub 43237*	An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵)) → ∪ 𝐴 ⊆ 𝐵)
Theorem	onfisupcl 43238	Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9323. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴))
Theorem	onelord 43239	Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6410 and eloni 6395. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	onepsuc 43240	Every ordinal is less than its successor, relationship version. Lemma 1.7 of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ (𝐴 ∈ On → 𝐴 E suc 𝐴)
Theorem	epsoon 43241	The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7793 and weso 5679. (Contributed by RP, 15-Jan-2025.)
⊢ E Or On
Theorem	epirron 43242	The strict order on the ordinals is irreflexive. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ (𝐴 ∈ On → ¬ 𝐴 E 𝐴)
Theorem	oneptr 43243	The strict order on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 E 𝐵 ∧ 𝐵 E 𝐶) → 𝐴 E 𝐶))
Theorem	oneltr 43244	The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6431. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	oneptri 43245	The strict, complete (linear) order on the ordinals is complete. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ∨ 𝐵 E 𝐴 ∨ 𝐴 = 𝐵))
Theorem	oneltri 43246	The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6417. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵))
Theorem	ordeldif 43247	Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ordeldifsucon 43248	Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordeldif1o 43249	Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.)
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅)))
Theorem	ordne0gt0 43250	Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6440. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
Theorem	ondif1i 43251	Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8537. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴)
Theorem	onsucelab 43252*	The successor of every ordinal is an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏})
Theorem	dflim6 43253*	A limit ordinal is a non-zero ordinal which is not a successor ordinal. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃𝑏 ∈ On 𝐴 = suc 𝑏))
Theorem	limnsuc 43254*	A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 → ¬ 𝐴 ∈ {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏})
Theorem	onsucss 43255	If one ordinal is less than another, then the successor of the first is less than or equal to the second. Lemma 1.13 of [Schloeder] p. 2. See ordsucss 7837. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴))
Theorem	ordnexbtwnsuc 43256*	For any distinct pair of ordinals, if there is no ordinal between the lesser and the greater, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → (∀𝑐 ∈ On ¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → 𝐵 = suc 𝐴))
Theorem	orddif0suc 43257	For any distinct pair of ordinals, if the set difference between the greater and the successor of the lesser is empty, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 17-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → ((𝐵 ∖ suc 𝐴) = ∅ → 𝐵 = suc 𝐴))
Theorem	onsucf1lem 43258*	For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the successor of. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ (𝐴 ∈ On → ∃*𝑏 ∈ On 𝐴 = suc 𝑏)
Theorem	onsucf1olem 43259*	The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) → ∃!𝑏 ∈ On 𝐴 = suc 𝑏)
Theorem	onsucrn 43260*	The successor operation is surjective onto its range, the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ 𝐹 = (𝑥 ∈ On ↦ suc 𝑥)    ⇒   ⊢ ran 𝐹 = {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏}
Theorem	onsucf1o 43261*	The successor operation is a bijective function between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ 𝐹 = (𝑥 ∈ On ↦ suc 𝑥)    ⇒   ⊢ 𝐹:On–1-1-onto→{𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏}
Theorem	dflim7 43262*	A limit ordinal is a non-zero ordinal that contains all the successors of its elements. Lemma 1.18 of [Schloeder] p. 2. Closely related to dflim4 7868. (Contributed by RP, 17-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∀𝑏 ∈ 𝐴 suc 𝑏 ∈ 𝐴 ∧ 𝐴 ≠ ∅))
Theorem	onov0suclim 43263	Compactly express rules for binary operations on ordinals. (Contributed by RP, 18-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)    &   ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)    &   ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 ⊗ 𝐵) = 𝐹)    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
Theorem	oa0suclim 43264*	Closed form expression of the value of ordinal addition for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.3 of [Schloeder] p. 4. See oa0 8552, oasuc 8560, and oalim 8568. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 +o 𝐵) = 𝐴) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 +o 𝐵) = suc (𝐴 +o 𝐶)) ∧ (Lim 𝐵 → (𝐴 +o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 +o 𝑐))))
Theorem	om0suclim 43265*	Closed form expression of the value of ordinal multiplication for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.5 of [Schloeder] p. 4. See om0 8553, omsuc 8562, and omlim 8569. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = ((𝐴 ·o 𝐶) +o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ·o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 ·o 𝑐))))
Theorem	oe0suclim 43266*	Closed form expression of the value of ordinal exponentiation for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.6 of [Schloeder] p. 4. See oe0 8558, oesuc 8563, oe0m1 8557, and oelim 8570. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅))))
Theorem	oaomoecl 43267	The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8571, omcl 8572, oecl 8573. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On))
Theorem	onsupsucismax 43268*	If the union of a set of ordinals is a successor ordinal, then that union is the maximum element of the set. This is not a bijection because sets where the maximum element is zero or a limit ordinal exist. Lemma 2.11 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → (∃𝑏 ∈ On ∪ 𝐴 = suc 𝑏 → ∪ 𝐴 ∈ 𝐴))
Theorem	onsssupeqcond 43269*	If for every element of a set of ordinals there is an element of a subset which is at least as large, then the union of the set and the subset is the same. Lemma 2.12 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐵 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) → ∪ 𝐴 = ∪ 𝐵))
Theorem	limexissup 43270	An ordinal which is a limit ordinal is equal to its supremum. Lemma 2.13 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 = sup(𝐴, On, E ))
Theorem	limiun 43271*	A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6446. (Contributed by RP, 27-Jan-2025.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥)
Theorem	limexissupab 43272*	An ordinal which is a limit ordinal is equal to the supremum of the class of all its elements. Lemma 2.13 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 = sup({𝑥 ∣ 𝑥 ∈ 𝐴}, On, E ))
Theorem	om1om1r 43273	Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8578 and om1r 8579 for individual statements. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ∈ On → ((1o ·o 𝐴) = (𝐴 ·o 1o) ∧ (𝐴 ·o 1o) = 𝐴))
Theorem	oe0rif 43274	Ordinal zero raised to any non-zero ordinal power is zero and zero to the zeroth power is one. Lemma 2.18 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ∈ On → (∅ ↑o 𝐴) = if(∅ ∈ 𝐴, ∅, 1o))
Theorem	oasubex 43275*	While subtraction can't be a binary operation on ordinals, for any pair of ordinals there exists an ordinal that can be added to the lessor (or equal) one which will sum to the greater. Theorem 2.19 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → ∃𝑐 ∈ On (𝑐 ⊆ 𝐴 ∧ (𝐵 +o 𝑐) = 𝐴))
Theorem	nnamecl 43276	Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8647, nnmcl 8648, nnecl 8649. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 +o 𝐵) ∈ ω ∧ (𝐴 ·o 𝐵) ∈ ω ∧ (𝐴 ↑o 𝐵) ∈ ω))
Theorem	onsucwordi 43277	The successor operation preserves the less-than-or-equal relationship between ordinals. Lemma 3.1 of [Schloeder] p. 7. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → suc 𝐴 ⊆ suc 𝐵))
Theorem	oalim2cl 43278	The ordinal sum of any ordinal with a limit ordinal on the right is a limit ordinal. (Contributed by RP, 6-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉) → Lim (𝐴 +o 𝐵))
Theorem	oaltublim 43279	Given 𝐶 is a limit ordinal, the sum of any ordinal with an ordinal less than 𝐶 is less than the sum of the first ordinal with 𝐶. Lemma 3.5 of [Schloeder] p. 7. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐴 +o 𝐵) ∈ (𝐴 +o 𝐶))
Theorem	oaordi3 43280	Ordinal addition of the same number on the left preserves the ordering of the numbers on the right. Lemma 3.6 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 +o 𝐵) ∈ (𝐴 +o 𝐶)))
Theorem	oaord3 43281	When the same ordinal is added on the left, ordering of the sums is equivalent to the ordering of the ordinals on the right. Theorem 3.7 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o 𝐶)))
Theorem	1oaomeqom 43282	Ordinal one plus omega is equal to omega. See oaabs 8684 for the sum of any natural number on the left and ordinal at least as large as omega on the right. Lemma 3.8 of [Schloeder] p. 8. See oaabs2 8685 where a power of omega is the upper bound of the left and a lower bound on the right. (Contributed by RP, 29-Jan-2025.)
⊢ (1o +o ω) = ω
Theorem	oaabsb 43283	The right addend absorbs the sum with an ordinal iff that ordinal times omega is less than or equal to the right addend. (Contributed by RP, 19-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o ω) ⊆ 𝐵 ↔ (𝐴 +o 𝐵) = 𝐵))
Theorem	oaordnrex 43284	When omega is added on the right to ordinals zero and one, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ¬ (∅ ∈ 1o ↔ (∅ +o ω) ∈ (1o +o ω))
Theorem	oaordnr 43285*	When the same ordinal is added on the right, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ On ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 +o 𝑐) ∈ (𝑏 +o 𝑐))
Theorem	omge1 43286	Any non-zero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of [Schloeder] p. 8. See omword1 8609. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ·o 𝐵))
Theorem	omge2 43287	Any non-zero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of [Schloeder] p. 9. See omword2 8610. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ⊆ (𝐴 ·o 𝐵))
Theorem	omlim2 43288	The non-zero product with an limit ordinal on the right is a limit ordinal. Lemma 3.13 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ·o 𝐵))
Theorem	omord2lim 43289	Given a limit ordinal, the product of any non-zero ordinal with an ordinal less than that limit ordinal is less than the product of the non-zero ordinal with the limit ordinal . Lemma 3.14 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	omord2i 43290	Ordinal multiplication of the same non-zero number on the left preserves the ordering of the numbers on the right. Lemma 3.15 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	omord2com 43291	When the same non-zero ordinal is multiplied on the left, ordering of the products is equivalent to the ordering of the ordinals on the right. Theorem 3.16 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	2omomeqom 43292	Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.)
⊢ (2o ·o ω) = ω
Theorem	omnord1ex 43293	When omega is multiplied on the right to ordinals one and two, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of [Schloeder] p. 10. (Contributed by RP, 29-Jan-2025.)
⊢ ¬ (1o ∈ 2o ↔ (1o ·o ω) ∈ (2o ·o ω))
Theorem	omnord1 43294*	When the same non-zero ordinal is multiplied on the right, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of [Schloeder] p. 10. (Contributed by RP, 4-Feb-2025.)
⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐))
Theorem	oege1 43295	Any non-zero ordinal power is greater-than-or-equal to the term on the left. Lemma 3.19 of [Schloeder] p. 10. See oewordi 8627. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ↑o 𝐵))
Theorem	oege2 43296	Any power of an ordinal at least as large as two is greater-than-or-equal to the term on the right. Lemma 3.20 of [Schloeder] p. 10. See oeworde 8629. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On) → 𝐵 ⊆ (𝐴 ↑o 𝐵))
Theorem	rp-oelim2 43297	The power of an ordinal at least as large as two with a limit ordinal on thr right is a limit ordinal. Lemma 3.21 of [Schloeder] p. 10. See oelimcl 8636. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ↑o 𝐵))
Theorem	oeord2lim 43298	Given a limit ordinal, the power of any base at least as large as two raised to an ordinal less than that limit ordinal is less than the power of that base raised to the limit ordinal . Lemma 3.22 of [Schloeder] p. 10. See oeordi 8623. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2i 43299	Ordinal exponentiation of the same base at least as large as two preserves the ordering of the exponents. Lemma 3.23 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2com 43300	When the same base at least as large as two is raised to ordinal powers, , ordering of the power is equivalent to the ordering of the exponents. Theorem 3.24 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 ↔ (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))