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 ⊢ 𝑋 = ∪ 𝐽
dnsconst.2 ⊢ 𝑌 = ∪ 𝐾
Assertion dnsconst ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐹 : 𝑋 ⟶ { 𝑃 } )

Proof

Step Hyp Ref Expression
1 dnsconst.1 ⊢ 𝑋 = ∪ 𝐽
2 dnsconst.2 ⊢ 𝑌 = ∪ 𝐾
3 simplr ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 1 2 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
5 ffn ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 Fn 𝑋 )
6 3 4 5 3syl ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐹 Fn 𝑋 )
7 simpr3 ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
8 simpll ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐾 ∈ Fre )
9 simpr1 ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝑃 ∈ 𝑌 )
10 2 t1sncld ⊢ ( ( 𝐾 ∈ Fre ∧ 𝑃 ∈ 𝑌 ) → { 𝑃 } ∈ ( Clsd ‘ 𝐾 ) )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → { 𝑃 } ∈ ( Clsd ‘ 𝐾 ) )
12 cnclima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ { 𝑃 } ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ { 𝑃 } ) ∈ ( Clsd ‘ 𝐽 ) )
13 3 11 12 syl2anc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ◡ 𝐹 “ { 𝑃 } ) ∈ ( Clsd ‘ 𝐽 ) )
14 simpr2 ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) )
15 1 clsss2 ⊢ ( ( ( ◡ 𝐹 “ { 𝑃 } ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( ◡ 𝐹 “ { 𝑃 } ) )
16 13 14 15 syl2anc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( ◡ 𝐹 “ { 𝑃 } ) )
17 7 16 eqsstrrd ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝑋 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) )
18 fconst3 ⊢ ( 𝐹 : 𝑋 ⟶ { 𝑃 } ↔ ( 𝐹 Fn 𝑋 ∧ 𝑋 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ) )
19 6 17 18 sylanbrc ⊢ ( ( ( 𝐾 ∈ Fre ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝑃 } ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐹 : 𝑋 ⟶ { 𝑃 } )