Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-glb Unicode version

Definition df-glb 14387
 Description: Define poset greatest lower bound. (Contributed by NM, 19-Jul-2012.)
Assertion
Ref Expression
df-glb
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-glb
StepHypRef Expression
1 cglb 14355 . 2
2 vp . . 3
3 cvv 2916 . . 3
4 vs . . . 4
52cv 1648 . . . . . 6
6 cbs 13424 . . . . . 6
75, 6cfv 5413 . . . . 5
87cpw 3759 . . . 4
9 vx . . . . . . . . 9
109cv 1648 . . . . . . . 8
11 vy . . . . . . . . 9
1211cv 1648 . . . . . . . 8
13 cple 13491 . . . . . . . . 9
145, 13cfv 5413 . . . . . . . 8
1510, 12, 14wbr 4172 . . . . . . 7
164cv 1648 . . . . . . 7
1715, 11, 16wral 2666 . . . . . 6
18 vz . . . . . . . . . . 11
1918cv 1648 . . . . . . . . . 10
2019, 12, 14wbr 4172 . . . . . . . . 9
2120, 11, 16wral 2666 . . . . . . . 8
2219, 10, 14wbr 4172 . . . . . . . 8
2321, 22wi 4 . . . . . . 7
2423, 18, 7wral 2666 . . . . . 6
2517, 24wa 359 . . . . 5
2625, 9, 7crio 6501 . . . 4
274, 8, 26cmpt 4226 . . 3
282, 3, 27cmpt 4226 . 2
291, 28wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  glbfval  14395
 Copyright terms: Public domain W3C validator