HomeTheorem List (p. 442 of 506)
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. 442 of 506) | < 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-31251) |
Hilbert Space Explorer
(31252-32774) |
Users' Mathboxes
(32775-50588) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nadd1rabon 44101* | 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 44102 | Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.) |
| ⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴) | ||
| Theorem | naddass1 44103 | 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 44104 | 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 44105 | 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 44106 | 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 44107 | 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 44108 | 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 44109* | 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 44110* | 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 8543. (Contributed by RP, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
| Theorem | naddwordnexlem4 44111* | 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 44112 | 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 44045 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
| Theorem | insucid 44113 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∩ suc 𝐴) = 𝐴 | ||
| Theorem | oaltom 44114 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴))) | ||
| Theorem | oe2 44115 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
| ⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o)) | ||
| Theorem | omltoe 44116 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴))) | ||
| Theorem | abeqabi 44117 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
| ⊢ 𝐴 = {𝑥 ∣ 𝜓} ⇒ ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
| Theorem | abpr 44118* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | abtp 44119* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | ralopabb 44120* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
| ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} & ⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒)) | ||
| Theorem | fpwfvss 44121 | 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 44122 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅) | ||
| Theorem | sdomne0d 44123 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 ≺ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
| Theorem | safesnsupfiss 44124 | 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 44125* | 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 44126 | 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 44127* | 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 44128 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
| Theorem | resisoeq45d 44129 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
| Theorem | negslem1 44130 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
| ⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵))) | ||
| Theorem | nvocnvb 44131* | 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 44132* | 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 brslts 27936. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
| ⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} ⇒ ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦))) | ||
| Theorem | nla0002 44133* | 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 44134* | 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 44135* | 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 44136* |
𝐵
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 44137 | 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 | onnoxpg 44138 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → (𝐴 × {𝐵}) ∈ No ) | ||
| Theorem | onnobdayg 44139 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → ( bday ‘(𝐴 × {𝐵})) = 𝐴) | ||
| Theorem | bdaybndex 44140 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → (𝐵 × {𝐶}) ∈ No ) | ||
| Theorem | bdaybndbday 44141 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → ( bday ‘(𝐵 × {𝐶})) = ( bday ‘𝐴)) | ||
| Theorem | onnoxp 44142 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (𝐴 ∈ On → (𝐴 × {2o}) ∈ No ) | ||
| Theorem | onnoxpi 44143 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 × {2o}) ∈ No | ||
| Theorem | 0fno 44144 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ ∅ ∈ No | ||
| Theorem | 1fno 44145 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (1o × {2o}) ∈ No | ||
| Theorem | 2fno 44146 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (2o × {2o}) ∈ No | ||
| Theorem | 3fno 44147 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (3o × {2o}) ∈ No | ||
| Theorem | 4fno 44148 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
| ⊢ (4o × {2o}) ∈ No | ||
| Theorem | fnimafnex 44149 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
| ⊢ 𝐹 Fn 𝐵 ⇒ ⊢ (𝐹 “ (𝐺‘𝐴)) ∈ V | ||
| Theorem | nlimsuc 44150 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
| ⊢ (𝐴 ∈ On → ¬ Lim suc 𝐴) | ||
| Theorem | nlim1NEW 44151 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 1o | ||
| Theorem | nlim2NEW 44152 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 2o | ||
| Theorem | nlim3 44153 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 3o | ||
| Theorem | nlim4 44154 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
| ⊢ ¬ Lim 4o | ||
| Theorem | oa1un 44155 | Given 𝐴 ∈ On, let 𝐴 +o 1o be defined to be the union of 𝐴 and {𝐴}. Compare with oa1suc 8517. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (𝐴 ∈ On → (𝐴 +o 1o) = (𝐴 ∪ {𝐴})) | ||
| Theorem | oa1cl 44156 | 𝐴 +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (𝐴 ∈ On → (𝐴 +o 1o) ∈ On) | ||
| Theorem | 0finon 44157 | 0 is a finite ordinal. See peano1 7886. (Contributed by RP, 27-Sep-2023.) |
| ⊢ ∅ ∈ (On ∩ Fin) | ||
| Theorem | 1finon 44158 | 1 is a finite ordinal. See 1onn 8627. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 1o ∈ (On ∩ Fin) | ||
| Theorem | 2finon 44159 | 2 is a finite ordinal. See 1onn 8627. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 2o ∈ (On ∩ Fin) | ||
| Theorem | 3finon 44160 | 3 is a finite ordinal. See 1onn 8627. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 3o ∈ (On ∩ Fin) | ||
| Theorem | 4finon 44161 | 4 is a finite ordinal. See 1onn 8627. (Contributed by RP, 27-Sep-2023.) |
| ⊢ 4o ∈ (On ∩ Fin) | ||
| Theorem | finona1cl 44162 | The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (𝑁 ∈ (On ∩ Fin) → (𝑁 +o 1o) ∈ (On ∩ Fin)) | ||
| Theorem | finonex 44163 | The finite ordinals are a set. See also onprc 7778 and fiprc 9042 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.) |
| ⊢ (On ∩ Fin) ∈ V | ||
| Theorem | fzunt 44164 | 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 44165 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | fzunt1d 44166 | Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ 𝐿) & ⊢ (𝜑 → 𝐿 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | fzuntgd 44167 | Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ (𝐿 + 1)) & ⊢ (𝜑 → 𝐿 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
| Theorem | ifpan123g 44168 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
| ⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
| Theorem | ifpan23 44169 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
| Theorem | ifpdfor2 44170 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
| Theorem | ifporcor 44171 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
| ⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
| Theorem | ifpdfan2 44172 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
| Theorem | ifpancor 44173 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
| Theorem | ifpdfor 44174 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
| Theorem | ifpdfan 44175 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
| Theorem | ifpbi2 44176 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
| Theorem | ifpbi3 44177 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
| Theorem | ifpim1 44178 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
| Theorem | ifpnot 44179 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
| Theorem | ifpid2 44180 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
| Theorem | ifpim2 44181 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
| Theorem | ifpbi23 44182 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
| Theorem | ifpbiidcor 44183 | Restatement of biid 264. (Contributed by RP, 25-Apr-2020.) |
| ⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
| Theorem | ifpbicor 44184 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
| Theorem | ifpxorcor 44185 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
| Theorem | ifpbi1 44186 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
| Theorem | ifpnot23 44187 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
| ⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
| Theorem | ifpnotnotb 44188 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
| Theorem | ifpnorcor 44189 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
| Theorem | ifpnancor 44190 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
| Theorem | ifpnot23b 44191 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
| Theorem | ifpbiidcor2 44192 | Restatement of biid 264. (Contributed by RP, 25-Apr-2020.) |
| ⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
| Theorem | ifpnot23c 44193 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
| Theorem | ifpnot23d 44194 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
| ⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
| Theorem | ifpdfnan 44195 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
| Theorem | ifpdfxor 44196 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
| Theorem | ifpbi12 44197 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏))) | ||
| Theorem | ifpbi13 44198 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃))) | ||
| Theorem | ifpbi123 44199 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂))) | ||
| Theorem | ifpidg 44200 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
| ⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |