Metamath Proof Explorer

Theorem isps

Description: The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008)

Ref Expression
Assertion isps 
|- ( R e. A -> ( R e. PosetRel <-> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) ) )

Proof

Step Hyp Ref Expression
1 releq 
 |-  ( r = R -> ( Rel r <-> Rel R ) )
2 coeq1 
 |-  ( r = R -> ( r o. r ) = ( R o. r ) )
3 coeq2 
 |-  ( r = R -> ( R o. r ) = ( R o. R ) )
4 2 3 eqtrd 
 |-  ( r = R -> ( r o. r ) = ( R o. R ) )
5 id 
 |-  ( r = R -> r = R )
6 4 5 sseq12d 
 |-  ( r = R -> ( ( r o. r ) C_ r <-> ( R o. R ) C_ R ) )
7 cnveq 
 |-  ( r = R -> `' r = `' R )
8 5 7 ineq12d 
 |-  ( r = R -> ( r i^i `' r ) = ( R i^i `' R ) )
9 unieq 
 |-  ( r = R -> U. r = U. R )
10 9 unieqd 
 |-  ( r = R -> U. U. r = U. U. R )
11 10 reseq2d 
 |-  ( r = R -> ( _I |` U. U. r ) = ( _I |` U. U. R ) )
12 8 11 eqeq12d 
 |-  ( r = R -> ( ( r i^i `' r ) = ( _I |` U. U. r ) <-> ( R i^i `' R ) = ( _I |` U. U. R ) ) )
13 1 6 12 3anbi123d 
 |-  ( r = R -> ( ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) <-> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) ) )
14 df-ps 
 |-  PosetRel = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }
15 13 14 elab2g 
 |-  ( R e. A -> ( R e. PosetRel <-> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) ) )