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 \in Tarski \land T \neq \emptyset) \to 2_{𝑜} ≺ T$

Step	Hyp	Ref	Expression
1		tsk2	$⊢ (T \in Tarski \land T \neq \emptyset) \to 2_{𝑜} \in T$
2		tsksdom	$⊢ (T \in Tarski \land 2_{𝑜} \in T) \to 2_{𝑜} ≺ T$
3	1 2	syldan	$⊢ (T \in Tarski \land T \neq \emptyset) \to 2_{𝑜} ≺ T$