Theorem tskpwss

Description: First axiom of a Tarski class. The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskpwss	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to 𝒫A\subseteq T$$

Proof

Step	Hyp	Ref	Expression
1		eltskg	$$⊢T\in \mathrm{Tarski}\to \left(T\in \mathrm{Tarski}\leftrightarrow \left(\forall x\in T\left(𝒫x\subseteq T\wedge \exists y\in T𝒫x\subseteq y\right)\wedge \forall x\in 𝒫T\left(x\approx T\vee x\in T\right)\right)\right)$$
2	1	ibi	$$⊢T\in \mathrm{Tarski}\to \left(\forall x\in T\left(𝒫x\subseteq T\wedge \exists y\in T𝒫x\subseteq y\right)\wedge \forall x\in 𝒫T\left(x\approx T\vee x\in T\right)\right)$$
3	2	simpld	$$⊢T\in \mathrm{Tarski}\to \forall x\in T\left(𝒫x\subseteq T\wedge \exists y\in T𝒫x\subseteq y\right)$$
4		simpl	$$⊢\left(𝒫x\subseteq T\wedge \exists y\in T𝒫x\subseteq y\right)\to 𝒫x\subseteq T$$
5	4	ralimi	$$⊢\forall x\in T\left(𝒫x\subseteq T\wedge \exists y\in T𝒫x\subseteq y\right)\to \forall x\in T𝒫x\subseteq T$$
6	3 5	syl	$$⊢T\in \mathrm{Tarski}\to \forall x\in T𝒫x\subseteq T$$
7		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
8	7	sseq1d	$$⊢x=A\to \left(𝒫x\subseteq T\leftrightarrow 𝒫A\subseteq T\right)$$
9	8	rspccva	$$⊢\left(\forall x\in T𝒫x\subseteq T\wedge A\in T\right)\to 𝒫A\subseteq T$$
10	6 9	sylan	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to 𝒫A\subseteq T$$