Theorem tskxpss

Description: A Cartesian product of two parts of a Tarski class is a part of the class. (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Jun-2013)

	Ref	Expression
Assertion	tskxpss	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge B\subseteq T\right)\to A\times B\subseteq T$$

Proof

Step	Hyp	Ref	Expression
1		elxp2	$$⊢z\in \left(T\times T\right)\leftrightarrow \exists x\in T\exists y\in Tz=⟨x,y⟩$$
2		tskop	$$⊢\left(T\in \mathrm{Tarski}\wedge x\in T\wedge y\in T\right)\to ⟨x,y⟩\in T$$
3		eleq1a	$$⊢⟨x,y⟩\in T\to \left(z=⟨x,y⟩\to z\in T\right)$$
4	2 3	syl	$$⊢\left(T\in \mathrm{Tarski}\wedge x\in T\wedge y\in T\right)\to \left(z=⟨x,y⟩\to z\in T\right)$$
5	4	3expib	$$⊢T\in \mathrm{Tarski}\to \left(\left(x\in T\wedge y\in T\right)\to \left(z=⟨x,y⟩\to z\in T\right)\right)$$
6	5	rexlimdvv	$$⊢T\in \mathrm{Tarski}\to \left(\exists x\in T\exists y\in Tz=⟨x,y⟩\to z\in T\right)$$
7	1 6	syl5bi	$$⊢T\in \mathrm{Tarski}\to \left(z\in \left(T\times T\right)\to z\in T\right)$$
8	7	ssrdv	$$⊢T\in \mathrm{Tarski}\to T\times T\subseteq T$$
9		xpss12	$$⊢\left(A\subseteq T\wedge B\subseteq T\right)\to A\times B\subseteq T\times T$$
10		sstr	$$⊢\left(A\times B\subseteq T\times T\wedge T\times T\subseteq T\right)\to A\times B\subseteq T$$
11	10	expcom	$$⊢T\times T\subseteq T\to \left(A\times B\subseteq T\times T\to A\times B\subseteq T\right)$$
12	8 9 11	syl2im	$$⊢T\in \mathrm{Tarski}\to \left(\left(A\subseteq T\wedge B\subseteq T\right)\to A\times B\subseteq T\right)$$
13	12	3impib	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge B\subseteq T\right)\to A\times B\subseteq T$$