Theorem naddonnn

Description: 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)

	Ref	Expression
Assertion	naddonnn	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) = ( 𝐴 +no 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) )
2		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 +no 𝑥 ) = ( 𝐴 +no ∅ ) )
3	1 2	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ↔ ( 𝐴 +o ∅ ) = ( 𝐴 +no ∅ ) ) )
4	3	imbi2d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∈ On → ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ) ↔ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = ( 𝐴 +no ∅ ) ) ) )
5		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
6		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 +no 𝑥 ) = ( 𝐴 +no 𝑦 ) )
7	5 6	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ↔ ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) )
8	7	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ On → ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ) ↔ ( 𝐴 ∈ On → ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) ) )
9		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) )
10		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 +no 𝑥 ) = ( 𝐴 +no suc 𝑦 ) )
11	9 10	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ↔ ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) ) )
12	11	imbi2d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ∈ On → ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ) ↔ ( 𝐴 ∈ On → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) ) ) )
13		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐵 ) )
14		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 +no 𝑥 ) = ( 𝐴 +no 𝐵 ) )
15	13 14	eqeq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) = ( 𝐴 +no 𝐵 ) ) )
16	15	imbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ On → ( 𝐴 +o 𝑥 ) = ( 𝐴 +no 𝑥 ) ) ↔ ( 𝐴 ∈ On → ( 𝐴 +o 𝐵 ) = ( 𝐴 +no 𝐵 ) ) ) )
17		oa0	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
18		naddrid	⊢ ( 𝐴 ∈ On → ( 𝐴 +no ∅ ) = 𝐴 )
19	17 18	eqtr4d	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = ( 𝐴 +no ∅ ) )
20		nnon	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
21		suceq	⊢ ( ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) → suc ( 𝐴 +o 𝑦 ) = suc ( 𝐴 +no 𝑦 ) )
22	21	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) → suc ( 𝐴 +o 𝑦 ) = suc ( 𝐴 +no 𝑦 ) )
23		oasuc	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
24	23	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
25		naddsuc2	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 +no suc 𝑦 ) = suc ( 𝐴 +no 𝑦 ) )
26	25	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) → ( 𝐴 +no suc 𝑦 ) = suc ( 𝐴 +no 𝑦 ) )
27	22 24 26	3eqtr4d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) )
28	27	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) ) )
29	28	expcom	⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) ) ) )
30	20 29	syl	⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ On → ( ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) ) ) )
31	30	a2d	⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ On → ( 𝐴 +o 𝑦 ) = ( 𝐴 +no 𝑦 ) ) → ( 𝐴 ∈ On → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +no suc 𝑦 ) ) ) )
32	4 8 12 16 19 31	finds	⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ On → ( 𝐴 +o 𝐵 ) = ( 𝐴 +no 𝐵 ) ) )
33	32	impcom	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) = ( 𝐴 +no 𝐵 ) )