Theorem tskpw

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

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

Proof

Step	Hyp	Ref	Expression
1		eltsk2g	$$⊢T\in \mathrm{Tarski}\to \left(T\in \mathrm{Tarski}\leftrightarrow \left(\forall x\in T\left(𝒫x\subseteq T\wedge 𝒫x\in T\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 𝒫x\in T\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 𝒫x\in T\right)$$
4		simpr	$$⊢\left(𝒫x\subseteq T\wedge 𝒫x\in T\right)\to 𝒫x\in T$$
5	4	ralimi	$$⊢\forall x\in T\left(𝒫x\subseteq T\wedge 𝒫x\in T\right)\to \forall x\in T𝒫x\in T$$
6	3 5	syl	$$⊢T\in \mathrm{Tarski}\to \forall x\in T𝒫x\in T$$
7		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
8	7	eleq1d	$$⊢x=A\to \left(𝒫x\in T\leftrightarrow 𝒫A\in T\right)$$
9	8	rspccva	$$⊢\left(\forall x\in T𝒫x\in T\wedge A\in T\right)\to 𝒫A\in T$$
10	6 9	sylan	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to 𝒫A\in T$$