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

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

Proof

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