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=BaseK
cvrcmp.l ⊢≤˙=≤K
cvrcmp.c ⊢C=⋖K
Assertion cvrcmp2 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→X≤˙Y↔X=Y

Proof

Step Hyp Ref Expression
1 cvrcmp.b ⊢B=BaseK
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∧XCZ∧YCZ→K∈Poset
6 simp1 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→K∈OP
7 simp22 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→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∧XCZ∧YCZ→oc⁡K⁡Y∈B
11 simp21 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→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∧XCZ∧YCZ→oc⁡K⁡X∈B
14 simp23 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→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∧XCZ∧YCZ→oc⁡K⁡Z∈B
17 1 8 3 cvrcon3b ⊢K∈OP∧X∈B∧Z∈B→XCZ↔oc⁡K⁡ZCoc⁡K⁡X
18 17 3adant3r2 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B→XCZ↔oc⁡K⁡ZCoc⁡K⁡X
19 1 8 3 cvrcon3b ⊢K∈OP∧Y∈B∧Z∈B→YCZ↔oc⁡K⁡ZCoc⁡K⁡Y
20 19 3adant3r1 ⊢K∈OP∧X∈B∧Y∈B∧Z∈B→YCZ↔oc⁡K⁡ZCoc⁡K⁡Y
21 18 20 anbi12d ⊢K∈OP∧X∈B∧Y∈B∧Z∈B→XCZ∧YCZ↔oc⁡K⁡ZCoc⁡K⁡X∧oc⁡K⁡ZCoc⁡K⁡Y
22 21 biimp3a ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→oc⁡K⁡ZCoc⁡K⁡X∧oc⁡K⁡ZCoc⁡K⁡Y
23 22 ancomd ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→oc⁡K⁡ZCoc⁡K⁡Y∧oc⁡K⁡ZCoc⁡K⁡X
24 1 2 3 cvrcmp ⊢K∈Poset∧oc⁡K⁡Y∈B∧oc⁡K⁡X∈B∧oc⁡K⁡Z∈B∧oc⁡K⁡ZCoc⁡K⁡Y∧oc⁡K⁡ZCoc⁡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∧XCZ∧YCZ→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∧XCZ∧YCZ→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∧XCZ∧YCZ→X=Y↔oc⁡K⁡Y=oc⁡K⁡X
30 25 27 29 3bitr4d ⊢K∈OP∧X∈B∧Y∈B∧Z∈B∧XCZ∧YCZ→X≤˙Y↔X=Y