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

Proof

Step	Hyp	Ref	Expression
1		tsk1	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 1o ∈ 𝑇 )
2		df-2o	⊢ 2o = suc 1o
3		1on	⊢ 1o ∈ On
4		tsksuc	⊢ ( ( 𝑇 ∈ Tarski ∧ 1o ∈ On ∧ 1o ∈ 𝑇 ) → suc 1o ∈ 𝑇 )
5	3 4	mp3an2	⊢ ( ( 𝑇 ∈ Tarski ∧ 1o ∈ 𝑇 ) → suc 1o ∈ 𝑇 )
6	2 5	eqeltrid	⊢ ( ( 𝑇 ∈ Tarski ∧ 1o ∈ 𝑇 ) → 2o ∈ 𝑇 )
7	1 6	syldan	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 2o ∈ 𝑇 )