tskinf

Description: A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011)

		Ref	Expression
	Assertion	tskinf	$⊢ (T \in Tarski \land T \neq \emptyset) \to ω ≼ T$

Step	Hyp	Ref	Expression
1		r111	$⊢ R_{1} : On \underset{1-1}{⟶} V$
2		omsson	$⊢ ω \subseteq On$
3		omex	$⊢ ω \in V$
4	3	f1imaen	$⊢ (R_{1} : On \underset{1-1}{⟶} V \land ω \subseteq On) \to R_{1} [ω] \approx ω$
5	1 2 4	mp2an	$⊢ R_{1} [ω] \approx ω$
6	5	ensymi	$⊢ ω \approx R_{1} [ω]$
7		simpl	$⊢ (T \in Tarski \land T \neq \emptyset) \to T \in Tarski$
8		tskr1om	$⊢ (T \in Tarski \land T \neq \emptyset) \to R_{1} [ω] \subseteq T$
9		ssdomg	$⊢ T \in Tarski \to (R_{1} [ω] \subseteq T \to R_{1} [ω] ≼ T)$
10	7 8 9	sylc	$⊢ (T \in Tarski \land T \neq \emptyset) \to R_{1} [ω] ≼ T$
11		endomtr	$⊢ (ω \approx R_{1} [ω] \land R_{1} [ω] ≼ T) \to ω ≼ T$
12	6 10 11	sylancr	$⊢ (T \in Tarski \land T \neq \emptyset) \to ω ≼ T$

Metamath Proof Explorer