cvrnbtwn2

Description: The covers relation implies no in-betweenness. ( cvnbtwn2 analog.) (Contributed by NM, 17-Nov-2011)

	Ref	Expression
Hypotheses	cvrletr.b	$⊢ B = {Base}_{K}$
	cvrletr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvrletr.s	$⊢ \underset{˙}{<} = <_{K}$
	cvrletr.c	$⊢ C = ⋖_{K}$
Assertion	cvrnbtwn2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \leftrightarrow Z = Y)$

Proof

Step	Hyp	Ref	Expression
1		cvrletr.b	$⊢ B = {Base}_{K}$
2		cvrletr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrletr.s	$⊢ \underset{˙}{<} = <_{K}$
4		cvrletr.c	$⊢ C = ⋖_{K}$
5	1 3 4	cvrnbtwn	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to \neg (X \underset{˙}{<} Z \land Z \underset{˙}{<} Y)$
6	5	3expia	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \to \neg (X \underset{˙}{<} Z \land Z \underset{˙}{<} Y))$
7		iman	$⊢ ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \to Z = Y) \leftrightarrow \neg ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \land \neg Z = Y)$
8		anass	$⊢ ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \land \neg Z = Y) \leftrightarrow (X \underset{˙}{<} Z \land (Z \underset{˙}{\leq} Y \land \neg Z = Y))$
9		simpl	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to K \in Poset$
10		simpr3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
11		simpr2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
12	2 3	pltval	$⊢ (K \in Poset \land Z \in B \land Y \in B) \to (Z \underset{˙}{<} Y \leftrightarrow (Z \underset{˙}{\leq} Y \land Z \neq Y))$
13	9 10 11 12	syl3anc	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{<} Y \leftrightarrow (Z \underset{˙}{\leq} Y \land Z \neq Y))$
14		df-ne	$⊢ Z \neq Y \leftrightarrow \neg Z = Y$
15	14	anbi2i	$⊢ (Z \underset{˙}{\leq} Y \land Z \neq Y) \leftrightarrow (Z \underset{˙}{\leq} Y \land \neg Z = Y)$
16	13 15	bitrdi	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{<} Y \leftrightarrow (Z \underset{˙}{\leq} Y \land \neg Z = Y))$
17	16	anbi2d	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Z \land Z \underset{˙}{<} Y) \leftrightarrow (X \underset{˙}{<} Z \land (Z \underset{˙}{\leq} Y \land \neg Z = Y)))$
18	8 17	bitr4id	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \land \neg Z = Y) \leftrightarrow (X \underset{˙}{<} Z \land Z \underset{˙}{<} Y))$
19	18	notbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (\neg ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \land \neg Z = Y) \leftrightarrow \neg (X \underset{˙}{<} Z \land Z \underset{˙}{<} Y))$
20	7 19	bitr2id	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (\neg (X \underset{˙}{<} Z \land Z \underset{˙}{<} Y) \leftrightarrow ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \to Z = Y))$
21	6 20	sylibd	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \to ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \to Z = Y))$
22	21	3impia	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \to Z = Y)$
23	1 3 4	cvrlt	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to X \underset{˙}{<} Y$
24	23	ex	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X C Y \to X \underset{˙}{<} Y)$
25	24	3adant3r3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \to X \underset{˙}{<} Y)$
26	25	3impia	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to X \underset{˙}{<} Y$
27		breq2	$⊢ Z = Y \to (X \underset{˙}{<} Z \leftrightarrow X \underset{˙}{<} Y)$
28	26 27	syl5ibrcom	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (Z = Y \to X \underset{˙}{<} Z)$
29	1 2	posref	$⊢ (K \in Poset \land Y \in B) \to Y \underset{˙}{\leq} Y$
30	29	3ad2antr2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\leq} Y$
31		breq1	$⊢ Z = Y \to (Z \underset{˙}{\leq} Y \leftrightarrow Y \underset{˙}{\leq} Y)$
32	30 31	syl5ibrcom	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (Z = Y \to Z \underset{˙}{\leq} Y)$
33	32	3adant3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (Z = Y \to Z \underset{˙}{\leq} Y)$
34	28 33	jcad	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (Z = Y \to (X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y))$
35	22 34	impbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X \underset{˙}{<} Z \land Z \underset{˙}{\leq} Y) \leftrightarrow Z = Y)$

Metamath Proof Explorer

Theorem cvrnbtwn2

Proof