This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) }