Theorem mulpiord

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

	Ref	Expression
Assertion	mulpiord	|- ( ( 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-mi	|- .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 ) )