This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Step	Hyp	Ref	Expression
1		tsk1	$⊢ (T \in Tarski \land T \neq \emptyset) \to 1_{𝑜} \in T$
2		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
3		1on	$⊢ 1_{𝑜} \in On$
4		tsksuc	$⊢ (T \in Tarski \land 1_{𝑜} \in On \land 1_{𝑜} \in T) \to suc 1_{𝑜} \in T$
5	3 4	mp3an2	$⊢ (T \in Tarski \land 1_{𝑜} \in T) \to suc 1_{𝑜} \in T$
6	2 5	eqeltrid	$⊢ (T \in Tarski \land 1_{𝑜} \in T) \to 2_{𝑜} \in T$
7	1 6	syldan	$⊢ (T \in Tarski \land T \neq \emptyset) \to 2_{𝑜} \in T$