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

Metamath Proof Explorer

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