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

Metamath Proof Explorer

Theorem dnsconst

Description: If a continuous mapping to a T_1 space is constant on a dense subset, it is constant on the entire space. Note that ( ( clsJ )A ) = X means " A is dense in X " and A C_ (`' F " { P } ) means " F is constant on A ` " (see funconstss ). (Contributed by NM, 15-Mar-2007) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses dnsconst.1 
|- X = U. J
dnsconst.2 
|- Y = U. K
Assertion dnsconst 
|- ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> F : X --> { P } )

Proof

Step Hyp Ref Expression
1 dnsconst.1 
 |-  X = U. J
2 dnsconst.2 
 |-  Y = U. K
3 simplr 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> F e. ( J Cn K ) )
4 1 2 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> Y )
5 ffn 
 |-  ( F : X --> Y -> F Fn X )
6 3 4 5 3syl 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> F Fn X )
7 simpr3 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> ( ( cls ` J ) ` A ) = X )
8 simpll 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> K e. Fre )
9 simpr1 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> P e. Y )
10 2 t1sncld 
 |-  ( ( K e. Fre /\ P e. Y ) -> { P } e. ( Clsd ` K ) )
11 8 9 10 syl2anc 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> { P } e. ( Clsd ` K ) )
12 cnclima 
 |-  ( ( F e. ( J Cn K ) /\ { P } e. ( Clsd ` K ) ) -> ( `' F " { P } ) e. ( Clsd ` J ) )
13 3 11 12 syl2anc 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> ( `' F " { P } ) e. ( Clsd ` J ) )
14 simpr2 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> A C_ ( `' F " { P } ) )
15 1 clsss2 
 |-  ( ( ( `' F " { P } ) e. ( Clsd ` J ) /\ A C_ ( `' F " { P } ) ) -> ( ( cls ` J ) ` A ) C_ ( `' F " { P } ) )
16 13 14 15 syl2anc 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> ( ( cls ` J ) ` A ) C_ ( `' F " { P } ) )
17 7 16 eqsstrrd 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> X C_ ( `' F " { P } ) )
18 fconst3 
 |-  ( F : X --> { P } <-> ( F Fn X /\ X C_ ( `' F " { P } ) ) )
19 6 17 18 sylanbrc 
 |-  ( ( ( K e. Fre /\ F e. ( J Cn K ) ) /\ ( P e. Y /\ A C_ ( `' F " { P } ) /\ ( ( cls ` J ) ` A ) = X ) ) -> F : X --> { P } )