Theorem xpab

Description: Cross product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	xpab	|- ( { x | ph } X. { y | ps } ) = { <. x , y >. | ( ph /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		relxp	|- Rel ( { x | ph } X. { y | ps } )
2		relopabv	|- Rel { <. x , y >. | ( ph /\ ps ) }
3		df-clab	|- ( a e. { x | ph } <-> [ a / x ] ph )
4		df-clab	|- ( b e. { y | ps } <-> [ b / y ] ps )
5	3 4	anbi12i	|- ( ( a e. { x | ph } /\ b e. { y | ps } ) <-> ( [ a / x ] ph /\ [ b / y ] ps ) )
6		sban	|- ( [ b / y ] ( ph /\ ps ) <-> ( [ b / y ] ph /\ [ b / y ] ps ) )
7		sbsbc	|- ( [ b / y ] ( ph /\ ps ) <-> [. b / y ]. ( ph /\ ps ) )
8		sbv	|- ( [ b / y ] ph <-> ph )
9	8	anbi1i	|- ( ( [ b / y ] ph /\ [ b / y ] ps ) <-> ( ph /\ [ b / y ] ps ) )
10	6 7 9	3bitr3i	|- ( [. b / y ]. ( ph /\ ps ) <-> ( ph /\ [ b / y ] ps ) )
11	10	sbbii	|- ( [ a / x ] [. b / y ]. ( ph /\ ps ) <-> [ a / x ] ( ph /\ [ b / y ] ps ) )
12		sbsbc	|- ( [ a / x ] [. b / y ]. ( ph /\ ps ) <-> [. a / x ]. [. b / y ]. ( ph /\ ps ) )
13		sban	|- ( [ a / x ] ( ph /\ [ b / y ] ps ) <-> ( [ a / x ] ph /\ [ a / x ] [ b / y ] ps ) )
14		sbv	|- ( [ a / x ] [ b / y ] ps <-> [ b / y ] ps )
15	14	anbi2i	|- ( ( [ a / x ] ph /\ [ a / x ] [ b / y ] ps ) <-> ( [ a / x ] ph /\ [ b / y ] ps ) )
16	13 15	bitri	|- ( [ a / x ] ( ph /\ [ b / y ] ps ) <-> ( [ a / x ] ph /\ [ b / y ] ps ) )
17	11 12 16	3bitr3i	|- ( [. a / x ]. [. b / y ]. ( ph /\ ps ) <-> ( [ a / x ] ph /\ [ b / y ] ps ) )
18	5 17	bitr4i	|- ( ( a e. { x | ph } /\ b e. { y | ps } ) <-> [. a / x ]. [. b / y ]. ( ph /\ ps ) )
19		brxp	|- ( a ( { x | ph } X. { y | ps } ) b <-> ( a e. { x | ph } /\ b e. { y | ps } ) )
20		eqid	|- { <. x , y >. | ( ph /\ ps ) } = { <. x , y >. | ( ph /\ ps ) }
21	20	brabsb	|- ( a { <. x , y >. | ( ph /\ ps ) } b <-> [. a / x ]. [. b / y ]. ( ph /\ ps ) )
22	18 19 21	3bitr4i	|- ( a ( { x | ph } X. { y | ps } ) b <-> a { <. x , y >. | ( ph /\ ps ) } b )
23	1 2 22	eqbrriv	|- ( { x | ph } X. { y | ps } ) = { <. x , y >. | ( ph /\ ps ) }