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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐵 ⊆ 𝑇 ) → ( 𝐴 × 𝐵 ) ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		elxp2	⊢ ( 𝑧 ∈ ( 𝑇 × 𝑇 ) ↔ ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
2		tskop	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑇 )
3		eleq1a	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑇 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝑇 ) )
4	2 3	syl	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝑇 ) )
5	4	3expib	⊢ ( 𝑇 ∈ Tarski → ( ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝑇 ) ) )
6	5	rexlimdvv	⊢ ( 𝑇 ∈ Tarski → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝑇 ) )
7	1 6	biimtrid	⊢ ( 𝑇 ∈ Tarski → ( 𝑧 ∈ ( 𝑇 × 𝑇 ) → 𝑧 ∈ 𝑇 ) )
8	7	ssrdv	⊢ ( 𝑇 ∈ Tarski → ( 𝑇 × 𝑇 ) ⊆ 𝑇 )
9		xpss12	⊢ ( ( 𝐴 ⊆ 𝑇 ∧ 𝐵 ⊆ 𝑇 ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝑇 × 𝑇 ) )
10		sstr	⊢ ( ( ( 𝐴 × 𝐵 ) ⊆ ( 𝑇 × 𝑇 ) ∧ ( 𝑇 × 𝑇 ) ⊆ 𝑇 ) → ( 𝐴 × 𝐵 ) ⊆ 𝑇 )
11	10	expcom	⊢ ( ( 𝑇 × 𝑇 ) ⊆ 𝑇 → ( ( 𝐴 × 𝐵 ) ⊆ ( 𝑇 × 𝑇 ) → ( 𝐴 × 𝐵 ) ⊆ 𝑇 ) )
12	8 9 11	syl2im	⊢ ( 𝑇 ∈ Tarski → ( ( 𝐴 ⊆ 𝑇 ∧ 𝐵 ⊆ 𝑇 ) → ( 𝐴 × 𝐵 ) ⊆ 𝑇 ) )
13	12	3impib	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐵 ⊆ 𝑇 ) → ( 𝐴 × 𝐵 ) ⊆ 𝑇 )