Metamath Proof Explorer

Theorem coxp

Description: Composition with a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion coxp 
|- ( A o. ( B X. C ) ) = ( B X. ( A " C ) )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( A o. ( B X. C ) )
2 relxp 
 |-  Rel ( B X. ( A " C ) )
3 brxp 
 |-  ( x ( B X. C ) z <-> ( x e. B /\ z e. C ) )
4 3 anbi1i 
 |-  ( ( x ( B X. C ) z /\ z A y ) <-> ( ( x e. B /\ z e. C ) /\ z A y ) )
5 anass 
 |-  ( ( ( x e. B /\ z e. C ) /\ z A y ) <-> ( x e. B /\ ( z e. C /\ z A y ) ) )
6 4 5 bitri 
 |-  ( ( x ( B X. C ) z /\ z A y ) <-> ( x e. B /\ ( z e. C /\ z A y ) ) )
7 6 exbii 
 |-  ( E. z ( x ( B X. C ) z /\ z A y ) <-> E. z ( x e. B /\ ( z e. C /\ z A y ) ) )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 opelco 
 |-  ( <. x , y >. e. ( A o. ( B X. C ) ) <-> E. z ( x ( B X. C ) z /\ z A y ) )
11 9 elima2 
 |-  ( y e. ( A " C ) <-> E. z ( z e. C /\ z A y ) )
12 11 anbi2i 
 |-  ( ( x e. B /\ y e. ( A " C ) ) <-> ( x e. B /\ E. z ( z e. C /\ z A y ) ) )
13 opelxp 
 |-  ( <. x , y >. e. ( B X. ( A " C ) ) <-> ( x e. B /\ y e. ( A " C ) ) )
14 19.42v 
 |-  ( E. z ( x e. B /\ ( z e. C /\ z A y ) ) <-> ( x e. B /\ E. z ( z e. C /\ z A y ) ) )
15 12 13 14 3bitr4i 
 |-  ( <. x , y >. e. ( B X. ( A " C ) ) <-> E. z ( x e. B /\ ( z e. C /\ z A y ) ) )
16 7 10 15 3bitr4i 
 |-  ( <. x , y >. e. ( A o. ( B X. C ) ) <-> <. x , y >. e. ( B X. ( A " C ) ) )
17 1 2 16 eqrelriiv 
 |-  ( A o. ( B X. C ) ) = ( B X. ( A " C ) )