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

Theorem leltctr 6212
 Description: Transitivity law for cardinal less than or equal and less than. (Contributed by SF, 16-Mar-2015.)
Assertion
Ref Expression
leltctr ((A NC B NC C NC ) → ((Ac B B <c C) → A <c C))

Proof of Theorem leltctr
StepHypRef Expression
1 lectr 6211 . . . . . 6 ((A NC B NC C NC ) → ((Ac B Bc C) → Ac C))
21expdimp 426 . . . . 5 (((A NC B NC C NC ) Ac B) → (Bc CAc C))
32adantrd 454 . . . 4 (((A NC B NC C NC ) Ac B) → ((Bc C BC) → Ac C))
4 breq1 4642 . . . . . . . . . . 11 (A = C → (Ac BCc B))
54anbi1d 685 . . . . . . . . . 10 (A = C → ((Ac B Bc C) ↔ (Cc B Bc C)))
65biimpac 472 . . . . . . . . 9 (((Ac B Bc C) A = C) → (Cc B Bc C))
7 sbth 6206 . . . . . . . . . . . 12 ((C NC B NC ) → ((Cc B Bc C) → C = B))
87ancoms 439 . . . . . . . . . . 11 ((B NC C NC ) → ((Cc B Bc C) → C = B))
983adant1 973 . . . . . . . . . 10 ((A NC B NC C NC ) → ((Cc B Bc C) → C = B))
10 eqcom 2355 . . . . . . . . . 10 (B = CC = B)
119, 10syl6ibr 218 . . . . . . . . 9 ((A NC B NC C NC ) → ((Cc B Bc C) → B = C))
126, 11syl5 28 . . . . . . . 8 ((A NC B NC C NC ) → (((Ac B Bc C) A = C) → B = C))
1312expdimp 426 . . . . . . 7 (((A NC B NC C NC ) (Ac B Bc C)) → (A = CB = C))
1413necon3d 2554 . . . . . 6 (((A NC B NC C NC ) (Ac B Bc C)) → (BCAC))
1514expr 598 . . . . 5 (((A NC B NC C NC ) Ac B) → (Bc C → (BCAC)))
1615imp3a 420 . . . 4 (((A NC B NC C NC ) Ac B) → ((Bc C BC) → AC))
173, 16jcad 519 . . 3 (((A NC B NC C NC ) Ac B) → ((Bc C BC) → (Ac C AC)))
18 brltc 6114 . . 3 (B <c C ↔ (Bc C BC))
19 brltc 6114 . . 3 (A <c C ↔ (Ac C AC))
2017, 18, 193imtr4g 261 . 2 (((A NC B NC C NC ) Ac B) → (B <c CA <c C))
2120expimpd 586 1 ((A NC B NC C NC ) → ((Ac B B <c C) → A <c C))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2516   class class class wbr 4639   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator