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	|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	|- ( ( A e. N. /\ B e. N. ) -> <. A , B >. e. ( N. X. N. ) )
2		fvres	|- ( <. A , B >. e. ( N. X. N. ) -> ( ( +o |` ( N. X. N. ) ) ` <. A , B >. ) = ( +o ` <. A , B >. ) )
3		df-ov	|- ( A +N B ) = ( +N ` <. A , B >. )
4		df-pli	|- +N = ( +o |` ( N. X. N. ) )
5	4	fveq1i	|- ( +N ` <. A , B >. ) = ( ( +o |` ( N. X. N. ) ) ` <. A , B >. )
6	3 5	eqtri	|- ( A +N B ) = ( ( +o |` ( N. X. N. ) ) ` <. A , B >. )
7		df-ov	|- ( A +o B ) = ( +o ` <. A , B >. )
8	2 6 7	3eqtr4g	|- ( <. A , B >. e. ( N. X. N. ) -> ( A +N B ) = ( A +o B ) )
9	1 8	syl	|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )