Theorem isfin3-4

Description: Weakly Dedekind-infinite sets are exactly those with an _om -indexed ascending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin3-4	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ suc 𝑥 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) ) = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) )
2	1	isf34lem6	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ suc 𝑥 ) → ∪ ran 𝑓 ∈ ran 𝑓 ) ) )