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 
|- ( ( 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 )