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

Step	Hyp	Ref	Expression
1		cps 18589	. 2 class PosetRel
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1533	. . . . 5 class 𝑟
4	3	wrel 5687	. . . 4 wff Rel 𝑟
5	3, 3	ccom 5686	. . . . 5 class (𝑟 ∘ 𝑟)
6	5, 3	wss 3947	. . . 4 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
7	3	ccnv 5681	. . . . . 6 class ◡𝑟
8	3, 7	cin 3946	. . . . 5 class (𝑟 ∩ ◡𝑟)
9		cid 5579	. . . . . 6 class I
10	3	cuni 4913	. . . . . . 7 class ∪ 𝑟
11	10	cuni 4913	. . . . . 6 class ∪ ∪ 𝑟
12	9, 11	cres 5684	. . . . 5 class ( I ↾ ∪ ∪ 𝑟)
13	8, 12	wceq 1534	. . . 4 wff (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟)
14	4, 6, 13	w3a 1084	. . 3 wff (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))
15	14, 2	cab 2703	. 2 class {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}
16	1, 15	wceq 1534	1 wff PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}

This definition is referenced by:  isps  18593