This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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