connima

Description: The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	connima.x	$⊢ X = ⋃ J$
	connima.f	$⊢ φ \to F \in (J Cn K)$
	connima.a	$⊢ φ \to A \subseteq X$
	connima.c	$⊢ φ \to J ↾_{𝑡} A \in Conn$
Assertion	connima	$⊢ φ \to K ↾_{𝑡} F [A] \in Conn$

Proof

Step	Hyp	Ref	Expression
1		connima.x	$⊢ X = ⋃ J$
2		connima.f	$⊢ φ \to F \in (J Cn K)$
3		connima.a	$⊢ φ \to A \subseteq X$
4		connima.c	$⊢ φ \to J ↾_{𝑡} A \in Conn$
5		eqid	$⊢ ⋃ K = ⋃ K$
6	1 5	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ ⋃ K$
7	2 6	syl	$⊢ φ \to F : X ⟶ ⋃ K$
8	7	ffund	$⊢ φ \to Fun F$
9	7	fdmd	$⊢ φ \to dom F = X$
10	3 9	sseqtrrd	$⊢ φ \to A \subseteq dom F$
11		fores	$⊢ (Fun F \land A \subseteq dom F) \to ({F ↾}_{A}) : A \underset{onto}{⟶} F [A]$
12	8 10 11	syl2anc	$⊢ φ \to ({F ↾}_{A}) : A \underset{onto}{⟶} F [A]$
13		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
14	2 13	syl	$⊢ φ \to K \in Top$
15		imassrn	$⊢ F [A] \subseteq ran F$
16	7	frnd	$⊢ φ \to ran F \subseteq ⋃ K$
17	15 16	sstrid	$⊢ φ \to F [A] \subseteq ⋃ K$
18	5	restuni	$⊢ (K \in Top \land F [A] \subseteq ⋃ K) \to F [A] = ⋃ (K ↾_{𝑡} F [A])$
19	14 17 18	syl2anc	$⊢ φ \to F [A] = ⋃ (K ↾_{𝑡} F [A])$
20		foeq3	$⊢ F [A] = ⋃ (K ↾_{𝑡} F [A]) \to (({F ↾}_{A}) : A \underset{onto}{⟶} F [A] \leftrightarrow ({F ↾}_{A}) : A \underset{onto}{⟶} ⋃ (K ↾_{𝑡} F [A]))$
21	19 20	syl	$⊢ φ \to (({F ↾}_{A}) : A \underset{onto}{⟶} F [A] \leftrightarrow ({F ↾}_{A}) : A \underset{onto}{⟶} ⋃ (K ↾_{𝑡} F [A]))$
22	12 21	mpbid	$⊢ φ \to ({F ↾}_{A}) : A \underset{onto}{⟶} ⋃ (K ↾_{𝑡} F [A])$
23	1	cnrest	$⊢ (F \in (J Cn K) \land A \subseteq X) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
24	2 3 23	syl2anc	$⊢ φ \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
25		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
26	14 25	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
27		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
28		eqimss2	$⊢ F [A] = ran ({F ↾}_{A}) \to ran ({F ↾}_{A}) \subseteq F [A]$
29	27 28	mp1i	$⊢ φ \to ran ({F ↾}_{A}) \subseteq F [A]$
30		cnrest2	$⊢ (K \in TopOn (⋃ K) \land ran ({F ↾}_{A}) \subseteq F [A] \land F [A] \subseteq ⋃ K) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} F [A])))$
31	26 29 17 30	syl3anc	$⊢ φ \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} F [A])))$
32	24 31	mpbid	$⊢ φ \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} F [A]))$
33		eqid	$⊢ ⋃ (K ↾_{𝑡} F [A]) = ⋃ (K ↾_{𝑡} F [A])$
34	33	cnconn	$⊢ (J ↾_{𝑡} A \in Conn \land ({F ↾}_{A}) : A \underset{onto}{⟶} ⋃ (K ↾_{𝑡} F [A]) \land {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} F [A]))) \to K ↾_{𝑡} F [A] \in Conn$
35	4 22 32 34	syl3anc	$⊢ φ \to K ↾_{𝑡} F [A] \in Conn$

Metamath Proof Explorer

Theorem connima

Proof