cvrnbtwn4

Description: The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of MaedaMaeda p. 31. ( cvnbtwn4 analog.) (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	cvrle.b	$⊢ B = {Base}_{K}$
	cvrle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvrle.c	$⊢ C = ⋖_{K}$
Assertion	cvrnbtwn4	$⊢ (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{˙}{\leq} Y) \leftrightarrow (X = Z \lor Z = Y))$

Proof

Step	Hyp	Ref	Expression
1		cvrle.b	$⊢ B = {Base}_{K}$
2		cvrle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrle.c	$⊢ C = ⋖_{K}$
4		eqid	$⊢ <_{K} = <_{K}$
5	1 4 3	cvrnbtwn	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to \neg (X <_{K} Z \land Z <_{K} Y)$
6		iman	$⊢ ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \to (X = Z \lor Z = Y)) \leftrightarrow \neg ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land \neg (X = Z \lor Z = Y))$
7		neanior	$⊢ (X \neq Z \land Z \neq Y) \leftrightarrow \neg (X = Z \lor Z = Y)$
8	7	anbi2i	$⊢ ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land (X \neq Z \land Z \neq Y)) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land \neg (X = Z \lor Z = Y))$
9		an4	$⊢ ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land (X \neq Z \land Z \neq Y)) \leftrightarrow ((X \underset{˙}{\leq} Z \land X \neq Z) \land (Z \underset{˙}{\leq} Y \land Z \neq Y))$
10	8 9	bitr3i	$⊢ ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land \neg (X = Z \lor Z = Y)) \leftrightarrow ((X \underset{˙}{\leq} Z \land X \neq Z) \land (Z \underset{˙}{\leq} Y \land Z \neq Y))$
11	2 4	pltval	$⊢ (K \in Poset \land X \in B \land Z \in B) \to (X <_{K} Z \leftrightarrow (X \underset{˙}{\leq} Z \land X \neq Z))$
12	11	3adant3r2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X <_{K} Z \leftrightarrow (X \underset{˙}{\leq} Z \land X \neq Z))$
13	2 4	pltval	$⊢ (K \in Poset \land Z \in B \land Y \in B) \to (Z <_{K} Y \leftrightarrow (Z \underset{˙}{\leq} Y \land Z \neq Y))$
14	13	3com23	$⊢ (K \in Poset \land Y \in B \land Z \in B) \to (Z <_{K} Y \leftrightarrow (Z \underset{˙}{\leq} Y \land Z \neq Y))$
15	14	3adant3r1	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (Z <_{K} Y \leftrightarrow (Z \underset{˙}{\leq} Y \land Z \neq Y))$
16	12 15	anbi12d	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X <_{K} Z \land Z <_{K} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land X \neq Z) \land (Z \underset{˙}{\leq} Y \land Z \neq Y)))$
17	10 16	bitr4id	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land \neg (X = Z \lor Z = Y)) \leftrightarrow (X <_{K} Z \land Z <_{K} Y))$
18	17	notbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (\neg ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \land \neg (X = Z \lor Z = Y)) \leftrightarrow \neg (X <_{K} Z \land Z <_{K} Y))$
19	6 18	syl5rbb	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (\neg (X <_{K} Z \land Z <_{K} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \to (X = Z \lor Z = Y)))$
20	19	3adant3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to (\neg (X <_{K} Z \land Z <_{K} Y) \leftrightarrow ((X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y) \to (X = Z \lor Z = Y)))$
21	5 20	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{˙}{\leq} Y) \to (X = Z \lor Z = Y))$
22	1 2	posref	$⊢ (K \in Poset \land Z \in B) \to Z \underset{˙}{\leq} Z$
23	22	3ad2antr3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to Z \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 Z \underset{˙}{\leq} Z$
25		breq1	$⊢ X = Z \to (X \underset{˙}{\leq} Z \leftrightarrow Z \underset{˙}{\leq} Z)$
26	24 25	syl5ibrcom	$⊢ (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)$
27	1 2 3	cvrle	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to X \underset{˙}{\leq} Y$
28	27	ex	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X C Y \to X \underset{˙}{\leq} Y)$
29	28	3adant3r3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \to X \underset{˙}{\leq} Y)$
30	29	3impia	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to X \underset{˙}{\leq} Y$
31		breq2	$⊢ Z = Y \to (X \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\leq} Y)$
32	30 31	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{˙}{\leq} Z)$
33	26 32	jaod	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X = Z \lor Z = Y) \to X \underset{˙}{\leq} Z)$
34		breq1	$⊢ X = Z \to (X \underset{˙}{\leq} Y \leftrightarrow Z \underset{˙}{\leq} Y)$
35	30 34	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{˙}{\leq} Y)$
36		breq2	$⊢ Z = Y \to (Z \underset{˙}{\leq} Z \leftrightarrow Z \underset{˙}{\leq} Y)$
37	24 36	syl5ibcom	$⊢ (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)$
38	35 37	jaod	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X = Z \lor Z = Y) \to Z \underset{˙}{\leq} Y)$
39	33 38	jcad	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land X C Y) \to ((X = Z \lor Z = Y) \to (X \underset{˙}{\leq} Z \land Z \underset{˙}{\leq} Y))$
40	21 39	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{˙}{\leq} Y) \leftrightarrow (X = Z \lor Z = Y))$

Metamath Proof Explorer

Theorem cvrnbtwn4

Proof