Metamath Proof Explorer

Theorem heibor1lem

Description: Lemma for heibor1 . A compact metric space is complete. This proof works by considering the collection cls ( F " ( ZZ>=n ) ) for each n e. NN , which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain ( F " ( ZZ>=m ) ) for some m . Thus, by compactness, the intersection contains a point y , which must then be the convergent point of F . (Contributed by Jeff Madsen, 17-Jan-2014) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses heibor.1 
|- J = ( MetOpen ` D )
heibor1.3 
|- ( ph -> D e. ( Met ` X ) )
heibor1.4 
|- ( ph -> J e. Comp )
heibor1.5 
|- ( ph -> F e. ( Cau ` D ) )
heibor1.6 
|- ( ph -> F : NN --> X )
Assertion heibor1lem 
|- ( ph -> F e. dom ( ~~>t ` J ) )

Proof

Step Hyp Ref Expression
1 heibor.1 
 |-  J = ( MetOpen ` D )
2 heibor1.3 
 |-  ( ph -> D e. ( Met ` X ) )
3 heibor1.4 
 |-  ( ph -> J e. Comp )
4 heibor1.5 
 |-  ( ph -> F e. ( Cau ` D ) )
5 heibor1.6 
 |-  ( ph -> F : NN --> X )
6 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
7 2 6 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
8 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
9 7 8 syl 
 |-  ( ph -> J e. Top )
10 imassrn 
 |-  ( F " u ) C_ ran F
11 5 frnd 
 |-  ( ph -> ran F C_ X )
12 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
13 7 12 syl 
 |-  ( ph -> X = U. J )
14 11 13 sseqtrd 
 |-  ( ph -> ran F C_ U. J )
15 10 14 sstrid 
 |-  ( ph -> ( F " u ) C_ U. J )
16 eqid 
 |-  U. J = U. J
17 16 clscld 
 |-  ( ( J e. Top /\ ( F " u ) C_ U. J ) -> ( ( cls ` J ) ` ( F " u ) ) e. ( Clsd ` J ) )
18 9 15 17 syl2anc 
 |-  ( ph -> ( ( cls ` J ) ` ( F " u ) ) e. ( Clsd ` J ) )
19 eleq1a 
 |-  ( ( ( cls ` J ) ` ( F " u ) ) e. ( Clsd ` J ) -> ( k = ( ( cls ` J ) ` ( F " u ) ) -> k e. ( Clsd ` J ) ) )
20 18 19 syl 
 |-  ( ph -> ( k = ( ( cls ` J ) ` ( F " u ) ) -> k e. ( Clsd ` J ) ) )
21 20 rexlimdvw 
 |-  ( ph -> ( E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> k e. ( Clsd ` J ) ) )
22 21 abssdv 
 |-  ( ph -> { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } C_ ( Clsd ` J ) )
23 fvex 
 |-  ( Clsd ` J ) e. _V
24 23 elpw2 
 |-  ( { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } e. ~P ( Clsd ` J ) <-> { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } C_ ( Clsd ` J ) )
25 22 24 sylibr 
 |-  ( ph -> { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } e. ~P ( Clsd ` J ) )
26 elin 
 |-  ( r e. ( ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } i^i Fin ) <-> ( r e. ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } /\ r e. Fin ) )
27 velpw 
 |-  ( r e. ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } <-> r C_ { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } )
28 ssabral 
 |-  ( r C_ { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } <-> A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) )
29 27 28 bitri 
 |-  ( r e. ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } <-> A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) )
30 29 anbi1i 
 |-  ( ( r e. ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } /\ r e. Fin ) <-> ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) )
31 26 30 bitri 
 |-  ( r e. ( ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } i^i Fin ) <-> ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) )
32 raleq 
 |-  ( m = (/) -> ( A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> A. k e. (/) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
33 32 anbi2d 
 |-  ( m = (/) -> ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) <-> ( ph /\ A. k e. (/) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) ) )
34 inteq 
 |-  ( m = (/) -> |^| m = |^| (/) )
35 34 sseq2d 
 |-  ( m = (/) -> ( ( F " k ) C_ |^| m <-> ( F " k ) C_ |^| (/) ) )
36 35 rexbidv 
 |-  ( m = (/) -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| m <-> E. k e. ran ZZ>= ( F " k ) C_ |^| (/) ) )
37 33 36 imbi12d 
 |-  ( m = (/) -> ( ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| m ) <-> ( ( ph /\ A. k e. (/) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| (/) ) ) )
38 raleq 
 |-  ( m = y -> ( A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
39 38 anbi2d 
 |-  ( m = y -> ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) <-> ( ph /\ A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) ) )
40 inteq 
 |-  ( m = y -> |^| m = |^| y )
41 40 sseq2d 
 |-  ( m = y -> ( ( F " k ) C_ |^| m <-> ( F " k ) C_ |^| y ) )
42 41 rexbidv 
 |-  ( m = y -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| m <-> E. k e. ran ZZ>= ( F " k ) C_ |^| y ) )
43 39 42 imbi12d 
 |-  ( m = y -> ( ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| m ) <-> ( ( ph /\ A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| y ) ) )
44 raleq 
 |-  ( m = ( y u. { n } ) -> ( A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
45 44 anbi2d 
 |-  ( m = ( y u. { n } ) -> ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) <-> ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) ) )
46 inteq 
 |-  ( m = ( y u. { n } ) -> |^| m = |^| ( y u. { n } ) )
47 46 sseq2d 
 |-  ( m = ( y u. { n } ) -> ( ( F " k ) C_ |^| m <-> ( F " k ) C_ |^| ( y u. { n } ) ) )
48 47 rexbidv 
 |-  ( m = ( y u. { n } ) -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| m <-> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) )
49 45 48 imbi12d 
 |-  ( m = ( y u. { n } ) -> ( ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| m ) <-> ( ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) ) )
50 raleq 
 |-  ( m = r -> ( A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
51 50 anbi2d 
 |-  ( m = r -> ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) <-> ( ph /\ A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) ) )
52 inteq 
 |-  ( m = r -> |^| m = |^| r )
53 52 sseq2d 
 |-  ( m = r -> ( ( F " k ) C_ |^| m <-> ( F " k ) C_ |^| r ) )
54 53 rexbidv 
 |-  ( m = r -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| m <-> E. k e. ran ZZ>= ( F " k ) C_ |^| r ) )
55 51 54 imbi12d 
 |-  ( m = r -> ( ( ( ph /\ A. k e. m E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| m ) <-> ( ( ph /\ A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| r ) ) )
56 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
57 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
58 56 57 ax-mp 
 |-  ZZ>= Fn ZZ
59 0z 
 |-  0 e. ZZ
60 fnfvelrn 
 |-  ( ( ZZ>= Fn ZZ /\ 0 e. ZZ ) -> ( ZZ>= ` 0 ) e. ran ZZ>= )
61 58 59 60 mp2an 
 |-  ( ZZ>= ` 0 ) e. ran ZZ>=
62 ssv 
 |-  ( F " ( ZZ>= ` 0 ) ) C_ _V
63 int0 
 |-  |^| (/) = _V
64 62 63 sseqtrri 
 |-  ( F " ( ZZ>= ` 0 ) ) C_ |^| (/)
65 imaeq2 
 |-  ( k = ( ZZ>= ` 0 ) -> ( F " k ) = ( F " ( ZZ>= ` 0 ) ) )
66 65 sseq1d 
 |-  ( k = ( ZZ>= ` 0 ) -> ( ( F " k ) C_ |^| (/) <-> ( F " ( ZZ>= ` 0 ) ) C_ |^| (/) ) )
67 66 rspcev 
 |-  ( ( ( ZZ>= ` 0 ) e. ran ZZ>= /\ ( F " ( ZZ>= ` 0 ) ) C_ |^| (/) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| (/) )
68 61 64 67 mp2an 
 |-  E. k e. ran ZZ>= ( F " k ) C_ |^| (/)
69 68 a1i 
 |-  ( ( ph /\ A. k e. (/) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| (/) )
70 ssun1 
 |-  y C_ ( y u. { n } )
71 ssralv 
 |-  ( y C_ ( y u. { n } ) -> ( A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
72 70 71 ax-mp 
 |-  ( A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) )
73 72 anim2i 
 |-  ( ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> ( ph /\ A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
74 73 imim1i 
 |-  ( ( ( ph /\ A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| y ) -> ( ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| y ) )
75 ssun2 
 |-  { n } C_ ( y u. { n } )
76 ssralv 
 |-  ( { n } C_ ( y u. { n } ) -> ( A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> A. k e. { n } E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) )
77 75 76 ax-mp 
 |-  ( A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> A. k e. { n } E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) )
78 vex 
 |-  n e. _V
79 eqeq1 
 |-  ( k = n -> ( k = ( ( cls ` J ) ` ( F " u ) ) <-> n = ( ( cls ` J ) ` ( F " u ) ) ) )
80 79 rexbidv 
 |-  ( k = n -> ( E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> E. u e. ran ZZ>= n = ( ( cls ` J ) ` ( F " u ) ) ) )
81 78 80 ralsn 
 |-  ( A. k e. { n } E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> E. u e. ran ZZ>= n = ( ( cls ` J ) ` ( F " u ) ) )
82 77 81 sylib 
 |-  ( A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> E. u e. ran ZZ>= n = ( ( cls ` J ) ` ( F " u ) ) )
83 uzin2 
 |-  ( ( u e. ran ZZ>= /\ k e. ran ZZ>= ) -> ( u i^i k ) e. ran ZZ>= )
84 10 11 sstrid 
 |-  ( ph -> ( F " u ) C_ X )
85 84 13 sseqtrd 
 |-  ( ph -> ( F " u ) C_ U. J )
86 16 sscls 
 |-  ( ( J e. Top /\ ( F " u ) C_ U. J ) -> ( F " u ) C_ ( ( cls ` J ) ` ( F " u ) ) )
87 9 85 86 syl2anc 
 |-  ( ph -> ( F " u ) C_ ( ( cls ` J ) ` ( F " u ) ) )
88 sseq2 
 |-  ( n = ( ( cls ` J ) ` ( F " u ) ) -> ( ( F " u ) C_ n <-> ( F " u ) C_ ( ( cls ` J ) ` ( F " u ) ) ) )
89 87 88 syl5ibrcom 
 |-  ( ph -> ( n = ( ( cls ` J ) ` ( F " u ) ) -> ( F " u ) C_ n ) )
90 inss2 
 |-  ( u i^i k ) C_ k
91 inss1 
 |-  ( u i^i k ) C_ u
92 imass2 
 |-  ( ( u i^i k ) C_ k -> ( F " ( u i^i k ) ) C_ ( F " k ) )
93 imass2 
 |-  ( ( u i^i k ) C_ u -> ( F " ( u i^i k ) ) C_ ( F " u ) )
94 92 93 anim12i 
 |-  ( ( ( u i^i k ) C_ k /\ ( u i^i k ) C_ u ) -> ( ( F " ( u i^i k ) ) C_ ( F " k ) /\ ( F " ( u i^i k ) ) C_ ( F " u ) ) )
95 ssin 
 |-  ( ( ( F " ( u i^i k ) ) C_ ( F " k ) /\ ( F " ( u i^i k ) ) C_ ( F " u ) ) <-> ( F " ( u i^i k ) ) C_ ( ( F " k ) i^i ( F " u ) ) )
96 94 95 sylib 
 |-  ( ( ( u i^i k ) C_ k /\ ( u i^i k ) C_ u ) -> ( F " ( u i^i k ) ) C_ ( ( F " k ) i^i ( F " u ) ) )
97 90 91 96 mp2an 
 |-  ( F " ( u i^i k ) ) C_ ( ( F " k ) i^i ( F " u ) )
98 ss2in 
 |-  ( ( ( F " k ) C_ |^| y /\ ( F " u ) C_ n ) -> ( ( F " k ) i^i ( F " u ) ) C_ ( |^| y i^i n ) )
99 97 98 sstrid 
 |-  ( ( ( F " k ) C_ |^| y /\ ( F " u ) C_ n ) -> ( F " ( u i^i k ) ) C_ ( |^| y i^i n ) )
100 78 intunsn 
 |-  |^| ( y u. { n } ) = ( |^| y i^i n )
101 99 100 sseqtrrdi 
 |-  ( ( ( F " k ) C_ |^| y /\ ( F " u ) C_ n ) -> ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) )
102 101 expcom 
 |-  ( ( F " u ) C_ n -> ( ( F " k ) C_ |^| y -> ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) ) )
103 89 102 syl6 
 |-  ( ph -> ( n = ( ( cls ` J ) ` ( F " u ) ) -> ( ( F " k ) C_ |^| y -> ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) ) ) )
104 103 impd 
 |-  ( ph -> ( ( n = ( ( cls ` J ) ` ( F " u ) ) /\ ( F " k ) C_ |^| y ) -> ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) ) )
105 imaeq2 
 |-  ( m = ( u i^i k ) -> ( F " m ) = ( F " ( u i^i k ) ) )
106 105 sseq1d 
 |-  ( m = ( u i^i k ) -> ( ( F " m ) C_ |^| ( y u. { n } ) <-> ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) ) )
107 106 rspcev 
 |-  ( ( ( u i^i k ) e. ran ZZ>= /\ ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) ) -> E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) )
108 107 expcom 
 |-  ( ( F " ( u i^i k ) ) C_ |^| ( y u. { n } ) -> ( ( u i^i k ) e. ran ZZ>= -> E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) ) )
109 104 108 syl6 
 |-  ( ph -> ( ( n = ( ( cls ` J ) ` ( F " u ) ) /\ ( F " k ) C_ |^| y ) -> ( ( u i^i k ) e. ran ZZ>= -> E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) ) ) )
110 109 com23 
 |-  ( ph -> ( ( u i^i k ) e. ran ZZ>= -> ( ( n = ( ( cls ` J ) ` ( F " u ) ) /\ ( F " k ) C_ |^| y ) -> E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) ) ) )
111 83 110 syl5 
 |-  ( ph -> ( ( u e. ran ZZ>= /\ k e. ran ZZ>= ) -> ( ( n = ( ( cls ` J ) ` ( F " u ) ) /\ ( F " k ) C_ |^| y ) -> E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) ) ) )
112 111 rexlimdvv 
 |-  ( ph -> ( E. u e. ran ZZ>= E. k e. ran ZZ>= ( n = ( ( cls ` J ) ` ( F " u ) ) /\ ( F " k ) C_ |^| y ) -> E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) ) )
113 reeanv 
 |-  ( E. u e. ran ZZ>= E. k e. ran ZZ>= ( n = ( ( cls ` J ) ` ( F " u ) ) /\ ( F " k ) C_ |^| y ) <-> ( E. u e. ran ZZ>= n = ( ( cls ` J ) ` ( F " u ) ) /\ E. k e. ran ZZ>= ( F " k ) C_ |^| y ) )
114 imaeq2 
 |-  ( m = k -> ( F " m ) = ( F " k ) )
115 114 sseq1d 
 |-  ( m = k -> ( ( F " m ) C_ |^| ( y u. { n } ) <-> ( F " k ) C_ |^| ( y u. { n } ) ) )
116 115 cbvrexvw 
 |-  ( E. m e. ran ZZ>= ( F " m ) C_ |^| ( y u. { n } ) <-> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) )
117 112 113 116 3imtr3g 
 |-  ( ph -> ( ( E. u e. ran ZZ>= n = ( ( cls ` J ) ` ( F " u ) ) /\ E. k e. ran ZZ>= ( F " k ) C_ |^| y ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) )
118 117 expd 
 |-  ( ph -> ( E. u e. ran ZZ>= n = ( ( cls ` J ) ` ( F " u ) ) -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| y -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) ) )
119 82 118 syl5 
 |-  ( ph -> ( A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| y -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) ) )
120 119 imp 
 |-  ( ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| y -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) )
121 74 120 sylcom 
 |-  ( ( ( ph /\ A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| y ) -> ( ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) )
122 121 a1i 
 |-  ( y e. Fin -> ( ( ( ph /\ A. k e. y E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| y ) -> ( ( ph /\ A. k e. ( y u. { n } ) E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| ( y u. { n } ) ) ) )
123 37 43 49 55 69 122 findcard2 
 |-  ( r e. Fin -> ( ( ph /\ A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| r ) )
124 123 com12 
 |-  ( ( ph /\ A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) ) -> ( r e. Fin -> E. k e. ran ZZ>= ( F " k ) C_ |^| r ) )
125 124 impr 
 |-  ( ( ph /\ ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) ) -> E. k e. ran ZZ>= ( F " k ) C_ |^| r )
126 5 ffnd 
 |-  ( ph -> F Fn NN )
127 inss1 
 |-  ( k i^i NN ) C_ k
128 imass2 
 |-  ( ( k i^i NN ) C_ k -> ( F " ( k i^i NN ) ) C_ ( F " k ) )
129 127 128 ax-mp 
 |-  ( F " ( k i^i NN ) ) C_ ( F " k )
130 nnuz 
 |-  NN = ( ZZ>= ` 1 )
131 1z 
 |-  1 e. ZZ
132 fnfvelrn 
 |-  ( ( ZZ>= Fn ZZ /\ 1 e. ZZ ) -> ( ZZ>= ` 1 ) e. ran ZZ>= )
133 58 131 132 mp2an 
 |-  ( ZZ>= ` 1 ) e. ran ZZ>=
134 130 133 eqeltri 
 |-  NN e. ran ZZ>=
135 uzin2 
 |-  ( ( k e. ran ZZ>= /\ NN e. ran ZZ>= ) -> ( k i^i NN ) e. ran ZZ>= )
136 134 135 mpan2 
 |-  ( k e. ran ZZ>= -> ( k i^i NN ) e. ran ZZ>= )
137 uzn0 
 |-  ( ( k i^i NN ) e. ran ZZ>= -> ( k i^i NN ) =/= (/) )
138 136 137 syl 
 |-  ( k e. ran ZZ>= -> ( k i^i NN ) =/= (/) )
139 n0 
 |-  ( ( k i^i NN ) =/= (/) <-> E. y y e. ( k i^i NN ) )
140 138 139 sylib 
 |-  ( k e. ran ZZ>= -> E. y y e. ( k i^i NN ) )
141 fnfun 
 |-  ( F Fn NN -> Fun F )
142 inss2 
 |-  ( k i^i NN ) C_ NN
143 fndm 
 |-  ( F Fn NN -> dom F = NN )
144 142 143 sseqtrrid 
 |-  ( F Fn NN -> ( k i^i NN ) C_ dom F )
145 funfvima2 
 |-  ( ( Fun F /\ ( k i^i NN ) C_ dom F ) -> ( y e. ( k i^i NN ) -> ( F ` y ) e. ( F " ( k i^i NN ) ) ) )
146 141 144 145 syl2anc 
 |-  ( F Fn NN -> ( y e. ( k i^i NN ) -> ( F ` y ) e. ( F " ( k i^i NN ) ) ) )
147 ne0i 
 |-  ( ( F ` y ) e. ( F " ( k i^i NN ) ) -> ( F " ( k i^i NN ) ) =/= (/) )
148 146 147 syl6 
 |-  ( F Fn NN -> ( y e. ( k i^i NN ) -> ( F " ( k i^i NN ) ) =/= (/) ) )
149 148 exlimdv 
 |-  ( F Fn NN -> ( E. y y e. ( k i^i NN ) -> ( F " ( k i^i NN ) ) =/= (/) ) )
150 140 149 syl5 
 |-  ( F Fn NN -> ( k e. ran ZZ>= -> ( F " ( k i^i NN ) ) =/= (/) ) )
151 150 imp 
 |-  ( ( F Fn NN /\ k e. ran ZZ>= ) -> ( F " ( k i^i NN ) ) =/= (/) )
152 ssn0 
 |-  ( ( ( F " ( k i^i NN ) ) C_ ( F " k ) /\ ( F " ( k i^i NN ) ) =/= (/) ) -> ( F " k ) =/= (/) )
153 129 151 152 sylancr 
 |-  ( ( F Fn NN /\ k e. ran ZZ>= ) -> ( F " k ) =/= (/) )
154 ssn0 
 |-  ( ( ( F " k ) C_ |^| r /\ ( F " k ) =/= (/) ) -> |^| r =/= (/) )
155 154 expcom 
 |-  ( ( F " k ) =/= (/) -> ( ( F " k ) C_ |^| r -> |^| r =/= (/) ) )
156 153 155 syl 
 |-  ( ( F Fn NN /\ k e. ran ZZ>= ) -> ( ( F " k ) C_ |^| r -> |^| r =/= (/) ) )
157 156 rexlimdva 
 |-  ( F Fn NN -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| r -> |^| r =/= (/) ) )
158 126 157 syl 
 |-  ( ph -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| r -> |^| r =/= (/) ) )
159 158 adantr 
 |-  ( ( ph /\ ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) ) -> ( E. k e. ran ZZ>= ( F " k ) C_ |^| r -> |^| r =/= (/) ) )
160 125 159 mpd 
 |-  ( ( ph /\ ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) ) -> |^| r =/= (/) )
161 160 necomd 
 |-  ( ( ph /\ ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) ) -> (/) =/= |^| r )
162 161 neneqd 
 |-  ( ( ph /\ ( A. k e. r E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) /\ r e. Fin ) ) -> -. (/) = |^| r )
163 31 162 sylan2b 
 |-  ( ( ph /\ r e. ( ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } i^i Fin ) ) -> -. (/) = |^| r )
164 163 nrexdv 
 |-  ( ph -> -. E. r e. ( ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } i^i Fin ) (/) = |^| r )
165 0ex 
 |-  (/) e. _V
166 zex 
 |-  ZZ e. _V
167 166 pwex 
 |-  ~P ZZ e. _V
168 frn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ran ZZ>= C_ ~P ZZ )
169 56 168 ax-mp 
 |-  ran ZZ>= C_ ~P ZZ
170 167 169 ssexi 
 |-  ran ZZ>= e. _V
171 170 abrexex 
 |-  { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } e. _V
172 elfi 
 |-  ( ( (/) e. _V /\ { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } e. _V ) -> ( (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) <-> E. r e. ( ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } i^i Fin ) (/) = |^| r ) )
173 165 171 172 mp2an 
 |-  ( (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) <-> E. r e. ( ~P { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } i^i Fin ) (/) = |^| r )
174 164 173 sylnibr 
 |-  ( ph -> -. (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) )
175 cmptop 
 |-  ( J e. Comp -> J e. Top )
176 cmpfi 
 |-  ( J e. Top -> ( J e. Comp <-> A. m e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` m ) -> |^| m =/= (/) ) ) )
177 175 176 syl 
 |-  ( J e. Comp -> ( J e. Comp <-> A. m e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` m ) -> |^| m =/= (/) ) ) )
178 177 ibi 
 |-  ( J e. Comp -> A. m e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` m ) -> |^| m =/= (/) ) )
179 fveq2 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> ( fi ` m ) = ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) )
180 179 eleq2d 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> ( (/) e. ( fi ` m ) <-> (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) ) )
181 180 notbid 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> ( -. (/) e. ( fi ` m ) <-> -. (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) ) )
182 inteq 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> |^| m = |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } )
183 182 neeq1d 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> ( |^| m =/= (/) <-> |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } =/= (/) ) )
184 n0 
 |-  ( |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } =/= (/) <-> E. y y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } )
185 183 184 bitrdi 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> ( |^| m =/= (/) <-> E. y y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) )
186 181 185 imbi12d 
 |-  ( m = { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> ( ( -. (/) e. ( fi ` m ) -> |^| m =/= (/) ) <-> ( -. (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) -> E. y y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) ) )
187 186 rspccv 
 |-  ( A. m e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` m ) -> |^| m =/= (/) ) -> ( { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } e. ~P ( Clsd ` J ) -> ( -. (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) -> E. y y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) ) )
188 178 187 syl 
 |-  ( J e. Comp -> ( { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } e. ~P ( Clsd ` J ) -> ( -. (/) e. ( fi ` { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) -> E. y y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) ) )
189 3 25 174 188 syl3c 
 |-  ( ph -> E. y y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } )
190 lmrel 
 |-  Rel ( ~~>t ` J )
191 r19.23v 
 |-  ( A. u e. ran ZZ>= ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) <-> ( E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) )
192 191 albii 
 |-  ( A. k A. u e. ran ZZ>= ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) <-> A. k ( E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) )
193 fvex 
 |-  ( ( cls ` J ) ` ( F " u ) ) e. _V
194 eleq2 
 |-  ( k = ( ( cls ` J ) ` ( F " u ) ) -> ( y e. k <-> y e. ( ( cls ` J ) ` ( F " u ) ) ) )
195 193 194 ceqsalv 
 |-  ( A. k ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) <-> y e. ( ( cls ` J ) ` ( F " u ) ) )
196 195 ralbii 
 |-  ( A. u e. ran ZZ>= A. k ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) <-> A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) )
197 ralcom4 
 |-  ( A. u e. ran ZZ>= A. k ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) <-> A. k A. u e. ran ZZ>= ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) )
198 196 197 bitr3i 
 |-  ( A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) <-> A. k A. u e. ran ZZ>= ( k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) )
199 vex 
 |-  y e. _V
200 199 elintab 
 |-  ( y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } <-> A. k ( E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) -> y e. k ) )
201 192 198 200 3bitr4i 
 |-  ( A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) <-> y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } )
202 eqid 
 |-  ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " NN ) )
203 imaeq2 
 |-  ( u = NN -> ( F " u ) = ( F " NN ) )
204 203 fveq2d 
 |-  ( u = NN -> ( ( cls ` J ) ` ( F " u ) ) = ( ( cls ` J ) ` ( F " NN ) ) )
205 204 rspceeqv 
 |-  ( ( NN e. ran ZZ>= /\ ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " NN ) ) ) -> E. u e. ran ZZ>= ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " u ) ) )
206 134 202 205 mp2an 
 |-  E. u e. ran ZZ>= ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " u ) )
207 fvex 
 |-  ( ( cls ` J ) ` ( F " NN ) ) e. _V
208 eqeq1 
 |-  ( k = ( ( cls ` J ) ` ( F " NN ) ) -> ( k = ( ( cls ` J ) ` ( F " u ) ) <-> ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " u ) ) ) )
209 208 rexbidv 
 |-  ( k = ( ( cls ` J ) ` ( F " NN ) ) -> ( E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) <-> E. u e. ran ZZ>= ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " u ) ) ) )
210 207 209 elab 
 |-  ( ( ( cls ` J ) ` ( F " NN ) ) e. { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } <-> E. u e. ran ZZ>= ( ( cls ` J ) ` ( F " NN ) ) = ( ( cls ` J ) ` ( F " u ) ) )
211 206 210 mpbir 
 |-  ( ( cls ` J ) ` ( F " NN ) ) e. { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) }
212 intss1 
 |-  ( ( ( cls ` J ) ` ( F " NN ) ) e. { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } -> |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } C_ ( ( cls ` J ) ` ( F " NN ) ) )
213 211 212 ax-mp 
 |-  |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } C_ ( ( cls ` J ) ` ( F " NN ) )
214 imassrn 
 |-  ( F " NN ) C_ ran F
215 214 14 sstrid 
 |-  ( ph -> ( F " NN ) C_ U. J )
216 16 clsss3 
 |-  ( ( J e. Top /\ ( F " NN ) C_ U. J ) -> ( ( cls ` J ) ` ( F " NN ) ) C_ U. J )
217 9 215 216 syl2anc 
 |-  ( ph -> ( ( cls ` J ) ` ( F " NN ) ) C_ U. J )
218 217 13 sseqtrrd 
 |-  ( ph -> ( ( cls ` J ) ` ( F " NN ) ) C_ X )
219 213 218 sstrid 
 |-  ( ph -> |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } C_ X )
220 219 sselda 
 |-  ( ( ph /\ y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) -> y e. X )
221 201 220 sylan2b 
 |-  ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) -> y e. X )
222 1zzd 
 |-  ( ph -> 1 e. ZZ )
223 130 7 222 iscau3 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) ) ) )
224 4 223 mpbid 
 |-  ( ph -> ( F e. ( X ^pm CC ) /\ A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) ) )
225 224 simprd 
 |-  ( ph -> A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) )
226 simp3 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) -> A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y )
227 226 ralimi 
 |-  ( A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) -> A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y )
228 227 reximi 
 |-  ( E. m e. NN A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) -> E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y )
229 228 ralimi 
 |-  ( A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y ) -> A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y )
230 225 229 syl 
 |-  ( ph -> A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y )
231 230 adantr 
 |-  ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) -> A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y )
232 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
233 breq2 
 |-  ( y = ( r / 2 ) -> ( ( ( F ` k ) D ( F ` n ) ) < y <-> ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) ) )
234 233 2ralbidv 
 |-  ( y = ( r / 2 ) -> ( A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y <-> A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) ) )
235 234 rexbidv 
 |-  ( y = ( r / 2 ) -> ( E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y <-> E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) ) )
236 235 rspccva 
 |-  ( ( A. y e. RR+ E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < y /\ ( r / 2 ) e. RR+ ) -> E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) )
237 231 232 236 syl2an 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ r e. RR+ ) -> E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) )
238 5 ffund 
 |-  ( ph -> Fun F )
239 238 ad2antrr 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> Fun F )
240 9 ad2antrr 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> J e. Top )
241 imassrn 
 |-  ( F " ( ZZ>= ` m ) ) C_ ran F
242 241 14 sstrid 
 |-  ( ph -> ( F " ( ZZ>= ` m ) ) C_ U. J )
243 242 ad2antrr 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( F " ( ZZ>= ` m ) ) C_ U. J )
244 nnz 
 |-  ( m e. NN -> m e. ZZ )
245 fnfvelrn 
 |-  ( ( ZZ>= Fn ZZ /\ m e. ZZ ) -> ( ZZ>= ` m ) e. ran ZZ>= )
246 58 244 245 sylancr 
 |-  ( m e. NN -> ( ZZ>= ` m ) e. ran ZZ>= )
247 246 ad2antll 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( ZZ>= ` m ) e. ran ZZ>= )
248 simplr 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) )
249 imaeq2 
 |-  ( u = ( ZZ>= ` m ) -> ( F " u ) = ( F " ( ZZ>= ` m ) ) )
250 249 fveq2d 
 |-  ( u = ( ZZ>= ` m ) -> ( ( cls ` J ) ` ( F " u ) ) = ( ( cls ` J ) ` ( F " ( ZZ>= ` m ) ) ) )
251 250 eleq2d 
 |-  ( u = ( ZZ>= ` m ) -> ( y e. ( ( cls ` J ) ` ( F " u ) ) <-> y e. ( ( cls ` J ) ` ( F " ( ZZ>= ` m ) ) ) ) )
252 251 rspcv 
 |-  ( ( ZZ>= ` m ) e. ran ZZ>= -> ( A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) -> y e. ( ( cls ` J ) ` ( F " ( ZZ>= ` m ) ) ) ) )
253 247 248 252 sylc 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> y e. ( ( cls ` J ) ` ( F " ( ZZ>= ` m ) ) ) )
254 7 ad2antrr 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> D e. ( *Met ` X ) )
255 221 adantr 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> y e. X )
256 232 ad2antrl 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( r / 2 ) e. RR+ )
257 256 rpxrd 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( r / 2 ) e. RR* )
258 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ y e. X /\ ( r / 2 ) e. RR* ) -> ( y ( ball ` D ) ( r / 2 ) ) e. J )
259 254 255 257 258 syl3anc 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( y ( ball ` D ) ( r / 2 ) ) e. J )
260 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ y e. X /\ ( r / 2 ) e. RR+ ) -> y e. ( y ( ball ` D ) ( r / 2 ) ) )
261 254 255 256 260 syl3anc 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> y e. ( y ( ball ` D ) ( r / 2 ) ) )
262 16 clsndisj 
 |-  ( ( ( J e. Top /\ ( F " ( ZZ>= ` m ) ) C_ U. J /\ y e. ( ( cls ` J ) ` ( F " ( ZZ>= ` m ) ) ) ) /\ ( ( y ( ball ` D ) ( r / 2 ) ) e. J /\ y e. ( y ( ball ` D ) ( r / 2 ) ) ) ) -> ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) =/= (/) )
263 240 243 253 259 261 262 syl32anc 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) =/= (/) )
264 n0 
 |-  ( ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) =/= (/) <-> E. n n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) )
265 inss2 
 |-  ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) C_ ( F " ( ZZ>= ` m ) )
266 265 sseli 
 |-  ( n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) -> n e. ( F " ( ZZ>= ` m ) ) )
267 fvelima 
 |-  ( ( Fun F /\ n e. ( F " ( ZZ>= ` m ) ) ) -> E. k e. ( ZZ>= ` m ) ( F ` k ) = n )
268 266 267 sylan2 
 |-  ( ( Fun F /\ n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) ) -> E. k e. ( ZZ>= ` m ) ( F ` k ) = n )
269 inss1 
 |-  ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) C_ ( y ( ball ` D ) ( r / 2 ) )
270 269 sseli 
 |-  ( n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) -> n e. ( y ( ball ` D ) ( r / 2 ) ) )
271 270 adantl 
 |-  ( ( Fun F /\ n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) ) -> n e. ( y ( ball ` D ) ( r / 2 ) ) )
272 eleq1a 
 |-  ( n e. ( y ( ball ` D ) ( r / 2 ) ) -> ( ( F ` k ) = n -> ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
273 271 272 syl 
 |-  ( ( Fun F /\ n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) ) -> ( ( F ` k ) = n -> ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
274 273 reximdv 
 |-  ( ( Fun F /\ n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) ) -> ( E. k e. ( ZZ>= ` m ) ( F ` k ) = n -> E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
275 268 274 mpd 
 |-  ( ( Fun F /\ n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) ) -> E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) )
276 275 ex 
 |-  ( Fun F -> ( n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) -> E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
277 276 exlimdv 
 |-  ( Fun F -> ( E. n n e. ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) -> E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
278 264 277 syl5bi 
 |-  ( Fun F -> ( ( ( y ( ball ` D ) ( r / 2 ) ) i^i ( F " ( ZZ>= ` m ) ) ) =/= (/) -> E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
279 239 263 278 sylc 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) )
280 r19.29 
 |-  ( ( A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) -> E. k e. ( ZZ>= ` m ) ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) )
281 uznnssnn 
 |-  ( m e. NN -> ( ZZ>= ` m ) C_ NN )
282 281 ad2antll 
 |-  ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( ZZ>= ` m ) C_ NN )
283 simprlr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) )
284 7 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> D e. ( *Met ` X ) )
285 simplrl 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> r e. RR+ )
286 285 232 syl 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( r / 2 ) e. RR+ )
287 286 rpxrd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( r / 2 ) e. RR* )
288 simpllr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> y e. X )
289 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> F : NN --> X )
290 eluznn 
 |-  ( ( m e. NN /\ k e. ( ZZ>= ` m ) ) -> k e. NN )
291 290 ad2ant2lr 
 |-  ( ( ( r e. RR+ /\ m e. NN ) /\ ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) ) -> k e. NN )
292 291 ad2ant2lr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> k e. NN )
293 289 292 ffvelrnd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( F ` k ) e. X )
294 elbl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( r / 2 ) e. RR* ) /\ ( y e. X /\ ( F ` k ) e. X ) ) -> ( ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) <-> ( ( F ` k ) D y ) < ( r / 2 ) ) )
295 284 287 288 293 294 syl22anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) <-> ( ( F ` k ) D y ) < ( r / 2 ) ) )
296 283 295 mpbid 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( F ` k ) D y ) < ( r / 2 ) )
297 2 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> D e. ( Met ` X ) )
298 simprr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> n e. ( ZZ>= ` k ) )
299 eluznn 
 |-  ( ( k e. NN /\ n e. ( ZZ>= ` k ) ) -> n e. NN )
300 292 298 299 syl2anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> n e. NN )
301 289 300 ffvelrnd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( F ` n ) e. X )
302 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` n ) e. X ) -> ( ( F ` k ) D ( F ` n ) ) e. RR )
303 297 293 301 302 syl3anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( F ` k ) D ( F ` n ) ) e. RR )
304 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ y e. X ) -> ( ( F ` k ) D y ) e. RR )
305 297 293 288 304 syl3anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( F ` k ) D y ) e. RR )
306 286 rpred 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( r / 2 ) e. RR )
307 lt2add 
 |-  ( ( ( ( ( F ` k ) D ( F ` n ) ) e. RR /\ ( ( F ` k ) D y ) e. RR ) /\ ( ( r / 2 ) e. RR /\ ( r / 2 ) e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( ( F ` k ) D y ) < ( r / 2 ) ) -> ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < ( ( r / 2 ) + ( r / 2 ) ) ) )
308 303 305 306 306 307 syl22anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( ( F ` k ) D y ) < ( r / 2 ) ) -> ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < ( ( r / 2 ) + ( r / 2 ) ) ) )
309 296 308 mpan2d 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < ( ( r / 2 ) + ( r / 2 ) ) ) )
310 285 rpcnd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> r e. CC )
311 310 2halvesd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( r / 2 ) + ( r / 2 ) ) = r )
312 311 breq2d 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < ( ( r / 2 ) + ( r / 2 ) ) <-> ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < r ) )
313 309 312 sylibd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < r ) )
314 mettri2 
 |-  ( ( D e. ( Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` n ) e. X /\ y e. X ) ) -> ( ( F ` n ) D y ) <_ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) )
315 297 293 301 288 314 syl13anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( F ` n ) D y ) <_ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) )
316 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` n ) e. X /\ y e. X ) -> ( ( F ` n ) D y ) e. RR )
317 297 301 288 316 syl3anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( F ` n ) D y ) e. RR )
318 303 305 readdcld 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) e. RR )
319 285 rpred 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> r e. RR )
320 lelttr 
 |-  ( ( ( ( F ` n ) D y ) e. RR /\ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) e. RR /\ r e. RR ) -> ( ( ( ( F ` n ) D y ) <_ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) /\ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < r ) -> ( ( F ` n ) D y ) < r ) )
321 317 318 319 320 syl3anc 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( ( F ` n ) D y ) <_ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) /\ ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < r ) -> ( ( F ` n ) D y ) < r ) )
322 315 321 mpand 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( ( F ` k ) D ( F ` n ) ) + ( ( F ` k ) D y ) ) < r -> ( ( F ` n ) D y ) < r ) )
323 313 322 syld 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) /\ n e. ( ZZ>= ` k ) ) ) -> ( ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> ( ( F ` n ) D y ) < r ) )
324 323 anassrs 
 |-  ( ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) ) /\ n e. ( ZZ>= ` k ) ) -> ( ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> ( ( F ` n ) D y ) < r ) )
325 324 ralimdva 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ ( k e. ( ZZ>= ` m ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) ) -> ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
326 325 expr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ k e. ( ZZ>= ` m ) ) -> ( ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) -> ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) ) )
327 326 com23 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ k e. ( ZZ>= ` m ) ) -> ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> ( ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) -> A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) ) )
328 327 impd 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) /\ k e. ( ZZ>= ` m ) ) -> ( ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) -> A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
329 328 reximdva 
 |-  ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( E. k e. ( ZZ>= ` m ) ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) -> E. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
330 ssrexv 
 |-  ( ( ZZ>= ` m ) C_ NN -> ( E. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
331 282 329 330 sylsyld 
 |-  ( ( ( ph /\ y e. X ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( E. k e. ( ZZ>= ` m ) ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
332 221 331 syldanl 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( E. k e. ( ZZ>= ` m ) ( A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
333 280 332 syl5 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( ( A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) /\ E. k e. ( ZZ>= ` m ) ( F ` k ) e. ( y ( ball ` D ) ( r / 2 ) ) ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
334 279 333 mpan2d 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ ( r e. RR+ /\ m e. NN ) ) -> ( A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
335 334 anassrs 
 |-  ( ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ r e. RR+ ) /\ m e. NN ) -> ( A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
336 335 rexlimdva 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ r e. RR+ ) -> ( E. m e. NN A. k e. ( ZZ>= ` m ) A. n e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` n ) ) < ( r / 2 ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) )
337 237 336 mpd 
 |-  ( ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) /\ r e. RR+ ) -> E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r )
338 337 ralrimiva 
 |-  ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) -> A. r e. RR+ E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r )
339 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( F ` n ) )
340 1 7 130 222 339 5 lmmbrf 
 |-  ( ph -> ( F ( ~~>t ` J ) y <-> ( y e. X /\ A. r e. RR+ E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) ) )
341 340 adantr 
 |-  ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) -> ( F ( ~~>t ` J ) y <-> ( y e. X /\ A. r e. RR+ E. k e. NN A. n e. ( ZZ>= ` k ) ( ( F ` n ) D y ) < r ) ) )
342 221 338 341 mpbir2and 
 |-  ( ( ph /\ A. u e. ran ZZ>= y e. ( ( cls ` J ) ` ( F " u ) ) ) -> F ( ~~>t ` J ) y )
343 201 342 sylan2br 
 |-  ( ( ph /\ y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) -> F ( ~~>t ` J ) y )
344 releldm 
 |-  ( ( Rel ( ~~>t ` J ) /\ F ( ~~>t ` J ) y ) -> F e. dom ( ~~>t ` J ) )
345 190 343 344 sylancr 
 |-  ( ( ph /\ y e. |^| { k | E. u e. ran ZZ>= k = ( ( cls ` J ) ` ( F " u ) ) } ) -> F e. dom ( ~~>t ` J ) )
346 189 345 exlimddv 
 |-  ( ph -> F e. dom ( ~~>t ` J ) )