Metamath Proof Explorer


Theorem caufpm

Description: Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)

Ref Expression
Assertion caufpm ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( Cau β€˜ 𝐷 ) ) β†’ 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) )

Proof

Step Hyp Ref Expression
1 iscau ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐹 ∈ ( Cau β€˜ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ β„€ ( 𝐹 β†Ύ ( β„€β‰₯ β€˜ 𝑦 ) ) : ( β„€β‰₯ β€˜ 𝑦 ) ⟢ ( ( 𝐹 β€˜ 𝑦 ) ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )
2 1 simprbda ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( Cau β€˜ 𝐷 ) ) β†’ 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) )