Definition df-ps 17812

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

Step	Hyp	Ref	Expression
1		cps 17810	. 2 class PosetRel
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1536	. . . . 5 class 𝑟
4	3	wrel 5562	. . . 4 wff Rel 𝑟
5	3, 3	ccom 5561	. . . . 5 class (𝑟 ∘ 𝑟)
6	5, 3	wss 3938	. . . 4 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
7	3	ccnv 5556	. . . . . 6 class ◡𝑟
8	3, 7	cin 3937	. . . . 5 class (𝑟 ∩ ◡𝑟)
9		cid 5461	. . . . . 6 class I
10	3	cuni 4840	. . . . . . 7 class ∪ 𝑟
11	10	cuni 4840	. . . . . 6 class ∪ ∪ 𝑟
12	9, 11	cres 5559	. . . . 5 class ( I ↾ ∪ ∪ 𝑟)
13	8, 12	wceq 1537	. . . 4 wff (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟)
14	4, 6, 13	w3a 1083	. . 3 wff (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))
15	14, 2	cab 2801	. 2 class {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}
16	1, 15	wceq 1537	1 wff PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}

This definition is referenced by:  isps  17814