Theorem cvrnrefN

Description: The covers relation is not reflexive. ( cvnref analog.) (Contributed by NM, 1-Nov-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cvrne.b	|- B = ( Base ` K )
2		cvrne.c	|- C = (
3		eqid	|- X = X
4		simpll	|- ( ( ( K e. A /\ X e. B ) /\ X C X ) -> K e. A )
5		simplr	|- ( ( ( K e. A /\ X e. B ) /\ X C X ) -> X e. B )
6		simpr	|- ( ( ( K e. A /\ X e. B ) /\ X C X ) -> X C X )
7	1 2	cvrne	|- ( ( ( K e. A /\ X e. B /\ X e. B ) /\ X C X ) -> X =/= X )
8	4 5 5 6 7	syl31anc	|- ( ( ( K e. A /\ X e. B ) /\ X C X ) -> X =/= X )
9	8	ex	|- ( ( K e. A /\ X e. B ) -> ( X C X -> X =/= X ) )
10	9	necon2bd	|- ( ( K e. A /\ X e. B ) -> ( X = X -> -. X C X ) )
11	3 10	mpi	|- ( ( K e. A /\ X e. B ) -> -. X C X )