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 \in V ⟼ \leq_{p} ∖ I)$

Detailed syntax breakdown

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