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