Theorem xpundir

Description: Distributive law for Cartesian product over union. Similar to Theorem 103 of Suppes p. 52. (Contributed by NM, 30-Sep-2002)

	Ref	Expression
Assertion	xpundir	⊢ ( ( 𝐴 ∪ 𝐵 ) × 𝐶 ) = ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-xp	⊢ ( ( 𝐴 ∪ 𝐵 ) × 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) }
2		df-xp	⊢ ( 𝐴 × 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) }
3		df-xp	⊢ ( 𝐵 × 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) }
4	2 3	uneq12i	⊢ ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } )
5		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
6	5	anbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) )
7		andir	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
8	6 7	bitri	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
9	8	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
10		unopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
11	9 10	eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) } = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } )
12	4 11	eqtr4i	⊢ ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) }
13	1 12	eqtr4i	⊢ ( ( 𝐴 ∪ 𝐵 ) × 𝐶 ) = ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) )