lcvnbtwn3

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

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		lcvnbtwn3.p	$⊢ φ \to R \subseteq U$
9		lcvnbtwn3.q	$⊢ φ \to U \subset T$
10	1 2 3 4 5 6 7	lcvnbtwn	$⊢ φ \to \neg (R \subset U \land U \subset T)$
11		iman	$⊢ ((R \subseteq U \land U \subset T) \to R = U) \leftrightarrow \neg ((R \subseteq U \land U \subset T) \land \neg R = U)$
12		eqcom	$⊢ U = R \leftrightarrow R = U$
13	12	imbi2i	$⊢ ((R \subseteq U \land U \subset T) \to U = R) \leftrightarrow ((R \subseteq U \land U \subset T) \to R = U)$
14		dfpss2	$⊢ R \subset U \leftrightarrow (R \subseteq U \land \neg R = U)$
15	14	anbi1i	$⊢ (R \subset U \land U \subset T) \leftrightarrow ((R \subseteq U \land \neg R = U) \land U \subset T)$
16		an32	$⊢ ((R \subseteq U \land \neg R = U) \land U \subset T) \leftrightarrow ((R \subseteq U \land U \subset T) \land \neg R = U)$
17	15 16	bitri	$⊢ (R \subset U \land U \subset T) \leftrightarrow ((R \subseteq U \land U \subset T) \land \neg R = U)$
18	17	notbii	$⊢ \neg (R \subset U \land U \subset T) \leftrightarrow \neg ((R \subseteq U \land U \subset T) \land \neg R = U)$
19	11 13 18	3bitr4ri	$⊢ \neg (R \subset U \land U \subset T) \leftrightarrow ((R \subseteq U \land U \subset T) \to U = R)$
20	10 19	sylib	$⊢ φ \to ((R \subseteq U \land U \subset T) \to U = R)$
21	8 9 20	mp2and	$⊢ φ \to U = R$

Metamath Proof Explorer