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