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 A V A FinIII f 𝒫 A ω x ω f suc x f x ran f ran f

Proof

Step Hyp Ref Expression
1 isf33lem FinIII = g | a 𝒫 g ω b ω a suc b a b ran a ran a
2 1 isfin3ds A V A FinIII f 𝒫 A ω x ω f suc x f x ran f ran f