Metamath Proof Explorer

Theorem 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=BaseK
cvrcmp.l ⊢≤˙=≤K
cvrcmp.c ⊢C=⋖K
Assertion cvrcmp ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→X≤˙Y↔X=Y

Proof

Step Hyp Ref Expression
1 cvrcmp.b ⊢B=BaseK
2 cvrcmp.l ⊢≤˙=≤K
3 cvrcmp.c ⊢C=⋖K
4 simpl1 ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→K∈Poset
5 simpl23 ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Z∈B
6 simpl21 ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→X∈B
7 simpl3l ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→ZCX
8 1 3 cvrne ⊢K∈Poset∧Z∈B∧X∈B∧ZCX→Z≠X
9 4 5 6 7 8 syl31anc ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Z≠X
10 1 2 3 cvrle ⊢K∈Poset∧Z∈B∧X∈B∧ZCX→Z≤˙X
11 4 5 6 7 10 syl31anc ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Z≤˙X
12 simpr ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→X≤˙Y
13 simpl22 ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Y∈B
14 simpl3r ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→ZCY
15 1 2 3 cvrnbtwn4 ⊢K∈Poset∧Z∈B∧Y∈B∧X∈B∧ZCY→Z≤˙X∧X≤˙Y↔Z=X∨X=Y
16 4 5 13 6 14 15 syl131anc ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Z≤˙X∧X≤˙Y↔Z=X∨X=Y
17 11 12 16 mpbi2and ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Z=X∨X=Y
18 neor ⊢Z=X∨X=Y↔Z≠X→X=Y
19 17 18 sylib ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→Z≠X→X=Y
20 9 19 mpd ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY∧X≤˙Y→X=Y
21 20 ex ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→X≤˙Y→X=Y
22 simp1 ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→K∈Poset
23 simp21 ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→X∈B
24 1 2 posref ⊢K∈Poset∧X∈B→X≤˙X
25 22 23 24 syl2anc ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→X≤˙X
26 breq2 ⊢X=Y→X≤˙X↔X≤˙Y
27 25 26 syl5ibcom ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→X=Y→X≤˙Y
28 21 27 impbid ⊢K∈Poset∧X∈B∧Y∈B∧Z∈B∧ZCX∧ZCY→X≤˙Y↔X=Y