Definition df-ps 18199

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 18197	. 2 class PosetRel
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1538	. . . . 5 class 𝑟
4	3	wrel 5585	. . . 4 wff Rel 𝑟
5	3, 3	ccom 5584	. . . . 5 class (𝑟 ∘ 𝑟)
6	5, 3	wss 3883	. . . 4 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
7	3	ccnv 5579	. . . . . 6 class ◡𝑟
8	3, 7	cin 3882	. . . . 5 class (𝑟 ∩ ◡𝑟)
9		cid 5479	. . . . . 6 class I
10	3	cuni 4836	. . . . . . 7 class ∪ 𝑟
11	10	cuni 4836	. . . . . 6 class ∪ ∪ 𝑟
12	9, 11	cres 5582	. . . . 5 class ( I ↾ ∪ ∪ 𝑟)
13	8, 12	wceq 1539	. . . 4 wff (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟)
14	4, 6, 13	w3a 1085	. . 3 wff (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))
15	14, 2	cab 2715	. 2 class {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}
16	1, 15	wceq 1539	1 wff PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}

This definition is referenced by:  isps  18201