Metamath Proof Explorer

Theorem cnpconn

Description: An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypothesis cnpconn.2 
|- Y = U. K
Assertion cnpconn 
|- ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. PConn )

Proof

Step Hyp Ref Expression
1 cnpconn.2 
 |-  Y = U. K
2 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
3 2 3ad2ant3 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. Top )
4 eqid 
 |-  U. J = U. J
5 4 pconncn 
 |-  ( ( J e. PConn /\ u e. U. J /\ v e. U. J ) -> E. g e. ( II Cn J ) ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) )
6 5 3expb 
 |-  ( ( J e. PConn /\ ( u e. U. J /\ v e. U. J ) ) -> E. g e. ( II Cn J ) ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) )
7 6 3ad2antl1 
 |-  ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) -> E. g e. ( II Cn J ) ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) )
8 simprl 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> g e. ( II Cn J ) )
9 simpll3 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> F e. ( J Cn K ) )
10 cnco 
 |-  ( ( g e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. g ) e. ( II Cn K ) )
11 8 9 10 syl2anc 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( F o. g ) e. ( II Cn K ) )
12 iiuni 
 |-  ( 0 [,] 1 ) = U. II
13 12 4 cnf 
 |-  ( g e. ( II Cn J ) -> g : ( 0 [,] 1 ) --> U. J )
14 8 13 syl 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> g : ( 0 [,] 1 ) --> U. J )
15 0elunit 
 |-  0 e. ( 0 [,] 1 )
16 fvco3 
 |-  ( ( g : ( 0 [,] 1 ) --> U. J /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. g ) ` 0 ) = ( F ` ( g ` 0 ) ) )
17 14 15 16 sylancl 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( ( F o. g ) ` 0 ) = ( F ` ( g ` 0 ) ) )
18 simprrl 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( g ` 0 ) = u )
19 18 fveq2d 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( F ` ( g ` 0 ) ) = ( F ` u ) )
20 17 19 eqtrd 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( ( F o. g ) ` 0 ) = ( F ` u ) )
21 1elunit 
 |-  1 e. ( 0 [,] 1 )
22 fvco3 
 |-  ( ( g : ( 0 [,] 1 ) --> U. J /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. g ) ` 1 ) = ( F ` ( g ` 1 ) ) )
23 14 21 22 sylancl 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( ( F o. g ) ` 1 ) = ( F ` ( g ` 1 ) ) )
24 simprrr 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( g ` 1 ) = v )
25 24 fveq2d 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( F ` ( g ` 1 ) ) = ( F ` v ) )
26 23 25 eqtrd 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> ( ( F o. g ) ` 1 ) = ( F ` v ) )
27 fveq1 
 |-  ( f = ( F o. g ) -> ( f ` 0 ) = ( ( F o. g ) ` 0 ) )
28 27 eqeq1d 
 |-  ( f = ( F o. g ) -> ( ( f ` 0 ) = ( F ` u ) <-> ( ( F o. g ) ` 0 ) = ( F ` u ) ) )
29 fveq1 
 |-  ( f = ( F o. g ) -> ( f ` 1 ) = ( ( F o. g ) ` 1 ) )
30 29 eqeq1d 
 |-  ( f = ( F o. g ) -> ( ( f ` 1 ) = ( F ` v ) <-> ( ( F o. g ) ` 1 ) = ( F ` v ) ) )
31 28 30 anbi12d 
 |-  ( f = ( F o. g ) -> ( ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) <-> ( ( ( F o. g ) ` 0 ) = ( F ` u ) /\ ( ( F o. g ) ` 1 ) = ( F ` v ) ) ) )
32 31 rspcev 
 |-  ( ( ( F o. g ) e. ( II Cn K ) /\ ( ( ( F o. g ) ` 0 ) = ( F ` u ) /\ ( ( F o. g ) ` 1 ) = ( F ` v ) ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) )
33 11 20 26 32 syl12anc 
 |-  ( ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) /\ ( g e. ( II Cn J ) /\ ( ( g ` 0 ) = u /\ ( g ` 1 ) = v ) ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) )
34 7 33 rexlimddv 
 |-  ( ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( u e. U. J /\ v e. U. J ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) )
35 34 ralrimivva 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> A. u e. U. J A. v e. U. J E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) )
36 4 1 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> Y )
37 36 3ad2ant3 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> F : U. J --> Y )
38 forn 
 |-  ( F : X -onto-> Y -> ran F = Y )
39 38 3ad2ant2 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> ran F = Y )
40 dffo2 
 |-  ( F : U. J -onto-> Y <-> ( F : U. J --> Y /\ ran F = Y ) )
41 37 39 40 sylanbrc 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> F : U. J -onto-> Y )
42 eqeq2 
 |-  ( ( F ` v ) = y -> ( ( f ` 1 ) = ( F ` v ) <-> ( f ` 1 ) = y ) )
43 42 anbi2d 
 |-  ( ( F ` v ) = y -> ( ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) <-> ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) ) )
44 43 rexbidv 
 |-  ( ( F ` v ) = y -> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) ) )
45 44 cbvfo 
 |-  ( F : U. J -onto-> Y -> ( A. v e. U. J E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) <-> A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) ) )
46 41 45 syl 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> ( A. v e. U. J E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) <-> A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) ) )
47 46 ralbidv 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> ( A. u e. U. J A. v e. U. J E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = ( F ` v ) ) <-> A. u e. U. J A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) ) )
48 35 47 mpbid 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> A. u e. U. J A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) )
49 eqeq2 
 |-  ( ( F ` u ) = x -> ( ( f ` 0 ) = ( F ` u ) <-> ( f ` 0 ) = x ) )
50 49 anbi1d 
 |-  ( ( F ` u ) = x -> ( ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) <-> ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
51 50 rexbidv 
 |-  ( ( F ` u ) = x -> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
52 51 ralbidv 
 |-  ( ( F ` u ) = x -> ( A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) <-> A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
53 52 cbvfo 
 |-  ( F : U. J -onto-> Y -> ( A. u e. U. J A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) <-> A. x e. Y A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
54 41 53 syl 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> ( A. u e. U. J A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = ( F ` u ) /\ ( f ` 1 ) = y ) <-> A. x e. Y A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
55 48 54 mpbid 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> A. x e. Y A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
56 1 ispconn 
 |-  ( K e. PConn <-> ( K e. Top /\ A. x e. Y A. y e. Y E. f e. ( II Cn K ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
57 3 55 56 sylanbrc 
 |-  ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. PConn )