Metamath Proof Explorer

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	$⊢ (C \times D) \circ (A \times B) \subseteq A \times D$

Proof

Step	Hyp	Ref	Expression
1		brxp	$⊢ x (A \times B) y \leftrightarrow (x \in A \land y \in B)$
2		brxp	$⊢ y (C \times D) t \leftrightarrow (y \in C \land t \in D)$
3	1 2	anbi12i	$⊢ (x (A \times B) y \land y (C \times D) t) \leftrightarrow ((x \in A \land y \in B) \land (y \in C \land t \in D))$
4		an43	$⊢ ((x \in A \land y \in B) \land (y \in C \land t \in D)) \leftrightarrow ((x \in A \land t \in D) \land (y \in B \land y \in C))$
5	3 4	bitri	$⊢ (x (A \times B) y \land y (C \times D) t) \leftrightarrow ((x \in A \land t \in D) \land (y \in B \land y \in C))$
6	5	exbii	$⊢ \exists y (x (A \times B) y \land y (C \times D) t) \leftrightarrow \exists y ((x \in A \land t \in D) \land (y \in B \land y \in C))$
7		19.42v	$⊢ \exists y ((x \in A \land t \in D) \land (y \in B \land y \in C)) \leftrightarrow ((x \in A \land t \in D) \land \exists y (y \in B \land y \in C))$
8	7	simplbi	$⊢ \exists y ((x \in A \land t \in D) \land (y \in B \land y \in C)) \to (x \in A \land t \in D)$
9	6 8	sylbi	$⊢ \exists y (x (A \times B) y \land y (C \times D) t) \to (x \in A \land t \in D)$
10	9	ssopab2i	$⊢ \{⟨x, t⟩ \| \exists y (x (A \times B) y \land y (C \times D) t)\} \subseteq \{⟨x, t⟩ \| (x \in A \land t \in D)\}$
11		df-co	$⊢ (C \times D) \circ (A \times B) = \{⟨x, t⟩ \| \exists y (x (A \times B) y \land y (C \times D) t)\}$
12		df-xp	$⊢ A \times D = \{⟨x, t⟩ \| (x \in A \land t \in D)\}$
13	10 11 12	3sstr4i	$⊢ (C \times D) \circ (A \times B) \subseteq A \times D$