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	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-lti	⊢ <N = ( E ∩ ( N × N ) )
2	1	breqi	⊢ ( 𝐴 <N 𝐵 ↔ 𝐴 ( E ∩ ( N × N ) ) 𝐵 )
3		brinxp	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 E 𝐵 ↔ 𝐴 ( E ∩ ( N × N ) ) 𝐵 ) )
4		epelg	⊢ ( 𝐵 ∈ N → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
5	4	adantl	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
6	3 5	bitr3d	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ( E ∩ ( N × N ) ) 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
7	2 6	bitrid	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵 ) )