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	Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. _om ) -> ( A +o B ) = ( A +no B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=\varnothing \to A{+}_{𝑜}x=A{+}_{𝑜}\varnothing$$
2		oveq2	Could not format ( x = (/) -> ( A +no x ) = ( A +no (/) ) ) : No typesetting found for |- ( x = (/) -> ( A +no x ) = ( A +no (/) ) ) with typecode |-
3	1 2	eqeq12d	Could not format ( x = (/) -> ( ( A +o x ) = ( A +no x ) <-> ( A +o (/) ) = ( A +no (/) ) ) ) : No typesetting found for |- ( x = (/) -> ( ( A +o x ) = ( A +no x ) <-> ( A +o (/) ) = ( A +no (/) ) ) ) with typecode |-
4	3	imbi2d	Could not format ( x = (/) -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o (/) ) = ( A +no (/) ) ) ) ) : No typesetting found for |- ( x = (/) -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o (/) ) = ( A +no (/) ) ) ) ) with typecode |-
5		oveq2	$$⊢x=y\to A{+}_{𝑜}x=A{+}_{𝑜}y$$
6		oveq2	Could not format ( x = y -> ( A +no x ) = ( A +no y ) ) : No typesetting found for |- ( x = y -> ( A +no x ) = ( A +no y ) ) with typecode |-
7	5 6	eqeq12d	Could not format ( x = y -> ( ( A +o x ) = ( A +no x ) <-> ( A +o y ) = ( A +no y ) ) ) : No typesetting found for |- ( x = y -> ( ( A +o x ) = ( A +no x ) <-> ( A +o y ) = ( A +no y ) ) ) with typecode |-
8	7	imbi2d	Could not format ( x = y -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o y ) = ( A +no y ) ) ) ) : No typesetting found for |- ( x = y -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o y ) = ( A +no y ) ) ) ) with typecode |-
9		oveq2	$$⊢x=\mathrm{suc}y\to A{+}_{𝑜}x=A{+}_{𝑜}\mathrm{suc}y$$
10		oveq2	Could not format ( x = suc y -> ( A +no x ) = ( A +no suc y ) ) : No typesetting found for |- ( x = suc y -> ( A +no x ) = ( A +no suc y ) ) with typecode |-
11	9 10	eqeq12d	Could not format ( x = suc y -> ( ( A +o x ) = ( A +no x ) <-> ( A +o suc y ) = ( A +no suc y ) ) ) : No typesetting found for |- ( x = suc y -> ( ( A +o x ) = ( A +no x ) <-> ( A +o suc y ) = ( A +no suc y ) ) ) with typecode |-
12	11	imbi2d	Could not format ( x = suc y -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o suc y ) = ( A +no suc y ) ) ) ) : No typesetting found for |- ( x = suc y -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o suc y ) = ( A +no suc y ) ) ) ) with typecode |-
13		oveq2	$$⊢x=B\to A{+}_{𝑜}x=A{+}_{𝑜}B$$
14		oveq2	Could not format ( x = B -> ( A +no x ) = ( A +no B ) ) : No typesetting found for |- ( x = B -> ( A +no x ) = ( A +no B ) ) with typecode |-
15	13 14	eqeq12d	Could not format ( x = B -> ( ( A +o x ) = ( A +no x ) <-> ( A +o B ) = ( A +no B ) ) ) : No typesetting found for |- ( x = B -> ( ( A +o x ) = ( A +no x ) <-> ( A +o B ) = ( A +no B ) ) ) with typecode |-
16	15	imbi2d	Could not format ( x = B -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o B ) = ( A +no B ) ) ) ) : No typesetting found for |- ( x = B -> ( ( A e. On -> ( A +o x ) = ( A +no x ) ) <-> ( A e. On -> ( A +o B ) = ( A +no B ) ) ) ) with typecode |-
17		oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$
18		naddrid	Could not format ( A e. On -> ( A +no (/) ) = A ) : No typesetting found for |- ( A e. On -> ( A +no (/) ) = A ) with typecode |-
19	17 18	eqtr4d	Could not format ( A e. On -> ( A +o (/) ) = ( A +no (/) ) ) : No typesetting found for |- ( A e. On -> ( A +o (/) ) = ( A +no (/) ) ) with typecode |-
20		nnon	$$⊢y\in \mathrm{\omega }\to y\in \mathrm{On}$$
21		suceq	Could not format ( ( A +o y ) = ( A +no y ) -> suc ( A +o y ) = suc ( A +no y ) ) : No typesetting found for |- ( ( A +o y ) = ( A +no y ) -> suc ( A +o y ) = suc ( A +no y ) ) with typecode |-
22	21	adantl	Could not format ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> suc ( A +o y ) = suc ( A +no y ) ) : No typesetting found for |- ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> suc ( A +o y ) = suc ( A +no y ) ) with typecode |-
23		oasuc	$$⊢\left(A\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to A{+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(A{+}_{𝑜}y\right)$$
24	23	adantr	Could not format ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +o suc y ) = suc ( A +o y ) ) : No typesetting found for |- ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +o suc y ) = suc ( A +o y ) ) with typecode |-
25		naddsuc2	Could not format ( ( A e. On /\ y e. On ) -> ( A +no suc y ) = suc ( A +no y ) ) : No typesetting found for |- ( ( A e. On /\ y e. On ) -> ( A +no suc y ) = suc ( A +no y ) ) with typecode |-
26	25	adantr	Could not format ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +no suc y ) = suc ( A +no y ) ) : No typesetting found for |- ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +no suc y ) = suc ( A +no y ) ) with typecode |-
27	22 24 26	3eqtr4d	Could not format ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +o suc y ) = ( A +no suc y ) ) : No typesetting found for |- ( ( ( A e. On /\ y e. On ) /\ ( A +o y ) = ( A +no y ) ) -> ( A +o suc y ) = ( A +no suc y ) ) with typecode |-
28	27	ex	Could not format ( ( A e. On /\ y e. On ) -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) : No typesetting found for |- ( ( A e. On /\ y e. On ) -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) with typecode |-
29	28	expcom	Could not format ( y e. On -> ( A e. On -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) ) : No typesetting found for |- ( y e. On -> ( A e. On -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) ) with typecode |-
30	20 29	syl	Could not format ( y e. _om -> ( A e. On -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) ) : No typesetting found for |- ( y e. _om -> ( A e. On -> ( ( A +o y ) = ( A +no y ) -> ( A +o suc y ) = ( A +no suc y ) ) ) ) with typecode |-
31	30	a2d	Could not format ( y e. _om -> ( ( A e. On -> ( A +o y ) = ( A +no y ) ) -> ( A e. On -> ( A +o suc y ) = ( A +no suc y ) ) ) ) : No typesetting found for |- ( y e. _om -> ( ( A e. On -> ( A +o y ) = ( A +no y ) ) -> ( A e. On -> ( A +o suc y ) = ( A +no suc y ) ) ) ) with typecode |-
32	4 8 12 16 19 31	finds	Could not format ( B e. _om -> ( A e. On -> ( A +o B ) = ( A +no B ) ) ) : No typesetting found for |- ( B e. _om -> ( A e. On -> ( A +o B ) = ( A +no B ) ) ) with typecode |-
33	32	impcom	Could not format ( ( A e. On /\ B e. _om ) -> ( A +o B ) = ( A +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. _om ) -> ( A +o B ) = ( A +no B ) ) with typecode |-