Metamath Proof Explorer

Theorem sstotbnd2

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 
|- N = ( M |` ( Y X. Y ) )
Assertion sstotbnd2 
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )

Proof

Step Hyp Ref Expression
1 sstotbnd.2 
 |-  N = ( M |` ( Y X. Y ) )
2 metres2 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( M |` ( Y X. Y ) ) e. ( Met ` Y ) )
3 1 2 eqeltrid 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> N e. ( Met ` Y ) )
4 istotbnd3 
 |-  ( N e. ( TotBnd ` Y ) <-> ( N e. ( Met ` Y ) /\ A. d e. RR+ E. v e. ( ~P Y i^i Fin ) U_ x e. v ( x ( ball ` N ) d ) = Y ) )
5 4 baib 
 |-  ( N e. ( Met ` Y ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ( ~P Y i^i Fin ) U_ x e. v ( x ( ball ` N ) d ) = Y ) )
6 3 5 syl 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ( ~P Y i^i Fin ) U_ x e. v ( x ( ball ` N ) d ) = Y ) )
7 simpllr 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> Y C_ X )
8 7 sspwd 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> ~P Y C_ ~P X )
9 8 ssrind 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> ( ~P Y i^i Fin ) C_ ( ~P X i^i Fin ) )
10 simprl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> v e. ( ~P Y i^i Fin ) )
11 9 10 sseldd 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> v e. ( ~P X i^i Fin ) )
12 simprr 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> U_ x e. v ( x ( ball ` N ) d ) = Y )
13 metxmet 
 |-  ( M e. ( Met ` X ) -> M e. ( *Met ` X ) )
14 13 ad4antr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> M e. ( *Met ` X ) )
15 elfpw 
 |-  ( v e. ( ~P Y i^i Fin ) <-> ( v C_ Y /\ v e. Fin ) )
16 15 simplbi 
 |-  ( v e. ( ~P Y i^i Fin ) -> v C_ Y )
17 16 adantl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) -> v C_ Y )
18 17 sselda 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> x e. Y )
19 simp-4r 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> Y C_ X )
20 sseqin2 
 |-  ( Y C_ X <-> ( X i^i Y ) = Y )
21 19 20 sylib 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> ( X i^i Y ) = Y )
22 18 21 eleqtrrd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> x e. ( X i^i Y ) )
23 simpllr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> d e. RR+ )
24 23 rpxrd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> d e. RR* )
25 1 blres 
 |-  ( ( M e. ( *Met ` X ) /\ x e. ( X i^i Y ) /\ d e. RR* ) -> ( x ( ball ` N ) d ) = ( ( x ( ball ` M ) d ) i^i Y ) )
26 14 22 24 25 syl3anc 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> ( x ( ball ` N ) d ) = ( ( x ( ball ` M ) d ) i^i Y ) )
27 inss1 
 |-  ( ( x ( ball ` M ) d ) i^i Y ) C_ ( x ( ball ` M ) d )
28 26 27 eqsstrdi 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) /\ x e. v ) -> ( x ( ball ` N ) d ) C_ ( x ( ball ` M ) d ) )
29 28 ralrimiva 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) -> A. x e. v ( x ( ball ` N ) d ) C_ ( x ( ball ` M ) d ) )
30 ss2iun 
 |-  ( A. x e. v ( x ( ball ` N ) d ) C_ ( x ( ball ` M ) d ) -> U_ x e. v ( x ( ball ` N ) d ) C_ U_ x e. v ( x ( ball ` M ) d ) )
31 29 30 syl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ v e. ( ~P Y i^i Fin ) ) -> U_ x e. v ( x ( ball ` N ) d ) C_ U_ x e. v ( x ( ball ` M ) d ) )
32 31 adantrr 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> U_ x e. v ( x ( ball ` N ) d ) C_ U_ x e. v ( x ( ball ` M ) d ) )
33 12 32 eqsstrrd 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> Y C_ U_ x e. v ( x ( ball ` M ) d ) )
34 11 33 jca 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) /\ ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) ) -> ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )
35 34 ex 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) -> ( ( v e. ( ~P Y i^i Fin ) /\ U_ x e. v ( x ( ball ` N ) d ) = Y ) -> ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) d ) ) ) )
36 35 reximdv2 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ d e. RR+ ) -> ( E. v e. ( ~P Y i^i Fin ) U_ x e. v ( x ( ball ` N ) d ) = Y -> E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )
37 36 ralimdva 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. v e. ( ~P Y i^i Fin ) U_ x e. v ( x ( ball ` N ) d ) = Y -> A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )
38 6 37 sylbid 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) -> A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )
39 simpr 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) -> c e. RR+ )
40 39 rphalfcld 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) -> ( c / 2 ) e. RR+ )
41 oveq2 
 |-  ( d = ( c / 2 ) -> ( x ( ball ` M ) d ) = ( x ( ball ` M ) ( c / 2 ) ) )
42 41 iuneq2d 
 |-  ( d = ( c / 2 ) -> U_ x e. v ( x ( ball ` M ) d ) = U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) )
43 42 sseq2d 
 |-  ( d = ( c / 2 ) -> ( Y C_ U_ x e. v ( x ( ball ` M ) d ) <-> Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) )
44 43 rexbidv 
 |-  ( d = ( c / 2 ) -> ( E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) <-> E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) )
45 44 rspcv 
 |-  ( ( c / 2 ) e. RR+ -> ( A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) )
46 40 45 syl 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) -> ( A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) )
47 elfpw 
 |-  ( v e. ( ~P X i^i Fin ) <-> ( v C_ X /\ v e. Fin ) )
48 47 simprbi 
 |-  ( v e. ( ~P X i^i Fin ) -> v e. Fin )
49 48 ad2antrl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> v e. Fin )
50 ssrab2 
 |-  { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } C_ v
51 ssfi 
 |-  ( ( v e. Fin /\ { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } C_ v ) -> { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } e. Fin )
52 49 50 51 sylancl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } e. Fin )
53 oveq1 
 |-  ( x = y -> ( x ( ball ` M ) ( c / 2 ) ) = ( y ( ball ` M ) ( c / 2 ) ) )
54 53 ineq1d 
 |-  ( x = y -> ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) = ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) )
55 incom 
 |-  ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = ( Y i^i ( y ( ball ` M ) ( c / 2 ) ) )
56 54 55 eqtrdi 
 |-  ( x = y -> ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) = ( Y i^i ( y ( ball ` M ) ( c / 2 ) ) ) )
57 dfin5 
 |-  ( Y i^i ( y ( ball ` M ) ( c / 2 ) ) ) = { z e. Y | z e. ( y ( ball ` M ) ( c / 2 ) ) }
58 56 57 eqtrdi 
 |-  ( x = y -> ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) = { z e. Y | z e. ( y ( ball ` M ) ( c / 2 ) ) } )
59 58 neeq1d 
 |-  ( x = y -> ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) <-> { z e. Y | z e. ( y ( ball ` M ) ( c / 2 ) ) } =/= (/) ) )
60 rabn0 
 |-  ( { z e. Y | z e. ( y ( ball ` M ) ( c / 2 ) ) } =/= (/) <-> E. z e. Y z e. ( y ( ball ` M ) ( c / 2 ) ) )
61 59 60 bitrdi 
 |-  ( x = y -> ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) <-> E. z e. Y z e. ( y ( ball ` M ) ( c / 2 ) ) ) )
62 61 elrab 
 |-  ( y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } <-> ( y e. v /\ E. z e. Y z e. ( y ( ball ` M ) ( c / 2 ) ) ) )
63 62 simprbi 
 |-  ( y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } -> E. z e. Y z e. ( y ( ball ` M ) ( c / 2 ) ) )
64 63 rgen 
 |-  A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } E. z e. Y z e. ( y ( ball ` M ) ( c / 2 ) )
65 eleq1 
 |-  ( z = ( f ` y ) -> ( z e. ( y ( ball ` M ) ( c / 2 ) ) <-> ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) )
66 65 ac6sfi 
 |-  ( ( { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } e. Fin /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } E. z e. Y z e. ( y ( ball ` M ) ( c / 2 ) ) ) -> E. f ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) )
67 52 64 66 sylancl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> E. f ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) )
68 fdm 
 |-  ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y -> dom f = { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } )
69 68 ad2antrl 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> dom f = { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } )
70 69 50 eqsstrdi 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> dom f C_ v )
71 simprl 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y )
72 69 feq2d 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( f : dom f --> Y <-> f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y ) )
73 71 72 mpbird 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> f : dom f --> Y )
74 simprr 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) )
75 ffn 
 |-  ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y -> f Fn { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } )
76 elpreima 
 |-  ( f Fn { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } -> ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> ( y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } /\ ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) )
77 75 76 syl 
 |-  ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y -> ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> ( y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } /\ ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) )
78 77 baibd 
 |-  ( ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ) -> ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) )
79 78 ralbidva 
 |-  ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y -> ( A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) )
80 79 ad2antrl 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) )
81 74 80 mpbird 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) )
82 id 
 |-  ( y = x -> y = x )
83 oveq1 
 |-  ( y = x -> ( y ( ball ` M ) ( c / 2 ) ) = ( x ( ball ` M ) ( c / 2 ) ) )
84 83 imaeq2d 
 |-  ( y = x -> ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) = ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) )
85 82 84 eleq12d 
 |-  ( y = x -> ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) )
86 85 ralrab2 
 |-  ( A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) )
87 81 86 sylib 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) )
88 70 73 87 3jca 
 |-  ( ( v e. Fin /\ ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) )
89 88 ex 
 |-  ( v e. Fin -> ( ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) -> ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) )
90 49 89 syl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) -> ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) )
91 simpr2 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> f : dom f --> Y )
92 91 frnd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> ran f C_ Y )
93 91 ffnd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> f Fn dom f )
94 49 adantr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> v e. Fin )
95 simpr1 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> dom f C_ v )
96 ssfi 
 |-  ( ( v e. Fin /\ dom f C_ v ) -> dom f e. Fin )
97 94 95 96 syl2anc 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> dom f e. Fin )
98 fnfi 
 |-  ( ( f Fn dom f /\ dom f e. Fin ) -> f e. Fin )
99 93 97 98 syl2anc 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> f e. Fin )
100 rnfi 
 |-  ( f e. Fin -> ran f e. Fin )
101 99 100 syl 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> ran f e. Fin )
102 elfpw 
 |-  ( ran f e. ( ~P Y i^i Fin ) <-> ( ran f C_ Y /\ ran f e. Fin ) )
103 92 101 102 sylanbrc 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> ran f e. ( ~P Y i^i Fin ) )
104 oveq1 
 |-  ( x = z -> ( x ( ball ` N ) c ) = ( z ( ball ` N ) c ) )
105 104 cbviunv 
 |-  U_ x e. ran f ( x ( ball ` N ) c ) = U_ z e. ran f ( z ( ball ` N ) c )
106 3 ad4antr 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ z e. ran f ) -> N e. ( Met ` Y ) )
107 metxmet 
 |-  ( N e. ( Met ` Y ) -> N e. ( *Met ` Y ) )
108 106 107 syl 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ z e. ran f ) -> N e. ( *Met ` Y ) )
109 92 sselda 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ z e. ran f ) -> z e. Y )
110 rpxr 
 |-  ( c e. RR+ -> c e. RR* )
111 110 ad4antlr 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ z e. ran f ) -> c e. RR* )
112 blssm 
 |-  ( ( N e. ( *Met ` Y ) /\ z e. Y /\ c e. RR* ) -> ( z ( ball ` N ) c ) C_ Y )
113 108 109 111 112 syl3anc 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ z e. ran f ) -> ( z ( ball ` N ) c ) C_ Y )
114 113 ralrimiva 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> A. z e. ran f ( z ( ball ` N ) c ) C_ Y )
115 iunss 
 |-  ( U_ z e. ran f ( z ( ball ` N ) c ) C_ Y <-> A. z e. ran f ( z ( ball ` N ) c ) C_ Y )
116 114 115 sylibr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> U_ z e. ran f ( z ( ball ` N ) c ) C_ Y )
117 iunin1 
 |-  U_ y e. v ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = ( U_ y e. v ( y ( ball ` M ) ( c / 2 ) ) i^i Y )
118 simplrr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) )
119 53 cbviunv 
 |-  U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) = U_ y e. v ( y ( ball ` M ) ( c / 2 ) )
120 118 119 sseqtrdi 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> Y C_ U_ y e. v ( y ( ball ` M ) ( c / 2 ) ) )
121 sseqin2 
 |-  ( Y C_ U_ y e. v ( y ( ball ` M ) ( c / 2 ) ) <-> ( U_ y e. v ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = Y )
122 120 121 sylib 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> ( U_ y e. v ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = Y )
123 117 122 eqtrid 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> U_ y e. v ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = Y )
124 0ss 
 |-  (/) C_ U_ z e. ran f ( z ( ball ` N ) c )
125 sseq1 
 |-  ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = (/) -> ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) <-> (/) C_ U_ z e. ran f ( z ( ball ` N ) c ) ) )
126 124 125 mpbiri 
 |-  ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = (/) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
127 126 a1i 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. v ) -> ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) = (/) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) ) )
128 simpr3 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) )
129 54 neeq1d 
 |-  ( x = y -> ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) <-> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) ) )
130 id 
 |-  ( x = y -> x = y )
131 53 imaeq2d 
 |-  ( x = y -> ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) = ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) )
132 130 131 eleq12d 
 |-  ( x = y -> ( x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) <-> y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) )
133 129 132 imbi12d 
 |-  ( x = y -> ( ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) <-> ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) ) )
134 133 rspccva 
 |-  ( ( A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ y e. v ) -> ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) )
135 128 134 sylan 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. v ) -> ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) )
136 13 ad5antr 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> M e. ( *Met ` X ) )
137 cnvimass 
 |-  ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) C_ dom f
138 47 simplbi 
 |-  ( v e. ( ~P X i^i Fin ) -> v C_ X )
139 138 ad2antrl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> v C_ X )
140 139 adantr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> v C_ X )
141 95 140 sstrd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> dom f C_ X )
142 137 141 sstrid 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) C_ X )
143 142 sselda 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> y e. X )
144 simp-4r 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> c e. RR+ )
145 144 rpred 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> c e. RR )
146 elpreima 
 |-  ( f Fn dom f -> ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) <-> ( y e. dom f /\ ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) )
147 146 simplbda 
 |-  ( ( f Fn dom f /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) )
148 93 147 sylan 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) )
149 blhalf 
 |-  ( ( ( M e. ( *Met ` X ) /\ y e. X ) /\ ( c e. RR /\ ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( y ( ball ` M ) ( c / 2 ) ) C_ ( ( f ` y ) ( ball ` M ) c ) )
150 136 143 145 148 149 syl22anc 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( y ( ball ` M ) ( c / 2 ) ) C_ ( ( f ` y ) ( ball ` M ) c ) )
151 150 ssrind 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ ( ( ( f ` y ) ( ball ` M ) c ) i^i Y ) )
152 137 sseli 
 |-  ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) -> y e. dom f )
153 ffvelcdm 
 |-  ( ( f : dom f --> Y /\ y e. dom f ) -> ( f ` y ) e. Y )
154 91 152 153 syl2an 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( f ` y ) e. Y )
155 simp-5r 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> Y C_ X )
156 155 20 sylib 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( X i^i Y ) = Y )
157 154 156 eleqtrrd 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( f ` y ) e. ( X i^i Y ) )
158 110 ad4antlr 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> c e. RR* )
159 1 blres 
 |-  ( ( M e. ( *Met ` X ) /\ ( f ` y ) e. ( X i^i Y ) /\ c e. RR* ) -> ( ( f ` y ) ( ball ` N ) c ) = ( ( ( f ` y ) ( ball ` M ) c ) i^i Y ) )
160 136 157 158 159 syl3anc 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( f ` y ) ( ball ` N ) c ) = ( ( ( f ` y ) ( ball ` M ) c ) i^i Y ) )
161 151 160 sseqtrrd 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ ( ( f ` y ) ( ball ` N ) c ) )
162 fnfvelrn 
 |-  ( ( f Fn dom f /\ y e. dom f ) -> ( f ` y ) e. ran f )
163 93 152 162 syl2an 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( f ` y ) e. ran f )
164 oveq1 
 |-  ( z = ( f ` y ) -> ( z ( ball ` N ) c ) = ( ( f ` y ) ( ball ` N ) c ) )
165 164 ssiun2s 
 |-  ( ( f ` y ) e. ran f -> ( ( f ` y ) ( ball ` N ) c ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
166 163 165 syl 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( f ` y ) ( ball ` N ) c ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
167 161 166 sstrd 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
168 167 adantlr 
 |-  ( ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. v ) /\ y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
169 168 ex 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. v ) -> ( y e. ( `' f " ( y ( ball ` M ) ( c / 2 ) ) ) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) ) )
170 135 169 syld 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. v ) -> ( ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) ) )
171 127 170 pm2.61dne 
 |-  ( ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) /\ y e. v ) -> ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
172 171 ralrimiva 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> A. y e. v ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
173 iunss 
 |-  ( U_ y e. v ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) <-> A. y e. v ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
174 172 173 sylibr 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> U_ y e. v ( ( y ( ball ` M ) ( c / 2 ) ) i^i Y ) C_ U_ z e. ran f ( z ( ball ` N ) c ) )
175 123 174 eqsstrrd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> Y C_ U_ z e. ran f ( z ( ball ` N ) c ) )
176 116 175 eqssd 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> U_ z e. ran f ( z ( ball ` N ) c ) = Y )
177 105 176 eqtrid 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> U_ x e. ran f ( x ( ball ` N ) c ) = Y )
178 iuneq1 
 |-  ( w = ran f -> U_ x e. w ( x ( ball ` N ) c ) = U_ x e. ran f ( x ( ball ` N ) c ) )
179 178 eqeq1d 
 |-  ( w = ran f -> ( U_ x e. w ( x ( ball ` N ) c ) = Y <-> U_ x e. ran f ( x ( ball ` N ) c ) = Y ) )
180 179 rspcev 
 |-  ( ( ran f e. ( ~P Y i^i Fin ) /\ U_ x e. ran f ( x ( ball ` N ) c ) = Y ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y )
181 103 177 180 syl2anc 
 |-  ( ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) /\ ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y )
182 181 ex 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( dom f C_ v /\ f : dom f --> Y /\ A. x e. v ( ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) -> x e. ( `' f " ( x ( ball ` M ) ( c / 2 ) ) ) ) ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
183 90 182 syld 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> ( ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
184 183 exlimdv 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> ( E. f ( f : { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } --> Y /\ A. y e. { x e. v | ( ( x ( ball ` M ) ( c / 2 ) ) i^i Y ) =/= (/) } ( f ` y ) e. ( y ( ball ` M ) ( c / 2 ) ) ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
185 67 184 mpd 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) /\ ( v e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) ) ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y )
186 185 rexlimdvaa 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) -> ( E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) ( c / 2 ) ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
187 46 186 syld 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ c e. RR+ ) -> ( A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
188 187 ralrimdva 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> A. c e. RR+ E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
189 istotbnd3 
 |-  ( N e. ( TotBnd ` Y ) <-> ( N e. ( Met ` Y ) /\ A. c e. RR+ E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
190 189 baib 
 |-  ( N e. ( Met ` Y ) -> ( N e. ( TotBnd ` Y ) <-> A. c e. RR+ E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
191 3 190 syl 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. c e. RR+ E. w e. ( ~P Y i^i Fin ) U_ x e. w ( x ( ball ` N ) c ) = Y ) )
192 188 191 sylibrd 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) -> N e. ( TotBnd ` Y ) ) )
193 38 192 impbid 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )