![]() |
Metamath
Proof Explorer Theorem List (p. 434 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnoeomeqom 43301 | 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 43302 | Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.) |
⊢ 3o = {∅, 1o, 2o} | ||
Theorem | df3o3 43303 | Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.) |
⊢ 3o = {∅, {∅}, {∅, {∅}}} | ||
Theorem | oenord1ex 43304 | 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 43305* | 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 𝑐)) | ||
Theorem | oaomoencom 43306* | Ordinal addition, multiplication, and exponentiation do not generally commute. Theorem 4.1 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
⊢ (∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎) ∧ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎) ∧ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎)) | ||
Theorem | oenassex 43307 | Ordinal two raised to two to the zeroth power is not the same as two squared then raised to the zeroth power. (Contributed by RP, 30-Jan-2025.) |
⊢ ¬ (2o ↑o (2o ↑o ∅)) = ((2o ↑o 2o) ↑o ∅) | ||
Theorem | oenass 43308* | Ordinal exponentiation is not associative. Remark 4.6 of [Schloeder] p. 14. (Contributed by RP, 30-Jan-2025.) |
⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ On ¬ (𝑎 ↑o (𝑏 ↑o 𝑐)) = ((𝑎 ↑o 𝑏) ↑o 𝑐) | ||
Theorem | cantnftermord 43309 | For terms of the form of a power of omega times a non-zero natural number, ordering of the exponents implies ordering of the terms. Lemma 5.1 of [Schloeder] p. 15. (Contributed by RP, 30-Jan-2025.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖ 1o) ∧ 𝐷 ∈ (ω ∖ 1o))) → (𝐴 ∈ 𝐵 → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω ↑o 𝐵) ·o 𝐷))) | ||
Theorem | cantnfub 43310* | Given a finite number of terms of the form ((ω ↑o (𝐴‘𝑛)) ·o (𝑀‘𝑛)) with distinct exponents, we may order them from largest to smallest and find the sum is less than (ω ↑o 𝑋) when (𝐴‘𝑛) is less than 𝑋 and (𝑀‘𝑛) is less than ω. Lemma 5.2 of [Schloeder] p. 15. (Contributed by RP, 31-Jan-2025.) |
⊢ (𝜑 → 𝑋 ∈ On) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝐴:𝑁–1-1→𝑋) & ⊢ (𝜑 → 𝑀:𝑁⟶ω) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (ω CNF 𝑋) ∧ ((ω CNF 𝑋)‘𝐹) ∈ (ω ↑o 𝑋))) | ||
Theorem | cantnfub2 43311* | Given a finite number of terms of the form ((ω ↑o (𝐴‘𝑛)) ·o (𝑀‘𝑛)) with distinct exponents, we may order them from largest to smallest and find the sum is less than (ω ↑o suc ∪ ran 𝐴) when (𝑀‘𝑛) is less than ω. Lemma 5.2 of [Schloeder] p. 15. (Contributed by RP, 9-Feb-2025.) |
⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝐴:𝑁–1-1→On) & ⊢ (𝜑 → 𝑀:𝑁⟶ω) & ⊢ 𝐹 = (𝑥 ∈ suc ∪ ran 𝐴 ↦ if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅)) ⇒ ⊢ (𝜑 → (suc ∪ ran 𝐴 ∈ On ∧ 𝐹 ∈ dom (ω CNF suc ∪ ran 𝐴) ∧ ((ω CNF suc ∪ ran 𝐴)‘𝐹) ∈ (ω ↑o suc ∪ ran 𝐴))) | ||
Theorem | bropabg 43312* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27844. (Contributed by RP, 26-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒)) | ||
Theorem | cantnfresb 43313* | 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 43314* | 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 43315* | If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8593 or oawordeu 8591. (Contributed by RP, 7-Jan-2025.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥 ∈ 𝐵 (𝐴 +o 𝑥) = 𝐶) | ||
Theorem | nnawordexg 43316* | 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 8673. (Contributed by RP, 7-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) | ||
Theorem | succlg 43317 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴 ∈ 𝐵) | ||
Theorem | dflim5 43318* | 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 43319 | 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 43320 | 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 43321 | 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 43322 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶) | ||
Theorem | omcl3g 43323 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶) | ||
Theorem | ordsssucb 43324 | 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 43391, limsssuc 7870. (Contributed by RP, 22-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
Theorem | tfsconcatlem 43325* | Lemma for tfsconcatun 43326. (Contributed by RP, 23-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ((𝐴 +o 𝐵) ∖ 𝐴)) → ∃!𝑥∃𝑦 ∈ 𝐵 (𝐶 = (𝐴 +o 𝑦) ∧ 𝑥 = (𝐹‘𝑦))) | ||
Theorem | tfsconcatun 43326* | 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 43327* | 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 43328* | 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 43329* | 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 43330* | 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 43331* | 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 43332* | 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 43333* | 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 43334* | 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 43335* | 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 43336* | 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 43337* | 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 43338* | 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 43339* | 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 43340* | 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 43341 | 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 43342* | The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025.) |
⊢ (𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 (𝐴‘𝑥) = ∪ ran 𝐴) | ||
Theorem | ofoafg 43343* | 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 43344 | 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 43345 | 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 43346 | 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 43347 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → (𝐹 ∘f +o (𝐴 × {∅})) = 𝐹) | ||
Theorem | ofoaid2 43348 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → ((𝐴 × {∅}) ∘f +o 𝐹) = 𝐹) | ||
Theorem | ofoaass 43349 | 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 43350 | Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹 ∈ (ω ↑m 𝐴) ∧ 𝐺 ∈ (ω ↑m 𝐴))) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹)) | ||
Theorem | naddcnff 43351 | 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 43352 | Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.) |
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆)) | ||
Theorem | naddcnffo 43353 | 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 43354 | Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) ∈ 𝑆) | ||
Theorem | naddcnfcom 43355 | Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.) |
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹)) | ||
Theorem | naddcnfid1 43356 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → (𝐹 ∘f +o (𝑋 × {∅})) = 𝐹) | ||
Theorem | naddcnfid2 43357 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → ((𝑋 × {∅}) ∘f +o 𝐹) = 𝐹) | ||
Theorem | naddcnfass 43358 | 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 43359* | 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 43360 | 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 43361 | 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 43362 | 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 43363* | The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 43371. (Contributed by RP, 13-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)}) | ||
Theorem | oaun3lem2 43364* | The class of all ordinal sums of elements from two ordinals is bounded by the sum. Lemma for oaun3 43371. (Contributed by RP, 13-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ (𝐴 +o 𝐵)) | ||
Theorem | oaun3lem3 43365* | The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 43371. (Contributed by RP, 13-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ On) | ||
Theorem | oaun3lem4 43366* | The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 43371. (Contributed by RP, 12-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ suc (𝐴 +o 𝐵)) | ||
Theorem | rp-abid 43367* | Two ways to express a class. (Contributed by RP, 13-Feb-2025.) |
⊢ 𝐴 = {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎} | ||
Theorem | oadif1lem 43368* | 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 43369* | 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 43370* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}}) | ||
Theorem | oaun3 43371* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}, {𝑧 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)}}) | ||
Theorem | naddov4 43372* | Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ ({𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 (𝑎 +no 𝐵) ∈ 𝑥} ∩ {𝑥 ∈ On ∣ ∀𝑏 ∈ 𝐵 (𝐴 +no 𝑏) ∈ 𝑥})) | ||
Theorem | nadd2rabtr 43373* | 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 43374* | 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 43375* | 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 43376* | 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 43377* | 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 43378* | 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 43379* | 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 43380* | 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 43381 | Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.) |
⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴) | ||
Theorem | naddass1 43382 | 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 43383 | 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 43384 | 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 43385 | 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 43386 | 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 43387 | 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 43388* | 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 43389* | 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 8593. (Contributed by RP, 14-Feb-2025.) |
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
Theorem | naddwordnexlem4 43390* | 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 43391 | 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 43324 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
Theorem | insucid 43392 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
⊢ (𝐴 ∩ suc 𝐴) = 𝐴 | ||
Theorem | om2 43393 | Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.) |
⊢ (𝐴 ∈ On → (𝐴 +o 𝐴) = (𝐴 ·o 2o)) | ||
Theorem | oaltom 43394 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴))) | ||
Theorem | oe2 43395 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o)) | ||
Theorem | omltoe 43396 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴))) | ||
Theorem | abeqabi 43397 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
⊢ 𝐴 = {𝑥 ∣ 𝜓} ⇒ ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | abpr 43398* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
Theorem | abtp 43399* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
Theorem | ralopabb 43400* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝑜 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |