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 Tarski T 2 𝑜 T

Proof

Step Hyp Ref Expression
1 tsk2 T Tarski T 2 𝑜 T
2 tsksdom T Tarski 2 𝑜 T 2 𝑜 T
3 1 2 syldan T Tarski T 2 𝑜 T