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

Definition df-ps 18591
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 PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟𝑟) ⊆ 𝑟 ∧ (𝑟𝑟) = ( I ↾ 𝑟))}

Detailed syntax breakdown of Definition df-ps
StepHypRef Expression
1 cps 18589 . 2 class PosetRel
2 vr . . . . . 6 setvar 𝑟
32cv 1533 . . . . 5 class 𝑟
43wrel 5687 . . . 4 wff Rel 𝑟
53, 3ccom 5686 . . . . 5 class (𝑟𝑟)
65, 3wss 3947 . . . 4 wff (𝑟𝑟) ⊆ 𝑟
73ccnv 5681 . . . . . 6 class 𝑟
83, 7cin 3946 . . . . 5 class (𝑟𝑟)
9 cid 5579 . . . . . 6 class I
103cuni 4913 . . . . . . 7 class 𝑟
1110cuni 4913 . . . . . 6 class 𝑟
129, 11cres 5684 . . . . 5 class ( I ↾ 𝑟)
138, 12wceq 1534 . . . 4 wff (𝑟𝑟) = ( I ↾ 𝑟)
144, 6, 13w3a 1084 . . 3 wff (Rel 𝑟 ∧ (𝑟𝑟) ⊆ 𝑟 ∧ (𝑟𝑟) = ( I ↾ 𝑟))
1514, 2cab 2703 . 2 class {𝑟 ∣ (Rel 𝑟 ∧ (𝑟𝑟) ⊆ 𝑟 ∧ (𝑟𝑟) = ( I ↾ 𝑟))}
161, 15wceq 1534 1 wff PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟𝑟) ⊆ 𝑟 ∧ (𝑟𝑟) = ( I ↾ 𝑟))}
Colors of variables: wff setvar class
This definition is referenced by:  isps  18593
  Copyright terms: Public domain W3C validator