Definition df-partial 5902

Description: Define the set of all partial orderings over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-partial	|- Po = (( Ref i^i Trans ) i^i Antisym )

Detailed syntax breakdown of Definition df-partial

Step	Hyp	Ref	Expression
1		cpartial 5891	. 2 class Po
2		cref 5889	. . . 4 class Ref
3		ctrans 5888	. . . 4 class Trans
4	2, 3	cin 3208	. . 3 class ( Ref i^i Trans )
5		cantisym 5890	. . 3 class Antisym
6	4, 5	cin 3208	. 2 class (( Ref i^i Trans ) i^i Antisym )
7	1, 6	wceq 1642	1 wff Po = (( Ref i^i Trans ) i^i Antisym )

This definition is referenced by:  partialex  5917  porta  5933  nchoicelem8  6296