Metamath Proof Explorer

Theorem cores

Description: Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion cores 
|- ( ran B C_ C -> ( ( A |` C ) o. B ) = ( A o. B ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  z e. _V
2 vex 
 |-  y e. _V
3 1 2 brelrn 
 |-  ( z B y -> y e. ran B )
4 ssel 
 |-  ( ran B C_ C -> ( y e. ran B -> y e. C ) )
5 vex 
 |-  x e. _V
6 5 brresi 
 |-  ( y ( A |` C ) x <-> ( y e. C /\ y A x ) )
7 6 baib 
 |-  ( y e. C -> ( y ( A |` C ) x <-> y A x ) )
8 3 4 7 syl56 
 |-  ( ran B C_ C -> ( z B y -> ( y ( A |` C ) x <-> y A x ) ) )
9 8 pm5.32d 
 |-  ( ran B C_ C -> ( ( z B y /\ y ( A |` C ) x ) <-> ( z B y /\ y A x ) ) )
10 9 exbidv 
 |-  ( ran B C_ C -> ( E. y ( z B y /\ y ( A |` C ) x ) <-> E. y ( z B y /\ y A x ) ) )
11 10 opabbidv 
 |-  ( ran B C_ C -> { <. z , x >. | E. y ( z B y /\ y ( A |` C ) x ) } = { <. z , x >. | E. y ( z B y /\ y A x ) } )
12 df-co 
 |-  ( ( A |` C ) o. B ) = { <. z , x >. | E. y ( z B y /\ y ( A |` C ) x ) }
13 df-co 
 |-  ( A o. B ) = { <. z , x >. | E. y ( z B y /\ y A x ) }
14 11 12 13 3eqtr4g 
 |-  ( ran B C_ C -> ( ( A |` C ) o. B ) = ( A o. B ) )