Metamath Proof Explorer


Theorem clatglb

Description: Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypotheses clatglb.b B=BaseK
clatglb.l ˙=K
clatglb.g G=glbK
Assertion clatglb KCLatSBySGS˙yzBySz˙yz˙GS

Proof

Step Hyp Ref Expression
1 clatglb.b B=BaseK
2 clatglb.l ˙=K
3 clatglb.g G=glbK
4 simpl KCLatSBKCLat
5 1 3 clatglbcl2 KCLatSBSdomG
6 1 2 3 4 5 glbprop KCLatSBySGS˙yzBySz˙yz˙GS