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

Metamath Proof Explorer

Theorem rncoeq

Description: Range of a composition. (Contributed by NM, 19-Mar-1998)

Ref Expression
Assertion rncoeq 
|- ( dom A = ran B -> ran ( A o. B ) = ran A )

Proof

Step Hyp Ref Expression
1 dmcoeq 
 |-  ( dom `' B = ran `' A -> dom ( `' B o. `' A ) = dom `' A )
2 eqcom 
 |-  ( dom A = ran B <-> ran B = dom A )
3 df-rn 
 |-  ran B = dom `' B
4 dfdm4 
 |-  dom A = ran `' A
5 3 4 eqeq12i 
 |-  ( ran B = dom A <-> dom `' B = ran `' A )
6 2 5 bitri 
 |-  ( dom A = ran B <-> dom `' B = ran `' A )
7 df-rn 
 |-  ran ( A o. B ) = dom `' ( A o. B )
8 cnvco 
 |-  `' ( A o. B ) = ( `' B o. `' A )
9 8 dmeqi 
 |-  dom `' ( A o. B ) = dom ( `' B o. `' A )
10 7 9 eqtri 
 |-  ran ( A o. B ) = dom ( `' B o. `' A )
11 df-rn 
 |-  ran A = dom `' A
12 10 11 eqeq12i 
 |-  ( ran ( A o. B ) = ran A <-> dom ( `' B o. `' A ) = dom `' A )
13 1 6 12 3imtr4i 
 |-  ( dom A = ran B -> ran ( A o. B ) = ran A )