Metamath Proof Explorer

Theorem iscmet3

Description: The property " D is a complete metric" expressed in terms of functions on NN (or any other upper integer set). Thus, we only have to look at functions on NN , and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006) (Revised by Mario Carneiro, 5-May-2014)

Ref Expression
Hypotheses iscmet3.1 
|- Z = ( ZZ>= ` M )
iscmet3.2 
|- J = ( MetOpen ` D )
iscmet3.3 
|- ( ph -> M e. ZZ )
iscmet3.4 
|- ( ph -> D e. ( Met ` X ) )
Assertion iscmet3 
|- ( ph -> ( D e. ( CMet ` X ) <-> A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) )

Proof

Step Hyp Ref Expression
1 iscmet3.1 
 |-  Z = ( ZZ>= ` M )
2 iscmet3.2 
 |-  J = ( MetOpen ` D )
3 iscmet3.3 
 |-  ( ph -> M e. ZZ )
4 iscmet3.4 
 |-  ( ph -> D e. ( Met ` X ) )
5 2 cmetcau 
 |-  ( ( D e. ( CMet ` X ) /\ f e. ( Cau ` D ) ) -> f e. dom ( ~~>t ` J ) )
6 5 a1d 
 |-  ( ( D e. ( CMet ` X ) /\ f e. ( Cau ` D ) ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) )
7 6 ralrimiva 
 |-  ( D e. ( CMet ` X ) -> A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) )
8 4 adantr 
 |-  ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) -> D e. ( Met ` X ) )
9 simpr 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) -> g e. ( CauFil ` D ) )
10 1rp 
 |-  1 e. RR+
11 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
12 10 11 ax-mp 
 |-  ( 1 / 2 ) e. RR+
13 rpexpcl 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ k e. ZZ ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
14 12 13 mpan 
 |-  ( k e. ZZ -> ( ( 1 / 2 ) ^ k ) e. RR+ )
15 cfili 
 |-  ( ( g e. ( CauFil ` D ) /\ ( ( 1 / 2 ) ^ k ) e. RR+ ) -> E. t e. g A. u e. t A. v e. t ( u D v ) < ( ( 1 / 2 ) ^ k ) )
16 9 14 15 syl2an 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) /\ k e. ZZ ) -> E. t e. g A. u e. t A. v e. t ( u D v ) < ( ( 1 / 2 ) ^ k ) )
17 16 ralrimiva 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) -> A. k e. ZZ E. t e. g A. u e. t A. v e. t ( u D v ) < ( ( 1 / 2 ) ^ k ) )
18 vex 
 |-  g e. _V
19 znnen 
 |-  ZZ ~~ NN
20 nnenom 
 |-  NN ~~ _om
21 19 20 entri 
 |-  ZZ ~~ _om
22 raleq 
 |-  ( t = ( s ` k ) -> ( A. v e. t ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
23 22 raleqbi1dv 
 |-  ( t = ( s ` k ) -> ( A. u e. t A. v e. t ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
24 18 21 23 axcc4 
 |-  ( A. k e. ZZ E. t e. g A. u e. t A. v e. t ( u D v ) < ( ( 1 / 2 ) ^ k ) -> E. s ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
25 17 24 syl 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) -> E. s ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
26 3 ad2antrr 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> M e. ZZ )
27 1 uzenom 
 |-  ( M e. ZZ -> Z ~~ _om )
28 endom 
 |-  ( Z ~~ _om -> Z ~<_ _om )
29 26 27 28 3syl 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> Z ~<_ _om )
30 dfin5 
 |-  ( ( _I ` X ) i^i |^|_ n e. ( M ... k ) ( s ` n ) ) = { x e. ( _I ` X ) | x e. |^|_ n e. ( M ... k ) ( s ` n ) }
31 fzn0 
 |-  ( ( M ... k ) =/= (/) <-> k e. ( ZZ>= ` M ) )
32 31 biimpri 
 |-  ( k e. ( ZZ>= ` M ) -> ( M ... k ) =/= (/) )
33 32 1 eleq2s 
 |-  ( k e. Z -> ( M ... k ) =/= (/) )
34 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
35 4 34 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
36 35 adantr 
 |-  ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) -> D e. ( *Met ` X ) )
37 simpl 
 |-  ( ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) -> g e. ( CauFil ` D ) )
38 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ g e. ( CauFil ` D ) ) -> g e. ( Fil ` X ) )
39 36 37 38 syl2an 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) -> g e. ( Fil ` X ) )
40 simprr 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) -> s : ZZ --> g )
41 elfzelz 
 |-  ( n e. ( M ... k ) -> n e. ZZ )
42 ffvelrn 
 |-  ( ( s : ZZ --> g /\ n e. ZZ ) -> ( s ` n ) e. g )
43 40 41 42 syl2an 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ n e. ( M ... k ) ) -> ( s ` n ) e. g )
44 filelss 
 |-  ( ( g e. ( Fil ` X ) /\ ( s ` n ) e. g ) -> ( s ` n ) C_ X )
45 39 43 44 syl2an2r 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ n e. ( M ... k ) ) -> ( s ` n ) C_ X )
46 45 ralrimiva 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) -> A. n e. ( M ... k ) ( s ` n ) C_ X )
47 r19.2z 
 |-  ( ( ( M ... k ) =/= (/) /\ A. n e. ( M ... k ) ( s ` n ) C_ X ) -> E. n e. ( M ... k ) ( s ` n ) C_ X )
48 33 46 47 syl2anr 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> E. n e. ( M ... k ) ( s ` n ) C_ X )
49 iinss 
 |-  ( E. n e. ( M ... k ) ( s ` n ) C_ X -> |^|_ n e. ( M ... k ) ( s ` n ) C_ X )
50 48 49 syl 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> |^|_ n e. ( M ... k ) ( s ` n ) C_ X )
51 8 ad2antrr 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> D e. ( Met ` X ) )
52 elfvdm 
 |-  ( D e. ( Met ` X ) -> X e. dom Met )
53 fvi 
 |-  ( X e. dom Met -> ( _I ` X ) = X )
54 51 52 53 3syl 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> ( _I ` X ) = X )
55 50 54 sseqtrrd 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> |^|_ n e. ( M ... k ) ( s ` n ) C_ ( _I ` X ) )
56 sseqin2 
 |-  ( |^|_ n e. ( M ... k ) ( s ` n ) C_ ( _I ` X ) <-> ( ( _I ` X ) i^i |^|_ n e. ( M ... k ) ( s ` n ) ) = |^|_ n e. ( M ... k ) ( s ` n ) )
57 55 56 sylib 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> ( ( _I ` X ) i^i |^|_ n e. ( M ... k ) ( s ` n ) ) = |^|_ n e. ( M ... k ) ( s ` n ) )
58 30 57 syl5eqr 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> { x e. ( _I ` X ) | x e. |^|_ n e. ( M ... k ) ( s ` n ) } = |^|_ n e. ( M ... k ) ( s ` n ) )
59 39 adantr 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> g e. ( Fil ` X ) )
60 43 ralrimiva 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) -> A. n e. ( M ... k ) ( s ` n ) e. g )
61 60 adantr 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> A. n e. ( M ... k ) ( s ` n ) e. g )
62 33 adantl 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> ( M ... k ) =/= (/) )
63 fzfid 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> ( M ... k ) e. Fin )
64 iinfi 
 |-  ( ( g e. ( Fil ` X ) /\ ( A. n e. ( M ... k ) ( s ` n ) e. g /\ ( M ... k ) =/= (/) /\ ( M ... k ) e. Fin ) ) -> |^|_ n e. ( M ... k ) ( s ` n ) e. ( fi ` g ) )
65 59 61 62 63 64 syl13anc 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> |^|_ n e. ( M ... k ) ( s ` n ) e. ( fi ` g ) )
66 filfi 
 |-  ( g e. ( Fil ` X ) -> ( fi ` g ) = g )
67 59 66 syl 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> ( fi ` g ) = g )
68 65 67 eleqtrd 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> |^|_ n e. ( M ... k ) ( s ` n ) e. g )
69 fileln0 
 |-  ( ( g e. ( Fil ` X ) /\ |^|_ n e. ( M ... k ) ( s ` n ) e. g ) -> |^|_ n e. ( M ... k ) ( s ` n ) =/= (/) )
70 39 68 69 syl2an2r 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> |^|_ n e. ( M ... k ) ( s ` n ) =/= (/) )
71 58 70 eqnetrd 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> { x e. ( _I ` X ) | x e. |^|_ n e. ( M ... k ) ( s ` n ) } =/= (/) )
72 rabn0 
 |-  ( { x e. ( _I ` X ) | x e. |^|_ n e. ( M ... k ) ( s ` n ) } =/= (/) <-> E. x e. ( _I ` X ) x e. |^|_ n e. ( M ... k ) ( s ` n ) )
73 71 72 sylib 
 |-  ( ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) /\ k e. Z ) -> E. x e. ( _I ` X ) x e. |^|_ n e. ( M ... k ) ( s ` n ) )
74 73 ralrimiva 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ s : ZZ --> g ) ) -> A. k e. Z E. x e. ( _I ` X ) x e. |^|_ n e. ( M ... k ) ( s ` n ) )
75 74 adantrrr 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> A. k e. Z E. x e. ( _I ` X ) x e. |^|_ n e. ( M ... k ) ( s ` n ) )
76 fvex 
 |-  ( _I ` X ) e. _V
77 eleq1 
 |-  ( x = ( f ` k ) -> ( x e. |^|_ n e. ( M ... k ) ( s ` n ) <-> ( f ` k ) e. |^|_ n e. ( M ... k ) ( s ` n ) ) )
78 fvex 
 |-  ( f ` k ) e. _V
79 eliin 
 |-  ( ( f ` k ) e. _V -> ( ( f ` k ) e. |^|_ n e. ( M ... k ) ( s ` n ) <-> A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) )
80 78 79 ax-mp 
 |-  ( ( f ` k ) e. |^|_ n e. ( M ... k ) ( s ` n ) <-> A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) )
81 77 80 bitrdi 
 |-  ( x = ( f ` k ) -> ( x e. |^|_ n e. ( M ... k ) ( s ` n ) <-> A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) )
82 76 81 axcc4dom 
 |-  ( ( Z ~<_ _om /\ A. k e. Z E. x e. ( _I ` X ) x e. |^|_ n e. ( M ... k ) ( s ` n ) ) -> E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) )
83 29 75 82 syl2anc 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) )
84 df-ral 
 |-  ( A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) <-> A. f ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) )
85 19.29 
 |-  ( ( A. f ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) -> E. f ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) )
86 84 85 sylanb 
 |-  ( ( A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) /\ E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) -> E. f ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) )
87 3 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> M e. ZZ )
88 4 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> D e. ( Met ` X ) )
89 simprrl 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> f : Z --> ( _I ` X ) )
90 feq3 
 |-  ( ( _I ` X ) = X -> ( f : Z --> ( _I ` X ) <-> f : Z --> X ) )
91 88 52 53 90 4syl 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> ( f : Z --> ( _I ` X ) <-> f : Z --> X ) )
92 89 91 mpbid 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> f : Z --> X )
93 simplrr 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
94 93 simprd 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
95 fveq2 
 |-  ( k = i -> ( s ` k ) = ( s ` i ) )
96 oveq2 
 |-  ( k = i -> ( ( 1 / 2 ) ^ k ) = ( ( 1 / 2 ) ^ i ) )
97 96 breq2d 
 |-  ( k = i -> ( ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> ( u D v ) < ( ( 1 / 2 ) ^ i ) ) )
98 95 97 raleqbidv 
 |-  ( k = i -> ( A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> A. v e. ( s ` i ) ( u D v ) < ( ( 1 / 2 ) ^ i ) ) )
99 95 98 raleqbidv 
 |-  ( k = i -> ( A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> A. u e. ( s ` i ) A. v e. ( s ` i ) ( u D v ) < ( ( 1 / 2 ) ^ i ) ) )
100 99 cbvralvw 
 |-  ( A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> A. i e. ZZ A. u e. ( s ` i ) A. v e. ( s ` i ) ( u D v ) < ( ( 1 / 2 ) ^ i ) )
101 94 100 sylib 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> A. i e. ZZ A. u e. ( s ` i ) A. v e. ( s ` i ) ( u D v ) < ( ( 1 / 2 ) ^ i ) )
102 simprrr 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) )
103 fveq2 
 |-  ( n = j -> ( s ` n ) = ( s ` j ) )
104 103 eleq2d 
 |-  ( n = j -> ( ( f ` k ) e. ( s ` n ) <-> ( f ` k ) e. ( s ` j ) ) )
105 104 cbvralvw 
 |-  ( A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) <-> A. j e. ( M ... k ) ( f ` k ) e. ( s ` j ) )
106 oveq2 
 |-  ( k = i -> ( M ... k ) = ( M ... i ) )
107 fveq2 
 |-  ( k = i -> ( f ` k ) = ( f ` i ) )
108 107 eleq1d 
 |-  ( k = i -> ( ( f ` k ) e. ( s ` j ) <-> ( f ` i ) e. ( s ` j ) ) )
109 106 108 raleqbidv 
 |-  ( k = i -> ( A. j e. ( M ... k ) ( f ` k ) e. ( s ` j ) <-> A. j e. ( M ... i ) ( f ` i ) e. ( s ` j ) ) )
110 105 109 syl5bb 
 |-  ( k = i -> ( A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) <-> A. j e. ( M ... i ) ( f ` i ) e. ( s ` j ) ) )
111 110 cbvralvw 
 |-  ( A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) <-> A. i e. Z A. j e. ( M ... i ) ( f ` i ) e. ( s ` j ) )
112 102 111 sylib 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> A. i e. Z A. j e. ( M ... i ) ( f ` i ) e. ( s ` j ) )
113 88 34 syl 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> D e. ( *Met ` X ) )
114 simplrl 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> g e. ( CauFil ` D ) )
115 113 114 38 syl2anc 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> g e. ( Fil ` X ) )
116 93 simpld 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> s : ZZ --> g )
117 1 2 87 88 92 101 112 iscmet3lem1 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> f e. ( Cau ` D ) )
118 simprl 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) )
119 117 92 118 mp2d 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> f e. dom ( ~~>t ` J ) )
120 1 2 87 88 92 101 112 115 116 119 iscmet3lem2 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) ) -> ( J fLim g ) =/= (/) )
121 120 ex 
 |-  ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> ( ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) -> ( J fLim g ) =/= (/) ) )
122 121 exlimdv 
 |-  ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> ( E. f ( ( f e. ( Cau ` D ) -> ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) -> ( J fLim g ) =/= (/) ) )
123 86 122 syl5 
 |-  ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> ( ( A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) /\ E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) ) -> ( J fLim g ) =/= (/) ) )
124 123 expdimp 
 |-  ( ( ( ph /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) -> ( E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) -> ( J fLim g ) =/= (/) ) )
125 124 an32s 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> ( E. f ( f : Z --> ( _I ` X ) /\ A. k e. Z A. n e. ( M ... k ) ( f ` k ) e. ( s ` n ) ) -> ( J fLim g ) =/= (/) ) )
126 83 125 mpd 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ ( g e. ( CauFil ` D ) /\ ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) ) ) -> ( J fLim g ) =/= (/) )
127 126 expr 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) -> ( ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) -> ( J fLim g ) =/= (/) ) )
128 127 exlimdv 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) -> ( E. s ( s : ZZ --> g /\ A. k e. ZZ A. u e. ( s ` k ) A. v e. ( s ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) -> ( J fLim g ) =/= (/) ) )
129 25 128 mpd 
 |-  ( ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) /\ g e. ( CauFil ` D ) ) -> ( J fLim g ) =/= (/) )
130 129 ralrimiva 
 |-  ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) -> A. g e. ( CauFil ` D ) ( J fLim g ) =/= (/) )
131 2 iscmet 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. g e. ( CauFil ` D ) ( J fLim g ) =/= (/) ) )
132 8 130 131 sylanbrc 
 |-  ( ( ph /\ A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) -> D e. ( CMet ` X ) )
133 132 ex 
 |-  ( ph -> ( A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) -> D e. ( CMet ` X ) ) )
134 7 133 impbid2 
 |-  ( ph -> ( D e. ( CMet ` X ) <-> A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~>t ` J ) ) ) )