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 )