Theorem tskxp

Description: The Cartesian product of two elements of a transitive Tarski class is an element of the class. JFM CLASSES2 th. 67 (partly). (Contributed by FL, 15-Apr-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskxp	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A X. B ) e. T )

Proof

Step	Hyp	Ref	Expression
1		ne0i	|- ( A e. T -> T =/= (/) )
2		tskwun	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> T e. WUni )
3	2	3expa	|- ( ( ( T e. Tarski /\ Tr T ) /\ T =/= (/) ) -> T e. WUni )
4	1 3	sylan2	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T ) -> T e. WUni )
5	4	3adant3	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> T e. WUni )
6		simp2	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> A e. T )
7		simp3	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> B e. T )
8	5 6 7	wunxp	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A X. B ) e. T )