This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem conncn

Description: A continuous function from a connected topology with one point in a clopen set must lie entirely within the set. (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses conncn.x 
|- X = U. J
conncn.j 
|- ( ph -> J e. Conn )
conncn.f 
|- ( ph -> F e. ( J Cn K ) )
conncn.u 
|- ( ph -> U e. K )
conncn.c 
|- ( ph -> U e. ( Clsd ` K ) )
conncn.a 
|- ( ph -> A e. X )
conncn.1 
|- ( ph -> ( F ` A ) e. U )
Assertion conncn 
|- ( ph -> F : X --> U )

Proof

Step Hyp Ref Expression
1 conncn.x 
 |-  X = U. J
2 conncn.j 
 |-  ( ph -> J e. Conn )
3 conncn.f 
 |-  ( ph -> F e. ( J Cn K ) )
4 conncn.u 
 |-  ( ph -> U e. K )
5 conncn.c 
 |-  ( ph -> U e. ( Clsd ` K ) )
6 conncn.a 
 |-  ( ph -> A e. X )
7 conncn.1 
 |-  ( ph -> ( F ` A ) e. U )
8 eqid 
 |-  U. K = U. K
9 1 8 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> U. K )
10 3 9 syl 
 |-  ( ph -> F : X --> U. K )
11 10 ffnd 
 |-  ( ph -> F Fn X )
12 10 frnd 
 |-  ( ph -> ran F C_ U. K )
13 dffn4 
 |-  ( F Fn X <-> F : X -onto-> ran F )
14 11 13 sylib 
 |-  ( ph -> F : X -onto-> ran F )
15 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
16 3 15 syl 
 |-  ( ph -> K e. Top )
17 8 restuni 
 |-  ( ( K e. Top /\ ran F C_ U. K ) -> ran F = U. ( K |`t ran F ) )
18 16 12 17 syl2anc 
 |-  ( ph -> ran F = U. ( K |`t ran F ) )
19 foeq3 
 |-  ( ran F = U. ( K |`t ran F ) -> ( F : X -onto-> ran F <-> F : X -onto-> U. ( K |`t ran F ) ) )
20 18 19 syl 
 |-  ( ph -> ( F : X -onto-> ran F <-> F : X -onto-> U. ( K |`t ran F ) ) )
21 14 20 mpbid 
 |-  ( ph -> F : X -onto-> U. ( K |`t ran F ) )
22 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
23 16 22 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
24 ssidd 
 |-  ( ph -> ran F C_ ran F )
25 cnrest2 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ran F C_ ran F /\ ran F C_ U. K ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) )
26 23 24 12 25 syl3anc 
 |-  ( ph -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) )
27 3 26 mpbid 
 |-  ( ph -> F e. ( J Cn ( K |`t ran F ) ) )
28 eqid 
 |-  U. ( K |`t ran F ) = U. ( K |`t ran F )
29 28 cnconn 
 |-  ( ( J e. Conn /\ F : X -onto-> U. ( K |`t ran F ) /\ F e. ( J Cn ( K |`t ran F ) ) ) -> ( K |`t ran F ) e. Conn )
30 2 21 27 29 syl3anc 
 |-  ( ph -> ( K |`t ran F ) e. Conn )
31 fnfvelrn 
 |-  ( ( F Fn X /\ A e. X ) -> ( F ` A ) e. ran F )
32 11 6 31 syl2anc 
 |-  ( ph -> ( F ` A ) e. ran F )
33 inelcm 
 |-  ( ( ( F ` A ) e. U /\ ( F ` A ) e. ran F ) -> ( U i^i ran F ) =/= (/) )
34 7 32 33 syl2anc 
 |-  ( ph -> ( U i^i ran F ) =/= (/) )
35 8 12 30 4 34 5 connsubclo 
 |-  ( ph -> ran F C_ U )
36 df-f 
 |-  ( F : X --> U <-> ( F Fn X /\ ran F C_ U ) )
37 11 35 36 sylanbrc 
 |-  ( ph -> F : X --> U )