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	|- ( ( T e. Tarski /\ A C_ T /\ B C_ T ) -> ( A X. B ) C_ T )

Proof

Step	Hyp	Ref	Expression
1		elxp2	|- ( z e. ( T X. T ) <-> E. x e. T E. y e. T z = <. x , y >. )
2		tskop	|- ( ( T e. Tarski /\ x e. T /\ y e. T ) -> <. x , y >. e. T )
3		eleq1a	|- ( <. x , y >. e. T -> ( z = <. x , y >. -> z e. T ) )
4	2 3	syl	|- ( ( T e. Tarski /\ x e. T /\ y e. T ) -> ( z = <. x , y >. -> z e. T ) )
5	4	3expib	|- ( T e. Tarski -> ( ( x e. T /\ y e. T ) -> ( z = <. x , y >. -> z e. T ) ) )
6	5	rexlimdvv	|- ( T e. Tarski -> ( E. x e. T E. y e. T z = <. x , y >. -> z e. T ) )
7	1 6	biimtrid	|- ( T e. Tarski -> ( z e. ( T X. T ) -> z e. T ) )
8	7	ssrdv	|- ( T e. Tarski -> ( T X. T ) C_ T )
9		xpss12	|- ( ( A C_ T /\ B C_ T ) -> ( A X. B ) C_ ( T X. T ) )
10		sstr	|- ( ( ( A X. B ) C_ ( T X. T ) /\ ( T X. T ) C_ T ) -> ( A X. B ) C_ T )
11	10	expcom	|- ( ( T X. T ) C_ T -> ( ( A X. B ) C_ ( T X. T ) -> ( A X. B ) C_ T ) )
12	8 9 11	syl2im	|- ( T e. Tarski -> ( ( A C_ T /\ B C_ T ) -> ( A X. B ) C_ T ) )
13	12	3impib	|- ( ( T e. Tarski /\ A C_ T /\ B C_ T ) -> ( A X. B ) C_ T )