Definition df-partial 5903

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 ∩ Trans ) ∩ Antisym )

Detailed syntax breakdown of Definition df-partial

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

This definition is referenced by:  partialex  5918  porta  5934  nchoicelem8  6297