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 } )