Metamath Proof Explorer

Theorem caun0

Description: A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)

Ref Expression
Assertion caun0 
|- ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )

Proof

Step Hyp Ref Expression
1 1rp 
 |-  1 e. RR+
2 1 ne0ii 
 |-  RR+ =/= (/)
3 iscau2 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
4 3 simplbda 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
5 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> E. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
6 2 4 5 sylancr 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> E. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
7 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
8 ne0i 
 |-  ( j e. ( ZZ>= ` j ) -> ( ZZ>= ` j ) =/= (/) )
9 r19.2z 
 |-  ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
10 9 ex 
 |-  ( ( ZZ>= ` j ) =/= (/) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
11 7 8 10 3syl 
 |-  ( j e. ZZ -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
12 ne0i 
 |-  ( ( F ` k ) e. X -> X =/= (/) )
13 12 3ad2ant2 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )
14 13 rexlimivw 
 |-  ( E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )
15 11 14 syl6 
 |-  ( j e. ZZ -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) ) )
16 15 rexlimiv 
 |-  ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )
17 16 rexlimivw 
 |-  ( E. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )
18 6 17 syl 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )