Metamath Proof Explorer


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 syl5bi
 |-  ( 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 )