Theorem dmxrn

Description: Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 22-Nov-2025)

	Ref	Expression
Assertion	dmxrn	|- dom ( R |X. S ) = ( dom R i^i dom S )

Proof

Step	Hyp	Ref	Expression
1		exdistrv	|- ( E. x E. y ( z R x /\ z S y ) <-> ( E. x z R x /\ E. y z S y ) )
2	1	abbii	|- { z | E. x E. y ( z R x /\ z S y ) } = { z | ( E. x z R x /\ E. y z S y ) }
3		dfxrn2	|- ( R |X. S ) = `' { <. <. x , y >. , z >. | ( z R x /\ z S y ) }
4	3	dmeqi	|- dom ( R |X. S ) = dom `' { <. <. x , y >. , z >. | ( z R x /\ z S y ) }
5		df-rn	|- ran { <. <. x , y >. , z >. | ( z R x /\ z S y ) } = dom `' { <. <. x , y >. , z >. | ( z R x /\ z S y ) }
6		rnoprab	|- ran { <. <. x , y >. , z >. | ( z R x /\ z S y ) } = { z | E. x E. y ( z R x /\ z S y ) }
7	4 5 6	3eqtr2i	|- dom ( R |X. S ) = { z | E. x E. y ( z R x /\ z S y ) }
8		inab	|- ( { z | E. x z R x } i^i { z | E. y z S y } ) = { z | ( E. x z R x /\ E. y z S y ) }
9	2 7 8	3eqtr4i	|- dom ( R |X. S ) = ( { z | E. x z R x } i^i { z | E. y z S y } )
10		df-dm	|- dom R = { z | E. x z R x }
11		df-dm	|- dom S = { z | E. y z S y }
12	10 11	ineq12i	|- ( dom R i^i dom S ) = ( { z | E. x z R x } i^i { z | E. y z S y } )
13	9 12	eqtr4i	|- dom ( R |X. S ) = ( dom R i^i dom S )