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