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

Theorem ltlenlec 6207
 Description: Cardinal less than is equivalent to one-way cardinal less than or equal. Theorem XI.2.21 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
Assertion
Ref Expression
ltlenlec ((M NC N NC ) → (M <c N ↔ (Mc N ¬ Nc M)))

Proof of Theorem ltlenlec
StepHypRef Expression
1 brltc 6114 . 2 (M <c N ↔ (Mc N MN))
2 nclecid 6197 . . . . . . 7 (M NCMc M)
3 breq1 4642 . . . . . . 7 (M = N → (Mc MNc M))
42, 3syl5ibcom 211 . . . . . 6 (M NC → (M = NNc M))
54ad2antrr 706 . . . . 5 (((M NC N NC ) Mc N) → (M = NNc M))
6 sbth 6206 . . . . . 6 ((M NC N NC ) → ((Mc N Nc M) → M = N))
76expdimp 426 . . . . 5 (((M NC N NC ) Mc N) → (Nc MM = N))
85, 7impbid 183 . . . 4 (((M NC N NC ) Mc N) → (M = NNc M))
98necon3abid 2549 . . 3 (((M NC N NC ) Mc N) → (MN ↔ ¬ Nc M))
109pm5.32da 622 . 2 ((M NC N NC ) → ((Mc N MN) ↔ (Mc N ¬ Nc M)))
111, 10syl5bb 248 1 ((M NC N NC ) → (M <c N ↔ (Mc N ¬ Nc M)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516   class class class wbr 4639   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator