Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltpiord Structured version   Visualization version   GIF version

Theorem ltpiord 9661
 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.)
Assertion
Ref Expression
ltpiord ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))

Proof of Theorem ltpiord
StepHypRef Expression
1 df-lti 9649 . . 3 <N = ( E ∩ (N × N))
21breqi 4624 . 2 (𝐴 <N 𝐵𝐴( E ∩ (N × N))𝐵)
3 brinxp 5147 . . 3 ((𝐴N𝐵N) → (𝐴 E 𝐵𝐴( E ∩ (N × N))𝐵))
4 epelg 4991 . . . 4 (𝐵N → (𝐴 E 𝐵𝐴𝐵))
54adantl 482 . . 3 ((𝐴N𝐵N) → (𝐴 E 𝐵𝐴𝐵))
63, 5bitr3d 270 . 2 ((𝐴N𝐵N) → (𝐴( E ∩ (N × N))𝐵𝐴𝐵))
72, 6syl5bb 272 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1987   ∩ cin 3558   class class class wbr 4618   E cep 4988   × cxp 5077  Ncnpi 9618
 Copyright terms: Public domain W3C validator