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	|- .< = ( lt ` K )
	ltltncvr.c	|- C = (
Assertion	ltcvrntr	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y C Z ) -> -. X C Z ) )

Proof

Step	Hyp	Ref	Expression
1		ltltncvr.b	|- B = ( Base ` K )
2		ltltncvr.s	|- .< = ( lt ` K )
3		ltltncvr.c	|- C = (
4	1 2 3	cvrlt	|- ( ( ( K e. A /\ Y e. B /\ Z e. B ) /\ Y C Z ) -> Y .< Z )
5	4	ex	|- ( ( K e. A /\ Y e. B /\ Z e. B ) -> ( Y C Z -> Y .< Z ) )
6	5	3adant3r1	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y C Z -> Y .< Z ) )
7	1 2 3	ltltncvr	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> -. X C Z ) )
8	6 7	sylan2d	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y C Z ) -> -. X C Z ) )