connpconn

Description: A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015)

		Ref	Expression
	Assertion	connpconn	$⊢ (J \in Conn \land J \in N-LocallyPConn\toJ \in PConn)$

Proof

Step	Hyp	Ref	Expression
1		conntop	$⊢ J \in Conn \to J \in Top$
2	1	adantr	$⊢ (J \in Conn \land J \in N-LocallyPConn\toJ \in Top)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		simpll	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\toJ \in Conn))$
5		inss1	$⊢ J \cap Clsd (J) \subseteq J$
6		simplr	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\toJ \in N-LocallyPConn))$
7	1	ad2antrr	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\toJ \in Top))$
8	3	topopn	$⊢ J \in Top \to ⋃ J \in J$
9	7 8	syl	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\to⋃ J \in J))$
10		simprr	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\toz \in ⋃ J))$
11		nlly2i	$⊢ (J \in N-LocallyPConn\land⋃ J \in J\landz \in ⋃ J\to\exists s \in 𝒫 ⋃ J \exists u \in J (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))$
12	6 9 10 11	syl3anc	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\to\exists s \in 𝒫 ⋃ J \exists u \in J (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn)))$
13		simprr1	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\toz \in u)))$
14		eqeq2	$⊢ y = w \to (f (1) = y \leftrightarrow f (1) = w)$
15	14	anbi2d	$⊢ y = w \to ((f (0) = x \land f (1) = y) \leftrightarrow (f (0) = x \land f (1) = w))$
16	15	rexbidv	$⊢ y = w \to (\exists f \in (II Cn J) (f (0) = x \land f (1) = y) \leftrightarrow \exists f \in (II Cn J) (f (0) = x \land f (1) = w))$
17	16	elrab	$⊢ w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \leftrightarrow (w \in ⋃ J \land \exists f \in (II Cn J) (f (0) = x \land f (1) = w))$
18	17	simprbi	$⊢ w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to \exists f \in (II Cn J) (f (0) = x \land f (1) = w)$
19		simprr3	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\toJ ↾_{𝑡} s \in PConn)))$
20	19	adantr	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\toJ ↾_{𝑡} s \in PConn))))$
21		simprr2	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\tou \subseteq s)))$
22	21	adantr	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\tou \subseteq s))))$
23		simprll	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\tow \in u))))$
24	22 23	sseldd	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\tow \in s))))$
25	7	ad2antrr	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\toJ \in Top))))$
26		elpwi	$⊢ s \in 𝒫 ⋃ J \to s \subseteq ⋃ J$
27	26	ad2antrl	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\tos \subseteq ⋃ J)))$
28	27	adantr	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\tos \subseteq ⋃ J))))$
29	3	restuni	$⊢ (J \in Top \land s \subseteq ⋃ J) \to s = ⋃ (J ↾_{𝑡} s)$
30	25 28 29	syl2anc	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\tos = ⋃ (J ↾_{𝑡} s)))))$
31	24 30	eleqtrd	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\tow \in ⋃ (J ↾_{𝑡} s)))))$
32		simprr	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\toy \in u))))$
33	22 32	sseldd	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\toy \in s))))$
34	33 30	eleqtrd	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\toy \in ⋃ (J ↾_{𝑡} s)))))$
35		eqid	$⊢ ⋃ (J ↾_{𝑡} s) = ⋃ (J ↾_{𝑡} s)$
36	35	pconncn	$⊢ (J ↾_{𝑡} s \in PConn \land w \in ⋃ (J ↾_{𝑡} s) \land y \in ⋃ (J ↾_{𝑡} s)) \to \exists h \in (II Cn (J ↾_{𝑡} s)) (h (0) = w \land h (1) = y)$
37	20 31 34 36	syl3anc	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\to\exists h \in (II Cn (J ↾_{𝑡} s)) (h (0) = w \land h (1) = y)))))$
38		simplrl	$⊢ ((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u) \to g \in (II Cn J)$
39	38	ad2antlr	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\tog \in (II Cn J))))))$
40	25	adantr	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\toJ \in Top)))))$
41		cnrest2r	$⊢ J \in Top \to II Cn (J ↾_{𝑡} s) \subseteq II Cn J$
42	40 41	syl	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\toII Cn (J ↾_{𝑡} s) \subseteq II Cn J)))))$
43		simprl	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\toh \in (II Cn (J ↾_{𝑡} s)))))))$
44	42 43	sseldd	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\toh \in (II Cn J))))))$
45		simplrr	$⊢ ((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u) \to (g (0) = x \land g (1) = w)$
46	45	ad2antlr	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\to(g (0) = x \land g (1) = w))))))$
47	46	simprd	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\tog (1) = w)))))$
48		simprrl	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\toh (0) = w)))))$
49	47 48	eqtr4d	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\tog (1) = h (0))))))$
50	39 44 49	pcocn	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\tog *_{𝑝} (J) h \in (II Cn J))))))$
51	39 44	pco0	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\to(g *_{𝑝} (J) h) (0) = g (0))))))$
52	46	simpld	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\tog (0) = x)))))$
53	51 52	eqtrd	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\to(g *_{𝑝} (J) h) (0) = x)))))$
54	39 44	pco1	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\to(g *_{𝑝} (J) h) (1) = h (1))))))$
55		simprrr	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\toh (1) = y)))))$
56	54 55	eqtrd	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\to(g *_{𝑝} (J) h) (1) = y)))))$
57		fveq1	$⊢ f = g _{𝑝} (J) h \to f (0) = (g _{𝑝} (J) h) (0)$
58	57	eqeq1d	$⊢ f = g _{𝑝} (J) h \to (f (0) = x \leftrightarrow (g _{𝑝} (J) h) (0) = x)$
59		fveq1	$⊢ f = g _{𝑝} (J) h \to f (1) = (g _{𝑝} (J) h) (1)$
60	59	eqeq1d	$⊢ f = g _{𝑝} (J) h \to (f (1) = y \leftrightarrow (g _{𝑝} (J) h) (1) = y)$
61	58 60	anbi12d	$⊢ f = g _{𝑝} (J) h \to ((f (0) = x \land f (1) = y) \leftrightarrow ((g _{𝑝} (J) h) (0) = x \land (g *_{𝑝} (J) h) (1) = y))$
62	61	rspcev	$⊢ (g _{𝑝} (J) h \in (II Cn J) \land ((g _{𝑝} (J) h) (0) = x \land (g *_{𝑝} (J) h) (1) = y)) \to \exists f \in (II Cn J) (f (0) = x \land f (1) = y)$
63	50 53 56 62	syl12anc	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\land(h \in (II Cn (J ↾_{𝑡} s)) \land (h (0) = w \land h (1) = y))\to\exists f \in (II Cn J) (f (0) = x \land f (1) = y))))))$
64	37 63	rexlimddv	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land((w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w))) \land y \in u)\to\exists f \in (II Cn J) (f (0) = x \land f (1) = y)))))$
65	64	anassrs	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land(w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w)))\landy \in u\to\exists f \in (II Cn J) (f (0) = x \land f (1) = y))))))$
66	65	ralrimiva	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\land(w \in u \land (g \in (II Cn J) \land (g (0) = x \land g (1) = w)))\to\forall y \in u \exists f \in (II Cn J) (f (0) = x \land f (1) = y)))))$
67	66	anassrs	$⊢ (((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\land(g \in (II Cn J) \land (g (0) = x \land g (1) = w))\to\forall y \in u \exists f \in (II Cn J) (f (0) = x \land f (1) = y))))))$
68	67	rexlimdvaa	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\to(\exists g \in (II Cn J) (g (0) = x \land g (1) = w) \to \forall y \in u \exists f \in (II Cn J) (f (0) = x \land f (1) = y))))))$
69	21	adantr	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\tou \subseteq s))))$
70		simplrl	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\tos \in 𝒫 ⋃ J))))$
71	70 26	syl	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\tos \subseteq ⋃ J))))$
72	69 71	sstrd	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\tou \subseteq ⋃ J))))$
73	68 72	jctild	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\to(\exists g \in (II Cn J) (g (0) = x \land g (1) = w) \to (u \subseteq ⋃ J \land \forall y \in u \exists f \in (II Cn J) (f (0) = x \land f (1) = y)))))))$
74		fveq1	$⊢ f = g \to f (0) = g (0)$
75	74	eqeq1d	$⊢ f = g \to (f (0) = x \leftrightarrow g (0) = x)$
76		fveq1	$⊢ f = g \to f (1) = g (1)$
77	76	eqeq1d	$⊢ f = g \to (f (1) = w \leftrightarrow g (1) = w)$
78	75 77	anbi12d	$⊢ f = g \to ((f (0) = x \land f (1) = w) \leftrightarrow (g (0) = x \land g (1) = w))$
79	78	cbvrexvw	$⊢ \exists f \in (II Cn J) (f (0) = x \land f (1) = w) \leftrightarrow \exists g \in (II Cn J) (g (0) = x \land g (1) = w)$
80		ssrab	$⊢ u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \leftrightarrow (u \subseteq ⋃ J \land \forall y \in u \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
81	73 79 80	3imtr4g	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\to(\exists f \in (II Cn J) (f (0) = x \land f (1) = w) \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))))$
82	18 81	syl5	$⊢ ((((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\landw \in u\to(w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))))$
83	82	ralrimiva	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\to\forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\}))))$
84	13 83	jca	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\land(s \in 𝒫 ⋃ J \land (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn))\to(z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))))$
85	84	expr	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\lands \in 𝒫 ⋃ J\to((z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn) \to (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\}))))))$
86	85	reximdv	$⊢ (((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\lands \in 𝒫 ⋃ J\to(\exists u \in J (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn) \to \exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\}))))))$
87	86	rexlimdva	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\to(\exists s \in 𝒫 ⋃ J \exists u \in J (z \in u \land u \subseteq s \land J ↾_{𝑡} s \in PConn) \to \exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))))$
88	12 87	mpd	$⊢ ((J \in Conn \land J \in N-LocallyPConn\land(x \in ⋃ J \land z \in ⋃ J)\to\exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\}))))$
89	88	anassrs	$⊢ (((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\landz \in ⋃ J\to\exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))))$
90	89	ralrimiva	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\forall z \in ⋃ J \exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\}))))$
91	1	ad2antrr	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\toJ \in Top))$
92		ssrab2	$⊢ \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \subseteq ⋃ J$
93	3	isclo2	$⊢ (J \in Top \land \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \subseteq ⋃ J) \to (\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \in (J \cap Clsd (J)) \leftrightarrow \forall z \in ⋃ J \exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))$
94	91 92 93	sylancl	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to(\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \in (J \cap Clsd (J)) \leftrightarrow \forall z \in ⋃ J \exists u \in J (z \in u \land \forall w \in u (w \in \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \to u \subseteq \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\})))))$
95	90 94	mpbird	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \in (J \cap Clsd (J))))$
96	5 95	sselid	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \in J))$
97		simpr	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\tox \in ⋃ J))$
98		iitopon	$⊢ II \in TopOn ([0, 1])$
99	98	a1i	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\toII \in TopOn ([0, 1])))$
100	3	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
101	91 100	sylib	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\toJ \in TopOn (⋃ J)))$
102		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (⋃ J) \land x \in ⋃ J) \to [0, 1] \times \{x\} \in (II Cn J)$
103	99 101 97 102	syl3anc	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to[0, 1] \times \{x\} \in (II Cn J)))$
104		0elunit	$⊢ 0 \in [0, 1]$
105		vex	$⊢ x \in V$
106	105	fvconst2	$⊢ 0 \in [0, 1] \to ([0, 1] \times \{x\}) (0) = x$
107	104 106	mp1i	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to([0, 1] \times \{x\}) (0) = x))$
108		1elunit	$⊢ 1 \in [0, 1]$
109	105	fvconst2	$⊢ 1 \in [0, 1] \to ([0, 1] \times \{x\}) (1) = x$
110	108 109	mp1i	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to([0, 1] \times \{x\}) (1) = x))$
111		eqeq2	$⊢ y = x \to (f (1) = y \leftrightarrow f (1) = x)$
112	111	anbi2d	$⊢ y = x \to ((f (0) = x \land f (1) = y) \leftrightarrow (f (0) = x \land f (1) = x))$
113		fveq1	$⊢ f = [0, 1] \times \{x\} \to f (0) = ([0, 1] \times \{x\}) (0)$
114	113	eqeq1d	$⊢ f = [0, 1] \times \{x\} \to (f (0) = x \leftrightarrow ([0, 1] \times \{x\}) (0) = x)$
115		fveq1	$⊢ f = [0, 1] \times \{x\} \to f (1) = ([0, 1] \times \{x\}) (1)$
116	115	eqeq1d	$⊢ f = [0, 1] \times \{x\} \to (f (1) = x \leftrightarrow ([0, 1] \times \{x\}) (1) = x)$
117	114 116	anbi12d	$⊢ f = [0, 1] \times \{x\} \to ((f (0) = x \land f (1) = x) \leftrightarrow (([0, 1] \times \{x\}) (0) = x \land ([0, 1] \times \{x\}) (1) = x))$
118	112 117	rspc2ev	$⊢ (x \in ⋃ J \land [0, 1] \times \{x\} \in (II Cn J) \land (([0, 1] \times \{x\}) (0) = x \land ([0, 1] \times \{x\}) (1) = x)) \to \exists y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y)$
119	97 103 107 110 118	syl112anc	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\exists y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y)))$
120		rabn0	$⊢ \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \neq \emptyset \leftrightarrow \exists y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y)$
121	119 120	sylibr	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \neq \emptyset))$
122		inss2	$⊢ J \cap Clsd (J) \subseteq Clsd (J)$
123	122 95	sselid	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \in Clsd (J)))$
124	3 4 96 121 123	connclo	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} = ⋃ J))$
125	124	eqcomd	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to⋃ J = \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\}))$
126		rabid2	$⊢ ⋃ J = \{y \in ⋃ J \| \exists f \in (II Cn J) (f (0) = x \land f (1) = y)\} \leftrightarrow \forall y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y)$
127	125 126	sylib	$⊢ ((J \in Conn \land J \in N-LocallyPConn\landx \in ⋃ J\to\forall y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y)))$
128	127	ralrimiva	$⊢ (J \in Conn \land J \in N-LocallyPConn\to\forall x \in ⋃ J \forall y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
129	3	ispconn	$⊢ J \in PConn \leftrightarrow (J \in Top \land \forall x \in ⋃ J \forall y \in ⋃ J \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
130	2 128 129	sylanbrc	$⊢ (J \in Conn \land J \in N-LocallyPConn\toJ \in PConn)$

Metamath Proof Explorer

Theorem connpconn

Proof