Theorem xpundi

Description: Distributive law for Cartesian product over union. Theorem 103 of Suppes p. 52. (Contributed by NM, 12-Aug-2004)

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

Proof

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