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 ) )