cvrnbtwn3

Description: The covers relation implies no in-betweenness. ( cvnbtwn3 analog.) (Contributed by NM, 4-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	cvrnbtwn3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \leftrightarrow X = Z)$

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	2 3	pltval	$⊢ (K \in Poset \land X \in B \land Z \in B) \to (X \underset{˙}{<} Z \leftrightarrow (X \underset{˙}{\leq} Z \land X \neq Z))$
7	6	3adant3r2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{<} Z \leftrightarrow (X \underset{˙}{\leq} Z \land X \neq Z))$
8	7	3adant3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (X \underset{˙}{<} Z \leftrightarrow (X \underset{˙}{\leq} Z \land X \neq Z))$
9	8	anbi1d	$⊢ (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{˙}{<} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land X \neq Z) \land Z \underset{˙}{<} Y))$
10	9	notbid	$⊢ (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) \leftrightarrow \neg ((X \underset{˙}{\leq} Z \land X \neq Z) \land Z \underset{˙}{<} Y))$
11		an32	$⊢ ((X \underset{˙}{\leq} Z \land X \neq Z) \land Z \underset{˙}{<} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \land X \neq Z)$
12		df-ne	$⊢ X \neq Z \leftrightarrow \neg X = Z$
13	12	anbi2i	$⊢ ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \land X \neq Z) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \land \neg X = Z)$
14	11 13	bitri	$⊢ ((X \underset{˙}{\leq} Z \land X \neq Z) \land Z \underset{˙}{<} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \land \neg X = Z)$
15	14	notbii	$⊢ \neg ((X \underset{˙}{\leq} Z \land X \neq Z) \land Z \underset{˙}{<} Y) \leftrightarrow \neg ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \land \neg X = Z)$
16		iman	$⊢ ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \to X = Z) \leftrightarrow \neg ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \land \neg X = Z)$
17	15 16	bitr4i	$⊢ \neg ((X \underset{˙}{\leq} Z \land X \neq Z) \land Z \underset{˙}{<} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \to X = Z)$
18	10 17	bitrdi	$⊢ (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) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \to X = Z))$
19	5 18	mpbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \to X = Z)$
20	1 2	posref	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\leq} X$
21		breq2	$⊢ X = Z \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Z)$
22	20 21	syl5ibcom	$⊢ (K \in Poset \land X \in B) \to (X = Z \to X \underset{˙}{\leq} Z)$
23	22	3ad2antr1	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X = Z \to X \underset{˙}{\leq} Z)$
24	23	3adant3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (X = Z \to X \underset{˙}{\leq} Z)$
25		simp1	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to K \in Poset$
26		simp21	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to X \in B$
27		simp22	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to Y \in B$
28		simp3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to X C Y$
29	1 3 4	cvrlt	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to X \underset{˙}{<} Y$
30	25 26 27 28 29	syl31anc	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to X \underset{˙}{<} Y$
31		breq1	$⊢ X = Z \to (X \underset{˙}{<} Y \leftrightarrow Z \underset{˙}{<} Y)$
32	30 31	syl5ibcom	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (X = Z \to Z \underset{˙}{<} Y)$
33	24 32	jcad	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (X = Z \to (X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y))$
34	19 33	impbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X \underset{˙}{\leq} Z \land Z \underset{˙}{<} Y) \leftrightarrow X = Z)$

Metamath Proof Explorer

Theorem cvrnbtwn3

Proof