Theorem xpiundi

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

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

Proof

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