Metamath Proof Explorer

Theorem tsksuc

Description: If an element of a Tarski class is an ordinal number, its successor is an element of the class. JFM CLASSES2 th. 6 (partly). (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tsksuc ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → suc ⁡ A ∈ T

Proof

Step Hyp Ref Expression
1 simp1 ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → T ∈ Tarski
2 tskpw ⊢ T ∈ Tarski ∧ A ∈ T → 𝒫 A ∈ T
3 2 3adant2 ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → 𝒫 A ∈ T
4 eloni ⊢ A ∈ On → Ord ⁡ A
5 4 3ad2ant2 ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → Ord ⁡ A
6 ordunisuc ⊢ Ord ⁡ A → ⋃ suc ⁡ A = A
7 eqimss ⊢ ⋃ suc ⁡ A = A → ⋃ suc ⁡ A ⊆ A
8 5 6 7 3syl ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → ⋃ suc ⁡ A ⊆ A
9 sspwuni ⊢ suc ⁡ A ⊆ 𝒫 A ↔ ⋃ suc ⁡ A ⊆ A
10 8 9 sylibr ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → suc ⁡ A ⊆ 𝒫 A
11 tskss ⊢ T ∈ Tarski ∧ 𝒫 A ∈ T ∧ suc ⁡ A ⊆ 𝒫 A → suc ⁡ A ∈ T
12 1 3 10 11 syl3anc ⊢ T ∈ Tarski ∧ A ∈ On ∧ A ∈ T → suc ⁡ A ∈ T