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