Definition df-ps 17668

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 17666	. 2 class PosetRel
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1506	. . . . 5 class 𝑟
4	3	wrel 5412	. . . 4 wff Rel 𝑟
5	3, 3	ccom 5411	. . . . 5 class (𝑟 ∘ 𝑟)
6	5, 3	wss 3830	. . . 4 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
7	3	ccnv 5406	. . . . . 6 class ◡𝑟
8	3, 7	cin 3829	. . . . 5 class (𝑟 ∩ ◡𝑟)
9		cid 5311	. . . . . 6 class I
10	3	cuni 4712	. . . . . . 7 class ∪ 𝑟
11	10	cuni 4712	. . . . . 6 class ∪ ∪ 𝑟
12	9, 11	cres 5409	. . . . 5 class ( I ↾ ∪ ∪ 𝑟)
13	8, 12	wceq 1507	. . . 4 wff (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟)
14	4, 6, 13	w3a 1068	. . 3 wff (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))
15	14, 2	cab 2759	. 2 class {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}
16	1, 15	wceq 1507	1 wff PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}

This definition is referenced by:  isps  17670