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 ⊢ 𝑋 = ∪ 𝐽
conncn.j ⊢ ( 𝜑 → 𝐽 ∈ Conn )
conncn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
conncn.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐾 )
conncn.c ⊢ ( 𝜑 → 𝑈 ∈ ( Clsd ‘ 𝐾 ) )
conncn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
conncn.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 )
Assertion conncn ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑈 )

Proof

Step Hyp Ref Expression
1 conncn.x ⊢ 𝑋 = ∪ 𝐽
2 conncn.j ⊢ ( 𝜑 → 𝐽 ∈ Conn )
3 conncn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 conncn.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐾 )
5 conncn.c ⊢ ( 𝜑 → 𝑈 ∈ ( Clsd ‘ 𝐾 ) )
6 conncn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
7 conncn.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 )
8 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
9 1 8 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
10 3 9 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
11 10 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
12 10 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ∪ 𝐾 )
13 dffn4 ⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
14 11 13 sylib ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ ran 𝐹 )
15 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
16 3 15 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
17 8 restuni ⊢ ( ( 𝐾 ∈ Top ∧ ran 𝐹 ⊆ ∪ 𝐾 ) → ran 𝐹 = ∪ ( 𝐾 ↾t ran 𝐹 ) )
18 16 12 17 syl2anc ⊢ ( 𝜑 → ran 𝐹 = ∪ ( 𝐾 ↾t ran 𝐹 ) )
19 foeq3 ⊢ ( ran 𝐹 = ∪ ( 𝐾 ↾t ran 𝐹 ) → ( 𝐹 : 𝑋 –onto→ ran 𝐹 ↔ 𝐹 : 𝑋 –onto→ ∪ ( 𝐾 ↾t ran 𝐹 ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( 𝐹 : 𝑋 –onto→ ran 𝐹 ↔ 𝐹 : 𝑋 –onto→ ∪ ( 𝐾 ↾t ran 𝐹 ) ) )
21 14 20 mpbid ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ ∪ ( 𝐾 ↾t ran 𝐹 ) )
22 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
23 16 22 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
24 ssidd ⊢ ( 𝜑 → ran 𝐹 ⊆ ran 𝐹 )
25 cnrest2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran 𝐹 ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ ∪ 𝐾 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) ) )
26 23 24 12 25 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) ) )
27 3 26 mpbid ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) )
28 eqid ⊢ ∪ ( 𝐾 ↾t ran 𝐹 ) = ∪ ( 𝐾 ↾t ran 𝐹 )
29 28 cnconn ⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ ∪ ( 𝐾 ↾t ran 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) ) → ( 𝐾 ↾t ran 𝐹 ) ∈ Conn )
30 2 21 27 29 syl3anc ⊢ ( 𝜑 → ( 𝐾 ↾t ran 𝐹 ) ∈ Conn )
31 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
32 11 6 31 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
33 inelcm ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) → ( 𝑈 ∩ ran 𝐹 ) ≠ ∅ )
34 7 32 33 syl2anc ⊢ ( 𝜑 → ( 𝑈 ∩ ran 𝐹 ) ≠ ∅ )
35 8 12 30 4 34 5 connsubclo ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑈 )
36 df-f ⊢ ( 𝐹 : 𝑋 ⟶ 𝑈 ↔ ( 𝐹 Fn 𝑋 ∧ ran 𝐹 ⊆ 𝑈 ) )
37 11 35 36 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑈 )