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