Metamath Proof Explorer


Theorem ltcvrntr

Description: Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses ltltncvr.b B = Base K
ltltncvr.s < ˙ = < K
ltltncvr.c C = K
Assertion ltcvrntr K A X B Y B Z B X < ˙ Y Y C Z ¬ X C Z

Proof

Step Hyp Ref Expression
1 ltltncvr.b B = Base K
2 ltltncvr.s < ˙ = < K
3 ltltncvr.c C = K
4 1 2 3 cvrlt K A Y B Z B Y C Z Y < ˙ Z
5 4 ex K A Y B Z B Y C Z Y < ˙ Z
6 5 3adant3r1 K A X B Y B Z B Y C Z Y < ˙ Z
7 1 2 3 ltltncvr K A X B Y B Z B X < ˙ Y Y < ˙ Z ¬ X C Z
8 6 7 sylan2d K A X B Y B Z B X < ˙ Y Y C Z ¬ X C Z