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	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A{<}_{𝑵}B\leftrightarrow A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-lti	$$⊢{<}_{𝑵}=\mathrm{E}\cap \left(𝑵\times 𝑵\right)$$
2	1	breqi	$$⊢A{<}_{𝑵}B\leftrightarrow A\left(\mathrm{E}\cap \left(𝑵\times 𝑵\right)\right)B$$
3		brinxp	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A\mathrm{E}B\leftrightarrow A\left(\mathrm{E}\cap \left(𝑵\times 𝑵\right)\right)B\right)$$
4		epelg	$$⊢B\in 𝑵\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$
5	4	adantl	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$
6	3 5	bitr3d	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A\left(\mathrm{E}\cap \left(𝑵\times 𝑵\right)\right)B\leftrightarrow A\in B\right)$$
7	2 6	bitrid	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A{<}_{𝑵}B\leftrightarrow A\in B\right)$$