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	$$⊢\mathrm{lt}=\left(p\in \mathrm{V}⟼{\le }_p\setminus \mathrm{I}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplt	$$class\mathrm{lt}$$
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3		cple	$$class\mathrm{le}$$
4	1	cv	$$setvarp$$
5	4 3	cfv	$$class{\le }_p$$
6		cid	$$class\mathrm{I}$$
7	5 6	cdif	$$class\left({\le }_p\setminus \mathrm{I}\right)$$
8	1 2 7	cmpt	$$class\left(p\in \mathrm{V}⟼{\le }_p\setminus \mathrm{I}\right)$$
9	0 8	wceq	$$wff\mathrm{lt}=\left(p\in \mathrm{V}⟼{\le }_p\setminus \mathrm{I}\right)$$