cvrcmp

Description: If two lattice elements that cover a third are comparable, then they are equal. (Contributed by NM, 6-Feb-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cvrcmp.b	$⊢ B = {Base}_{K}$
2		cvrcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrcmp.c	$⊢ C = ⋖_{K}$
4		simpl1	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to K \in Poset$
5		simpl23	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to Z \in B$
6		simpl21	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to X \in B$
7		simpl3l	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to Z C X$
8	1 3	cvrne	$⊢ ((K \in Poset \land Z \in B \land X \in B) \land Z C X) \to Z \neq X$
9	4 5 6 7 8	syl31anc	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to Z \neq X$
10	1 2 3	cvrle	$⊢ ((K \in Poset \land Z \in B \land X \in B) \land Z C X) \to Z \underset{˙}{\leq} X$
11	4 5 6 7 10	syl31anc	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to Z \underset{˙}{\leq} X$
12		simpr	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y$
13		simpl22	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to Y \in B$
14		simpl3r	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to Z C Y$
15	1 2 3	cvrnbtwn4	$⊢ (K \in Poset \land (Z \in B \land Y \in B \land X \in B) \land Z C Y) \to ((Z \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \leftrightarrow (Z = X \lor X = Y))$
16	4 5 13 6 14 15	syl131anc	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to ((Z \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \leftrightarrow (Z = X \lor X = Y))$
17	11 12 16	mpbi2and	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to (Z = X \lor X = Y)$
18		neor	$⊢ (Z = X \lor X = Y) \leftrightarrow (Z \neq X \to X = Y)$
19	17 18	sylib	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to (Z \neq X \to X = Y)$
20	9 19	mpd	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \land X \underset{˙}{\leq} Y) \to X = Y$
21	20	ex	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \to (X \underset{˙}{\leq} Y \to X = Y)$
22		simp1	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \to K \in Poset$
23		simp21	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \to X \in B$
24	1 2	posref	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\leq} X$
25	22 23 24	syl2anc	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \to X \underset{˙}{\leq} X$
26		breq2	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Y)$
27	25 26	syl5ibcom	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \to (X = Y \to X \underset{˙}{\leq} Y)$
28	21 27	impbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B) \land (Z C X \land Z C Y)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem cvrcmp

Proof