cnconn

Description: Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Hypothesis	cnconn.2	$⊢ Y = ⋃ K$
	Assertion	cnconn	$⊢ (J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Conn$

Proof

Step	Hyp	Ref	Expression
1		cnconn.2	$⊢ Y = ⋃ K$
2		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
3	2	3ad2ant3	$⊢ (J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Top$
4		df-ne	$⊢ x \neq \emptyset \leftrightarrow \neg x = \emptyset$
5		eqid	$⊢ ⋃ J = ⋃ J$
6		simpl1	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to J \in Conn$
7		simpl3	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F \in (J Cn K)$
8		simprl	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \in (K \cap Clsd (K))$
9	8	elin1d	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \in K$
10		cnima	$⊢ (F \in (J Cn K) \land x \in K) \to F^{-1} [x] \in J$
11	7 9 10	syl2anc	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F^{-1} [x] \in J$
12		elssuni	$⊢ x \in K \to x \subseteq ⋃ K$
13	9 12	syl	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \subseteq ⋃ K$
14	13 1	sseqtrrdi	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \subseteq Y$
15		simpl2	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F : X \underset{onto}{⟶} Y$
16		forn	$⊢ F : X \underset{onto}{⟶} Y \to ran F = Y$
17	15 16	syl	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to ran F = Y$
18	14 17	sseqtrrd	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \subseteq ran F$
19		df-rn	$⊢ ran F = dom F^{-1}$
20	18 19	sseqtrdi	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \subseteq dom F^{-1}$
21		sseqin2	$⊢ x \subseteq dom F^{-1} \leftrightarrow dom F^{-1} \cap x = x$
22	20 21	sylib	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to dom F^{-1} \cap x = x$
23		simprr	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \neq \emptyset$
24	22 23	eqnetrd	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to dom F^{-1} \cap x \neq \emptyset$
25		imadisj	$⊢ F^{-1} [x] = \emptyset \leftrightarrow dom F^{-1} \cap x = \emptyset$
26	25	necon3bii	$⊢ F^{-1} [x] \neq \emptyset \leftrightarrow dom F^{-1} \cap x \neq \emptyset$
27	24 26	sylibr	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F^{-1} [x] \neq \emptyset$
28	8	elin2d	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x \in Clsd (K)$
29		cnclima	$⊢ (F \in (J Cn K) \land x \in Clsd (K)) \to F^{-1} [x] \in Clsd (J)$
30	7 28 29	syl2anc	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F^{-1} [x] \in Clsd (J)$
31	5 6 11 27 30	connclo	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F^{-1} [x] = ⋃ J$
32	5 1	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ Y$
33		fdm	$⊢ F : ⋃ J ⟶ Y \to dom F = ⋃ J$
34	7 32 33	3syl	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to dom F = ⋃ J$
35		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
36		fdm	$⊢ F : X ⟶ Y \to dom F = X$
37	15 35 36	3syl	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to dom F = X$
38	31 34 37	3eqtr2d	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F^{-1} [x] = X$
39	38	imaeq2d	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F [F^{-1} [x]] = F [X]$
40		foimacnv	$⊢ (F : X \underset{onto}{⟶} Y \land x \subseteq Y) \to F [F^{-1} [x]] = x$
41	15 14 40	syl2anc	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F [F^{-1} [x]] = x$
42		foima	$⊢ F : X \underset{onto}{⟶} Y \to F [X] = Y$
43	15 42	syl	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to F [X] = Y$
44	39 41 43	3eqtr3d	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (x \in (K \cap Clsd (K)) \land x \neq \emptyset)) \to x = Y$
45	44	expr	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land x \in (K \cap Clsd (K))) \to (x \neq \emptyset \to x = Y)$
46	4 45	syl5bir	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land x \in (K \cap Clsd (K))) \to (\neg x = \emptyset \to x = Y)$
47	46	orrd	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land x \in (K \cap Clsd (K))) \to (x = \emptyset \lor x = Y)$
48		vex	$⊢ x \in V$
49	48	elpr	$⊢ x \in \{\emptyset, Y\} \leftrightarrow (x = \emptyset \lor x = Y)$
50	47 49	sylibr	$⊢ ((J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land x \in (K \cap Clsd (K))) \to x \in \{\emptyset, Y\}$
51	50	ex	$⊢ (J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to (x \in (K \cap Clsd (K)) \to x \in \{\emptyset, Y\})$
52	51	ssrdv	$⊢ (J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \cap Clsd (K) \subseteq \{\emptyset, Y\}$
53	1	isconn2	$⊢ K \in Conn \leftrightarrow (K \in Top \land K \cap Clsd (K) \subseteq \{\emptyset, Y\})$
54	3 52 53	sylanbrc	$⊢ (J \in Conn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Conn$

Metamath Proof Explorer

Theorem cnconn

Proof