Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  posglbd Structured version   Unicode version

Theorem posglbd 14568
 Description: Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
Hypotheses
Ref Expression
posglbd.l
posglbd.b
posglbd.g
posglbd.k
posglbd.s
posglbd.t
posglbd.lb
posglbd.gt
Assertion
Ref Expression
posglbd
Distinct variable groups:   , ,   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem posglbd
StepHypRef Expression
1 eqid 2435 . . 3 ODual ODual
2 posglbd.l . . 3
31, 2oduleval 14550 . 2 ODual
4 posglbd.b . . 3
5 eqid 2435 . . . 4
61, 5odubas 14552 . . 3 ODual
74, 6syl6eq 2483 . 2 ODual
8 posglbd.g . . 3
9 posglbd.k . . . 4
10 eqid 2435 . . . . 5
111, 10odulub 14560 . . . 4 ODual
129, 11syl 16 . . 3 ODual
138, 12eqtrd 2467 . 2 ODual
141odupos 14554 . . 3 ODual
159, 14syl 16 . 2 ODual
16 posglbd.s . 2
17 posglbd.t . 2
18 posglbd.lb . . 3
19 vex 2951 . . . . 5
20 brcnvg 5045 . . . . 5
2119, 17, 20sylancr 645 . . . 4