Definition df-plt

Description: Define less-than ordering for posets and related structures. Unlike df-base and df-ple , 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)

	Ref	Expression
Assertion	df-plt	|- lt = ( p e. _V |-> ( ( le ` p ) \ _I ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplt	|- lt
1		vp	|- p
2		cvv	|- _V
3		cple	|- le
4	1	cv	|- p
5	4 3	cfv	|- ( le ` p )
6		cid	|- _I
7	5 6	cdif	|- ( ( le ` p ) \ _I )
8	1 2 7	cmpt	|- ( p e. _V |-> ( ( le ` p ) \ _I ) )
9	0 8	wceq	|- lt = ( p e. _V |-> ( ( le ` p ) \ _I ) )