Theorem tsktrss

Description: A transitive element of a Tarski class is a part of the class. JFM CLASSES2 th. 8. (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tsktrss	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝐴 ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝐴 ∧ 𝐴 ∈ 𝑇 ) → Tr 𝐴 )
2		dftr4	⊢ ( Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴 )
3	1 2	sylib	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝐴 ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ⊆ 𝒫 𝐴 )
4		tskpwss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ⊆ 𝑇 )
5	4	3adant2	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝐴 ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ⊆ 𝑇 )
6	3 5	sstrd	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝐴 ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ⊆ 𝑇 )