naddass1

Description: Natural addition of ordinal numbers is associative when the third element is 1. (Contributed by RP, 1-Jan-2025)

		Ref	Expression
	Assertion	naddass1	$⊢ (A \in On \land B \in On) \to (A + B) + 1_{𝑜} = A + (B + 1_{𝑜})$

Step	Hyp	Ref	Expression
1		naddsuc2	$⊢ (A \in On \land B \in On) \to A + suc B = suc (A + B)$
2		nadd1suc	$⊢ B \in On \to B + 1_{𝑜} = suc B$
3	2	adantl	$⊢ (A \in On \land B \in On) \to B + 1_{𝑜} = suc B$
4	3	oveq2d	$⊢ (A \in On \land B \in On) \to A + (B + 1_{𝑜}) = A + suc B$
5		naddcl	$⊢ (A \in On \land B \in On) \to A + B \in On$
6		nadd1suc	$⊢ A + B \in On \to (A + B) + 1_{𝑜} = suc (A + B)$
7	5 6	syl	$⊢ (A \in On \land B \in On) \to (A + B) + 1_{𝑜} = suc (A + B)$
8	1 4 7	3eqtr4rd	$⊢ (A \in On \land B \in On) \to (A + B) + 1_{𝑜} = A + (B + 1_{𝑜})$

Metamath Proof Explorer