Metamath Proof Explorer

Theorem dmrnxp

Description: A Cartesian product is the Cartesian product of its domain and range. (Contributed by Zhi Wang, 30-Oct-2025)

Ref Expression
Assertion dmrnxp 
|- ( R = ( A X. B ) -> R = ( dom R X. ran R ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> R = ( A X. B ) )
2 simpr 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> -. A =/= (/) )
3 nne 
 |-  ( -. A =/= (/) <-> A = (/) )
4 2 3 sylib 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> A = (/) )
5 4 xpeq1d 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> ( A X. B ) = ( (/) X. B ) )
6 0xp 
 |-  ( (/) X. B ) = (/)
7 5 6 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> ( A X. B ) = (/) )
8 1 7 eqtrd 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> R = (/) )
9 8 dmeqd 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> dom R = dom (/) )
10 dm0 
 |-  dom (/) = (/)
11 9 10 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> dom R = (/) )
12 8 rneqd 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> ran R = ran (/) )
13 rn0 
 |-  ran (/) = (/)
14 12 13 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> ran R = (/) )
15 11 14 xpeq12d 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> ( dom R X. ran R ) = ( (/) X. (/) ) )
16 0xp 
 |-  ( (/) X. (/) ) = (/)
17 15 16 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> ( dom R X. ran R ) = (/) )
18 8 17 eqtr4d 
 |-  ( ( R = ( A X. B ) /\ -. A =/= (/) ) -> R = ( dom R X. ran R ) )
19 simpl 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> R = ( A X. B ) )
20 simpr 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> -. B =/= (/) )
21 nne 
 |-  ( -. B =/= (/) <-> B = (/) )
22 20 21 sylib 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> B = (/) )
23 22 xpeq2d 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> ( A X. B ) = ( A X. (/) ) )
24 xp0 
 |-  ( A X. (/) ) = (/)
25 23 24 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> ( A X. B ) = (/) )
26 19 25 eqtrd 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> R = (/) )
27 26 dmeqd 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> dom R = dom (/) )
28 27 10 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> dom R = (/) )
29 26 rneqd 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> ran R = ran (/) )
30 29 13 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> ran R = (/) )
31 28 30 xpeq12d 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> ( dom R X. ran R ) = ( (/) X. (/) ) )
32 31 16 eqtrdi 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> ( dom R X. ran R ) = (/) )
33 26 32 eqtr4d 
 |-  ( ( R = ( A X. B ) /\ -. B =/= (/) ) -> R = ( dom R X. ran R ) )
34 simpl 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> R = ( A X. B ) )
35 34 dmeqd 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> dom R = dom ( A X. B ) )
36 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
37 36 ad2antll 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> dom ( A X. B ) = A )
38 35 37 eqtrd 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> dom R = A )
39 34 rneqd 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> ran R = ran ( A X. B ) )
40 rnxp 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )
41 40 ad2antrl 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> ran ( A X. B ) = B )
42 39 41 eqtrd 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> ran R = B )
43 38 42 xpeq12d 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> ( dom R X. ran R ) = ( A X. B ) )
44 34 43 eqtr4d 
 |-  ( ( R = ( A X. B ) /\ ( A =/= (/) /\ B =/= (/) ) ) -> R = ( dom R X. ran R ) )
45 18 33 44 pm2.61dda 
 |-  ( R = ( A X. B ) -> R = ( dom R X. ran R ) )