HomeTheorem List (p. 437 of 501)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 437 of 501) | < 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: | Metamath Proof Explorer
(1-30976) |
Hilbert Space Explorer
(30977-32499) |
Users' Mathboxes
(32500-50086) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bropabg 43601* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27762. (Contributed by RP, 26-Sep-2024.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒)) | ||
| Theorem | cantnfresb 43602* | A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025.) |
| ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) | ||
| Theorem | cantnf2 43603* | For every ordinal, 𝐴, there is a an ordinal exponent 𝑏 such that 𝐴 is less than (ω ↑o 𝑏) and for every ordinal at least as large as 𝑏 there is a unique Cantor normal form, 𝑓, with zeros for all the unnecessary higher terms, that sums to 𝐴. Theorem 5.3 of [Schloeder] p. 16. (Contributed by RP, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ On → ∃𝑏 ∈ On ∀𝑐 ∈ (On ∖ 𝑏)∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))) | ||
| Theorem | oawordex2 43604* | If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8486 or oawordeu 8484. (Contributed by RP, 7-Jan-2025.) |
| ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥 ∈ 𝐵 (𝐴 +o 𝑥) = 𝐶) | ||
| Theorem | nnawordexg 43605* | If an ordinal, 𝐵, is in a half-open interval between some 𝐴 and the next limit ordinal, 𝐵 is the sum of the 𝐴 and some natural number. This weakens the antecedent of nnawordex 8567. (Contributed by RP, 7-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) | ||
| Theorem | succlg 43606 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴 ∈ 𝐵) | ||
| Theorem | dflim5 43607* | A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025.) |
| ⊢ (Lim 𝐴 ↔ (𝐴 = On ∨ ∃𝑥 ∈ (On ∖ 1o)𝐴 = (ω ·o 𝑥))) | ||
| Theorem | oacl2g 43608 | Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o 𝐷) ∧ 𝐷 ∈ On))) → (𝐴 +o 𝐵) ∈ 𝐶) | ||
| Theorem | onmcl 43609 | If an ordinal is less than a power of omega, the product with a natural number is also less than that power of omega. (Contributed by RP, 19-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → (𝐴 ∈ (ω ↑o 𝐵) → (𝐴 ·o 𝑁) ∈ (ω ↑o 𝐵))) | ||
| Theorem | omabs2 43610 | Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or ω raised to some power of ω. (Contributed by RP, 12-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵) | ||
| Theorem | omcl2 43611 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶) | ||
| Theorem | omcl3g 43612 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶) | ||
| Theorem | ordsssucb 43613 | An ordinal number is less than or equal to the successor of an ordinal class iff the ordinal number is either less than or equal to the ordinal class or the ordinal number is equal to the successor of the ordinal class. See also ordsssucim 43680, limsssuc 7794. (Contributed by RP, 22-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
| Theorem | tfsconcatlem 43614* | Lemma for tfsconcatun 43615. (Contributed by RP, 23-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ((𝐴 +o 𝐵) ∖ 𝐴)) → ∃!𝑥∃𝑦 ∈ 𝐵 (𝐶 = (𝐴 +o 𝑦) ∧ 𝑥 = (𝐹‘𝑦))) | ||
| Theorem | tfsconcatun 43615* | The concatenation of two transfinite series is a union of functions. (Contributed by RP, 23-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵) = (𝐴 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))})) | ||
| Theorem | tfsconcatfn 43616* | The concatenation of two transfinite series is a transfinite series. (Contributed by RP, 22-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵) Fn (𝐶 +o 𝐷)) | ||
| Theorem | tfsconcatfv1 43617* | An early value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑋 ∈ 𝐶) → ((𝐴 + 𝐵)‘𝑋) = (𝐴‘𝑋)) | ||
| Theorem | tfsconcatfv2 43618* | A latter value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑋 ∈ 𝐷) → ((𝐴 + 𝐵)‘(𝐶 +o 𝑋)) = (𝐵‘𝑋)) | ||
| Theorem | tfsconcatfv 43619* | The value of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑋 ∈ (𝐶 +o 𝐷)) → ((𝐴 + 𝐵)‘𝑋) = if(𝑋 ∈ 𝐶, (𝐴‘𝑋), (𝐵‘(℩𝑑 ∈ 𝐷 (𝐶 +o 𝑑) = 𝑋)))) | ||
| Theorem | tfsconcatrn 43620* | The range of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ran (𝐴 + 𝐵) = (ran 𝐴 ∪ ran 𝐵)) | ||
| Theorem | tfsconcatfo 43621* | The concatenation of two transfinite series is onto the union of the ranges. (Contributed by RP, 24-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵):(𝐶 +o 𝐷)–onto→(ran 𝐴 ∪ ran 𝐵)) | ||
| Theorem | tfsconcatb0 43622* | The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 25-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵 = ∅ ↔ (𝐴 + 𝐵) = 𝐴)) | ||
| Theorem | tfsconcat0i 43623* | The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 28-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 = ∅ → (𝐴 + 𝐵) = 𝐵)) | ||
| Theorem | tfsconcat0b 43624* | The concatentation with the empty series leaves the finite series unchanged. (Contributed by RP, 1-Mar-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ ω)) → (𝐴 = ∅ ↔ (𝐴 + 𝐵) = 𝐵)) | ||
| Theorem | tfsconcat00 43625* | The concatentation of two empty series results in an empty series. (Contributed by RP, 25-Feb-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 + 𝐵) = ∅)) | ||
| Theorem | tfsconcatrev 43626* | If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ ((𝐹 Fn (𝐶 +o 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ∃𝑢 ∈ (ran 𝐹 ↑m 𝐶)∃𝑣 ∈ (ran 𝐹 ↑m 𝐷)((𝑢 + 𝑣) = 𝐹 ∧ dom 𝑢 = 𝐶 ∧ dom 𝑣 = 𝐷)) | ||
| Theorem | tfsconcatrnss12 43627* | The range of the concatenation of transfinite sequences is a superset of the ranges of both sequences. Theorem 3 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (ran 𝐴 ⊆ ran (𝐴 + 𝐵) ∧ ran 𝐵 ⊆ ran (𝐴 + 𝐵))) | ||
| Theorem | tfsconcatrnss 43628* | The concatenation of transfinite sequences yields elements from a class iff both sequences yield elements from that class. (Contributed by RP, 2-Mar-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (ran (𝐴 + 𝐵) ⊆ 𝑋 ↔ (ran 𝐴 ⊆ 𝑋 ∧ ran 𝐵 ⊆ 𝑋))) | ||
| Theorem | tfsconcatrnsson 43629* | The concatenation of transfinite sequences yields ordinals iff both sequences yield ordinals. Theorem 4 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.) |
| ⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))})) ⇒ ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (ran (𝐴 + 𝐵) ⊆ On ↔ (ran 𝐴 ⊆ On ∧ ran 𝐵 ⊆ On))) | ||
| Theorem | tfsnfin 43630 | A transfinite sequence is infinite iff its domain is greater than or equal to omega. Theorem 5 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 1-Mar-2025.) |
| ⊢ ((𝐴 Fn 𝐵 ∧ 𝐵 ∈ On) → (¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵)) | ||
| Theorem | rp-tfslim 43631* | The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025.) |
| ⊢ (𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 (𝐴‘𝑥) = ∪ ran 𝐴) | ||
| Theorem | ofoafg 43632* | Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 (𝑑 +o 𝐸))) → ( ∘f +o ↾ ((𝐷 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐷 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐹 ↑m 𝐶)) | ||
| Theorem | ofoaf 43633 | Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷))) → ( ∘f +o ↾ ((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶)) | ||
| Theorem | ofoafo 43634 | Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ( ∘f +o ↾ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))):((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))–onto→(𝐶 ↑m 𝐴)) | ||
| Theorem | ofoacl 43635 | Closure law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐴))) → (𝐹 ∘f +o 𝐺) ∈ (𝐶 ↑m 𝐴)) | ||
| Theorem | ofoaid1 43636 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → (𝐹 ∘f +o (𝐴 × {∅})) = 𝐹) | ||
| Theorem | ofoaid2 43637 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → ((𝐴 × {∅}) ∘f +o 𝐹) = 𝐹) | ||
| Theorem | ofoaass 43638 | Component-wise addition of ordinal-yielding functions is associative. (Contributed by RP, 5-Jan-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ (𝐹 ∈ (𝐵 ↑m 𝐴) ∧ 𝐺 ∈ (𝐵 ↑m 𝐴) ∧ 𝐻 ∈ (𝐵 ↑m 𝐴))) → ((𝐹 ∘f +o 𝐺) ∘f +o 𝐻) = (𝐹 ∘f +o (𝐺 ∘f +o 𝐻))) | ||
| Theorem | ofoacom 43639 | Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹 ∈ (ω ↑m 𝐴) ∧ 𝐺 ∈ (ω ↑m 𝐴))) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹)) | ||
| Theorem | naddcnff 43640 | Addition operator for Cantor normal forms is a function into Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
| ⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)⟶𝑆) | ||
| Theorem | naddcnffn 43641 | Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.) |
| ⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆)) | ||
| Theorem | naddcnffo 43642 | Addition of Cantor normal forms is a function onto Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
| ⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)–onto→𝑆) | ||
| Theorem | naddcnfcl 43643 | Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
| ⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) ∈ 𝑆) | ||
| Theorem | naddcnfcom 43644 | Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.) |
| ⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹)) | ||
| Theorem | naddcnfid1 43645 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → (𝐹 ∘f +o (𝑋 × {∅})) = 𝐹) | ||
| Theorem | naddcnfid2 43646 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → ((𝑋 × {∅}) ∘f +o 𝐹) = 𝐹) | ||
| Theorem | naddcnfass 43647 | Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) → ((𝐹 ∘f +o 𝐺) ∘f +o 𝐻) = (𝐹 ∘f +o (𝐺 ∘f +o 𝐻))) | ||
| Theorem | onsucunifi 43648* | The successor to the union of any non-empty, finite subset of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.) |
| ⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → suc ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 suc 𝑥) | ||
| Theorem | sucunisn 43649 | The successor to the union of any singleton of a set is the successor of the set. (Contributed by RP, 11-Feb-2025.) |
| ⊢ (𝐴 ∈ 𝑉 → suc ∪ {𝐴} = suc 𝐴) | ||
| Theorem | onsucunipr 43650 | The successor to the union of any pair of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc ∪ {𝐴, 𝐵} = ∪ {suc 𝐴, suc 𝐵}) | ||
| Theorem | onsucunitp 43651 | The successor to the union of any triple of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → suc ∪ {𝐴, 𝐵, 𝐶} = ∪ {suc 𝐴, suc 𝐵, suc 𝐶}) | ||
| Theorem | oaun3lem1 43652* | The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 43660. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}) | ||
| Theorem | oaun3lem2 43653* | The class of all ordinal sums of elements from two ordinals is bounded by the sum. Lemma for oaun3 43660. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ (𝐴 +o 𝐵)) | ||
| Theorem | oaun3lem3 43654* | The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 43660. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ On) | ||
| Theorem | oaun3lem4 43655* | The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 43660. (Contributed by RP, 12-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ suc (𝐴 +o 𝐵)) | ||
| Theorem | rp-abid 43656* | Two ways to express a class. (Contributed by RP, 13-Feb-2025.) |
| ⊢ 𝐴 = {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎} | ||
| Theorem | oadif1lem 43657* | Express the set difference of a continuous sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊕ 𝐵) ∈ On) & ⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On) → (𝐴 ⊕ 𝑏) ∈ On) & ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵))) → ∃𝑏 ∈ 𝐵 (𝐴 ⊕ 𝑏) = 𝑦) & ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑏 ∈ 𝐵 → (𝐴 ⊕ 𝑏) ∈ (𝐴 ⊕ 𝐵))) & ⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On) → 𝐴 ⊆ (𝐴 ⊕ 𝑏)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ⊕ 𝐵) ∖ 𝐴) = {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 ⊕ 𝑏)}) | ||
| Theorem | oadif1 43658* | Express the set difference of an ordinal sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∖ 𝐴) = {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 +o 𝑏)}) | ||
| Theorem | oaun2 43659* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}}) | ||
| Theorem | oaun3 43660* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}, {𝑧 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)}}) | ||
| Theorem | naddov4 43661* | Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ ({𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 (𝑎 +no 𝐵) ∈ 𝑥} ∩ {𝑥 ∈ On ∣ ∀𝑏 ∈ 𝐵 (𝐴 +no 𝑏) ∈ 𝑥})) | ||
| Theorem | nadd2rabtr 43662* | The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Tr {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶}) | ||
| Theorem | nadd2rabord 43663* | The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Ord {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶}) | ||
| Theorem | nadd2rabex 43664* | The class of ordinals which have a natural sum less than some ordinal is a set. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶} ∈ V) | ||
| Theorem | nadd2rabon 43665* | The set of ordinals which have a natural sum less than some ordinal is an ordinal number. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶} ∈ On) | ||
| Theorem | nadd1rabtr 43666* | The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Tr {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶}) | ||
| Theorem | nadd1rabord 43667* | The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Ord {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶}) | ||
| Theorem | nadd1rabex 43668* | The class of ordinals which have a natural sum less than some ordinal is a set. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶} ∈ V) | ||
| Theorem | nadd1rabon 43669* | The set of ordinals which have a natural sum less than some ordinal is an ordinal number. (Contributed by RP, 20-Dec-2024.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶} ∈ On) | ||
| Theorem | nadd1suc 43670 | Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.) |
| ⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴) | ||
| Theorem | naddass1 43671 | Natural addition of ordinal numbers is associative when the third element is 1. (Contributed by RP, 1-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) +no 1o) = (𝐴 +no (𝐵 +no 1o))) | ||
| Theorem | naddgeoa 43672 | Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ⊆ (𝐴 +no 𝐵)) | ||
| Theorem | naddonnn 43673 | Natural addition with a natural number on the right results in a value equal to that of ordinal addition. (Contributed by RP, 1-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐴 +no 𝐵)) | ||
| Theorem | naddwordnexlem0 43674 | When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, (ω ·o suc 𝐶) lies between 𝐴 and 𝐵. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → (𝐴 ∈ (ω ·o suc 𝐶) ∧ (ω ·o suc 𝐶) ⊆ 𝐵)) | ||
| Theorem | naddwordnexlem1 43675 | When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, 𝐵 is equal to or larger than 𝐴. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| Theorem | naddwordnexlem2 43676 | When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, 𝐵 is larger than 𝐴. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐵) | ||
| Theorem | naddwordnexlem3 43677* | When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, every natural sum of 𝐴 with a natural number is less that 𝐵. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐴 +no 𝑥) ∈ 𝐵) | ||
| Theorem | oawordex3 43678* | When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, some ordinal sum of 𝐴 is equal to 𝐵. This is a specialization of oawordex 8486. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
| Theorem | naddwordnexlem4 43679* | When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, there exists a product with omega such that the ordinal sum with 𝐴 is less than or equal to 𝐵 while the natural sum is larger than 𝐵. (Contributed by RP, 15-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) & ⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥)))) | ||
| Theorem | ordsssucim 43680 | If an ordinal is less than or equal to the successor of another, then the first is either less than or equal to the second or the first is equal to the successor of the second. Theorem 1 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 See also ordsssucb 43613 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
| Theorem | insucid 43681 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∩ suc 𝐴) = 𝐴 | ||
| Theorem | oaltom 43682 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴))) | ||
| Theorem | oe2 43683 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o)) | ||
| Theorem | omltoe 43684 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴))) | ||
| Theorem | abeqabi 43685 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
| ⊢ 𝐴 = {𝑥 ∣ 𝜓} ⇒ ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
| Theorem | abpr 43686* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | abtp 43687* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | ralopabb 43688* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
| ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} & ⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒)) | ||
| Theorem | fpwfvss 43689 | Functions into a powerset always have values which are subsets. This is dependant on our convention when the argument is not part of the domain. (Contributed by RP, 13-Sep-2024.) |
| ⊢ 𝐹:𝐶⟶𝒫 𝐵 ⇒ ⊢ (𝐹‘𝐴) ⊆ 𝐵 | ||
| Theorem | sdomne0 43690 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅) | ||
| Theorem | sdomne0d 43691 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 ≺ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
| Theorem | safesnsupfiss 43692 | If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
| ⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ⊆ 𝐵) | ||
| Theorem | safesnsupfiub 43693* | If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
| ⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑥𝑅𝑦) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)∀𝑦 ∈ 𝐶 𝑥𝑅𝑦) | ||
| Theorem | safesnsupfidom1o 43694 | If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
| ⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) | ||
| Theorem | safesnsupfilb 43695* | If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 3-Sep-2024.) |
| ⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦) | ||
| Theorem | isoeq145d 43696 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
| Theorem | resisoeq45d 43697 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
| Theorem | negslem1 43698 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
| ⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵))) | ||
| Theorem | nvocnvb 43699* | Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) ↔ (𝐹:𝐴–1-1-onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥)) | ||
| Theorem | rp-brsslt 43700* | Binary relation form of a relation, <, which has been extended from relation 𝑅 to subsets of class 𝑆. Usually, we will assume 𝑅 Or 𝑆. Definition in [Alling], p. 2. Generalization of brsslt 27762. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
| ⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} ⇒ ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |