Metamath Proof Explorer

Theorem cnpco

Description: The composition of a function F continuous at P with a function continuous at ( FP ) is continuous at P . Proposition 2 of BourbakiTop1 p. I.9. (Contributed by FL, 16-Nov-2006) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion cnpco 
|- ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( G o. F ) e. ( ( J CnP L ) ` P ) )

Proof

Step Hyp Ref Expression
1 cnptop1 
 |-  ( F e. ( ( J CnP K ) ` P ) -> J e. Top )
2 1 adantr 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> J e. Top )
3 cnptop2 
 |-  ( G e. ( ( K CnP L ) ` ( F ` P ) ) -> L e. Top )
4 3 adantl 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> L e. Top )
5 eqid 
 |-  U. J = U. J
6 5 cnprcl 
 |-  ( F e. ( ( J CnP K ) ` P ) -> P e. U. J )
7 6 adantr 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> P e. U. J )
8 2 4 7 3jca 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( J e. Top /\ L e. Top /\ P e. U. J ) )
9 eqid 
 |-  U. K = U. K
10 eqid 
 |-  U. L = U. L
11 9 10 cnpf 
 |-  ( G e. ( ( K CnP L ) ` ( F ` P ) ) -> G : U. K --> U. L )
12 11 adantl 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> G : U. K --> U. L )
13 5 9 cnpf 
 |-  ( F e. ( ( J CnP K ) ` P ) -> F : U. J --> U. K )
14 13 adantr 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> F : U. J --> U. K )
15 fco 
 |-  ( ( G : U. K --> U. L /\ F : U. J --> U. K ) -> ( G o. F ) : U. J --> U. L )
16 12 14 15 syl2anc 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( G o. F ) : U. J --> U. L )
17 simplr 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> G e. ( ( K CnP L ) ` ( F ` P ) ) )
18 simprl 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> z e. L )
19 fvco3 
 |-  ( ( F : U. J --> U. K /\ P e. U. J ) -> ( ( G o. F ) ` P ) = ( G ` ( F ` P ) ) )
20 14 7 19 syl2anc 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( ( G o. F ) ` P ) = ( G ` ( F ` P ) ) )
21 20 adantr 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> ( ( G o. F ) ` P ) = ( G ` ( F ` P ) ) )
22 simprr 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> ( ( G o. F ) ` P ) e. z )
23 21 22 eqeltrrd 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> ( G ` ( F ` P ) ) e. z )
24 cnpimaex 
 |-  ( ( G e. ( ( K CnP L ) ` ( F ` P ) ) /\ z e. L /\ ( G ` ( F ` P ) ) e. z ) -> E. y e. K ( ( F ` P ) e. y /\ ( G " y ) C_ z ) )
25 17 18 23 24 syl3anc 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> E. y e. K ( ( F ` P ) e. y /\ ( G " y ) C_ z ) )
26 simplll 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> F e. ( ( J CnP K ) ` P ) )
27 simprl 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> y e. K )
28 simprrl 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> ( F ` P ) e. y )
29 cnpimaex 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ y e. K /\ ( F ` P ) e. y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) )
30 26 27 28 29 syl3anc 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) )
31 imaco 
 |-  ( ( G o. F ) " x ) = ( G " ( F " x ) )
32 imass2 
 |-  ( ( F " x ) C_ y -> ( G " ( F " x ) ) C_ ( G " y ) )
33 31 32 eqsstrid 
 |-  ( ( F " x ) C_ y -> ( ( G o. F ) " x ) C_ ( G " y ) )
34 simprrr 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> ( G " y ) C_ z )
35 sstr2 
 |-  ( ( ( G o. F ) " x ) C_ ( G " y ) -> ( ( G " y ) C_ z -> ( ( G o. F ) " x ) C_ z ) )
36 33 34 35 syl2imc 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> ( ( F " x ) C_ y -> ( ( G o. F ) " x ) C_ z ) )
37 36 anim2d 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. x /\ ( ( G o. F ) " x ) C_ z ) ) )
38 37 reximdv 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) ) )
39 30 38 mpd 
 |-  ( ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) /\ ( y e. K /\ ( ( F ` P ) e. y /\ ( G " y ) C_ z ) ) ) -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) )
40 25 39 rexlimddv 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ ( z e. L /\ ( ( G o. F ) ` P ) e. z ) ) -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) )
41 40 expr 
 |-  ( ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) /\ z e. L ) -> ( ( ( G o. F ) ` P ) e. z -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) ) )
42 41 ralrimiva 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> A. z e. L ( ( ( G o. F ) ` P ) e. z -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) ) )
43 16 42 jca 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( ( G o. F ) : U. J --> U. L /\ A. z e. L ( ( ( G o. F ) ` P ) e. z -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) ) ) )
44 5 10 iscnp2 
 |-  ( ( G o. F ) e. ( ( J CnP L ) ` P ) <-> ( ( J e. Top /\ L e. Top /\ P e. U. J ) /\ ( ( G o. F ) : U. J --> U. L /\ A. z e. L ( ( ( G o. F ) ` P ) e. z -> E. x e. J ( P e. x /\ ( ( G o. F ) " x ) C_ z ) ) ) ) )
45 8 43 44 sylanbrc 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( G o. F ) e. ( ( J CnP L ) ` P ) )