This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐶 × ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 )