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

Definition df-glb 14437
 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 14405 . 2
2 vp . . 3
3 cvv 2958 . . 3
4 vs . . . 4
52cv 1652 . . . . . 6
6 cbs 13474 . . . . . 6
75, 6cfv 5457 . . . . 5
87cpw 3801 . . . 4
9 vx . . . . . . . . 9
109cv 1652 . . . . . . . 8
11 vy . . . . . . . . 9
1211cv 1652 . . . . . . . 8
13 cple 13541 . . . . . . . . 9
145, 13cfv 5457 . . . . . . . 8
1510, 12, 14wbr 4215 . . . . . . 7
164cv 1652 . . . . . . 7
1715, 11, 16wral 2707 . . . . . 6
18 vz . . . . . . . . . . 11
1918cv 1652 . . . . . . . . . 10
2019, 12, 14wbr 4215 . . . . . . . . 9
2120, 11, 16wral 2707 . . . . . . . 8
2219, 10, 14wbr 4215 . . . . . . . 8
2321, 22wi 4 . . . . . . 7
2423, 18, 7wral 2707 . . . . . 6
2517, 24wa 360 . . . . 5
2625, 9, 7crio 6545 . . . 4
274, 8, 26cmpt 4269 . . 3
282, 3, 27cmpt 4269 . 2
291, 28wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  glbfval  14445
 Copyright terms: Public domain W3C validator