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=J
dnsconst.2 Y=K
Assertion dnsconst KFreFJCnKPYAF-1PclsJA=XF:XP

Proof

Step Hyp Ref Expression
1 dnsconst.1 X=J
2 dnsconst.2 Y=K
3 simplr KFreFJCnKPYAF-1PclsJA=XFJCnK
4 1 2 cnf FJCnKF:XY
5 ffn F:XYFFnX
6 3 4 5 3syl KFreFJCnKPYAF-1PclsJA=XFFnX
7 simpr3 KFreFJCnKPYAF-1PclsJA=XclsJA=X
8 simpll KFreFJCnKPYAF-1PclsJA=XKFre
9 simpr1 KFreFJCnKPYAF-1PclsJA=XPY
10 2 t1sncld KFrePYPClsdK
11 8 9 10 syl2anc KFreFJCnKPYAF-1PclsJA=XPClsdK
12 cnclima FJCnKPClsdKF-1PClsdJ
13 3 11 12 syl2anc KFreFJCnKPYAF-1PclsJA=XF-1PClsdJ
14 simpr2 KFreFJCnKPYAF-1PclsJA=XAF-1P
15 1 clsss2 F-1PClsdJAF-1PclsJAF-1P
16 13 14 15 syl2anc KFreFJCnKPYAF-1PclsJA=XclsJAF-1P
17 7 16 eqsstrrd KFreFJCnKPYAF-1PclsJA=XXF-1P
18 fconst3 F:XPFFnXXF-1P
19 6 17 18 sylanbrc KFreFJCnKPYAF-1PclsJA=XF:XP