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

Metamath Proof Explorer

Theorem xpcogend

Description: The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019)

Ref Expression
Hypothesis xpcogend.1 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
Assertion xpcogend ( 𝜑 → ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐷 ) )

Proof

Step Hyp Ref Expression
1 xpcogend.1 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
2 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3 brxp ⊢ ( 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) )
4 3 biancomi ⊢ ( 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ↔ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) )
5 2 4 anbi12i ⊢ ( ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) )
7 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
8 7 exbii ⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
9 19.42v ⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
10 6 8 9 3bitri ⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
11 ndisj ⊢ ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
12 1 11 sylib ⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
13 12 biantrud ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
14 10 13 bitr4id ⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) ) )
15 14 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) } )
16 df-co ⊢ ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑧 ) }
17 df-xp ⊢ ( 𝐴 × 𝐷 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷 ) }
18 15 16 17 3eqtr4g ⊢ ( 𝜑 → ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐷 ) )