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) Avoid ax-11 . (Revised by TM, 24-Jan-2026)

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 breq1 
 |-  ( x = w -> ( x B z <-> w B z ) )
6 5 anbi1d 
 |-  ( x = w -> ( ( x B z /\ z A y ) <-> ( w B z /\ z A y ) ) )
7 breq2 
 |-  ( z = w -> ( x B z <-> x B w ) )
8 breq1 
 |-  ( z = w -> ( z A y <-> w A y ) )
9 7 8 anbi12d 
 |-  ( z = w -> ( ( x B z /\ z A y ) <-> ( x B w /\ w A y ) ) )
10 6 9 excomw 
 |-  ( E. x E. z ( x B z /\ z A y ) <-> E. z E. x ( x B z /\ z A y ) )
11 vex 
 |-  z e. _V
12 11 elrn 
 |-  ( z e. ran B <-> E. x x B z )
13 12 anbi1i 
 |-  ( ( z e. ran B /\ z A y ) <-> ( E. x x B z /\ z A y ) )
14 2 brresi 
 |-  ( z ( A |` ran B ) y <-> ( z e. ran B /\ z A y ) )
15 19.41v 
 |-  ( E. x ( x B z /\ z A y ) <-> ( E. x x B z /\ z A y ) )
16 13 14 15 3bitr4ri 
 |-  ( E. x ( x B z /\ z A y ) <-> z ( A |` ran B ) y )
17 16 exbii 
 |-  ( E. z E. x ( x B z /\ z A y ) <-> E. z z ( A |` ran B ) y )
18 4 10 17 3bitri 
 |-  ( E. x x ( A o. B ) y <-> E. z z ( A |` ran B ) y )
19 2 elrn 
 |-  ( y e. ran ( A o. B ) <-> E. x x ( A o. B ) y )
20 2 elrn 
 |-  ( y e. ran ( A |` ran B ) <-> E. z z ( A |` ran B ) y )
21 18 19 20 3bitr4i 
 |-  ( y e. ran ( A o. B ) <-> y e. ran ( A |` ran B ) )
22 21 eqriv 
 |-  ran ( A o. B ) = ran ( A |` ran B )