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

Metamath Proof Explorer

Theorem xpco

Description: Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion xpco 
|- ( B =/= (/) -> ( ( B X. C ) o. ( A X. B ) ) = ( A X. C ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
2 1 biimpi 
 |-  ( B =/= (/) -> E. y y e. B )
3 2 biantrurd 
 |-  ( B =/= (/) -> ( ( x e. A /\ z e. C ) <-> ( E. y y e. B /\ ( x e. A /\ z e. C ) ) ) )
4 ancom 
 |-  ( ( x e. A /\ y e. B ) <-> ( y e. B /\ x e. A ) )
5 4 anbi1i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( y e. B /\ z e. C ) ) <-> ( ( y e. B /\ x e. A ) /\ ( y e. B /\ z e. C ) ) )
6 brxp 
 |-  ( x ( A X. B ) y <-> ( x e. A /\ y e. B ) )
7 brxp 
 |-  ( y ( B X. C ) z <-> ( y e. B /\ z e. C ) )
8 6 7 anbi12i 
 |-  ( ( x ( A X. B ) y /\ y ( B X. C ) z ) <-> ( ( x e. A /\ y e. B ) /\ ( y e. B /\ z e. C ) ) )
9 anandi 
 |-  ( ( y e. B /\ ( x e. A /\ z e. C ) ) <-> ( ( y e. B /\ x e. A ) /\ ( y e. B /\ z e. C ) ) )
10 5 8 9 3bitr4i 
 |-  ( ( x ( A X. B ) y /\ y ( B X. C ) z ) <-> ( y e. B /\ ( x e. A /\ z e. C ) ) )
11 10 exbii 
 |-  ( E. y ( x ( A X. B ) y /\ y ( B X. C ) z ) <-> E. y ( y e. B /\ ( x e. A /\ z e. C ) ) )
12 19.41v 
 |-  ( E. y ( y e. B /\ ( x e. A /\ z e. C ) ) <-> ( E. y y e. B /\ ( x e. A /\ z e. C ) ) )
13 11 12 bitr2i 
 |-  ( ( E. y y e. B /\ ( x e. A /\ z e. C ) ) <-> E. y ( x ( A X. B ) y /\ y ( B X. C ) z ) )
14 3 13 bitr2di 
 |-  ( B =/= (/) -> ( E. y ( x ( A X. B ) y /\ y ( B X. C ) z ) <-> ( x e. A /\ z e. C ) ) )
15 14 opabbidv 
 |-  ( B =/= (/) -> { <. x , z >. | E. y ( x ( A X. B ) y /\ y ( B X. C ) z ) } = { <. x , z >. | ( x e. A /\ z e. C ) } )
16 df-co 
 |-  ( ( B X. C ) o. ( A X. B ) ) = { <. x , z >. | E. y ( x ( A X. B ) y /\ y ( B X. C ) z ) }
17 df-xp 
 |-  ( A X. C ) = { <. x , z >. | ( x e. A /\ z e. C ) }
18 15 16 17 3eqtr4g 
 |-  ( B =/= (/) -> ( ( B X. C ) o. ( A X. B ) ) = ( A X. C ) )