This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin^III ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑_m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isf33lem	⊢ Fin^III = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑_m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2	1	isfin3ds	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin^III ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑_m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )