![]() |
Metamath
Proof Explorer Theorem List (p. 429 of 483) | < 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-30721) |
![]() (30722-32244) |
![]() (32245-48210) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | naddwordnexlem3 42801* | 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 42802* | 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 8571. (Contributed by RP, 14-Feb-2025.) |
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) & ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ 𝑀) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
Theorem | naddwordnexlem4 42803* | 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 42804 | 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 42736 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵))) | ||
Theorem | insucid 42805 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
⊢ (𝐴 ∩ suc 𝐴) = 𝐴 | ||
Theorem | om2 42806 | Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.) |
⊢ (𝐴 ∈ On → (𝐴 +o 𝐴) = (𝐴 ·o 2o)) | ||
Theorem | oaltom 42807 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴))) | ||
Theorem | oe2 42808 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o)) | ||
Theorem | omltoe 42809 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴))) | ||
Theorem | abeqabi 42810 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
⊢ 𝐴 = {𝑥 ∣ 𝜓} ⇒ ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | abpr 42811* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
Theorem | abtp 42812* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
Theorem | ralopabb 42813* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝑜 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒)) | ||
Theorem | fpwfvss 42814 | 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 42815 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | sdomne0d 42816 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
⊢ (𝜑 → 𝐵 ≺ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
Theorem | safesnsupfiss 42817 | 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 42818* | 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 42819 | 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 42820* | 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 42821 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
Theorem | resisoeq45d 42822 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))) | ||
Theorem | negslem1 42823 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵))) | ||
Theorem | nvocnvb 42824* | 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 42825* | 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 27711. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
⊢ < = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)} ⇒ ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦))) | ||
Theorem | nla0002 42826* | 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 42827* | 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 42828* | 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 42829* |
𝐵
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 42830 | 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 42831 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → (𝐴 × {𝐵}) ∈ No ) | ||
Theorem | onnobdayg 42832 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → ( bday ‘(𝐴 × {𝐵})) = 𝐴) | ||
Theorem | bdaybndex 42833 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → (𝐵 × {𝐶}) ∈ No ) | ||
Theorem | bdaybndbday 42834 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → ( bday ‘(𝐵 × {𝐶})) = ( bday ‘𝐴)) | ||
Theorem | onno 42835 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ (𝐴 ∈ On → (𝐴 × {2o}) ∈ No ) | ||
Theorem | onnoi 42836 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 × {2o}) ∈ No | ||
Theorem | 0no 42837 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ ∅ ∈ No | ||
Theorem | 1no 42838 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ (1o × {2o}) ∈ No | ||
Theorem | 2no 42839 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ (2o × {2o}) ∈ No | ||
Theorem | 3no 42840 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ (3o × {2o}) ∈ No | ||
Theorem | 4no 42841 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
⊢ (4o × {2o}) ∈ No | ||
Theorem | fnimafnex 42842 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
⊢ 𝐹 Fn 𝐵 ⇒ ⊢ (𝐹 “ (𝐺‘𝐴)) ∈ V | ||
Theorem | nlimsuc 42843 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
⊢ (𝐴 ∈ On → ¬ Lim suc 𝐴) | ||
Theorem | nlim1NEW 42844 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
⊢ ¬ Lim 1o | ||
Theorem | nlim2NEW 42845 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
⊢ ¬ Lim 2o | ||
Theorem | nlim3 42846 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
⊢ ¬ Lim 3o | ||
Theorem | nlim4 42847 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
⊢ ¬ Lim 4o | ||
Theorem | oa1un 42848 | Given 𝐴 ∈ On, let 𝐴 +o 1o be defined to be the union of 𝐴 and {𝐴}. Compare with oa1suc 8545. (Contributed by RP, 27-Sep-2023.) |
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = (𝐴 ∪ {𝐴})) | ||
Theorem | oa1cl 42849 | 𝐴 +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
⊢ (𝐴 ∈ On → (𝐴 +o 1o) ∈ On) | ||
Theorem | 0finon 42850 | 0 is a finite ordinal. See peano1 7888. (Contributed by RP, 27-Sep-2023.) |
⊢ ∅ ∈ (On ∩ Fin) | ||
Theorem | 1finon 42851 | 1 is a finite ordinal. See 1onn 8654. (Contributed by RP, 27-Sep-2023.) |
⊢ 1o ∈ (On ∩ Fin) | ||
Theorem | 2finon 42852 | 2 is a finite ordinal. See 1onn 8654. (Contributed by RP, 27-Sep-2023.) |
⊢ 2o ∈ (On ∩ Fin) | ||
Theorem | 3finon 42853 | 3 is a finite ordinal. See 1onn 8654. (Contributed by RP, 27-Sep-2023.) |
⊢ 3o ∈ (On ∩ Fin) | ||
Theorem | 4finon 42854 | 4 is a finite ordinal. See 1onn 8654. (Contributed by RP, 27-Sep-2023.) |
⊢ 4o ∈ (On ∩ Fin) | ||
Theorem | finona1cl 42855 | The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.) |
⊢ (𝑁 ∈ (On ∩ Fin) → (𝑁 +o 1o) ∈ (On ∩ Fin)) | ||
Theorem | finonex 42856 | The finite ordinals are a set. See also onprc 7774 and fiprc 9063 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.) |
⊢ (On ∩ Fin) ∈ V | ||
Theorem | fzunt 42857 | 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 42858 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
Theorem | fzunt1d 42859 | Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ 𝐿) & ⊢ (𝜑 → 𝐿 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
Theorem | fzuntgd 42860 | Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) & ⊢ (𝜑 → 𝑀 ≤ (𝐿 + 1)) & ⊢ (𝜑 → 𝐿 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁)) | ||
Theorem | ifpan123g 42861 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
Theorem | ifpan23 42862 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
Theorem | ifpdfor2 42863 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
Theorem | ifporcor 42864 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
Theorem | ifpdfan2 42865 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
Theorem | ifpancor 42866 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
Theorem | ifpdfor 42867 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
Theorem | ifpdfan 42868 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
Theorem | ifpbi2 42869 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
Theorem | ifpbi3 42870 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
Theorem | ifpim1 42871 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
Theorem | ifpnot 42872 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
Theorem | ifpid2 42873 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
Theorem | ifpim2 42874 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
Theorem | ifpbi23 42875 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
Theorem | ifpbiidcor 42876 | Restatement of biid 261. (Contributed by RP, 25-Apr-2020.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | ifpbicor 42877 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | ifpxorcor 42878 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
Theorem | ifpbi1 42879 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
Theorem | ifpnot23 42880 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | ifpnotnotb 42881 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpnorcor 42882 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnancor 42883 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
Theorem | ifpnot23b 42884 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
Theorem | ifpbiidcor2 42885 | Restatement of biid 261. (Contributed by RP, 25-Apr-2020.) |
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
Theorem | ifpnot23c 42886 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
Theorem | ifpnot23d 42887 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpdfnan 42888 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
Theorem | ifpdfxor 42889 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
Theorem | ifpbi12 42890 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏))) | ||
Theorem | ifpbi13 42891 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃))) | ||
Theorem | ifpbi123 42892 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂))) | ||
Theorem | ifpidg 42893 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒))))) | ||
Theorem | ifpid3g 42894 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓))) | ||
Theorem | ifpid2g 42895 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpid1g 42896 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓))) | ||
Theorem | ifpim23g 42897 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpim3 42898 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim1 42899 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim4 42900 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |