lcvnbtwn2

Description: The covers relation implies no in-betweenness. ( cvnbtwn2 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		lcvnbtwn2.p	$⊢ φ \to R \subset U$
9		lcvnbtwn2.q	$⊢ φ \to U \subseteq T$
10	1 2 3 4 5 6 7	lcvnbtwn	$⊢ φ \to \neg (R \subset U \land U \subset T)$
11		iman	$⊢ ((R \subset U \land U \subseteq T) \to U = T) \leftrightarrow \neg ((R \subset U \land U \subseteq T) \land \neg U = T)$
12		anass	$⊢ ((R \subset U \land U \subseteq T) \land \neg U = T) \leftrightarrow (R \subset U \land (U \subseteq T \land \neg U = T))$
13		dfpss2	$⊢ U \subset T \leftrightarrow (U \subseteq T \land \neg U = T)$
14	13	anbi2i	$⊢ (R \subset U \land U \subset T) \leftrightarrow (R \subset U \land (U \subseteq T \land \neg U = T))$
15	12 14	bitr4i	$⊢ ((R \subset U \land U \subseteq T) \land \neg U = T) \leftrightarrow (R \subset U \land U \subset T)$
16	15	notbii	$⊢ \neg ((R \subset U \land U \subseteq T) \land \neg U = T) \leftrightarrow \neg (R \subset U \land U \subset T)$
17	11 16	bitr2i	$⊢ \neg (R \subset U \land U \subset T) \leftrightarrow ((R \subset U \land U \subseteq T) \to U = T)$
18	10 17	sylib	$⊢ φ \to ((R \subset U \land U \subseteq T) \to U = T)$
19	8 9 18	mp2and	$⊢ φ \to U = T$

Metamath Proof Explorer