Metamath Proof Explorer

Theorem dmcoss3

Description: The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019)

Ref Expression
Assertion dmcoss3 
|- dom ,~ R = dom `' R

Proof

Step Hyp Ref Expression
1 dfcoss3 
 |-  ,~ R = ( R o. `' R )
2 1 dmeqi 
 |-  dom ,~ R = dom ( R o. `' R )
3 rncnv 
 |-  ran `' R = dom R
4 3 eqimssi 
 |-  ran `' R C_ dom R
5 dmcosseq 
 |-  ( ran `' R C_ dom R -> dom ( R o. `' R ) = dom `' R )
6 4 5 ax-mp 
 |-  dom ( R o. `' R ) = dom `' R
7 2 6 eqtri 
 |-  dom ,~ R = dom `' R