Theorem naddoa

Description: Natural addition of a natural is the same as regular addition. (Contributed by Scott Fenton, 20-Aug-2025)

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

Proof

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