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

Definition df-nfw 14325
Description: Define the class of all infima of a weak ordering relation. (Contributed by FL, 6-Sep-2009.)
Assertion
Ref Expression
df-nfw  |-  inf w  =  ( r  e. 
_V ,  x  e. 
_V  |->  ( `' r  sup w  x ) )
Distinct variable group:    x, r

Detailed syntax breakdown of Definition df-nfw
StepHypRef Expression
1 cinf 14320 . 2  class  inf w
2 vr . . 3  set  r
3 vx . . 3  set  x
4 cvv 2801 . . 3  class  _V
52cv 1631 . . . . 5  class  r
65ccnv 4704 . . . 4  class  `' r
73cv 1631 . . . 4  class  x
8 cspw 14319 . . . 4  class  sup w
96, 7, 8co 5874 . . 3  class  ( `' r  sup w  x
)
102, 3, 4, 4, 9cmpt2 5876 . 2  class  ( r  e.  _V ,  x  e.  _V  |->  ( `' r  sup w  x ) )
111, 10wceq 1632 1  wff  inf w  =  ( r  e. 
_V ,  x  e. 
_V  |->  ( `' r  sup w  x ) )
Colors of variables: wff set class
This definition is referenced by:  nfwval  25348
  Copyright terms: Public domain W3C validator