New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-partial		Unicode version

---

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

---

Detailed syntax breakdown of Definition df-partial

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

Colors of variables: wff setvar class

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

Copyright terms: Public domain

W3C validator