![]() |
Metamath
Proof Explorer Theorem List (p. 430 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30854) |
![]() (30855-32377) |
![]() (32378-48571) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | unielss 42901* | Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.) |
⊢ (𝐴 ⊆ 𝐵 → (∪ 𝐵 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥)) | ||
Theorem | unielid 42902* | Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.) |
⊢ (∪ 𝐴 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥) | ||
Theorem | ssunib 42903* | Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.) |
⊢ (𝐴 ⊆ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦) | ||
Theorem | rp-intrabeq 42904* | Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.) |
⊢ (𝐴 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥}) | ||
Theorem | rp-unirabeq 42905* | Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.) |
⊢ (𝐴 = 𝐵 → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦}) | ||
Theorem | onmaxnelsup 42906* | 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 42907 | 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 42908 | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 ∈ On) | ||
Theorem | onuniintrab 42909* | 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 7812. (Contributed by RP, 28-Jan-2025.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥}) | ||
Theorem | onintunirab 42910* | 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 42911 | 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 42912 | 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 42913 | 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 42914* | 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 42915* | 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 42916* | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ On) | ||
Theorem | onsupex3 42917* | The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ V) | ||
Theorem | onuniintrab2 42918* | 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 42919 | 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 42920* | 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 42921* | The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ On) | ||
Theorem | onsupmaxb 42922 | 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 42923* | For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.) |
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ 𝑥) | ||
Theorem | onexomgt 42924* | For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.) |
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ·o 𝑥)) | ||
Theorem | omlimcl2 42925 | 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 42926* | For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.) |
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥)) | ||
Theorem | onexoegt 42927* | For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.) |
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) | ||
Theorem | oninfex2 42928* | The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V) | ||
Theorem | onsupeqmax 42929* | 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 42930* | 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 42931* | The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.) |
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (𝐵 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝐵 ∈ 𝑧)) | ||
Theorem | onsupnub 42932* | An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.) |
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵)) → ∪ 𝐴 ⊆ 𝐵) | ||
Theorem | onfisupcl 42933 | Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9329. (Contributed by RP, 27-Jan-2025.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)) | ||
Theorem | onelord 42934 | Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6403 and eloni 6388. (Contributed by RP, 15-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||
Theorem | onepsuc 42935 | 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 42936 | The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7785 and weso 5675. (Contributed by RP, 15-Jan-2025.) |
⊢ E Or On | ||
Theorem | epirron 42937 | 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 42938 | 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 42939 | The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6424. (Contributed by RP, 15-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | oneptri 42940 | 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 42941 | The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6410. (Contributed by RP, 15-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵)) | ||
Theorem | ordeldif 42942 | Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶))) | ||
Theorem | ordeldifsucon 42943 | Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))) | ||
Theorem | ordeldif1o 42944 | Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.) |
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅))) | ||
Theorem | ordne0gt0 42945 | Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6433. (Contributed by RP, 16-Jan-2025.) |
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴) | ||
Theorem | ondif1i 42946 | Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8533. (Contributed by RP, 16-Jan-2025.) |
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴) | ||
Theorem | onsucelab 42947* | 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 42948* | 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 42949* | 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 42950 | 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 7829. (Contributed by RP, 16-Jan-2025.) |
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴)) | ||
Theorem | ordnexbtwnsuc 42951* | 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 42952 | 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 42953* | 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 42954* | 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 42955* | 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 42956* | 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 42957* | 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 7860. (Contributed by RP, 17-Jan-2025.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∀𝑏 ∈ 𝐴 suc 𝑏 ∈ 𝐴 ∧ 𝐴 ≠ ∅)) | ||
Theorem | onov0suclim 42958 | 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 42959* | 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 8548, oasuc 8556, and oalim 8564. (Contributed by RP, 18-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 +o 𝐵) = 𝐴) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 +o 𝐵) = suc (𝐴 +o 𝐶)) ∧ (Lim 𝐵 → (𝐴 +o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 +o 𝑐)))) | ||
Theorem | om0suclim 42960* | 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 8549, omsuc 8558, and omlim 8565. (Contributed by RP, 18-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = ((𝐴 ·o 𝐶) +o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ·o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 ·o 𝑐)))) | ||
Theorem | oe0suclim 42961* | 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 8554, oesuc 8559, oe0m1 8553, and oelim 8566. (Contributed by RP, 18-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)))) | ||
Theorem | oaomoecl 42962 | The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8567, omcl 8568, oecl 8569. (Contributed by RP, 18-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On)) | ||
Theorem | onsupsucismax 42963* | 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 42964* | 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 42965 | 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 42966* | A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6439. (Contributed by RP, 27-Jan-2025.) |
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥) | ||
Theorem | limexissupab 42967* | 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 42968 | Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8574 and om1r 8575 for individual statements. (Contributed by RP, 29-Jan-2025.) |
⊢ (𝐴 ∈ On → ((1o ·o 𝐴) = (𝐴 ·o 1o) ∧ (𝐴 ·o 1o) = 𝐴)) | ||
Theorem | oe0rif 42969 | 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 42970* | 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 42971 | Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8643, nnmcl 8644, nnecl 8645. (Contributed by RP, 29-Jan-2025.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 +o 𝐵) ∈ ω ∧ (𝐴 ·o 𝐵) ∈ ω ∧ (𝐴 ↑o 𝐵) ∈ ω)) | ||
Theorem | onsucwordi 42972 | 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 42973 | 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 42974 | 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 42975 | 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 42976 | 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 42977 | Ordinal one plus omega is equal to omega. See oaabs 8680 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 8681 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 42978 | 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 42979 | 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 42980* | 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 42981 | 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 8605. (Contributed by RP, 29-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ·o 𝐵)) | ||
Theorem | omge2 42982 | 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 8606. (Contributed by RP, 29-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ⊆ (𝐴 ·o 𝐵)) | ||
Theorem | omlim2 42983 | 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 42984 | 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 42985 | 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 42986 | 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 42987 | Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.) |
⊢ (2o ·o ω) = ω | ||
Theorem | omnord1ex 42988 | 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 42989* | 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 42990 | 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 8623. (Contributed by RP, 29-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ↑o 𝐵)) | ||
Theorem | oege2 42991 | 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 8625. (Contributed by RP, 29-Jan-2025.) |
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On) → 𝐵 ⊆ (𝐴 ↑o 𝐵)) | ||
Theorem | rp-oelim2 42992 | 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 8632. (Contributed by RP, 30-Jan-2025.) |
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ↑o 𝐵)) | ||
Theorem | oeord2lim 42993 | 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 8619. (Contributed by RP, 30-Jan-2025.) |
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶))) | ||
Theorem | oeord2i 42994 | 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 42995 | 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 𝐶))) | ||
Theorem | nnoeomeqom 42996 | Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
⊢ ((𝐴 ∈ ω ∧ 1o ∈ 𝐴) → (𝐴 ↑o ω) = ω) | ||
Theorem | df3o2 42997 | Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.) |
⊢ 3o = {∅, 1o, 2o} | ||
Theorem | df3o3 42998 | Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.) |
⊢ 3o = {∅, {∅}, {∅, {∅}}} | ||
Theorem | oenord1ex 42999 | When ordinals two and three are both raised to the power of omega, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
⊢ ¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω)) | ||
Theorem | oenord1 43000* | When two ordinals (both at least as large as two) are raised to the same power, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of [Schloeder] p. 11. (Contributed by RP, 4-Feb-2025.) |
⊢ ∃𝑎 ∈ (On ∖ 2o)∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |