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 = ( 𝑝 ∈ V ↦ ( ( le ‘ 𝑝 ) ∖ I ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplt	⊢ lt
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		cple	⊢ le
4	1	cv	⊢ 𝑝
5	4 3	cfv	⊢ ( le ‘ 𝑝 )
6		cid	⊢ I
7	5 6	cdif	⊢ ( ( le ‘ 𝑝 ) ∖ I )
8	1 2 7	cmpt	⊢ ( 𝑝 ∈ V ↦ ( ( le ‘ 𝑝 ) ∖ I ) )
9	0 8	wceq	⊢ lt = ( 𝑝 ∈ V ↦ ( ( le ‘ 𝑝 ) ∖ I ) )