Metamath Proof Explorer

Theorem cnconn

Description: Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 cnconn.2 
 |-  Y = U. K
2 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
3 2 3ad2ant3 
 |-  ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. Top )
4 df-ne 
 |-  ( x =/= (/) <-> -. x = (/) )
5 eqid 
 |-  U. J = U. J
6 simpl1 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> J e. Conn )
7 simpl3 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> F e. ( J Cn K ) )
8 simprl 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x e. ( K i^i ( Clsd ` K ) ) )
9 8 elin1d 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x e. K )
10 cnima 
 |-  ( ( F e. ( J Cn K ) /\ x e. K ) -> ( `' F " x ) e. J )
11 7 9 10 syl2anc 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( `' F " x ) e. J )
12 elssuni 
 |-  ( x e. K -> x C_ U. K )
13 9 12 syl 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x C_ U. K )
14 13 1 sseqtrrdi 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x C_ Y )
15 simpl2 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> F : X -onto-> Y )
16 forn 
 |-  ( F : X -onto-> Y -> ran F = Y )
17 15 16 syl 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ran F = Y )
18 14 17 sseqtrrd 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x C_ ran F )
19 df-rn 
 |-  ran F = dom `' F
20 18 19 sseqtrdi 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x C_ dom `' F )
21 sseqin2 
 |-  ( x C_ dom `' F <-> ( dom `' F i^i x ) = x )
22 20 21 sylib 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( dom `' F i^i x ) = x )
23 simprr 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x =/= (/) )
24 22 23 eqnetrd 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( dom `' F i^i x ) =/= (/) )
25 imadisj 
 |-  ( ( `' F " x ) = (/) <-> ( dom `' F i^i x ) = (/) )
26 25 necon3bii 
 |-  ( ( `' F " x ) =/= (/) <-> ( dom `' F i^i x ) =/= (/) )
27 24 26 sylibr 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( `' F " x ) =/= (/) )
28 8 elin2d 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x e. ( Clsd ` K ) )
29 cnclima 
 |-  ( ( F e. ( J Cn K ) /\ x e. ( Clsd ` K ) ) -> ( `' F " x ) e. ( Clsd ` J ) )
30 7 28 29 syl2anc 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( `' F " x ) e. ( Clsd ` J ) )
31 5 6 11 27 30 connclo 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( `' F " x ) = U. J )
32 5 1 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> Y )
33 fdm 
 |-  ( F : U. J --> Y -> dom F = U. J )
34 7 32 33 3syl 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> dom F = U. J )
35 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
36 fdm 
 |-  ( F : X --> Y -> dom F = X )
37 15 35 36 3syl 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> dom F = X )
38 31 34 37 3eqtr2d 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( `' F " x ) = X )
39 38 imaeq2d 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( F " ( `' F " x ) ) = ( F " X ) )
40 foimacnv 
 |-  ( ( F : X -onto-> Y /\ x C_ Y ) -> ( F " ( `' F " x ) ) = x )
41 15 14 40 syl2anc 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( F " ( `' F " x ) ) = x )
42 foima 
 |-  ( F : X -onto-> Y -> ( F " X ) = Y )
43 15 42 syl 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> ( F " X ) = Y )
44 39 41 43 3eqtr3d 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ ( x e. ( K i^i ( Clsd ` K ) ) /\ x =/= (/) ) ) -> x = Y )
45 44 expr 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ x e. ( K i^i ( Clsd ` K ) ) ) -> ( x =/= (/) -> x = Y ) )
46 4 45 syl5bir 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ x e. ( K i^i ( Clsd ` K ) ) ) -> ( -. x = (/) -> x = Y ) )
47 46 orrd 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ x e. ( K i^i ( Clsd ` K ) ) ) -> ( x = (/) \/ x = Y ) )
48 vex 
 |-  x e. _V
49 48 elpr 
 |-  ( x e. { (/) , Y } <-> ( x = (/) \/ x = Y ) )
50 47 49 sylibr 
 |-  ( ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) /\ x e. ( K i^i ( Clsd ` K ) ) ) -> x e. { (/) , Y } )
51 50 ex 
 |-  ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> ( x e. ( K i^i ( Clsd ` K ) ) -> x e. { (/) , Y } ) )
52 51 ssrdv 
 |-  ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> ( K i^i ( Clsd ` K ) ) C_ { (/) , Y } )
53 1 isconn2 
 |-  ( K e. Conn <-> ( K e. Top /\ ( K i^i ( Clsd ` K ) ) C_ { (/) , Y } ) )
54 3 52 53 sylanbrc 
 |-  ( ( J e. Conn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. Conn )