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
⊢ A ∈ V → A ∈ Fin III ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
Proof
Step
Hyp
Ref
Expression
1
isf33lem
⊢ Fin III = g | ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a
2
1
isfin3ds
⊢ A ∈ V → A ∈ Fin III ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f