Metamath Proof Explorer


Theorem posglbmo

Description: Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018)

Ref Expression
Hypotheses poslubmo.l ˙=K
poslubmo.b B=BaseK
Assertion posglbmo KPosetSB*xBySx˙yzBySz˙yz˙x

Proof

Step Hyp Ref Expression
1 poslubmo.l ˙=K
2 poslubmo.b B=BaseK
3 simprrl KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wySw˙y
4 breq1 z=wz˙yw˙y
5 4 ralbidv z=wySz˙yySw˙y
6 breq1 z=wz˙xw˙x
7 5 6 imbi12d z=wySz˙yz˙xySw˙yw˙x
8 simprlr KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wzBySz˙yz˙x
9 simplrr KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wwB
10 7 8 9 rspcdva KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wySw˙yw˙x
11 3 10 mpd KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙ww˙x
12 simprll KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wySx˙y
13 breq1 z=xz˙yx˙y
14 13 ralbidv z=xySz˙yySx˙y
15 breq1 z=xz˙wx˙w
16 14 15 imbi12d z=xySz˙yz˙wySx˙yx˙w
17 simprrr KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wzBySz˙yz˙w
18 simplrl KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wxB
19 16 17 18 rspcdva KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wySx˙yx˙w
20 12 19 mpd KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wx˙w
21 ancom w˙xx˙wx˙ww˙x
22 2 1 posasymb KPosetxBwBx˙ww˙xx=w
23 21 22 bitrid KPosetxBwBw˙xx˙wx=w
24 23 3expb KPosetxBwBw˙xx˙wx=w
25 24 ad4ant13 KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙ww˙xx˙wx=w
26 11 20 25 mpbi2and KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wx=w
27 26 ex KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wx=w
28 27 ralrimivva KPosetSBxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wx=w
29 breq1 x=wx˙yw˙y
30 29 ralbidv x=wySx˙yySw˙y
31 breq2 x=wz˙xz˙w
32 31 imbi2d x=wySz˙yz˙xySz˙yz˙w
33 32 ralbidv x=wzBySz˙yz˙xzBySz˙yz˙w
34 30 33 anbi12d x=wySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙w
35 34 rmo4 *xBySx˙yzBySz˙yz˙xxBwBySx˙yzBySz˙yz˙xySw˙yzBySz˙yz˙wx=w
36 28 35 sylibr KPosetSB*xBySx˙yzBySz˙yz˙x