Metamath Proof Explorer

Theorem connima

Description: The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses connima.x 
|- X = U. J
connima.f 
|- ( ph -> F e. ( J Cn K ) )
connima.a 
|- ( ph -> A C_ X )
connima.c 
|- ( ph -> ( J |`t A ) e. Conn )
Assertion connima 
|- ( ph -> ( K |`t ( F " A ) ) e. Conn )

Proof

Step Hyp Ref Expression
1 connima.x 
 |-  X = U. J
2 connima.f 
 |-  ( ph -> F e. ( J Cn K ) )
3 connima.a 
 |-  ( ph -> A C_ X )
4 connima.c 
 |-  ( ph -> ( J |`t A ) e. Conn )
5 eqid 
 |-  U. K = U. K
6 1 5 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> U. K )
7 2 6 syl 
 |-  ( ph -> F : X --> U. K )
8 7 ffund 
 |-  ( ph -> Fun F )
9 7 fdmd 
 |-  ( ph -> dom F = X )
10 3 9 sseqtrrd 
 |-  ( ph -> A C_ dom F )
11 fores 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) : A -onto-> ( F " A ) )
12 8 10 11 syl2anc 
 |-  ( ph -> ( F |` A ) : A -onto-> ( F " A ) )
13 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
14 2 13 syl 
 |-  ( ph -> K e. Top )
15 imassrn 
 |-  ( F " A ) C_ ran F
16 7 frnd 
 |-  ( ph -> ran F C_ U. K )
17 15 16 sstrid 
 |-  ( ph -> ( F " A ) C_ U. K )
18 5 restuni 
 |-  ( ( K e. Top /\ ( F " A ) C_ U. K ) -> ( F " A ) = U. ( K |`t ( F " A ) ) )
19 14 17 18 syl2anc 
 |-  ( ph -> ( F " A ) = U. ( K |`t ( F " A ) ) )
20 foeq3 
 |-  ( ( F " A ) = U. ( K |`t ( F " A ) ) -> ( ( F |` A ) : A -onto-> ( F " A ) <-> ( F |` A ) : A -onto-> U. ( K |`t ( F " A ) ) ) )
21 19 20 syl 
 |-  ( ph -> ( ( F |` A ) : A -onto-> ( F " A ) <-> ( F |` A ) : A -onto-> U. ( K |`t ( F " A ) ) ) )
22 12 21 mpbid 
 |-  ( ph -> ( F |` A ) : A -onto-> U. ( K |`t ( F " A ) ) )
23 1 cnrest 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
24 2 3 23 syl2anc 
 |-  ( ph -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
25 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
26 14 25 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
27 df-ima 
 |-  ( F " A ) = ran ( F |` A )
28 eqimss2 
 |-  ( ( F " A ) = ran ( F |` A ) -> ran ( F |` A ) C_ ( F " A ) )
29 27 28 mp1i 
 |-  ( ph -> ran ( F |` A ) C_ ( F " A ) )
30 cnrest2 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ran ( F |` A ) C_ ( F " A ) /\ ( F " A ) C_ U. K ) -> ( ( F |` A ) e. ( ( J |`t A ) Cn K ) <-> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t ( F " A ) ) ) ) )
31 26 29 17 30 syl3anc 
 |-  ( ph -> ( ( F |` A ) e. ( ( J |`t A ) Cn K ) <-> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t ( F " A ) ) ) ) )
32 24 31 mpbid 
 |-  ( ph -> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t ( F " A ) ) ) )
33 eqid 
 |-  U. ( K |`t ( F " A ) ) = U. ( K |`t ( F " A ) )
34 33 cnconn 
 |-  ( ( ( J |`t A ) e. Conn /\ ( F |` A ) : A -onto-> U. ( K |`t ( F " A ) ) /\ ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t ( F " A ) ) ) ) -> ( K |`t ( F " A ) ) e. Conn )
35 4 22 32 34 syl3anc 
 |-  ( ph -> ( K |`t ( F " A ) ) e. Conn )