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

Metamath Proof Explorer

Theorem rncoOLD

Description: Obsolete version of rnco as of 24-Jan-2026. (Contributed by NM, 12-Dec-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rncoOLD 
|- 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 )