Step |
Hyp |
Ref |
Expression |
1 |
|
equivcau.1 |
β’ ( π β πΆ β ( Met β π ) ) |
2 |
|
equivcau.2 |
β’ ( π β π· β ( Met β π ) ) |
3 |
|
equivcau.3 |
β’ ( π β π
β β+ ) |
4 |
|
equivcau.4 |
β’ ( ( π β§ ( π₯ β π β§ π¦ β π ) ) β ( π₯ πΆ π¦ ) β€ ( π
Β· ( π₯ π· π¦ ) ) ) |
5 |
|
simpr |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β π β β+ ) |
6 |
3
|
ad2antrr |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β π
β β+ ) |
7 |
5 6
|
rpdivcld |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β ( π / π
) β β+ ) |
8 |
|
oveq2 |
β’ ( π = ( π / π
) β ( π₯ ( ball β π· ) π ) = ( π₯ ( ball β π· ) ( π / π
) ) ) |
9 |
8
|
eleq1d |
β’ ( π = ( π / π
) β ( ( π₯ ( ball β π· ) π ) β π β ( π₯ ( ball β π· ) ( π / π
) ) β π ) ) |
10 |
9
|
rexbidv |
β’ ( π = ( π / π
) β ( β π₯ β π ( π₯ ( ball β π· ) π ) β π β β π₯ β π ( π₯ ( ball β π· ) ( π / π
) ) β π ) ) |
11 |
10
|
rspcv |
β’ ( ( π / π
) β β+ β ( β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π β β π₯ β π ( π₯ ( ball β π· ) ( π / π
) ) β π ) ) |
12 |
7 11
|
syl |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β ( β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π β β π₯ β π ( π₯ ( ball β π· ) ( π / π
) ) β π ) ) |
13 |
|
simpllr |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β π β ( Fil β π ) ) |
14 |
|
eqid |
β’ ( MetOpen β πΆ ) = ( MetOpen β πΆ ) |
15 |
|
eqid |
β’ ( MetOpen β π· ) = ( MetOpen β π· ) |
16 |
14 15 1 2 3 4
|
metss2lem |
β’ ( ( π β§ ( π₯ β π β§ π β β+ ) ) β ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) ) |
17 |
16
|
ancom2s |
β’ ( ( π β§ ( π β β+ β§ π₯ β π ) ) β ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) ) |
18 |
17
|
adantlr |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ ( π β β+ β§ π₯ β π ) ) β ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) ) |
19 |
18
|
anassrs |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) ) |
20 |
1
|
ad3antrrr |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β πΆ β ( Met β π ) ) |
21 |
|
metxmet |
β’ ( πΆ β ( Met β π ) β πΆ β ( βMet β π ) ) |
22 |
20 21
|
syl |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β πΆ β ( βMet β π ) ) |
23 |
|
simpr |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β π₯ β π ) |
24 |
|
rpxr |
β’ ( π β β+ β π β β* ) |
25 |
24
|
ad2antlr |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β π β β* ) |
26 |
|
blssm |
β’ ( ( πΆ β ( βMet β π ) β§ π₯ β π β§ π β β* ) β ( π₯ ( ball β πΆ ) π ) β π ) |
27 |
22 23 25 26
|
syl3anc |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β ( π₯ ( ball β πΆ ) π ) β π ) |
28 |
|
filss |
β’ ( ( π β ( Fil β π ) β§ ( ( π₯ ( ball β π· ) ( π / π
) ) β π β§ ( π₯ ( ball β πΆ ) π ) β π β§ ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) ) ) β ( π₯ ( ball β πΆ ) π ) β π ) |
29 |
28
|
3exp2 |
β’ ( π β ( Fil β π ) β ( ( π₯ ( ball β π· ) ( π / π
) ) β π β ( ( π₯ ( ball β πΆ ) π ) β π β ( ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) β ( π₯ ( ball β πΆ ) π ) β π ) ) ) ) |
30 |
29
|
com24 |
β’ ( π β ( Fil β π ) β ( ( π₯ ( ball β π· ) ( π / π
) ) β ( π₯ ( ball β πΆ ) π ) β ( ( π₯ ( ball β πΆ ) π ) β π β ( ( π₯ ( ball β π· ) ( π / π
) ) β π β ( π₯ ( ball β πΆ ) π ) β π ) ) ) ) |
31 |
13 19 27 30
|
syl3c |
β’ ( ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β§ π₯ β π ) β ( ( π₯ ( ball β π· ) ( π / π
) ) β π β ( π₯ ( ball β πΆ ) π ) β π ) ) |
32 |
31
|
reximdva |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β ( β π₯ β π ( π₯ ( ball β π· ) ( π / π
) ) β π β β π₯ β π ( π₯ ( ball β πΆ ) π ) β π ) ) |
33 |
12 32
|
syld |
β’ ( ( ( π β§ π β ( Fil β π ) ) β§ π β β+ ) β ( β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π β β π₯ β π ( π₯ ( ball β πΆ ) π ) β π ) ) |
34 |
33
|
ralrimdva |
β’ ( ( π β§ π β ( Fil β π ) ) β ( β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π β β π β β+ β π₯ β π ( π₯ ( ball β πΆ ) π ) β π ) ) |
35 |
34
|
imdistanda |
β’ ( π β ( ( π β ( Fil β π ) β§ β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π ) β ( π β ( Fil β π ) β§ β π β β+ β π₯ β π ( π₯ ( ball β πΆ ) π ) β π ) ) ) |
36 |
|
metxmet |
β’ ( π· β ( Met β π ) β π· β ( βMet β π ) ) |
37 |
|
iscfil3 |
β’ ( π· β ( βMet β π ) β ( π β ( CauFil β π· ) β ( π β ( Fil β π ) β§ β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π ) ) ) |
38 |
2 36 37
|
3syl |
β’ ( π β ( π β ( CauFil β π· ) β ( π β ( Fil β π ) β§ β π β β+ β π₯ β π ( π₯ ( ball β π· ) π ) β π ) ) ) |
39 |
|
iscfil3 |
β’ ( πΆ β ( βMet β π ) β ( π β ( CauFil β πΆ ) β ( π β ( Fil β π ) β§ β π β β+ β π₯ β π ( π₯ ( ball β πΆ ) π ) β π ) ) ) |
40 |
1 21 39
|
3syl |
β’ ( π β ( π β ( CauFil β πΆ ) β ( π β ( Fil β π ) β§ β π β β+ β π₯ β π ( π₯ ( ball β πΆ ) π ) β π ) ) ) |
41 |
35 38 40
|
3imtr4d |
β’ ( π β ( π β ( CauFil β π· ) β π β ( CauFil β πΆ ) ) ) |
42 |
41
|
ssrdv |
β’ ( π β ( CauFil β π· ) β ( CauFil β πΆ ) ) |