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={\mathrm{Base}}_K$$
	cvrne.c	$$⊢C={⋖}_K$$
Assertion	cvrnrefN	$$⊢\left(K\in A\wedge X\in B\right)\to \neg XCX$$

Proof

Step	Hyp	Ref	Expression
1		cvrne.b	$$⊢B={\mathrm{Base}}_K$$
2		cvrne.c	$$⊢C={⋖}_K$$
3		eqid	$$⊢X=X$$
4		simpll	$$⊢\left(\left(K\in A\wedge X\in B\right)\wedge XCX\right)\to K\in A$$
5		simplr	$$⊢\left(\left(K\in A\wedge X\in B\right)\wedge XCX\right)\to X\in B$$
6		simpr	$$⊢\left(\left(K\in A\wedge X\in B\right)\wedge XCX\right)\to XCX$$
7	1 2	cvrne	$$⊢\left(\left(K\in A\wedge X\in B\wedge X\in B\right)\wedge XCX\right)\to X\ne X$$
8	4 5 5 6 7	syl31anc	$$⊢\left(\left(K\in A\wedge X\in B\right)\wedge XCX\right)\to X\ne X$$
9	8	ex	$$⊢\left(K\in A\wedge X\in B\right)\to \left(XCX\to X\ne X\right)$$
10	9	necon2bd	$$⊢\left(K\in A\wedge X\in B\right)\to \left(X=X\to \neg XCX\right)$$
11	3 10	mpi	$$⊢\left(K\in A\wedge X\in B\right)\to \neg XCX$$