Metamath Proof Explorer

Theorem xpco2

Description: Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Assertion xpco2 
|- ( F : A --> B -> ( ( B X. C ) o. F ) = ( A X. C ) )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( ( B X. C ) o. F )
2 relxp 
 |-  Rel ( A X. C )
3 vex 
 |-  x e. _V
4 vex 
 |-  z e. _V
5 3 4 breldm 
 |-  ( x F z -> x e. dom F )
6 5 ad2antrl 
 |-  ( ( F : A --> B /\ ( x F z /\ z ( B X. C ) y ) ) -> x e. dom F )
7 fdm 
 |-  ( F : A --> B -> dom F = A )
8 7 adantr 
 |-  ( ( F : A --> B /\ ( x F z /\ z ( B X. C ) y ) ) -> dom F = A )
9 6 8 eleqtrd 
 |-  ( ( F : A --> B /\ ( x F z /\ z ( B X. C ) y ) ) -> x e. A )
10 brxp 
 |-  ( z ( B X. C ) y <-> ( z e. B /\ y e. C ) )
11 10 simprbi 
 |-  ( z ( B X. C ) y -> y e. C )
12 11 ad2antll 
 |-  ( ( F : A --> B /\ ( x F z /\ z ( B X. C ) y ) ) -> y e. C )
13 9 12 jca 
 |-  ( ( F : A --> B /\ ( x F z /\ z ( B X. C ) y ) ) -> ( x e. A /\ y e. C ) )
14 13 ex 
 |-  ( F : A --> B -> ( ( x F z /\ z ( B X. C ) y ) -> ( x e. A /\ y e. C ) ) )
15 14 exlimdv 
 |-  ( F : A --> B -> ( E. z ( x F z /\ z ( B X. C ) y ) -> ( x e. A /\ y e. C ) ) )
16 15 imp 
 |-  ( ( F : A --> B /\ E. z ( x F z /\ z ( B X. C ) y ) ) -> ( x e. A /\ y e. C ) )
17 ffvelcdm 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
18 17 adantrr 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. C ) ) -> ( F ` x ) e. B )
19 ffvbr 
 |-  ( ( F : A --> B /\ x e. A ) -> x F ( F ` x ) )
20 19 adantrr 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. C ) ) -> x F ( F ` x ) )
21 simprr 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. C ) ) -> y e. C )
22 brxp 
 |-  ( ( F ` x ) ( B X. C ) y <-> ( ( F ` x ) e. B /\ y e. C ) )
23 18 21 22 sylanbrc 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. C ) ) -> ( F ` x ) ( B X. C ) y )
24 20 23 jca 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. C ) ) -> ( x F ( F ` x ) /\ ( F ` x ) ( B X. C ) y ) )
25 breq2 
 |-  ( z = ( F ` x ) -> ( x F z <-> x F ( F ` x ) ) )
26 breq1 
 |-  ( z = ( F ` x ) -> ( z ( B X. C ) y <-> ( F ` x ) ( B X. C ) y ) )
27 25 26 anbi12d 
 |-  ( z = ( F ` x ) -> ( ( x F z /\ z ( B X. C ) y ) <-> ( x F ( F ` x ) /\ ( F ` x ) ( B X. C ) y ) ) )
28 18 24 27 spcedv 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. C ) ) -> E. z ( x F z /\ z ( B X. C ) y ) )
29 16 28 impbida 
 |-  ( F : A --> B -> ( E. z ( x F z /\ z ( B X. C ) y ) <-> ( x e. A /\ y e. C ) ) )
30 vex 
 |-  y e. _V
31 3 30 brco 
 |-  ( x ( ( B X. C ) o. F ) y <-> E. z ( x F z /\ z ( B X. C ) y ) )
32 brxp 
 |-  ( x ( A X. C ) y <-> ( x e. A /\ y e. C ) )
33 29 31 32 3bitr4g 
 |-  ( F : A --> B -> ( x ( ( B X. C ) o. F ) y <-> x ( A X. C ) y ) )
34 1 2 33 eqbrrdiv 
 |-  ( F : A --> B -> ( ( B X. C ) o. F ) = ( A X. C ) )