| Metamath
Proof Explorer Theorem List (p. 433 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mendlmod 43201 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) | ||
| Theorem | mendassa 43202 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
| ⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) | ||
| Theorem | idomodle 43203* | Limit on the number of 𝑁-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ 𝑁) | ||
| Theorem | fiuneneq 43204 | Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → ((𝐴 ∪ 𝐵) ≈ 𝐴 ↔ 𝐴 = 𝐵)) | ||
| Theorem | idomsubgmo 43205* | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
| ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → ∃*𝑦 ∈ (SubGrp‘𝐺)(♯‘𝑦) = 𝑁) | ||
| Theorem | proot1mul 43206 | Any primitive 𝑁-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
| ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (𝐾‘{𝑌})) | ||
| Theorem | proot1hash 43207 | If an integral domain has a primitive 𝑁-th root of unity, it has exactly (ϕ‘𝑁) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ (◡𝑂 “ {𝑁})) → (♯‘(◡𝑂 “ {𝑁})) = (ϕ‘𝑁)) | ||
| Theorem | proot1ex 43208 | The complex field has primitive 𝑁-th roots of unity for all 𝑁. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁})) | ||
| Syntax | ccytp 43209 | Syntax for the sequence of cyclotomic polynomials. |
| class CytP | ||
| Definition | df-cytp 43210* | The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ CytP = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))) | ||
| Theorem | mon1psubm 43211 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑃) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈)) | ||
| Theorem | deg1mhm 43212 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
| ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑌 = ((mulGrp‘𝑃) ↾s (𝐵 ∖ { 0 })) & ⊢ 𝑁 = (ℂfld ↾s ℕ0) ⇒ ⊢ (𝑅 ∈ Domn → (𝐷 ↾ (𝐵 ∖ { 0 })) ∈ (𝑌 MndHom 𝑁)) | ||
| Theorem | cytpfn 43213 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ CytP Fn ℕ | ||
| Theorem | cytpval 43214* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝑇) & ⊢ 𝑃 = (Poly1‘ℂfld) & ⊢ 𝑋 = (var1‘ℂfld) & ⊢ 𝑄 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ (𝑁 ∈ ℕ → (CytP‘𝑁) = (𝑄 Σg (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟))))) | ||
| Theorem | fgraphopab 43215* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
| ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) | ||
| Theorem | fgraphxp 43216* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
| ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)}) | ||
| Theorem | hausgraph 43217 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
| ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) | ||
| Syntax | ctopsep 43218 | The class of separable topologies. |
| class TopSep | ||
| Syntax | ctoplnd 43219 | The class of Lindelöf topologies. |
| class TopLnd | ||
| Definition | df-topsep 43220* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
| ⊢ TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)} | ||
| Definition | df-toplnd 43221* | A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
| ⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))} | ||
| Theorem | r1sssucd 43222 | Deductive form of r1sssuc 9823. (Contributed by Noam Pasman, 19-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴)) | ||
| Theorem | iocunico 43223 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)) | ||
| Theorem | iocinico 43224 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵}) | ||
| Theorem | iocmbl 43225 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol) | ||
| Theorem | cnioobibld 43226* | 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 25876 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) | ||
| Theorem | arearect 43227 | 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 43228* | 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)) · (𝐵 − 𝐴)) | ||
| Theorem | uniel 43229* | Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.) |
| ⊢ (∪ 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦)) | ||
| Theorem | unielss 43230* | Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∪ 𝐵 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥)) | ||
| Theorem | unielid 43231* | Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.) |
| ⊢ (∪ 𝐴 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥) | ||
| Theorem | ssunib 43232* | Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.) |
| ⊢ (𝐴 ⊆ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦) | ||
| Theorem | rp-intrabeq 43233* | Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.) |
| ⊢ (𝐴 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥}) | ||
| Theorem | rp-unirabeq 43234* | Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.) |
| ⊢ (𝐴 = 𝐵 → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦}) | ||
| Theorem | onmaxnelsup 43235* | 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 43236 | 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 43237 | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
| ⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 ∈ On) | ||
| Theorem | onuniintrab 43238* | 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 7821. (Contributed by RP, 28-Jan-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥}) | ||
| Theorem | onintunirab 43239* | 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 43240 | 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 43241 | 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 43242 | 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 43243* | 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 43244* | 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 43245* | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ On) | ||
| Theorem | onsupex3 43246* | The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ V) | ||
| Theorem | onuniintrab2 43247* | 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 43248 | 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 43249* | 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 43250* | The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ On) | ||
| Theorem | onsupmaxb 43251 | 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 43252* | For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.) |
| ⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ 𝑥) | ||
| Theorem | onexomgt 43253* | For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.) |
| ⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ·o 𝑥)) | ||
| Theorem | omlimcl2 43254 | 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 43255* | For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.) |
| ⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥)) | ||
| Theorem | onexoegt 43256* | For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.) |
| ⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) | ||
| Theorem | oninfex2 43257* | The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V) | ||
| Theorem | onsupeqmax 43258* | 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 43259* | 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 43260* | The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.) |
| ⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (𝐵 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝐵 ∈ 𝑧)) | ||
| Theorem | onsupnub 43261* | An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.) |
| ⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵)) → ∪ 𝐴 ⊆ 𝐵) | ||
| Theorem | onfisupcl 43262 | Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9326. (Contributed by RP, 27-Jan-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)) | ||
| Theorem | onelord 43263 | Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6409 and eloni 6394. (Contributed by RP, 15-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||
| Theorem | onepsuc 43264 | 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 43265 | The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7795 and weso 5676. (Contributed by RP, 15-Jan-2025.) |
| ⊢ E Or On | ||
| Theorem | epirron 43266 | 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 43267 | 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 43268 | The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6430. (Contributed by RP, 15-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
| Theorem | oneptri 43269 | 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 43270 | The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6416. (Contributed by RP, 15-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵)) | ||
| Theorem | ordeldif 43271 | Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶))) | ||
| Theorem | ordeldifsucon 43272 | Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))) | ||
| Theorem | ordeldif1o 43273 | Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.) |
| ⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅))) | ||
| Theorem | ordne0gt0 43274 | Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6439. (Contributed by RP, 16-Jan-2025.) |
| ⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴) | ||
| Theorem | ondif1i 43275 | Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8539. (Contributed by RP, 16-Jan-2025.) |
| ⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴) | ||
| Theorem | onsucelab 43276* | 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 43277* | 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 43278* | 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 43279 | 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 7838. (Contributed by RP, 16-Jan-2025.) |
| ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴)) | ||
| Theorem | ordnexbtwnsuc 43280* | 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 43281 | 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 43282* | 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 43283* | 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 43284* | 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 43285* | 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 43286* | 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 7869. (Contributed by RP, 17-Jan-2025.) |
| ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∀𝑏 ∈ 𝐴 suc 𝑏 ∈ 𝐴 ∧ 𝐴 ≠ ∅)) | ||
| Theorem | onov0suclim 43287 | 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 43288* | 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 8554, oasuc 8562, and oalim 8570. (Contributed by RP, 18-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 +o 𝐵) = 𝐴) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 +o 𝐵) = suc (𝐴 +o 𝐶)) ∧ (Lim 𝐵 → (𝐴 +o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 +o 𝑐)))) | ||
| Theorem | om0suclim 43289* | 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 8555, omsuc 8564, and omlim 8571. (Contributed by RP, 18-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = ((𝐴 ·o 𝐶) +o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ·o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 ·o 𝑐)))) | ||
| Theorem | oe0suclim 43290* | 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 8560, oesuc 8565, oe0m1 8559, and oelim 8572. (Contributed by RP, 18-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅)))) | ||
| Theorem | oaomoecl 43291 | The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8573, omcl 8574, oecl 8575. (Contributed by RP, 18-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On)) | ||
| Theorem | onsupsucismax 43292* | 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 43293* | 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 43294 | 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 43295* | A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6445. (Contributed by RP, 27-Jan-2025.) |
| ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥) | ||
| Theorem | limexissupab 43296* | 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 43297 | Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8580 and om1r 8581 for individual statements. (Contributed by RP, 29-Jan-2025.) |
| ⊢ (𝐴 ∈ On → ((1o ·o 𝐴) = (𝐴 ·o 1o) ∧ (𝐴 ·o 1o) = 𝐴)) | ||
| Theorem | oe0rif 43298 | 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 43299* | 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 43300 | Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8649, nnmcl 8650, nnecl 8651. (Contributed by RP, 29-Jan-2025.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 +o 𝐵) ∈ ω ∧ (𝐴 ·o 𝐵) ∈ ω ∧ (𝐴 ↑o 𝐵) ∈ ω)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |