Theorem lcvntr

Description: The covers relation is not transitive. ( cvntr analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lcvnbtwn.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lcvnbtwn.c	$$⊢C={⋖}_L\left(W\right)$$
	lcvnbtwn.w	$$⊢\phi \to W\in X$$
	lcvnbtwn.r	$$⊢\phi \to R\in S$$
	lcvnbtwn.t	$$⊢\phi \to T\in S$$
	lcvnbtwn.u	$$⊢\phi \to U\in S$$
	lcvnbtwn.d	$$⊢\phi \to RCT$$
	lcvntr.p	$$⊢\phi \to TCU$$
Assertion	lcvntr	$$⊢\phi \to \neg RCU$$

Proof

Step	Hyp	Ref	Expression
1		lcvnbtwn.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lcvnbtwn.c	$$⊢C={⋖}_L\left(W\right)$$
3		lcvnbtwn.w	$$⊢\phi \to W\in X$$
4		lcvnbtwn.r	$$⊢\phi \to R\in S$$
5		lcvnbtwn.t	$$⊢\phi \to T\in S$$
6		lcvnbtwn.u	$$⊢\phi \to U\in S$$
7		lcvnbtwn.d	$$⊢\phi \to RCT$$
8		lcvntr.p	$$⊢\phi \to TCU$$
9	1 2 3 4 5 7	lcvpss	$$⊢\phi \to R\subset T$$
10	1 2 3 5 6 8	lcvpss	$$⊢\phi \to T\subset U$$
11	9 10	jca	$$⊢\phi \to \left(R\subset T\wedge T\subset U\right)$$
12	3	adantr	$$⊢\left(\phi \wedge RCU\right)\to W\in X$$
13	4	adantr	$$⊢\left(\phi \wedge RCU\right)\to R\in S$$
14	6	adantr	$$⊢\left(\phi \wedge RCU\right)\to U\in S$$
15	5	adantr	$$⊢\left(\phi \wedge RCU\right)\to T\in S$$
16		simpr	$$⊢\left(\phi \wedge RCU\right)\to RCU$$
17	1 2 12 13 14 15 16	lcvnbtwn	$$⊢\left(\phi \wedge RCU\right)\to \neg \left(R\subset T\wedge T\subset U\right)$$
18	17	ex	$$⊢\phi \to \left(RCU\to \neg \left(R\subset T\wedge T\subset U\right)\right)$$
19	11 18	mt2d	$$⊢\phi \to \neg RCU$$