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

Metamath Proof Explorer

Theorem xpcogend

Description: The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019)

Ref Expression
Hypothesis xpcogend.1 
|- ( ph -> ( B i^i C ) =/= (/) )
Assertion xpcogend 
|- ( ph -> ( ( C X. D ) o. ( A X. B ) ) = ( A X. D ) )

Proof

Step Hyp Ref Expression
1 xpcogend.1 
 |-  ( ph -> ( B i^i C ) =/= (/) )
2 brxp 
 |-  ( x ( A X. B ) y <-> ( x e. A /\ y e. B ) )
3 brxp 
 |-  ( y ( C X. D ) z <-> ( y e. C /\ z e. D ) )
4 3 biancomi 
 |-  ( y ( C X. D ) z <-> ( z e. D /\ y e. C ) )
5 2 4 anbi12i 
 |-  ( ( x ( A X. B ) y /\ y ( C X. D ) z ) <-> ( ( x e. A /\ y e. B ) /\ ( z e. D /\ y e. C ) ) )
6 5 exbii 
 |-  ( E. y ( x ( A X. B ) y /\ y ( C X. D ) z ) <-> E. y ( ( x e. A /\ y e. B ) /\ ( z e. D /\ y e. C ) ) )
7 an4 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. D /\ y e. C ) ) <-> ( ( x e. A /\ z e. D ) /\ ( y e. B /\ y e. C ) ) )
8 7 exbii 
 |-  ( E. y ( ( x e. A /\ y e. B ) /\ ( z e. D /\ y e. C ) ) <-> E. y ( ( x e. A /\ z e. D ) /\ ( y e. B /\ y e. C ) ) )
9 19.42v 
 |-  ( E. y ( ( x e. A /\ z e. D ) /\ ( y e. B /\ y e. C ) ) <-> ( ( x e. A /\ z e. D ) /\ E. y ( y e. B /\ y e. C ) ) )
10 6 8 9 3bitri 
 |-  ( E. y ( x ( A X. B ) y /\ y ( C X. D ) z ) <-> ( ( x e. A /\ z e. D ) /\ E. y ( y e. B /\ y e. C ) ) )
11 ndisj 
 |-  ( ( B i^i C ) =/= (/) <-> E. y ( y e. B /\ y e. C ) )
12 1 11 sylib 
 |-  ( ph -> E. y ( y e. B /\ y e. C ) )
13 12 biantrud 
 |-  ( ph -> ( ( x e. A /\ z e. D ) <-> ( ( x e. A /\ z e. D ) /\ E. y ( y e. B /\ y e. C ) ) ) )
14 10 13 bitr4id 
 |-  ( ph -> ( E. y ( x ( A X. B ) y /\ y ( C X. D ) z ) <-> ( x e. A /\ z e. D ) ) )
15 14 opabbidv 
 |-  ( ph -> { <. x , z >. | E. y ( x ( A X. B ) y /\ y ( C X. D ) z ) } = { <. x , z >. | ( x e. A /\ z e. D ) } )
16 df-co 
 |-  ( ( C X. D ) o. ( A X. B ) ) = { <. x , z >. | E. y ( x ( A X. B ) y /\ y ( C X. D ) z ) }
17 df-xp 
 |-  ( A X. D ) = { <. x , z >. | ( x e. A /\ z e. D ) }
18 15 16 17 3eqtr4g 
 |-  ( ph -> ( ( C X. D ) o. ( A X. B ) ) = ( A X. D ) )