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

Metamath Proof Explorer

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 )