Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Eight inequivalent definitions of finite set
isfin3-3
Metamath Proof Explorer
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 𝑓 ) ) )