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 ( 𝐵 ≠ ∅ → ( ( 𝐵 × 𝐶 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐶 ) )