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 eqtr3id
 |-  ( ( ( ( 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 ) ) ) )