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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 2o ≺ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		tsk2	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 2o ∈ 𝑇 )
2		tsksdom	⊢ ( ( 𝑇 ∈ Tarski ∧ 2o ∈ 𝑇 ) → 2o ≺ 𝑇 )
3	1 2	syldan	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 2o ≺ 𝑇 )