Step |
Hyp |
Ref |
Expression |
1 |
|
xlebnum.j |
|- J = ( MetOpen ` D ) |
2 |
|
xlebnum.d |
|- ( ph -> D e. ( *Met ` X ) ) |
3 |
|
xlebnum.c |
|- ( ph -> J e. Comp ) |
4 |
|
xlebnum.s |
|- ( ph -> U C_ J ) |
5 |
|
xlebnum.u |
|- ( ph -> X = U. U ) |
6 |
|
eqid |
|- ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) = ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) |
7 |
|
1rp |
|- 1 e. RR+ |
8 |
|
eqid |
|- ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) = ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) |
9 |
8
|
stdbdmet |
|- ( ( D e. ( *Met ` X ) /\ 1 e. RR+ ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) ) |
10 |
2 7 9
|
sylancl |
|- ( ph -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) ) |
11 |
|
rpxr |
|- ( 1 e. RR+ -> 1 e. RR* ) |
12 |
7 11
|
mp1i |
|- ( ph -> 1 e. RR* ) |
13 |
|
0lt1 |
|- 0 < 1 |
14 |
13
|
a1i |
|- ( ph -> 0 < 1 ) |
15 |
8 1
|
stdbdmopn |
|- ( ( D e. ( *Met ` X ) /\ 1 e. RR* /\ 0 < 1 ) -> J = ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) ) |
16 |
2 12 14 15
|
syl3anc |
|- ( ph -> J = ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) ) |
17 |
16 3
|
eqeltrrd |
|- ( ph -> ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) e. Comp ) |
18 |
4 16
|
sseqtrd |
|- ( ph -> U C_ ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) ) |
19 |
6 10 17 18 5
|
lebnum |
|- ( ph -> E. r e. RR+ A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u ) |
20 |
|
simpr |
|- ( ( ph /\ r e. RR+ ) -> r e. RR+ ) |
21 |
|
ifcl |
|- ( ( r e. RR+ /\ 1 e. RR+ ) -> if ( r <_ 1 , r , 1 ) e. RR+ ) |
22 |
20 7 21
|
sylancl |
|- ( ( ph /\ r e. RR+ ) -> if ( r <_ 1 , r , 1 ) e. RR+ ) |
23 |
2
|
ad2antrr |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> D e. ( *Met ` X ) ) |
24 |
7 11
|
mp1i |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> 1 e. RR* ) |
25 |
13
|
a1i |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> 0 < 1 ) |
26 |
|
simpr |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> x e. X ) |
27 |
22
|
adantr |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) e. RR+ ) |
28 |
|
rpxr |
|- ( if ( r <_ 1 , r , 1 ) e. RR+ -> if ( r <_ 1 , r , 1 ) e. RR* ) |
29 |
27 28
|
syl |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) e. RR* ) |
30 |
|
rpre |
|- ( r e. RR+ -> r e. RR ) |
31 |
30
|
ad2antlr |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> r e. RR ) |
32 |
|
1re |
|- 1 e. RR |
33 |
|
min2 |
|- ( ( r e. RR /\ 1 e. RR ) -> if ( r <_ 1 , r , 1 ) <_ 1 ) |
34 |
31 32 33
|
sylancl |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) <_ 1 ) |
35 |
8
|
stdbdbl |
|- ( ( ( D e. ( *Met ` X ) /\ 1 e. RR* /\ 0 < 1 ) /\ ( x e. X /\ if ( r <_ 1 , r , 1 ) e. RR* /\ if ( r <_ 1 , r , 1 ) <_ 1 ) ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) = ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) ) |
36 |
23 24 25 26 29 34 35
|
syl33anc |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) = ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) ) |
37 |
10
|
ad2antrr |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) ) |
38 |
|
metxmet |
|- ( ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( *Met ` X ) ) |
39 |
37 38
|
syl |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( *Met ` X ) ) |
40 |
|
rpxr |
|- ( r e. RR+ -> r e. RR* ) |
41 |
40
|
ad2antlr |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> r e. RR* ) |
42 |
|
min1 |
|- ( ( r e. RR /\ 1 e. RR ) -> if ( r <_ 1 , r , 1 ) <_ r ) |
43 |
31 32 42
|
sylancl |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) <_ r ) |
44 |
|
ssbl |
|- ( ( ( ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( *Met ` X ) /\ x e. X ) /\ ( if ( r <_ 1 , r , 1 ) e. RR* /\ r e. RR* ) /\ if ( r <_ 1 , r , 1 ) <_ r ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) ) |
45 |
39 26 29 41 43 44
|
syl221anc |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) ) |
46 |
36 45
|
eqsstrrd |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) ) |
47 |
|
sstr2 |
|- ( ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) -> ( ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
48 |
46 47
|
syl |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
49 |
48
|
reximdv |
|- ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
50 |
49
|
ralimdva |
|- ( ( ph /\ r e. RR+ ) -> ( A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> A. x e. X E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
51 |
|
oveq2 |
|- ( d = if ( r <_ 1 , r , 1 ) -> ( x ( ball ` D ) d ) = ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) ) |
52 |
51
|
sseq1d |
|- ( d = if ( r <_ 1 , r , 1 ) -> ( ( x ( ball ` D ) d ) C_ u <-> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
53 |
52
|
rexbidv |
|- ( d = if ( r <_ 1 , r , 1 ) -> ( E. u e. U ( x ( ball ` D ) d ) C_ u <-> E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
54 |
53
|
ralbidv |
|- ( d = if ( r <_ 1 , r , 1 ) -> ( A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u <-> A. x e. X E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) ) |
55 |
54
|
rspcev |
|- ( ( if ( r <_ 1 , r , 1 ) e. RR+ /\ A. x e. X E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |
56 |
22 50 55
|
syl6an |
|- ( ( ph /\ r e. RR+ ) -> ( A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) ) |
57 |
56
|
rexlimdva |
|- ( ph -> ( E. r e. RR+ A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) ) |
58 |
19 57
|
mpd |
|- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |