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

Definition df-lub 14386
 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 14354 . 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 vy . . . . . . . . 9
109cv 1648 . . . . . . . 8
11 vx . . . . . . . . 9
1211cv 1648 . . . . . . . 8
13 cple 13491 . . . . . . . . 9
145, 13cfv 5413 . . . . . . . 8
1510, 12, 14wbr 4172 . . . . . . 7
164cv 1648 . . . . . . 7
1715, 9, 16wral 2666 . . . . . 6
18 vz . . . . . . . . . . 11
1918cv 1648 . . . . . . . . . 10
2010, 19, 14wbr 4172 . . . . . . . . 9
2120, 9, 16wral 2666 . . . . . . . 8
2212, 19, 14wbr 4172 . . . . . . . 8
2321, 22wi 4 . . . . . . 7
2423, 18, 7wral 2666 . . . . . 6
2517, 24wa 359 . . . . 5
2625, 11, 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:  lubfval  14390
 Copyright terms: Public domain W3C validator