This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ T ∈ Tarski ∧ A ∈ T → 𝒫 A ∈ T

Proof

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