Description: Two is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tsk2 | |- ( ( T e. Tarski /\ T =/= (/) ) -> 2o e. T ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tsk1 | |- ( ( T e. Tarski /\ T =/= (/) ) -> 1o e. T ) |
|
| 2 | df-2o | |- 2o = suc 1o |
|
| 3 | 1on | |- 1o e. On |
|
| 4 | tsksuc | |- ( ( T e. Tarski /\ 1o e. On /\ 1o e. T ) -> suc 1o e. T ) |
|
| 5 | 3 4 | mp3an2 | |- ( ( T e. Tarski /\ 1o e. T ) -> suc 1o e. T ) |
| 6 | 2 5 | eqeltrid | |- ( ( T e. Tarski /\ 1o e. T ) -> 2o e. T ) |
| 7 | 1 6 | syldan | |- ( ( T e. Tarski /\ T =/= (/) ) -> 2o e. T ) |