Theorem xpiundir

Description: Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014)

	Ref	Expression
Assertion	xpiundir	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
2		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
3	2	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
4		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5	4	anbi1i	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
6		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
7	5 6	bitr4i	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
8	7	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
9	1 3 8	3bitr4ri	⊢ ( ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ )
10		df-rex	⊢ ( ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ↔ ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ) )
11		elxp2	⊢ ( 𝑧 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ )
12	11	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ )
13	9 10 12	3bitr4i	⊢ ( ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( 𝐵 × 𝐶 ) )
14		elxp2	⊢ ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐶 ) ↔ ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∃ 𝑤 ∈ 𝐶 𝑧 = ⟨ 𝑦 , 𝑤 ⟩ )
15		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( 𝐵 × 𝐶 ) )
16	13 14 15	3bitr4i	⊢ ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐶 ) ↔ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) )
17	16	eqriv	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 × 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 )