| Metamath
Proof Explorer Theorem List (p. 435 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 | nadd1rabtr 43401* | 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 43402* | 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 43403* | 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 43404* | 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 43405 | Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.) |
| ⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴) | ||
| Theorem | naddass1 43406 | 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 43407 | 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 43408 | 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 43409 | 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 43410 | 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 43411 | 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 43412* | 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 43413* | 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 8595. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
| Theorem | naddwordnexlem4 43414* | 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 43415 | 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 43348 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
| Theorem | insucid 43416 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∩ suc 𝐴) = 𝐴 | ||
| Theorem | om2 43417 | Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∈ On → (𝐴 +o 𝐴) = (𝐴 ·o 2o)) | ||
| Theorem | oaltom 43418 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴))) | ||
| Theorem | oe2 43419 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o)) | ||
| Theorem | omltoe 43420 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴))) | ||
| Theorem | abeqabi 43421 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
| ⊢ 𝐴 = {𝑥 ∣ 𝜓} ⇒ ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
| Theorem | abpr 43422* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | abtp 43423* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | ralopabb 43424* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
| ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝑜 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒)) | ||
| Theorem | fpwfvss 43425 | 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 43426 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅) | ||
| Theorem | sdomne0d 43427 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 ≺ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
| Theorem | safesnsupfiss 43428 | 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 43429* | 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 43430 | 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 43431* | 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 43432 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
| Theorem | resisoeq45d 43433 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
| Theorem | negslem1 43434 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
| ⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵))) | ||
| Theorem | nvocnvb 43435* | 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 43436* | 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 27830. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
| ⊢ < = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} ⇒ ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦))) | ||
| Theorem | nla0002 43437* | Extending a linear order to subsets, the empty set is less than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
| ⊢ < = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → ∅ < 𝐴) | ||
| Theorem | nla0003 43438* | Extending a linear order to subsets, the empty set is greater than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
| ⊢ < = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 < ∅) | ||
| Theorem | nla0001 43439* | Extending a linear order to subsets, the empty set is less than itself. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
| ⊢ < = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} ⇒ ⊢ (𝜑 → ∅ < ∅) | ||
| Theorem | faosnf0.11b 43440* |
𝐵
is called a non-limit ordinal if it is not a limit ordinal.
(Contributed by RP, 27-Sep-2023.)
Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243. |
| ⊢ ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) | ||
| Theorem | dfno2 43441 | A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025.) |
| ⊢ No = {𝑓 ∈ 𝒫 (On × {1o, 2o}) ∣ (Fun 𝑓 ∧ dom 𝑓 ∈ On)} | ||
| Theorem | onnog 43442 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → (𝐴 × {𝐵}) ∈ No ) | ||
| Theorem | onnobdayg 43443 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → ( bday ‘(𝐴 × {𝐵})) = 𝐴) | ||
| Theorem | bdaybndex 43444 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → (𝐵 × {𝐶}) ∈ No ) | ||
| Theorem | bdaybndbday 43445 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → ( bday ‘(𝐵 × {𝐶})) = ( bday ‘𝐴)) | ||
| Theorem | onno 43446 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (𝐴 ∈ On → (𝐴 × {2o}) ∈ No ) | ||
| Theorem | onnoi 43447 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 × {2o}) ∈ No | ||
| Theorem | 0no 43448 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ∅ ∈ No | ||
| Theorem | 1no 43449 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (1o × {2o}) ∈ No | ||
| Theorem | 2no 43450 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (2o × {2o}) ∈ No | ||
| Theorem | 3no 43451 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (3o × {2o}) ∈ No | ||
| Theorem | 4no 43452 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (4o × {2o}) ∈ No | ||
| Theorem | fnimafnex 43453 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
| ⊢ 𝐹 Fn 𝐵 ⇒ ⊢ (𝐹 “ (𝐺‘𝐴)) ∈ V | ||
| Theorem | nlimsuc 43454 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
| ⊢ (𝐴 ∈ On → ¬ Lim suc 𝐴) | ||
| Theorem | nlim1NEW 43455 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 1o | ||
| Theorem | nlim2NEW 43456 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 2o | ||
| Theorem | nlim3 43457 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 3o | ||
| Theorem | nlim4 43458 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 4o | ||
| Theorem | oa1un 43459 | Given 𝐴 ∈ On, let 𝐴 +o 1o be defined to be the union of 𝐴 and {𝐴}. Compare with oa1suc 8569. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (𝐴 ∈ On → (𝐴 +o 1o) = (𝐴 ∪ {𝐴})) | ||
| Theorem | oa1cl 43460 | 𝐴 +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (𝐴 ∈ On → (𝐴 +o 1o) ∈ On) | ||
| Theorem | 0finon 43461 | 0 is a finite ordinal. See peano1 7910. (Contributed by RP, 27-Sep-2023.) |
| ⊢ ∅ ∈ (On ∩ Fin) | ||
| Theorem | 1finon 43462 | 1 is a finite ordinal. See 1onn 8678. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 1o ∈ (On ∩ Fin) | ||
| Theorem | 2finon 43463 | 2 is a finite ordinal. See 1onn 8678. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 2o ∈ (On ∩ Fin) | ||
| Theorem | 3finon 43464 | 3 is a finite ordinal. See 1onn 8678. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 3o ∈ (On ∩ Fin) | ||
| Theorem | 4finon 43465 | 4 is a finite ordinal. See 1onn 8678. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 4o ∈ (On ∩ Fin) | ||
| Theorem | finona1cl 43466 | The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (𝑁 ∈ (On ∩ Fin) → (𝑁 +o 1o) ∈ (On ∩ Fin)) | ||
| Theorem | finonex 43467 | The finite ordinals are a set. See also onprc 7798 and fiprc 9085 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (On ∩ Fin) ∈ V | ||
| Theorem | fzunt 43468 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024.) |
| ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | fzuntd 43469 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | fzunt1d 43470 | Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ 𝐿) & ⊢ (𝜑 → 𝐿 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | fzuntgd 43471 | Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ (𝐿 + 1)) & ⊢ (𝜑 → 𝐿 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | ifpan123g 43472 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
| ⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
| Theorem | ifpan23 43473 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
| Theorem | ifpdfor2 43474 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
| Theorem | ifporcor 43475 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
| ⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
| Theorem | ifpdfan2 43476 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
| Theorem | ifpancor 43477 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
| Theorem | ifpdfor 43478 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
| Theorem | ifpdfan 43479 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
| Theorem | ifpbi2 43480 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
| Theorem | ifpbi3 43481 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
| Theorem | ifpim1 43482 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
| Theorem | ifpnot 43483 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
| Theorem | ifpid2 43484 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
| Theorem | ifpim2 43485 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
| Theorem | ifpbi23 43486 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
| Theorem | ifpbiidcor 43487 | Restatement of biid 261. (Contributed by RP, 25-Apr-2020.) |
| ⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
| Theorem | ifpbicor 43488 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
| Theorem | ifpxorcor 43489 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
| Theorem | ifpbi1 43490 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
| Theorem | ifpnot23 43491 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
| ⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
| Theorem | ifpnotnotb 43492 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
| Theorem | ifpnorcor 43493 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
| Theorem | ifpnancor 43494 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
| Theorem | ifpnot23b 43495 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
| Theorem | ifpbiidcor2 43496 | Restatement of biid 261. (Contributed by RP, 25-Apr-2020.) |
| ⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
| Theorem | ifpnot23c 43497 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
| Theorem | ifpnot23d 43498 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
| Theorem | ifpdfnan 43499 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
| Theorem | ifpdfxor 43500 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |