Metamath Proof Explorer


Theorem isfin3-3

Description: Weakly Dedekind-infinite sets are exactly those with an _om -indexed descending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 isf33lem FinIII = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎𝑏 ) → ran 𝑎 ∈ ran 𝑎 ) }
2 1 isfin3ds ( 𝐴𝑉 → ( 𝐴 ∈ FinIII ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓𝑥 ) → ran 𝑓 ∈ ran 𝑓 ) ) )