ltltncvr

Description: A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012)

	Ref	Expression
Hypotheses	ltltncvr.b	$⊢ B = {Base}_{K}$
	ltltncvr.s	$⊢ \underset{˙}{<} = <_{K}$
	ltltncvr.c	$⊢ C = ⋖_{K}$
Assertion	ltltncvr	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{<} Z) \to \neg X C Z)$

Step	Hyp	Ref	Expression
1		ltltncvr.b	$⊢ B = {Base}_{K}$
2		ltltncvr.s	$⊢ \underset{˙}{<} = <_{K}$
3		ltltncvr.c	$⊢ C = ⋖_{K}$
4		simpll	$⊢ ((K \in A \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to K \in A$
5		simplr1	$⊢ ((K \in A \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to X \in B$
6		simplr3	$⊢ ((K \in A \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to Z \in B$
7		simplr2	$⊢ ((K \in A \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to Y \in B$
8		simpr	$⊢ ((K \in A \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to X C Z$
9	1 2 3	cvrnbtwn	$⊢ (K \in A \land (X \in B \land Z \in B \land Y \in B) \land X C Z) \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} Z)$
10	4 5 6 7 8 9	syl131anc	$⊢ ((K \in A \land (X \in B \land Y \in B \land Z \in B)) \land X C Z) \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} Z)$
11	10	ex	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to (X C Z \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} Z))$
12	11	con2d	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{<} Z) \to \neg X C Z)$

Metamath Proof Explorer