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 e. Tarski /\ A e. On /\ A e. T ) -> suc A e. T )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( T e. Tarski /\ A e. On /\ A e. T ) -> T e. Tarski )
2		tskpw	|- ( ( T e. Tarski /\ A e. T ) -> ~P A e. T )
3	2	3adant2	|- ( ( T e. Tarski /\ A e. On /\ A e. T ) -> ~P A e. T )
4		eloni	|- ( A e. On -> Ord A )
5	4	3ad2ant2	|- ( ( T e. Tarski /\ A e. On /\ A e. T ) -> Ord A )
6		ordunisuc	|- ( Ord A -> U. suc A = A )
7		eqimss	|- ( U. suc A = A -> U. suc A C_ A )
8	5 6 7	3syl	|- ( ( T e. Tarski /\ A e. On /\ A e. T ) -> U. suc A C_ A )
9		sspwuni	|- ( suc A C_ ~P A <-> U. suc A C_ A )
10	8 9	sylibr	|- ( ( T e. Tarski /\ A e. On /\ A e. T ) -> suc A C_ ~P A )
11		tskss	|- ( ( T e. Tarski /\ ~P A e. T /\ suc A C_ ~P A ) -> suc A e. T )
12	1 3 10 11	syl3anc	|- ( ( T e. Tarski /\ A e. On /\ A e. T ) -> suc A e. T )