P. 435 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43401-43500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nadd1rabord 43401*	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 43402*	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 43403*	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 43404	Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.)
⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴)
Theorem	naddass1 43405	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 43406	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 43407	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 43408	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 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, 𝐵 is equal to or larger than 𝐴. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	naddwordnexlem2 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 larger than 𝐴. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	naddwordnexlem3 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, 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 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, some ordinal sum of 𝐴 is equal to 𝐵. This is a specialization of oawordex 8467. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)
Theorem	naddwordnexlem4 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, 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 43414	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 43347 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	insucid 43415	The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∩ suc 𝐴) = 𝐴
Theorem	om2 43416	Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 +o 𝐴) = (𝐴 ·o 2o))
Theorem	oaltom 43417	Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴)))
Theorem	oe2 43418	Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o))
Theorem	omltoe 43419	Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴)))
21.36.3  Surreal Contributions
Theorem	abeqabi 43420	Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.)
⊢ 𝐴 = {𝑥 ∣ 𝜓}    ⇒   ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	abpr 43421*	Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍)))
Theorem	abtp 43422*	Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍)))
Theorem	ralopabb 43423*	Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.)
⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    &   ⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒))
Theorem	fpwfvss 43424	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 43425	A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.)
⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅)
Theorem	sdomne0d 43426	A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.)
⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	safesnsupfiss 43427	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 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	safesnsupfidom1o 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)    ⇒   ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o)
Theorem	safesnsupfilb 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, 3-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)
Theorem	isoeq145d 43431	Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)))
Theorem	resisoeq45d 43432	Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)))
Theorem	negslem1 43433	An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.)
⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵)))
Theorem	nvocnvb 43434*	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 43435*	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 27718. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    ⇒   ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦)))
Theorem	nla0002 43436*	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 43437*	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 43438*	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 43439*	𝐵 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 43440	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 43441	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → (𝐴 × {𝐵}) ∈ No )
Theorem	onnobdayg 43442	Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → ( bday ‘(𝐴 × {𝐵})) = 𝐴)
Theorem	bdaybndex 43443	Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → (𝐵 × {𝐶}) ∈ No )
Theorem	bdaybndbday 43444	Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.)
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → ( bday ‘(𝐵 × {𝐶})) = ( bday ‘𝐴))
Theorem	onno 43445	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 × {2o}) ∈ No )
Theorem	onnoi 43446	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 × {2o}) ∈ No
Theorem	0no 43447	Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ ∅ ∈ No
Theorem	1no 43448	Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (1o × {2o}) ∈ No
Theorem	2no 43449	Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (2o × {2o}) ∈ No
Theorem	3no 43450	Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (3o × {2o}) ∈ No
Theorem	4no 43451	Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (4o × {2o}) ∈ No
Theorem	fnimafnex 43452	The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.)
⊢ 𝐹 Fn 𝐵    ⇒   ⊢ (𝐹 “ (𝐺‘𝐴)) ∈ V
21.36.4  Short Studies
Theorem	nlimsuc 43453	A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
⊢ (𝐴 ∈ On → ¬ Lim suc 𝐴)
Theorem	nlim1NEW 43454	1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.)
⊢ ¬ Lim 1o
Theorem	nlim2NEW 43455	2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.)
⊢ ¬ Lim 2o
Theorem	nlim3 43456	3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
⊢ ¬ Lim 3o
Theorem	nlim4 43457	4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
⊢ ¬ Lim 4o
Theorem	oa1un 43458	Given 𝐴 ∈ On, let 𝐴 +o 1o be defined to be the union of 𝐴 and {𝐴}. Compare with oa1suc 8441. (Contributed by RP, 27-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = (𝐴 ∪ {𝐴}))
Theorem	oa1cl 43459	𝐴 +o 1o is in On. (Contributed by RP, 27-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 +o 1o) ∈ On)
Theorem	0finon 43460	0 is a finite ordinal. See peano1 7814. (Contributed by RP, 27-Sep-2023.)
⊢ ∅ ∈ (On ∩ Fin)
Theorem	1finon 43461	1 is a finite ordinal. See 1onn 8550. (Contributed by RP, 27-Sep-2023.)
⊢ 1o ∈ (On ∩ Fin)
Theorem	2finon 43462	2 is a finite ordinal. See 1onn 8550. (Contributed by RP, 27-Sep-2023.)
⊢ 2o ∈ (On ∩ Fin)
Theorem	3finon 43463	3 is a finite ordinal. See 1onn 8550. (Contributed by RP, 27-Sep-2023.)
⊢ 3o ∈ (On ∩ Fin)
Theorem	4finon 43464	4 is a finite ordinal. See 1onn 8550. (Contributed by RP, 27-Sep-2023.)
⊢ 4o ∈ (On ∩ Fin)
Theorem	finona1cl 43465	The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.)
⊢ (𝑁 ∈ (On ∩ Fin) → (𝑁 +o 1o) ∈ (On ∩ Fin))
Theorem	finonex 43466	The finite ordinals are a set. See also onprc 7706 and fiprc 8961 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.)
⊢ (On ∩ Fin) ∈ V
Theorem	fzunt 43467	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 43468	Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzunt1d 43469	Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzuntgd 43470	Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐿 + 1))    &   ⊢ (𝜑 → 𝐿 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
21.36.4.1  Additional work on conditional logical operator
Theorem	ifpan123g 43471	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
Theorem	ifpan23 43472	Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏)))
Theorem	ifpdfor2 43473	Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓))
Theorem	ifporcor 43474	Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.)
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑))
Theorem	ifpdfan2 43475	Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑))
Theorem	ifpancor 43476	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓))
Theorem	ifpdfor 43477	Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓))
Theorem	ifpdfan 43478	Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥))
Theorem	ifpbi2 43479	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃)))
Theorem	ifpbi3 43480	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓)))
Theorem	ifpim1 43481	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓))
Theorem	ifpnot 43482	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤))
Theorem	ifpid2 43483	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥))
Theorem	ifpim2 43484	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑))
Theorem	ifpbi23 43485	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃)))
Theorem	ifpbiidcor 43486	Restatement of biid 261. (Contributed by RP, 25-Apr-2020.)
⊢ if-(𝜑, 𝜑, ¬ 𝜑)
Theorem	ifpbicor 43487	Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	ifpxorcor 43488	Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑))
Theorem	ifpbi1 43489	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)))
Theorem	ifpnot23 43490	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒))
Theorem	ifpnotnotb 43491	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpnorcor 43492	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑))
Theorem	ifpnancor 43493	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓))
Theorem	ifpnot23b 43494	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒))
Theorem	ifpbiidcor2 43495	Restatement of biid 261. (Contributed by RP, 25-Apr-2020.)
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑)
Theorem	ifpnot23c 43496	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒))
Theorem	ifpnot23d 43497	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpdfnan 43498	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤))
Theorem	ifpdfxor 43499	Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓))
Theorem	ifpbi12 43500	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏)))