Theorem bj-xpcossxp

Description: The composition of two Cartesian products is included in the expected Cartesian product. There is equality if ( B i^i C ) =/= (/) , see xpcogend . (Contributed by BJ, 22-May-2024)

	Ref	Expression
Assertion	bj-xpcossxp	⊢ ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		brxp	⊢ ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
2		brxp	⊢ ( 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑡 ∈ 𝐷 ) )
3	1 2	anbi12i	⊢ ( ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑡 ∈ 𝐷 ) ) )
4		an43	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑡 ∈ 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
5	3 4	bitri	⊢ ( ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
6	5	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
7		19.42v	⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
8	7	simplbi	⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) )
9	6 8	sylbi	⊢ ( ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) )
10	9	ssopab2i	⊢ { ⟨ 𝑥 , 𝑡 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ) } ⊆ { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) }
11		df-co	⊢ ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ∃ 𝑦 ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ∧ 𝑦 ( 𝐶 × 𝐷 ) 𝑡 ) }
12		df-xp	⊢ ( 𝐴 × 𝐷 ) = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐷 ) }
13	10 11 12	3sstr4i	⊢ ( ( 𝐶 × 𝐷 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐷 )