Metamath Proof Explorer

Theorem resco

Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006)

Ref Expression
Assertion resco 
|- ( ( A o. B ) |` C ) = ( A o. ( B |` C ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( ( A o. B ) |` C )
2 relco 
 |-  Rel ( A o. ( B |` C ) )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 brco 
 |-  ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
6 5 anbi2i 
 |-  ( ( x e. C /\ x ( A o. B ) y ) <-> ( x e. C /\ E. z ( x B z /\ z A y ) ) )
7 19.42v 
 |-  ( E. z ( x e. C /\ ( x B z /\ z A y ) ) <-> ( x e. C /\ E. z ( x B z /\ z A y ) ) )
8 vex 
 |-  z e. _V
9 8 brresi 
 |-  ( x ( B |` C ) z <-> ( x e. C /\ x B z ) )
10 9 anbi1i 
 |-  ( ( x ( B |` C ) z /\ z A y ) <-> ( ( x e. C /\ x B z ) /\ z A y ) )
11 anass 
 |-  ( ( ( x e. C /\ x B z ) /\ z A y ) <-> ( x e. C /\ ( x B z /\ z A y ) ) )
12 10 11 bitr2i 
 |-  ( ( x e. C /\ ( x B z /\ z A y ) ) <-> ( x ( B |` C ) z /\ z A y ) )
13 12 exbii 
 |-  ( E. z ( x e. C /\ ( x B z /\ z A y ) ) <-> E. z ( x ( B |` C ) z /\ z A y ) )
14 6 7 13 3bitr2i 
 |-  ( ( x e. C /\ x ( A o. B ) y ) <-> E. z ( x ( B |` C ) z /\ z A y ) )
15 4 brresi 
 |-  ( x ( ( A o. B ) |` C ) y <-> ( x e. C /\ x ( A o. B ) y ) )
16 3 4 brco 
 |-  ( x ( A o. ( B |` C ) ) y <-> E. z ( x ( B |` C ) z /\ z A y ) )
17 14 15 16 3bitr4i 
 |-  ( x ( ( A o. B ) |` C ) y <-> x ( A o. ( B |` C ) ) y )
18 1 2 17 eqbrriv 
 |-  ( ( A o. B ) |` C ) = ( A o. ( B |` C ) )