New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ltfinasym GIF version

Theorem ltfinasym 4460
 Description: Asymmetry law for finite less than. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
ltfinasym ((A Nn B Nn ) → (⟪A, B <fin → ¬ ⟪B, A <fin ))

Proof of Theorem ltfinasym
StepHypRef Expression
1 ltfinirr 4457 . . . 4 (A Nn → ¬ ⟪A, A <fin )
21ad2antrr 706 . . 3 (((A Nn B Nn ) A, B <fin ) → ¬ ⟪A, A <fin )
3 ltfintr 4459 . . . . 5 ((A Nn B Nn A Nn ) → ((⟪A, B <fin B, A <fin ) → ⟪A, A <fin ))
433anidm13 1240 . . . 4 ((A Nn B Nn ) → ((⟪A, B <fin B, A <fin ) → ⟪A, A <fin ))
54expdimp 426 . . 3 (((A Nn B Nn ) A, B <fin ) → (⟪B, A <fin → ⟪A, A <fin ))
62, 5mtod 168 . 2 (((A Nn B Nn ) A, B <fin ) → ¬ ⟪B, A <fin )
76ex 423 1 ((A Nn B Nn ) → (⟪A, B <fin → ¬ ⟪B, A <fin ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358   ∈ wcel 1710  ⟪copk 4057   Nn cnnc 4373
 Copyright terms: Public domain W3C validator