Step |
Hyp |
Ref |
Expression |
1 |
|
sstotbnd.2 |
|- N = ( M |` ( Y X. Y ) ) |
2 |
1
|
sstotbnd2 |
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) |
3 |
|
elfpw |
|- ( u e. ( ~P X i^i Fin ) <-> ( u C_ X /\ u e. Fin ) ) |
4 |
3
|
simprbi |
|- ( u e. ( ~P X i^i Fin ) -> u e. Fin ) |
5 |
|
mptfi |
|- ( u e. Fin -> ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin ) |
6 |
|
rnfi |
|- ( ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin ) |
7 |
4 5 6
|
3syl |
|- ( u e. ( ~P X i^i Fin ) -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin ) |
8 |
7
|
ad2antrl |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin ) |
9 |
|
simprr |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> Y C_ U_ x e. u ( x ( ball ` M ) d ) ) |
10 |
|
eqid |
|- ( x e. u |-> ( x ( ball ` M ) d ) ) = ( x e. u |-> ( x ( ball ` M ) d ) ) |
11 |
10
|
rnmpt |
|- ran ( x e. u |-> ( x ( ball ` M ) d ) ) = { b | E. x e. u b = ( x ( ball ` M ) d ) } |
12 |
3
|
simplbi |
|- ( u e. ( ~P X i^i Fin ) -> u C_ X ) |
13 |
|
ssrexv |
|- ( u C_ X -> ( E. x e. u b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) ) |
14 |
12 13
|
syl |
|- ( u e. ( ~P X i^i Fin ) -> ( E. x e. u b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) ) |
15 |
14
|
ad2antrl |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> ( E. x e. u b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) ) |
16 |
15
|
ss2abdv |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> { b | E. x e. u b = ( x ( ball ` M ) d ) } C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) |
17 |
11 16
|
eqsstrid |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) |
18 |
|
unieq |
|- ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> U. v = U. ran ( x e. u |-> ( x ( ball ` M ) d ) ) ) |
19 |
|
ovex |
|- ( x ( ball ` M ) d ) e. _V |
20 |
19
|
dfiun3 |
|- U_ x e. u ( x ( ball ` M ) d ) = U. ran ( x e. u |-> ( x ( ball ` M ) d ) ) |
21 |
18 20
|
eqtr4di |
|- ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> U. v = U_ x e. u ( x ( ball ` M ) d ) ) |
22 |
21
|
sseq2d |
|- ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( Y C_ U. v <-> Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) |
23 |
|
ssabral |
|- ( v C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } <-> A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) |
24 |
|
sseq1 |
|- ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( v C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } <-> ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) |
25 |
23 24
|
bitr3id |
|- ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( A. b e. v E. x e. X b = ( x ( ball ` M ) d ) <-> ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) |
26 |
22 25
|
anbi12d |
|- ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) <-> ( Y C_ U_ x e. u ( x ( ball ` M ) d ) /\ ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) ) |
27 |
26
|
rspcev |
|- ( ( ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin /\ ( Y C_ U_ x e. u ( x ( ball ` M ) d ) /\ ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) -> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) |
28 |
8 9 17 27
|
syl12anc |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) |
29 |
28
|
rexlimdvaa |
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) -> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) |
30 |
|
oveq1 |
|- ( x = ( f ` b ) -> ( x ( ball ` M ) d ) = ( ( f ` b ) ( ball ` M ) d ) ) |
31 |
30
|
eqeq2d |
|- ( x = ( f ` b ) -> ( b = ( x ( ball ` M ) d ) <-> b = ( ( f ` b ) ( ball ` M ) d ) ) ) |
32 |
31
|
ac6sfi |
|- ( ( v e. Fin /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> E. f ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) |
33 |
32
|
adantrl |
|- ( ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) -> E. f ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) |
34 |
33
|
adantl |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) -> E. f ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) |
35 |
|
frn |
|- ( f : v --> X -> ran f C_ X ) |
36 |
35
|
ad2antrl |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> ran f C_ X ) |
37 |
|
simplrl |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> v e. Fin ) |
38 |
|
ffn |
|- ( f : v --> X -> f Fn v ) |
39 |
38
|
ad2antrl |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> f Fn v ) |
40 |
|
dffn4 |
|- ( f Fn v <-> f : v -onto-> ran f ) |
41 |
39 40
|
sylib |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> f : v -onto-> ran f ) |
42 |
|
fofi |
|- ( ( v e. Fin /\ f : v -onto-> ran f ) -> ran f e. Fin ) |
43 |
37 41 42
|
syl2anc |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> ran f e. Fin ) |
44 |
|
elfpw |
|- ( ran f e. ( ~P X i^i Fin ) <-> ( ran f C_ X /\ ran f e. Fin ) ) |
45 |
36 43 44
|
sylanbrc |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> ran f e. ( ~P X i^i Fin ) ) |
46 |
|
simprrl |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) -> Y C_ U. v ) |
47 |
46
|
adantr |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> Y C_ U. v ) |
48 |
|
uniiun |
|- U. v = U_ b e. v b |
49 |
|
iuneq2 |
|- ( A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) -> U_ b e. v b = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) |
50 |
48 49
|
syl5eq |
|- ( A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) -> U. v = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) |
51 |
50
|
ad2antll |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> U. v = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) |
52 |
47 51
|
sseqtrd |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> Y C_ U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) |
53 |
30
|
eleq2d |
|- ( x = ( f ` b ) -> ( y e. ( x ( ball ` M ) d ) <-> y e. ( ( f ` b ) ( ball ` M ) d ) ) ) |
54 |
53
|
rexrn |
|- ( f Fn v -> ( E. x e. ran f y e. ( x ( ball ` M ) d ) <-> E. b e. v y e. ( ( f ` b ) ( ball ` M ) d ) ) ) |
55 |
|
eliun |
|- ( y e. U_ x e. ran f ( x ( ball ` M ) d ) <-> E. x e. ran f y e. ( x ( ball ` M ) d ) ) |
56 |
|
eliun |
|- ( y e. U_ b e. v ( ( f ` b ) ( ball ` M ) d ) <-> E. b e. v y e. ( ( f ` b ) ( ball ` M ) d ) ) |
57 |
54 55 56
|
3bitr4g |
|- ( f Fn v -> ( y e. U_ x e. ran f ( x ( ball ` M ) d ) <-> y e. U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) ) |
58 |
57
|
eqrdv |
|- ( f Fn v -> U_ x e. ran f ( x ( ball ` M ) d ) = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) |
59 |
39 58
|
syl |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> U_ x e. ran f ( x ( ball ` M ) d ) = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) |
60 |
52 59
|
sseqtrrd |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> Y C_ U_ x e. ran f ( x ( ball ` M ) d ) ) |
61 |
|
iuneq1 |
|- ( u = ran f -> U_ x e. u ( x ( ball ` M ) d ) = U_ x e. ran f ( x ( ball ` M ) d ) ) |
62 |
61
|
sseq2d |
|- ( u = ran f -> ( Y C_ U_ x e. u ( x ( ball ` M ) d ) <-> Y C_ U_ x e. ran f ( x ( ball ` M ) d ) ) ) |
63 |
62
|
rspcev |
|- ( ( ran f e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. ran f ( x ( ball ` M ) d ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) |
64 |
45 60 63
|
syl2anc |
|- ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) |
65 |
34 64
|
exlimddv |
|- ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) |
66 |
65
|
rexlimdvaa |
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) |
67 |
29 66
|
impbid |
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) <-> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) |
68 |
67
|
ralbidv |
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) <-> A. d e. RR+ E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) |
69 |
2 68
|
bitrd |
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) |