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 𝐴 ∈ 𝑇 )