This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )