Metamath Proof Explorer

Theorem tskinf

Description: A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011)

Ref Expression
Assertion tskinf 
|- ( ( T e. Tarski /\ T =/= (/) ) -> _om ~<_ T )

Proof

Step Hyp Ref Expression
1 r111 
 |-  R1 : On -1-1-> _V
2 omsson 
 |-  _om C_ On
3 omex 
 |-  _om e. _V
4 3 f1imaen 
 |-  ( ( R1 : On -1-1-> _V /\ _om C_ On ) -> ( R1 " _om ) ~~ _om )
5 1 2 4 mp2an 
 |-  ( R1 " _om ) ~~ _om
6 5 ensymi 
 |-  _om ~~ ( R1 " _om )
7 simpl 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> T e. Tarski )
8 tskr1om 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) C_ T )
9 ssdomg 
 |-  ( T e. Tarski -> ( ( R1 " _om ) C_ T -> ( R1 " _om ) ~<_ T ) )
10 7 8 9 sylc 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) ~<_ T )
11 endomtr 
 |-  ( ( _om ~~ ( R1 " _om ) /\ ( R1 " _om ) ~<_ T ) -> _om ~<_ T )
12 6 10 11 sylancr 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> _om ~<_ T )