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