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