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

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

Proof

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