Definition df-ple

Description: Define "less than or equal to" ordering extractor for posets and related structures. We use ; 1 0 for the index to avoid conflict with 1 through 9 used for other purposes. (Contributed by NM, 4-Sep-2011) (Revised by Mario Carneiro, 14-Aug-2015) (Revised by AV, 9-Sep-2021)

	Ref	Expression
Assertion	df-ple	|- le = Slot ; 1 0

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cple	|- le
1		c1	|- 1
2		cc0	|- 0
3	1 2	cdc	|- ; 1 0
4	3	cslot	|- Slot ; 1 0
5	0 4	wceq	|- le = Slot ; 1 0