Metamath Proof Explorer


Theorem unixp

Description: The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006)

Ref Expression
Assertion unixp ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 relxp Rel ( 𝐴 × 𝐵 )
2 relfld ( Rel ( 𝐴 × 𝐵 ) → ( 𝐴 × 𝐵 ) = ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) )
3 1 2 ax-mp ( 𝐴 × 𝐵 ) = ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) )
4 xpeq2 ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
5 xp0 ( 𝐴 × ∅ ) = ∅
6 4 5 eqtrdi ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
7 6 necon3i ( ( 𝐴 × 𝐵 ) ≠ ∅ → 𝐵 ≠ ∅ )
8 xpeq1 ( 𝐴 = ∅ → ( 𝐴 × 𝐵 ) = ( ∅ × 𝐵 ) )
9 0xp ( ∅ × 𝐵 ) = ∅
10 8 9 eqtrdi ( 𝐴 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
11 10 necon3i ( ( 𝐴 × 𝐵 ) ≠ ∅ → 𝐴 ≠ ∅ )
12 dmxp ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
13 rnxp ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
14 uneq12 ( ( dom ( 𝐴 × 𝐵 ) = 𝐴 ∧ ran ( 𝐴 × 𝐵 ) = 𝐵 ) → ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) = ( 𝐴𝐵 ) )
15 12 13 14 syl2an ( ( 𝐵 ≠ ∅ ∧ 𝐴 ≠ ∅ ) → ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) = ( 𝐴𝐵 ) )
16 7 11 15 syl2anc ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( dom ( 𝐴 × 𝐵 ) ∪ ran ( 𝐴 × 𝐵 ) ) = ( 𝐴𝐵 ) )
17 3 16 eqtrid ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴𝐵 ) )