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

Metamath Proof Explorer

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 ∧ 𝑇 ≠ ∅ ) → ω ≼ 𝑇 )