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

Proof

Step	Hyp	Ref	Expression
1		elxp2	$⊢ z \in (T \times T) \leftrightarrow \exists x \in T \exists y \in T z = ⟨x, y⟩$
2		tskop	$⊢ (T \in Tarski \land x \in T \land y \in T) \to ⟨x, y⟩ \in T$
3		eleq1a	$⊢ ⟨x, y⟩ \in T \to (z = ⟨x, y⟩ \to z \in T)$
4	2 3	syl	$⊢ (T \in Tarski \land x \in T \land y \in T) \to (z = ⟨x, y⟩ \to z \in T)$
5	4	3expib	$⊢ T \in Tarski \to ((x \in T \land y \in T) \to (z = ⟨x, y⟩ \to z \in T))$
6	5	rexlimdvv	$⊢ T \in Tarski \to (\exists x \in T \exists y \in T z = ⟨x, y⟩ \to z \in T)$
7	1 6	biimtrid	$⊢ T \in Tarski \to (z \in (T \times T) \to z \in T)$
8	7	ssrdv	$⊢ T \in Tarski \to T \times T \subseteq T$
9		xpss12	$⊢ (A \subseteq T \land B \subseteq T) \to A \times B \subseteq T \times T$
10		sstr	$⊢ (A \times B \subseteq T \times T \land T \times T \subseteq T) \to A \times B \subseteq T$
11	10	expcom	$⊢ T \times T \subseteq T \to (A \times B \subseteq T \times T \to A \times B \subseteq T)$
12	8 9 11	syl2im	$⊢ T \in Tarski \to ((A \subseteq T \land B \subseteq T) \to A \times B \subseteq T)$
13	12	3impib	$⊢ (T \in Tarski \land A \subseteq T \land B \subseteq T) \to A \times B \subseteq T$