Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 eltskg ⊢ T ∈ Tarski → T ∈ Tarski ↔ ∀ x ∈ T 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y ∧ ∀ x ∈ 𝒫 T x ≈ T ∨ x ∈ T
2 1 ibi ⊢ T ∈ Tarski → ∀ x ∈ T 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y ∧ ∀ x ∈ 𝒫 T x ≈ T ∨ x ∈ T
3 2 simpld ⊢ T ∈ Tarski → ∀ x ∈ T 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y
4 simpl ⊢ 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y → 𝒫 x ⊆ T
5 4 ralimi ⊢ ∀ x ∈ T 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y → ∀ x ∈ T 𝒫 x ⊆ T
6 3 5 syl ⊢ T ∈ Tarski → ∀ x ∈ T 𝒫 x ⊆ T
7 pweq ⊢ x = A → 𝒫 x = 𝒫 A
8 7 sseq1d ⊢ 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