Metamath Proof Explorer
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 β ) ) |