Metamath Proof Explorer

Theorem rnco

Description: The range of the composition of two classes. (Contributed by NM, 12-Dec-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion rnco 
|- ran ( A o. B ) = ran ( A |` ran B )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 brco 
 |-  ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
4 3 exbii 
 |-  ( E. x x ( A o. B ) y <-> E. x E. z ( x B z /\ z A y ) )
5 excom 
 |-  ( E. x E. z ( x B z /\ z A y ) <-> E. z E. x ( x B z /\ z A y ) )
6 vex 
 |-  z e. _V
7 6 elrn 
 |-  ( z e. ran B <-> E. x x B z )
8 7 anbi1i 
 |-  ( ( z e. ran B /\ z A y ) <-> ( E. x x B z /\ z A y ) )
9 2 brresi 
 |-  ( z ( A |` ran B ) y <-> ( z e. ran B /\ z A y ) )
10 19.41v 
 |-  ( E. x ( x B z /\ z A y ) <-> ( E. x x B z /\ z A y ) )
11 8 9 10 3bitr4ri 
 |-  ( E. x ( x B z /\ z A y ) <-> z ( A |` ran B ) y )
12 11 exbii 
 |-  ( E. z E. x ( x B z /\ z A y ) <-> E. z z ( A |` ran B ) y )
13 4 5 12 3bitri 
 |-  ( E. x x ( A o. B ) y <-> E. z z ( A |` ran B ) y )
14 2 elrn 
 |-  ( y e. ran ( A o. B ) <-> E. x x ( A o. B ) y )
15 2 elrn 
 |-  ( y e. ran ( A |` ran B ) <-> E. z z ( A |` ran B ) y )
16 13 14 15 3bitr4i 
 |-  ( y e. ran ( A o. B ) <-> y e. ran ( A |` ran B ) )
17 16 eqriv 
 |-  ran ( A o. B ) = ran ( A |` ran B )