This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Infinity Eight inequivalent definitions of finite set 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 𝑓 ) ) )