Step |
Hyp |
Ref |
Expression |
1 |
|
cncfco.4 |
|- ( ph -> F e. ( A -cn-> B ) ) |
2 |
|
cncfco.5 |
|- ( ph -> G e. ( B -cn-> C ) ) |
3 |
|
cncff |
|- ( G e. ( B -cn-> C ) -> G : B --> C ) |
4 |
2 3
|
syl |
|- ( ph -> G : B --> C ) |
5 |
|
cncff |
|- ( F e. ( A -cn-> B ) -> F : A --> B ) |
6 |
1 5
|
syl |
|- ( ph -> F : A --> B ) |
7 |
|
fco |
|- ( ( G : B --> C /\ F : A --> B ) -> ( G o. F ) : A --> C ) |
8 |
4 6 7
|
syl2anc |
|- ( ph -> ( G o. F ) : A --> C ) |
9 |
2
|
adantr |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> G e. ( B -cn-> C ) ) |
10 |
6
|
adantr |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> F : A --> B ) |
11 |
|
simprl |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> x e. A ) |
12 |
10 11
|
ffvelrnd |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> ( F ` x ) e. B ) |
13 |
|
simprr |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> y e. RR+ ) |
14 |
|
cncfi |
|- ( ( G e. ( B -cn-> C ) /\ ( F ` x ) e. B /\ y e. RR+ ) -> E. u e. RR+ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) |
15 |
9 12 13 14
|
syl3anc |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> E. u e. RR+ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) |
16 |
1
|
ad2antrr |
|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> F e. ( A -cn-> B ) ) |
17 |
|
simplrl |
|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> x e. A ) |
18 |
|
simpr |
|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> u e. RR+ ) |
19 |
|
cncfi |
|- ( ( F e. ( A -cn-> B ) /\ x e. A /\ u e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) ) |
20 |
16 17 18 19
|
syl3anc |
|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) ) |
21 |
6
|
ad3antrrr |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> F : A --> B ) |
22 |
|
simprr |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> w e. A ) |
23 |
21 22
|
ffvelrnd |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( F ` w ) e. B ) |
24 |
|
fvoveq1 |
|- ( v = ( F ` w ) -> ( abs ` ( v - ( F ` x ) ) ) = ( abs ` ( ( F ` w ) - ( F ` x ) ) ) ) |
25 |
24
|
breq1d |
|- ( v = ( F ` w ) -> ( ( abs ` ( v - ( F ` x ) ) ) < u <-> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) ) |
26 |
25
|
imbrov2fvoveq |
|- ( v = ( F ` w ) -> ( ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) <-> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) ) |
27 |
26
|
rspcv |
|- ( ( F ` w ) e. B -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) ) |
28 |
23 27
|
syl |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) ) |
29 |
|
fvco3 |
|- ( ( F : A --> B /\ w e. A ) -> ( ( G o. F ) ` w ) = ( G ` ( F ` w ) ) ) |
30 |
21 22 29
|
syl2anc |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( G o. F ) ` w ) = ( G ` ( F ` w ) ) ) |
31 |
17
|
adantr |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> x e. A ) |
32 |
|
fvco3 |
|- ( ( F : A --> B /\ x e. A ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) ) |
33 |
21 31 32
|
syl2anc |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) ) |
34 |
30 33
|
oveq12d |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) = ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) |
35 |
34
|
fveq2d |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) = ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) ) |
36 |
35
|
breq1d |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y <-> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) |
37 |
36
|
imbi2d |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) <-> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` ( F ` w ) ) - ( G ` ( F ` x ) ) ) ) < y ) ) ) |
38 |
28 37
|
sylibrd |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
39 |
38
|
imp |
|- ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ ( z e. RR+ /\ w e. A ) ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) |
40 |
39
|
an32s |
|- ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) |
41 |
40
|
imim2d |
|- ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ ( z e. RR+ /\ w e. A ) ) -> ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
42 |
41
|
anassrs |
|- ( ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ z e. RR+ ) /\ w e. A ) -> ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
43 |
42
|
ralimdva |
|- ( ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) /\ z e. RR+ ) -> ( A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
44 |
43
|
reximdva |
|- ( ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) /\ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) ) -> ( E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
45 |
44
|
ex |
|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> ( E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < u ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) ) |
46 |
20 45
|
mpid |
|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ u e. RR+ ) -> ( A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
47 |
46
|
rexlimdva |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> ( E. u e. RR+ A. v e. B ( ( abs ` ( v - ( F ` x ) ) ) < u -> ( abs ` ( ( G ` v ) - ( G ` ( F ` x ) ) ) ) < y ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) |
48 |
15 47
|
mpd |
|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) |
49 |
48
|
ralrimivva |
|- ( ph -> A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) |
50 |
|
cncfrss |
|- ( F e. ( A -cn-> B ) -> A C_ CC ) |
51 |
1 50
|
syl |
|- ( ph -> A C_ CC ) |
52 |
|
cncfrss2 |
|- ( G e. ( B -cn-> C ) -> C C_ CC ) |
53 |
2 52
|
syl |
|- ( ph -> C C_ CC ) |
54 |
|
elcncf2 |
|- ( ( A C_ CC /\ C C_ CC ) -> ( ( G o. F ) e. ( A -cn-> C ) <-> ( ( G o. F ) : A --> C /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) ) |
55 |
51 53 54
|
syl2anc |
|- ( ph -> ( ( G o. F ) e. ( A -cn-> C ) <-> ( ( G o. F ) : A --> C /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( ( G o. F ) ` w ) - ( ( G o. F ) ` x ) ) ) < y ) ) ) ) |
56 |
8 49 55
|
mpbir2and |
|- ( ph -> ( G o. F ) e. ( A -cn-> C ) ) |