Metamath Proof Explorer

Theorem 2domtsk

Description: If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011)

Ref Expression
Assertion 2domtsk 
|- ( ( T e. Tarski /\ T =/= (/) ) -> 2o ~< T )

Proof

Step Hyp Ref Expression
1 tsk2 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> 2o e. T )
2 tsksdom 
 |-  ( ( T e. Tarski /\ 2o e. T ) -> 2o ~< T )
3 1 2 syldan 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> 2o ~< T )