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

Metamath Proof Explorer

Theorem xpco

Description: Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion xpco ( 𝐵 ≠ ∅ → ( ( 𝐵 × 𝐶 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
2 1 biimpi ⊢ ( 𝐵 ≠ ∅ → ∃ 𝑦 𝑦 ∈ 𝐵 )
3 2 biantrurd ⊢ ( 𝐵 ≠ ∅ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ∃ 𝑦 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) )
4 ancom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
5 4 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
6 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
7 brxp ⊢ ( 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
8 6 7 anbi12i ⊢ ( ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
9 anandi ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
10 5 8 9 3bitr4i ⊢ ( ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) )
11 10 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) )
12 19.41v ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ↔ ( ∃ 𝑦 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) )
13 11 12 bitr2i ⊢ ( ( ∃ 𝑦 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) )
14 3 13 bitr2di ⊢ ( 𝐵 ≠ ∅ → ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) )
15 14 opabbidv ⊢ ( 𝐵 ≠ ∅ → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) } )
16 df-co ⊢ ( ( 𝐵 × 𝐶 ) ∘ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐵 × 𝐶 ) 𝑧 ) }
17 df-xp ⊢ ( 𝐴 × 𝐶 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) }
18 15 16 17 3eqtr4g ⊢ ( 𝐵 ≠ ∅ → ( ( 𝐵 × 𝐶 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐶 ) )