Metamath Proof Explorer

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 ∈ 𝑵 ∧ B ∈ 𝑵 → A < 𝑵 B ↔ A ∈ B

Proof

Step Hyp Ref Expression
1 df-lti ⊢ < 𝑵 = E ∩ 𝑵 × 𝑵
2 1 breqi ⊢ A < 𝑵 B ↔ A E ∩ 𝑵 × 𝑵 B
3 brinxp ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A E B ↔ A E ∩ 𝑵 × 𝑵 B
4 epelg ⊢ B ∈ 𝑵 → A E B ↔ A ∈ B
5 4 adantl ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A E B ↔ A ∈ B
6 3 5 bitr3d ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A E ∩ 𝑵 × 𝑵 B ↔ A ∈ B
7 2 6 bitrid ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A < 𝑵 B ↔ A ∈ B