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