Theorem cvrne

Description: The covers relation implies inequality. (Contributed by NM, 13-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		cvrne.b	|- B = ( Base ` K )
2		cvrne.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		eqid	|- ( le ` K ) = ( le ` K )
6	5 3	pltval	|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X ( lt ` K ) Y <-> ( X ( le ` K ) Y /\ X =/= Y ) ) )
7	6	simplbda	|- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X ( lt ` K ) Y ) -> X =/= Y )
8	4 7	syldan	|- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X =/= Y )