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	$⊢ X = ⋃ J$
	conncn.j	$⊢ φ \to J \in Conn$
	conncn.f	$⊢ φ \to F \in (J Cn K)$
	conncn.u	$⊢ φ \to U \in K$
	conncn.c	$⊢ φ \to U \in Clsd (K)$
	conncn.a	$⊢ φ \to A \in X$
	conncn.1	$⊢ φ \to F (A) \in U$
Assertion	conncn	$⊢ φ \to F : X ⟶ U$

Proof

Step	Hyp	Ref	Expression
1		conncn.x	$⊢ X = ⋃ J$
2		conncn.j	$⊢ φ \to J \in Conn$
3		conncn.f	$⊢ φ \to F \in (J Cn K)$
4		conncn.u	$⊢ φ \to U \in K$
5		conncn.c	$⊢ φ \to U \in Clsd (K)$
6		conncn.a	$⊢ φ \to A \in X$
7		conncn.1	$⊢ φ \to F (A) \in U$
8		eqid	$⊢ ⋃ K = ⋃ K$
9	1 8	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ ⋃ K$
10	3 9	syl	$⊢ φ \to F : X ⟶ ⋃ K$
11	10	ffnd	$⊢ φ \to F Fn X$
12	10	frnd	$⊢ φ \to ran F \subseteq ⋃ K$
13		dffn4	$⊢ F Fn X \leftrightarrow F : X \underset{onto}{⟶} ran F$
14	11 13	sylib	$⊢ φ \to F : X \underset{onto}{⟶} ran F$
15		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
16	3 15	syl	$⊢ φ \to K \in Top$
17	8	restuni	$⊢ (K \in Top \land ran F \subseteq ⋃ K) \to ran F = ⋃ (K ↾_{𝑡} ran F)$
18	16 12 17	syl2anc	$⊢ φ \to ran F = ⋃ (K ↾_{𝑡} ran F)$
19		foeq3	$⊢ ran F = ⋃ (K ↾_{𝑡} ran F) \to (F : X \underset{onto}{⟶} ran F \leftrightarrow F : X \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F))$
20	18 19	syl	$⊢ φ \to (F : X \underset{onto}{⟶} ran F \leftrightarrow F : X \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F))$
21	14 20	mpbid	$⊢ φ \to F : X \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F)$
22		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
23	16 22	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
24		ssidd	$⊢ φ \to ran F \subseteq ran F$
25		cnrest2	$⊢ (K \in TopOn (⋃ K) \land ran F \subseteq ran F \land ran F \subseteq ⋃ K) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} ran F)))$
26	23 24 12 25	syl3anc	$⊢ φ \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} ran F)))$
27	3 26	mpbid	$⊢ φ \to F \in (J Cn (K ↾_{𝑡} ran F))$
28		eqid	$⊢ ⋃ (K ↾_{𝑡} ran F) = ⋃ (K ↾_{𝑡} ran F)$
29	28	cnconn	$⊢ (J \in Conn \land F : X \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F) \land F \in (J Cn (K ↾_{𝑡} ran F))) \to K ↾_{𝑡} ran F \in Conn$
30	2 21 27 29	syl3anc	$⊢ φ \to K ↾_{𝑡} ran F \in Conn$
31		fnfvelrn	$⊢ (F Fn X \land A \in X) \to F (A) \in ran F$
32	11 6 31	syl2anc	$⊢ φ \to F (A) \in ran F$
33		inelcm	$⊢ (F (A) \in U \land F (A) \in ran F) \to U \cap ran F \neq \emptyset$
34	7 32 33	syl2anc	$⊢ φ \to U \cap ran F \neq \emptyset$
35	8 12 30 4 34 5	connsubclo	$⊢ φ \to ran F \subseteq U$
36		df-f	$⊢ F : X ⟶ U \leftrightarrow (F Fn X \land ran F \subseteq U)$
37	11 35 36	sylanbrc	$⊢ φ \to F : X ⟶ U$

Metamath Proof Explorer

Theorem conncn

Proof