Metamath Proof Explorer


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 𝐴𝐴𝑇 ) → 𝐴𝑇 )