Theorem isfin3-2

Description: Weakly Dedekind-infinite sets are exactly those which can be mapped onto _om . (Contributed by Stefan O'Rear, 6-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin3-2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ¬ ω ≼* 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isfin32i	⊢ ( 𝐴 ∈ FinIII → ¬ ω ≼* 𝐴 )
2		isf33lem	⊢ FinIII = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3	2	isf32lem12	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ ω ≼* 𝐴 → 𝐴 ∈ FinIII ) )
4	1 3	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ¬ ω ≼* 𝐴 ) )