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

Definition df-plt 14094
Description: Define less-than ordering for posets and related structures. Unlike df-base 13155 and df-ple 13230, this is a derived component extractor and not an extensible structure component extractor that defines the poset. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
Assertion
Ref Expression
df-plt  |-  lt  =  ( p  e.  _V  |->  ( ( le `  p )  \  _I  ) )

Detailed syntax breakdown of Definition df-plt
StepHypRef Expression
1 cplt 14077 . 2  class  lt
2 vp . . 3  set  p
3 cvv 2790 . . 3  class  _V
42cv 1624 . . . . 5  class  p
5 cple 13217 . . . . 5  class  le
64, 5cfv 5257 . . . 4  class  ( le
`  p )
7 cid 4306 . . . 4  class  _I
86, 7cdif 3151 . . 3  class  ( ( le `  p ) 
\  _I  )
92, 3, 8cmpt 4079 . 2  class  ( p  e.  _V  |->  ( ( le `  p ) 
\  _I  ) )
101, 9wceq 1625 1  wff  lt  =  ( p  e.  _V  |->  ( ( le `  p )  \  _I  ) )
Colors of variables: wff set class
This definition is referenced by:  pltfval  14095
  Copyright terms: Public domain W3C validator