Metamath Proof Explorer

Theorem cnvtsr

Description: The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion cnvtsr 
|- ( R e. TosetRel -> `' R e. TosetRel )

Proof

Step Hyp Ref Expression
1 tsrps 
 |-  ( R e. TosetRel -> R e. PosetRel )
2 cnvps 
 |-  ( R e. PosetRel -> `' R e. PosetRel )
3 1 2 syl 
 |-  ( R e. TosetRel -> `' R e. PosetRel )
4 eqid 
 |-  dom R = dom R
5 4 istsr 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ ( dom R X. dom R ) C_ ( R u. `' R ) ) )
6 5 simprbi 
 |-  ( R e. TosetRel -> ( dom R X. dom R ) C_ ( R u. `' R ) )
7 4 psrn 
 |-  ( R e. PosetRel -> dom R = ran R )
8 1 7 syl 
 |-  ( R e. TosetRel -> dom R = ran R )
9 8 sqxpeqd 
 |-  ( R e. TosetRel -> ( dom R X. dom R ) = ( ran R X. ran R ) )
10 psrel 
 |-  ( R e. PosetRel -> Rel R )
11 1 10 syl 
 |-  ( R e. TosetRel -> Rel R )
12 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
13 11 12 sylib 
 |-  ( R e. TosetRel -> `' `' R = R )
14 13 uneq2d 
 |-  ( R e. TosetRel -> ( `' R u. `' `' R ) = ( `' R u. R ) )
15 uncom 
 |-  ( `' R u. R ) = ( R u. `' R )
16 14 15 eqtr2di 
 |-  ( R e. TosetRel -> ( R u. `' R ) = ( `' R u. `' `' R ) )
17 6 9 16 3sstr3d 
 |-  ( R e. TosetRel -> ( ran R X. ran R ) C_ ( `' R u. `' `' R ) )
18 df-rn 
 |-  ran R = dom `' R
19 18 istsr 
 |-  ( `' R e. TosetRel <-> ( `' R e. PosetRel /\ ( ran R X. ran R ) C_ ( `' R u. `' `' R ) ) )
20 3 17 19 sylanbrc 
 |-  ( R e. TosetRel -> `' R e. TosetRel )