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

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 ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ∪ ∪ ( 𝐴 × 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )