Theorem ltpiord

Description: Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Assertion	ltpiord	|- ( ( A e. N. /\ B e. N. ) -> ( A A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		df-lti	|-
2	1	breqi	|- ( A A ( _E i^i ( N. X. N. ) ) B )
3		brinxp	|- ( ( A e. N. /\ B e. N. ) -> ( A _E B <-> A ( _E i^i ( N. X. N. ) ) B ) )
4		epelg	|- ( B e. N. -> ( A _E B <-> A e. B ) )
5	4	adantl	|- ( ( A e. N. /\ B e. N. ) -> ( A _E B <-> A e. B ) )
6	3 5	bitr3d	|- ( ( A e. N. /\ B e. N. ) -> ( A ( _E i^i ( N. X. N. ) ) B <-> A e. B ) )
7	2 6	syl5bb	|- ( ( A e. N. /\ B e. N. ) -> ( A A e. B ) )