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 syl5eq
 |-  ( ( ( ( ( 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 ffvelrn
 |-  ( ( 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 syl5eq
 |-  ( ( ( ( ( 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 ) ) )