Theorem tskinf

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

	Ref	Expression
Assertion	tskinf	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ω ≼ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		r111	⊢ 𝑅1 : On –1-1→ V
2		omsson	⊢ ω ⊆ On
3		omex	⊢ ω ∈ V
4	3	f1imaen	⊢ ( ( 𝑅1 : On –1-1→ V ∧ ω ⊆ On ) → ( 𝑅1 “ ω ) ≈ ω )
5	1 2 4	mp2an	⊢ ( 𝑅1 “ ω ) ≈ ω
6	5	ensymi	⊢ ω ≈ ( 𝑅1 “ ω )
7		simpl	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ Tarski )
8		tskr1om	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 “ ω ) ⊆ 𝑇 )
9		ssdomg	⊢ ( 𝑇 ∈ Tarski → ( ( 𝑅1 “ ω ) ⊆ 𝑇 → ( 𝑅1 “ ω ) ≼ 𝑇 ) )
10	7 8 9	sylc	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 “ ω ) ≼ 𝑇 )
11		endomtr	⊢ ( ( ω ≈ ( 𝑅1 “ ω ) ∧ ( 𝑅1 “ ω ) ≼ 𝑇 ) → ω ≼ 𝑇 )
12	6 10 11	sylancr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ω ≼ 𝑇 )