Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sup Unicode version

Definition df-sup 6456
 Description: Define the supremum of class . It is meaningful when is a relation that strictly orders and when the supremum exists. (Contributed by NM, 22-May-1999.)
Assertion
Ref Expression
df-sup
Distinct variable groups:   ,,,   ,,,   ,,,

Detailed syntax breakdown of Definition df-sup
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
41, 2, 3csup 6454 . 2
5 vx . . . . . . . . 9
65cv 1284 . . . . . . . 8
7 vy . . . . . . . . 9
87cv 1284 . . . . . . . 8
96, 8, 3wbr 3793 . . . . . . 7
109wn 3 . . . . . 6
1110, 7, 1wral 2349 . . . . 5
128, 6, 3wbr 3793 . . . . . . 7
13 vz . . . . . . . . . 10
1413cv 1284 . . . . . . . . 9
158, 14, 3wbr 3793 . . . . . . . 8
1615, 13, 1wrex 2350 . . . . . . 7
1712, 16wi 4 . . . . . 6
1817, 7, 2wral 2349 . . . . 5
1911, 18wa 102 . . . 4
2019, 5, 2crab 2353 . . 3
2120cuni 3609 . 2
224, 21wceq 1285 1
 Colors of variables: wff set class This definition is referenced by:  supeq1  6458  supeq2  6461  supeq3  6462  supeq123d  6463  nfsup  6464  supval2ti  6467  sup00  6475  dfinfre  8101
 Copyright terms: Public domain W3C validator