Theorem cvrntr

Description: The covers relation is not transitive. ( cvntr analog.) (Contributed by NM, 18-Jun-2012)

	Ref	Expression
Hypotheses	cvrntr.b	|- B = ( Base ` K )
	cvrntr.c	|- C = (
Assertion	cvrntr	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X C Y /\ Y C Z ) -> -. X C Z ) )

Proof

Step	Hyp	Ref	Expression
1		cvrntr.b	|- B = ( Base ` K )
2		cvrntr.c	|- C = (
3		eqid	|- ( lt ` K ) = ( lt ` K )
4	1 3 2	cvrlt	|- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( lt ` K ) Y )
5	4	ex	|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y -> X ( lt ` K ) Y ) )
6	5	3adant3r3	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y -> X ( lt ` K ) Y ) )
7	1 3 2	ltcvrntr	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ( lt ` K ) Y /\ Y C Z ) -> -. X C Z ) )
8	6 7	syland	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X C Y /\ Y C Z ) -> -. X C Z ) )