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	$⊢ (T \in Tarski \land Tr A \land A \in T) \to A \subseteq T$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (T \in Tarski \land Tr A \land A \in T) \to Tr A$
2		dftr4	$⊢ Tr A \leftrightarrow A \subseteq 𝒫 A$
3	1 2	sylib	$⊢ (T \in Tarski \land Tr A \land A \in T) \to A \subseteq 𝒫 A$
4		tskpwss	$⊢ (T \in Tarski \land A \in T) \to 𝒫 A \subseteq T$
5	4	3adant2	$⊢ (T \in Tarski \land Tr A \land A \in T) \to 𝒫 A \subseteq T$
6	3 5	sstrd	$⊢ (T \in Tarski \land Tr A \land A \in T) \to A \subseteq T$

Metamath Proof Explorer

Theorem tsktrss

Proof