Definition df-ps 17200

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 = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }

Detailed syntax breakdown of Definition df-ps

Step	Hyp	Ref	Expression
1		cps 17198	. 2 class PosetRel
2		vr	. . . . . 6 setvar r
3	2	cv 1482	. . . . 5 class r
4	3	wrel 5119	. . . 4 wff Rel r
5	3, 3	ccom 5118	. . . . 5 class ( r o. r )
6	5, 3	wss 3574	. . . 4 wff ( r o. r ) C_ r
7	3	ccnv 5113	. . . . . 6 class `' r
8	3, 7	cin 3573	. . . . 5 class ( r i^i `' r )
9		cid 5023	. . . . . 6 class _I
10	3	cuni 4436	. . . . . . 7 class U. r
11	10	cuni 4436	. . . . . 6 class U. U. r
12	9, 11	cres 5116	. . . . 5 class ( _I |` U. U. r )
13	8, 12	wceq 1483	. . . 4 wff ( r i^i `' r ) = ( _I |` U. U. r )
14	4, 6, 13	w3a 1037	. . 3 wff ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) )
15	14, 2	cab 2608	. 2 class { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }
16	1, 15	wceq 1483	1 wff PosetRel = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }

This definition is referenced by:  isps  17202