Theorem addpiord

Description: Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addpiord	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=A{+}_{𝑜}B$$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to ⟨A,B⟩\in \left(𝑵\times 𝑵\right)$$
2		fvres	$$⊢⟨A,B⟩\in \left(𝑵\times 𝑵\right)\to \left({{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}\right)\left(⟨A,B⟩\right)={+}_{𝑜}\left(⟨A,B⟩\right)$$
3		df-ov	$$⊢A{+}_{𝑵}B={+}_{𝑵}\left(⟨A,B⟩\right)$$
4		df-pli	$$⊢{+}_{𝑵}={{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}$$
5	4	fveq1i	$$⊢{+}_{𝑵}\left(⟨A,B⟩\right)=\left({{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}\right)\left(⟨A,B⟩\right)$$
6	3 5	eqtri	$$⊢A{+}_{𝑵}B=\left({{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}\right)\left(⟨A,B⟩\right)$$
7		df-ov	$$⊢A{+}_{𝑜}B={+}_{𝑜}\left(⟨A,B⟩\right)$$
8	2 6 7	3eqtr4g	$$⊢⟨A,B⟩\in \left(𝑵\times 𝑵\right)\to A{+}_{𝑵}B=A{+}_{𝑜}B$$
9	1 8	syl	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=A{+}_{𝑜}B$$