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	$$⊢\mathrm{le}=\mathrm{Slot}10$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cple	$$class\mathrm{le}$$
1		c1	$$class1$$
2		cc0	$$class0$$
3	1 2	cdc	$$class10$$
4	3	cslot	$$class\mathrm{Slot}10$$
5	0 4	wceq	$$wff\mathrm{le}=\mathrm{Slot}10$$