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