Step |
Hyp |
Ref |
Expression |
1 |
|
cncfmet.1 |
|- C = ( ( abs o. - ) |` ( A X. A ) ) |
2 |
|
cncfmet.2 |
|- D = ( ( abs o. - ) |` ( B X. B ) ) |
3 |
|
cncfmet.3 |
|- J = ( MetOpen ` C ) |
4 |
|
cncfmet.4 |
|- K = ( MetOpen ` D ) |
5 |
|
simplll |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> A C_ CC ) |
6 |
|
simprl |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> x e. A ) |
7 |
|
simprr |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> w e. A ) |
8 |
1
|
oveqi |
|- ( x C w ) = ( x ( ( abs o. - ) |` ( A X. A ) ) w ) |
9 |
|
ovres |
|- ( ( x e. A /\ w e. A ) -> ( x ( ( abs o. - ) |` ( A X. A ) ) w ) = ( x ( abs o. - ) w ) ) |
10 |
8 9
|
syl5eq |
|- ( ( x e. A /\ w e. A ) -> ( x C w ) = ( x ( abs o. - ) w ) ) |
11 |
10
|
ad2ant2l |
|- ( ( ( A C_ CC /\ x e. A ) /\ ( A C_ CC /\ w e. A ) ) -> ( x C w ) = ( x ( abs o. - ) w ) ) |
12 |
|
ssel2 |
|- ( ( A C_ CC /\ x e. A ) -> x e. CC ) |
13 |
|
ssel2 |
|- ( ( A C_ CC /\ w e. A ) -> w e. CC ) |
14 |
|
eqid |
|- ( abs o. - ) = ( abs o. - ) |
15 |
14
|
cnmetdval |
|- ( ( x e. CC /\ w e. CC ) -> ( x ( abs o. - ) w ) = ( abs ` ( x - w ) ) ) |
16 |
12 13 15
|
syl2an |
|- ( ( ( A C_ CC /\ x e. A ) /\ ( A C_ CC /\ w e. A ) ) -> ( x ( abs o. - ) w ) = ( abs ` ( x - w ) ) ) |
17 |
11 16
|
eqtrd |
|- ( ( ( A C_ CC /\ x e. A ) /\ ( A C_ CC /\ w e. A ) ) -> ( x C w ) = ( abs ` ( x - w ) ) ) |
18 |
5 6 5 7 17
|
syl22anc |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( x C w ) = ( abs ` ( x - w ) ) ) |
19 |
18
|
breq1d |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( x C w ) < z <-> ( abs ` ( x - w ) ) < z ) ) |
20 |
|
ffvelrn |
|- ( ( f : A --> B /\ x e. A ) -> ( f ` x ) e. B ) |
21 |
20
|
ad2ant2lr |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` x ) e. B ) |
22 |
|
ffvelrn |
|- ( ( f : A --> B /\ w e. A ) -> ( f ` w ) e. B ) |
23 |
22
|
ad2ant2l |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` w ) e. B ) |
24 |
2
|
oveqi |
|- ( ( f ` x ) D ( f ` w ) ) = ( ( f ` x ) ( ( abs o. - ) |` ( B X. B ) ) ( f ` w ) ) |
25 |
|
ovres |
|- ( ( ( f ` x ) e. B /\ ( f ` w ) e. B ) -> ( ( f ` x ) ( ( abs o. - ) |` ( B X. B ) ) ( f ` w ) ) = ( ( f ` x ) ( abs o. - ) ( f ` w ) ) ) |
26 |
24 25
|
syl5eq |
|- ( ( ( f ` x ) e. B /\ ( f ` w ) e. B ) -> ( ( f ` x ) D ( f ` w ) ) = ( ( f ` x ) ( abs o. - ) ( f ` w ) ) ) |
27 |
21 23 26
|
syl2anc |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( f ` x ) D ( f ` w ) ) = ( ( f ` x ) ( abs o. - ) ( f ` w ) ) ) |
28 |
|
simpllr |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> B C_ CC ) |
29 |
28 21
|
sseldd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` x ) e. CC ) |
30 |
28 23
|
sseldd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( f ` w ) e. CC ) |
31 |
14
|
cnmetdval |
|- ( ( ( f ` x ) e. CC /\ ( f ` w ) e. CC ) -> ( ( f ` x ) ( abs o. - ) ( f ` w ) ) = ( abs ` ( ( f ` x ) - ( f ` w ) ) ) ) |
32 |
29 30 31
|
syl2anc |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( f ` x ) ( abs o. - ) ( f ` w ) ) = ( abs ` ( ( f ` x ) - ( f ` w ) ) ) ) |
33 |
27 32
|
eqtrd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( f ` x ) D ( f ` w ) ) = ( abs ` ( ( f ` x ) - ( f ` w ) ) ) ) |
34 |
33
|
breq1d |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( ( f ` x ) D ( f ` w ) ) < y <-> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) |
35 |
19 34
|
imbi12d |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) |
36 |
35
|
anassrs |
|- ( ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) /\ w e. A ) -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) |
37 |
36
|
ralbidva |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) -> ( A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) |
38 |
37
|
rexbidv |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) -> ( E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) |
39 |
38
|
ralbidv |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) /\ x e. A ) -> ( A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) |
40 |
39
|
ralbidva |
|- ( ( ( A C_ CC /\ B C_ CC ) /\ f : A --> B ) -> ( A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) |
41 |
40
|
pm5.32da |
|- ( ( A C_ CC /\ B C_ CC ) -> ( ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) ) |
42 |
|
cnxmet |
|- ( abs o. - ) e. ( *Met ` CC ) |
43 |
|
xmetres2 |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A C_ CC ) -> ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) ) |
44 |
42 43
|
mpan |
|- ( A C_ CC -> ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) ) |
45 |
1 44
|
eqeltrid |
|- ( A C_ CC -> C e. ( *Met ` A ) ) |
46 |
|
xmetres2 |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ B C_ CC ) -> ( ( abs o. - ) |` ( B X. B ) ) e. ( *Met ` B ) ) |
47 |
42 46
|
mpan |
|- ( B C_ CC -> ( ( abs o. - ) |` ( B X. B ) ) e. ( *Met ` B ) ) |
48 |
2 47
|
eqeltrid |
|- ( B C_ CC -> D e. ( *Met ` B ) ) |
49 |
3 4
|
metcn |
|- ( ( C e. ( *Met ` A ) /\ D e. ( *Met ` B ) ) -> ( f e. ( J Cn K ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) ) |
50 |
45 48 49
|
syl2an |
|- ( ( A C_ CC /\ B C_ CC ) -> ( f e. ( J Cn K ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) ) |
51 |
|
elcncf |
|- ( ( A C_ CC /\ B C_ CC ) -> ( f e. ( A -cn-> B ) <-> ( f : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) ) ) ) |
52 |
41 50 51
|
3bitr4rd |
|- ( ( A C_ CC /\ B C_ CC ) -> ( f e. ( A -cn-> B ) <-> f e. ( J Cn K ) ) ) |
53 |
52
|
eqrdv |
|- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( J Cn K ) ) |