Definition df-ps

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)

	Ref	Expression
Assertion	df-ps	|- PosetRel = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cps	|- PosetRel
1		vr	|- r
2	1	cv	|- r
3	2	wrel	|- Rel r
4	2 2	ccom	|- ( r o. r )
5	4 2	wss	|- ( r o. r ) C_ r
6	2	ccnv	|- `' r
7	2 6	cin	|- ( r i^i `' r )
8		cid	|- _I
9	2	cuni	|- U. r
10	9	cuni	|- U. U. r
11	8 10	cres	|- ( _I |` U. U. r )
12	7 11	wceq	|- ( r i^i `' r ) = ( _I |` U. U. r )
13	3 5 12	w3a	|- ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) )
14	13 1	cab	|- { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }
15	0 14	wceq	|- PosetRel = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }