Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ps Unicode version

Definition df-ps 14322
 Description: Define the class of all posets (partially ordered sets) with weak ordering (e.g. "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.)
Assertion
Ref Expression
df-ps

Detailed syntax breakdown of Definition df-ps
StepHypRef Expression
1 cps 14317 . 2
2 vr . . . . . 6
32cv 1631 . . . . 5
43wrel 4710 . . . 4
53, 3ccom 4709 . . . . 5
65, 3wss 3165 . . . 4
73ccnv 4704 . . . . . 6
83, 7cin 3164 . . . . 5
9 cid 4320 . . . . . 6
103cuni 3843 . . . . . . 7
1110cuni 3843 . . . . . 6
129, 11cres 4707 . . . . 5
138, 12wceq 1632 . . . 4
144, 6, 13w3a 934 . . 3
1514, 2cab 2282 . 2
161, 15wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  isps  14327  posprsr  25343  dfps2  25392
 Copyright terms: Public domain W3C validator