Theorem cvrlt

Description: The covers relation implies the less-than relation. ( cvpss analog.) (Contributed by NM, 8-Oct-2011)

	Ref	Expression
Hypotheses	cvrfval.b	$$⊢B={\mathrm{Base}}_K$$
	cvrfval.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	cvrfval.c	$$⊢C={⋖}_K$$
Assertion	cvrlt	$$⊢\left(\left(K\in A\wedge X\in B\wedge Y\in B\right)\wedge XCY\right)\to X\underset{\dot{}}{<}Y$$

Proof

Step	Hyp	Ref	Expression
1		cvrfval.b	$$⊢B={\mathrm{Base}}_K$$
2		cvrfval.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		cvrfval.c	$$⊢C={⋖}_K$$
4	1 2 3	cvrval	$$⊢\left(K\in A\wedge X\in B\wedge Y\in B\right)\to \left(XCY\leftrightarrow \left(X\underset{\dot{}}{<}Y\wedge \neg \exists z\in B\left(X\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{<}Y\right)\right)\right)$$
5	4	simprbda	$$⊢\left(\left(K\in A\wedge X\in B\wedge Y\in B\right)\wedge XCY\right)\to X\underset{\dot{}}{<}Y$$