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