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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		eltsk2g	⊢ ( 𝑇 ∈ Tarski → ( 𝑇 ∈ Tarski ↔ ( ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ⊆ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) ) ) )
2	1	ibi	⊢ ( 𝑇 ∈ Tarski → ( ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ⊆ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) ) )
3	2	simpld	⊢ ( 𝑇 ∈ Tarski → ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ⊆ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) )
4		simpr	⊢ ( ( 𝒫 𝑥 ⊆ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) → 𝒫 𝑥 ∈ 𝑇 )
5	4	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ⊆ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) → ∀ 𝑥 ∈ 𝑇 𝒫 𝑥 ∈ 𝑇 )
6	3 5	syl	⊢ ( 𝑇 ∈ Tarski → ∀ 𝑥 ∈ 𝑇 𝒫 𝑥 ∈ 𝑇 )
7		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝒫 𝑥 ∈ 𝑇 ↔ 𝒫 𝐴 ∈ 𝑇 ) )
9	8	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑇 𝒫 𝑥 ∈ 𝑇 ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ∈ 𝑇 )
10	6 9	sylan	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ∈ 𝑇 )