cnpconn

Description: An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cnpconn.2	$⊢ Y = ⋃ K$
2		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
3	2	3ad2ant3	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Top$
4		eqid	$⊢ ⋃ J = ⋃ J$
5	4	pconncn	$⊢ (J \in PConn \land u \in ⋃ J \land v \in ⋃ J) \to \exists g \in (II Cn J) (g (0) = u \land g (1) = v)$
6	5	3expb	$⊢ (J \in PConn \land (u \in ⋃ J \land v \in ⋃ J)) \to \exists g \in (II Cn J) (g (0) = u \land g (1) = v)$
7	6	3ad2antl1	$⊢ ((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \to \exists g \in (II Cn J) (g (0) = u \land g (1) = v)$
8		simprl	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to g \in (II Cn J)$
9		simpll3	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to F \in (J Cn K)$
10		cnco	$⊢ (g \in (II Cn J) \land F \in (J Cn K)) \to F \circ g \in (II Cn K)$
11	8 9 10	syl2anc	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to F \circ g \in (II Cn K)$
12		iiuni	$⊢ [0, 1] = ⋃ II$
13	12 4	cnf	$⊢ g \in (II Cn J) \to g : [0, 1] ⟶ ⋃ J$
14	8 13	syl	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to g : [0, 1] ⟶ ⋃ J$
15		0elunit	$⊢ 0 \in [0, 1]$
16		fvco3	$⊢ (g : [0, 1] ⟶ ⋃ J \land 0 \in [0, 1]) \to (F \circ g) (0) = F (g (0))$
17	14 15 16	sylancl	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to (F \circ g) (0) = F (g (0))$
18		simprrl	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to g (0) = u$
19	18	fveq2d	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to F (g (0)) = F (u)$
20	17 19	eqtrd	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to (F \circ g) (0) = F (u)$
21		1elunit	$⊢ 1 \in [0, 1]$
22		fvco3	$⊢ (g : [0, 1] ⟶ ⋃ J \land 1 \in [0, 1]) \to (F \circ g) (1) = F (g (1))$
23	14 21 22	sylancl	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to (F \circ g) (1) = F (g (1))$
24		simprrr	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to g (1) = v$
25	24	fveq2d	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to F (g (1)) = F (v)$
26	23 25	eqtrd	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to (F \circ g) (1) = F (v)$
27		fveq1	$⊢ f = F \circ g \to f (0) = (F \circ g) (0)$
28	27	eqeq1d	$⊢ f = F \circ g \to (f (0) = F (u) \leftrightarrow (F \circ g) (0) = F (u))$
29		fveq1	$⊢ f = F \circ g \to f (1) = (F \circ g) (1)$
30	29	eqeq1d	$⊢ f = F \circ g \to (f (1) = F (v) \leftrightarrow (F \circ g) (1) = F (v))$
31	28 30	anbi12d	$⊢ f = F \circ g \to ((f (0) = F (u) \land f (1) = F (v)) \leftrightarrow ((F \circ g) (0) = F (u) \land (F \circ g) (1) = F (v)))$
32	31	rspcev	$⊢ (F \circ g \in (II Cn K) \land ((F \circ g) (0) = F (u) \land (F \circ g) (1) = F (v))) \to \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v))$
33	11 20 26 32	syl12anc	$⊢ (((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \land (g \in (II Cn J) \land (g (0) = u \land g (1) = v))) \to \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v))$
34	7 33	rexlimddv	$⊢ ((J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \in ⋃ J \land v \in ⋃ J)) \to \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v))$
35	34	ralrimivva	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to \forall u \in ⋃ J \forall v \in ⋃ J \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v))$
36	4 1	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ Y$
37	36	3ad2ant3	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to F : ⋃ J ⟶ Y$
38		forn	$⊢ F : X \underset{onto}{⟶} Y \to ran F = Y$
39	38	3ad2ant2	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to ran F = Y$
40		dffo2	$⊢ F : ⋃ J \underset{onto}{⟶} Y \leftrightarrow (F : ⋃ J ⟶ Y \land ran F = Y)$
41	37 39 40	sylanbrc	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to F : ⋃ J \underset{onto}{⟶} Y$
42		eqeq2	$⊢ F (v) = y \to (f (1) = F (v) \leftrightarrow f (1) = y)$
43	42	anbi2d	$⊢ F (v) = y \to ((f (0) = F (u) \land f (1) = F (v)) \leftrightarrow (f (0) = F (u) \land f (1) = y))$
44	43	rexbidv	$⊢ F (v) = y \to (\exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v)) \leftrightarrow \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y))$
45	44	cbvfo	$⊢ F : ⋃ J \underset{onto}{⟶} Y \to (\forall v \in ⋃ J \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v)) \leftrightarrow \forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y))$
46	41 45	syl	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to (\forall v \in ⋃ J \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v)) \leftrightarrow \forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y))$
47	46	ralbidv	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to (\forall u \in ⋃ J \forall v \in ⋃ J \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = F (v)) \leftrightarrow \forall u \in ⋃ J \forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y))$
48	35 47	mpbid	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to \forall u \in ⋃ J \forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y)$
49		eqeq2	$⊢ F (u) = x \to (f (0) = F (u) \leftrightarrow f (0) = x)$
50	49	anbi1d	$⊢ F (u) = x \to ((f (0) = F (u) \land f (1) = y) \leftrightarrow (f (0) = x \land f (1) = y))$
51	50	rexbidv	$⊢ F (u) = x \to (\exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y) \leftrightarrow \exists f \in (II Cn K) (f (0) = x \land f (1) = y))$
52	51	ralbidv	$⊢ F (u) = x \to (\forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y) \leftrightarrow \forall y \in Y \exists f \in (II Cn K) (f (0) = x \land f (1) = y))$
53	52	cbvfo	$⊢ F : ⋃ J \underset{onto}{⟶} Y \to (\forall u \in ⋃ J \forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y) \leftrightarrow \forall x \in Y \forall y \in Y \exists f \in (II Cn K) (f (0) = x \land f (1) = y))$
54	41 53	syl	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to (\forall u \in ⋃ J \forall y \in Y \exists f \in (II Cn K) (f (0) = F (u) \land f (1) = y) \leftrightarrow \forall x \in Y \forall y \in Y \exists f \in (II Cn K) (f (0) = x \land f (1) = y))$
55	48 54	mpbid	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to \forall x \in Y \forall y \in Y \exists f \in (II Cn K) (f (0) = x \land f (1) = y)$
56	1	ispconn	$⊢ K \in PConn \leftrightarrow (K \in Top \land \forall x \in Y \forall y \in Y \exists f \in (II Cn K) (f (0) = x \land f (1) = y))$
57	3 55 56	sylanbrc	$⊢ (J \in PConn \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in PConn$

Metamath Proof Explorer

Theorem cnpconn

Proof