Definition df-ps 17408

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 17406	. 2 class PosetRel
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1636	. . . . 5 class 𝑟
4	3	wrel 5323	. . . 4 wff Rel 𝑟
5	3, 3	ccom 5322	. . . . 5 class (𝑟 ∘ 𝑟)
6	5, 3	wss 3776	. . . 4 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
7	3	ccnv 5317	. . . . . 6 class ◡𝑟
8	3, 7	cin 3775	. . . . 5 class (𝑟 ∩ ◡𝑟)
9		cid 5225	. . . . . 6 class I
10	3	cuni 4637	. . . . . . 7 class ∪ 𝑟
11	10	cuni 4637	. . . . . 6 class ∪ ∪ 𝑟
12	9, 11	cres 5320	. . . . 5 class ( I ↾ ∪ ∪ 𝑟)
13	8, 12	wceq 1637	. . . 4 wff (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟)
14	4, 6, 13	w3a 1100	. . 3 wff (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))
15	14, 2	cab 2799	. 2 class {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}
16	1, 15	wceq 1637	1 wff PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}

This definition is referenced by:  isps  17410