Metamath Proof Explorer

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 \in Tarski \land Tr T) \land A \in T \land B \in T) \to A \times B \in T$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$⊢ A \in T \to T \neq \emptyset$
2		tskwun	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to T \in WUni$
3	2	3expa	$⊢ ((T \in Tarski \land Tr T) \land T \neq \emptyset) \to T \in WUni$
4	1 3	sylan2	$⊢ ((T \in Tarski \land Tr T) \land A \in T) \to T \in WUni$
5	4	3adant3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to T \in WUni$
6		simp2	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to A \in T$
7		simp3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to B \in T$
8	5 6 7	wunxp	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to A \times B \in T$