tskss

Description: The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 18-Jun-2013)

		Ref	Expression
	Assertion	tskss	$⊢ (T \in Tarski \land A \in T \land B \subseteq A) \to B \in T$

Proof

Step	Hyp	Ref	Expression
1		elpw2g	$⊢ A \in T \to (B \in 𝒫 A \leftrightarrow B \subseteq A)$
2	1	adantl	$⊢ (T \in Tarski \land A \in T) \to (B \in 𝒫 A \leftrightarrow B \subseteq A)$
3		tskpwss	$⊢ (T \in Tarski \land A \in T) \to 𝒫 A \subseteq T$
4	3	sseld	$⊢ (T \in Tarski \land A \in T) \to (B \in 𝒫 A \to B \in T)$
5	2 4	sylbird	$⊢ (T \in Tarski \land A \in T) \to (B \subseteq A \to B \in T)$
6	5	3impia	$⊢ (T \in Tarski \land A \in T \land B \subseteq A) \to B \in T$

Metamath Proof Explorer

Theorem tskss

Proof