Metamath Proof Explorer


Theorem tsk2

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 TTarskiT2𝑜T

Proof

Step Hyp Ref Expression
1 tsk1 TTarskiT1𝑜T
2 df-2o 2𝑜=suc1𝑜
3 1on 1𝑜On
4 tsksuc TTarski1𝑜On1𝑜Tsuc1𝑜T
5 3 4 mp3an2 TTarski1𝑜Tsuc1𝑜T
6 2 5 eqeltrid TTarski1𝑜T2𝑜T
7 1 6 syldan TTarskiT2𝑜T