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