Metamath Proof Explorer

Theorem cvrcmp2

Description: If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012)

Ref Expression
Hypotheses cvrcmp.b ⊢ B = Base K
cvrcmp.l ⊢ ≤ ˙ = ≤ K
cvrcmp.c ⊢ C = ⋖ K
Assertion cvrcmp2 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → X ≤ ˙ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 cvrcmp.b ⊢ B = Base K
2 cvrcmp.l ⊢ ≤ ˙ = ≤ K
3 cvrcmp.c ⊢ C = ⋖ K
4 opposet ⊢ K ∈ OP → K ∈ Poset
5 4 3ad2ant1 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → K ∈ Poset
6 simp1 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → K ∈ OP
7 simp22 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → Y ∈ B
8 eqid ⊢ oc ⁡ K = oc ⁡ K
9 1 8 opoccl ⊢ K ∈ OP ∧ Y ∈ B → oc ⁡ K ⁡ Y ∈ B
10 6 7 9 syl2anc ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → oc ⁡ K ⁡ Y ∈ B
11 simp21 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → X ∈ B
12 1 8 opoccl ⊢ K ∈ OP ∧ X ∈ B → oc ⁡ K ⁡ X ∈ B
13 6 11 12 syl2anc ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → oc ⁡ K ⁡ X ∈ B
14 simp23 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → Z ∈ B
15 1 8 opoccl ⊢ K ∈ OP ∧ Z ∈ B → oc ⁡ K ⁡ Z ∈ B
16 6 14 15 syl2anc ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → oc ⁡ K ⁡ Z ∈ B
17 1 8 3 cvrcon3b ⊢ K ∈ OP ∧ X ∈ B ∧ Z ∈ B → X C Z ↔ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ X
18 17 3adant3r2 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X C Z ↔ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ X
19 1 8 3 cvrcon3b ⊢ K ∈ OP ∧ Y ∈ B ∧ Z ∈ B → Y C Z ↔ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ Y
20 19 3adant3r1 ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y C Z ↔ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ Y
21 18 20 anbi12d ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X C Z ∧ Y C Z ↔ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ X ∧ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ Y
22 21 biimp3a ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → oc ⁡ K ⁡ Z C oc ⁡ K ⁡ X ∧ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ Y
23 22 ancomd ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → oc ⁡ K ⁡ Z C oc ⁡ K ⁡ Y ∧ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ X
24 1 2 3 cvrcmp ⊢ K ∈ Poset ∧ oc ⁡ K ⁡ Y ∈ B ∧ oc ⁡ K ⁡ X ∈ B ∧ oc ⁡ K ⁡ Z ∈ B ∧ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ Y ∧ oc ⁡ K ⁡ Z C oc ⁡ K ⁡ X → oc ⁡ K ⁡ Y ≤ ˙ oc ⁡ K ⁡ X ↔ oc ⁡ K ⁡ Y = oc ⁡ K ⁡ X
25 5 10 13 16 23 24 syl131anc ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → oc ⁡ K ⁡ Y ≤ ˙ oc ⁡ K ⁡ X ↔ oc ⁡ K ⁡ Y = oc ⁡ K ⁡ X
26 1 2 8 oplecon3b ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ oc ⁡ K ⁡ Y ≤ ˙ oc ⁡ K ⁡ X
27 6 11 7 26 syl3anc ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → X ≤ ˙ Y ↔ oc ⁡ K ⁡ Y ≤ ˙ oc ⁡ K ⁡ X
28 1 8 opcon3b ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B → X = Y ↔ oc ⁡ K ⁡ Y = oc ⁡ K ⁡ X
29 6 11 7 28 syl3anc ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → X = Y ↔ oc ⁡ K ⁡ Y = oc ⁡ K ⁡ X
30 25 27 29 3bitr4d ⊢ K ∈ OP ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z ∧ Y C Z → X ≤ ˙ Y ↔ X = Y