This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 ne0i ⊢ ( 𝐴 ∈ 𝑇 → 𝑇 ≠ ∅ )
2 tskwun ⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ WUni )
3 2 3expa ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ WUni )
4 1 3 sylan2 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ∈ WUni )
5 4 3adant3 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝑇 ∈ WUni )
6 simp2 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝐴 ∈ 𝑇 )
7 simp3 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝐵 ∈ 𝑇 )
8 5 6 7 wunxp ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 × 𝐵 ) ∈ 𝑇 )