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

Definition df-lub 14431
 Description: Define poset least upper bound. If it doesn't exist, an undefined value not in the base set is returned. (Contributed by NM, 12-Sep-2011.)
Assertion
Ref Expression
df-lub
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-lub
StepHypRef Expression
1 club 14399 . 2
2 vp . . 3
3 cvv 2956 . . 3
4 vs . . . 4
52cv 1651 . . . . . 6
6 cbs 13469 . . . . . 6
75, 6cfv 5454 . . . . 5
87cpw 3799 . . . 4
9 vy . . . . . . . . 9
109cv 1651 . . . . . . . 8
11 vx . . . . . . . . 9
1211cv 1651 . . . . . . . 8
13 cple 13536 . . . . . . . . 9
145, 13cfv 5454 . . . . . . . 8
1510, 12, 14wbr 4212 . . . . . . 7
164cv 1651 . . . . . . 7
1715, 9, 16wral 2705 . . . . . 6
18 vz . . . . . . . . . . 11
1918cv 1651 . . . . . . . . . 10
2010, 19, 14wbr 4212 . . . . . . . . 9
2120, 9, 16wral 2705 . . . . . . . 8
2212, 19, 14wbr 4212 . . . . . . . 8
2321, 22wi 4 . . . . . . 7
2423, 18, 7wral 2705 . . . . . 6
2517, 24wa 359 . . . . 5
2625, 11, 7crio 6542 . . . 4
274, 8, 26cmpt 4266 . . 3
282, 3, 27cmpt 4266 . 2
291, 28wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  lubfval  14435
 Copyright terms: Public domain W3C validator