lcvnbtwn

Description: The covers relation implies no in-betweenness. ( cvnbtwn analog.) (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	lcvnbtwn.s	$⊢ S = LSubSp (W)$
	lcvnbtwn.c	$⊢ C = ⋖_{L} (W)$
	lcvnbtwn.w	$⊢ φ \to W \in X$
	lcvnbtwn.r	$⊢ φ \to R \in S$
	lcvnbtwn.t	$⊢ φ \to T \in S$
	lcvnbtwn.u	$⊢ φ \to U \in S$
	lcvnbtwn.d	$⊢ φ \to R C T$
Assertion	lcvnbtwn	$⊢ φ \to \neg (R \subset U \land U \subset T)$

Step	Hyp	Ref	Expression
1		lcvnbtwn.s	$⊢ S = LSubSp (W)$
2		lcvnbtwn.c	$⊢ C = ⋖_{L} (W)$
3		lcvnbtwn.w	$⊢ φ \to W \in X$
4		lcvnbtwn.r	$⊢ φ \to R \in S$
5		lcvnbtwn.t	$⊢ φ \to T \in S$
6		lcvnbtwn.u	$⊢ φ \to U \in S$
7		lcvnbtwn.d	$⊢ φ \to R C T$
8	1 2 3 4 5	lcvbr	$⊢ φ \to (R C T \leftrightarrow (R \subset T \land \neg \exists u \in S (R \subset u \land u \subset T)))$
9	7 8	mpbid	$⊢ φ \to (R \subset T \land \neg \exists u \in S (R \subset u \land u \subset T))$
10	9	simprd	$⊢ φ \to \neg \exists u \in S (R \subset u \land u \subset T)$
11		psseq2	$⊢ u = U \to (R \subset u \leftrightarrow R \subset U)$
12		psseq1	$⊢ u = U \to (u \subset T \leftrightarrow U \subset T)$
13	11 12	anbi12d	$⊢ u = U \to ((R \subset u \land u \subset T) \leftrightarrow (R \subset U \land U \subset T))$
14	13	rspcev	$⊢ (U \in S \land (R \subset U \land U \subset T)) \to \exists u \in S (R \subset u \land u \subset T)$
15	6 14	sylan	$⊢ (φ \land (R \subset U \land U \subset T)) \to \exists u \in S (R \subset u \land u \subset T)$
16	10 15	mtand	$⊢ φ \to \neg (R \subset U \land U \subset T)$

Metamath Proof Explorer