pconnconn

Description: A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	pconnconn	$⊢ J \in PConn \to J \in Conn$

Proof

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \leftrightarrow ((x \neq \emptyset \land y \neq \emptyset) \land x \cap y = \emptyset)$
2		n0	$⊢ x \neq \emptyset \leftrightarrow \exists a a \in x$
3		n0	$⊢ y \neq \emptyset \leftrightarrow \exists b b \in y$
4	2 3	anbi12i	$⊢ (x \neq \emptyset \land y \neq \emptyset) \leftrightarrow (\exists a a \in x \land \exists b b \in y)$
5		exdistrv	$⊢ \exists a \exists b (a \in x \land b \in y) \leftrightarrow (\exists a a \in x \land \exists b b \in y)$
6	4 5	bitr4i	$⊢ (x \neq \emptyset \land y \neq \emptyset) \leftrightarrow \exists a \exists b (a \in x \land b \in y)$
7		simpll	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to J \in PConn$
8		simprll	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to a \in x$
9		simplrl	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to x \in J$
10		elunii	$⊢ (a \in x \land x \in J) \to a \in ⋃ J$
11	8 9 10	syl2anc	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to a \in ⋃ J$
12		simprlr	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to b \in y$
13		simplrr	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to y \in J$
14		elunii	$⊢ (b \in y \land y \in J) \to b \in ⋃ J$
15	12 13 14	syl2anc	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to b \in ⋃ J$
16		eqid	$⊢ ⋃ J = ⋃ J$
17	16	pconncn	$⊢ (J \in PConn \land a \in ⋃ J \land b \in ⋃ J) \to \exists f \in (II Cn J) (f (0) = a \land f (1) = b)$
18	7 11 15 17	syl3anc	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to \exists f \in (II Cn J) (f (0) = a \land f (1) = b)$
19		simplrr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to x \cap y = \emptyset$
20		simplrr	$⊢ ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J) \to f (1) = b$
21	20	adantl	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to f (1) = b$
22		iiuni	$⊢ [0, 1] = ⋃ II$
23		iiconn	$⊢ II \in Conn$
24	23	a1i	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to II \in Conn$
25		simprll	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to f \in (II Cn J)$
26	9	adantr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to x \in J$
27		uncom	$⊢ y \cup x = x \cup y$
28		simprr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to x \cup y = ⋃ J$
29	27 28	syl5eq	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to y \cup x = ⋃ J$
30	13	adantr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to y \in J$
31		elssuni	$⊢ y \in J \to y \subseteq ⋃ J$
32	30 31	syl	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to y \subseteq ⋃ J$
33		incom	$⊢ y \cap x = x \cap y$
34	33 19	syl5eq	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to y \cap x = \emptyset$
35		uneqdifeq	$⊢ (y \subseteq ⋃ J \land y \cap x = \emptyset) \to (y \cup x = ⋃ J \leftrightarrow ⋃ J ∖ y = x)$
36	32 34 35	syl2anc	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to (y \cup x = ⋃ J \leftrightarrow ⋃ J ∖ y = x)$
37	29 36	mpbid	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to ⋃ J ∖ y = x$
38		pconntop	$⊢ J \in PConn \to J \in Top$
39	38	ad3antrrr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to J \in Top$
40	16	opncld	$⊢ (J \in Top \land y \in J) \to ⋃ J ∖ y \in Clsd (J)$
41	39 30 40	syl2anc	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to ⋃ J ∖ y \in Clsd (J)$
42	37 41	eqeltrrd	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to x \in Clsd (J)$
43		0elunit	$⊢ 0 \in [0, 1]$
44	43	a1i	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to 0 \in [0, 1]$
45		simplrl	$⊢ ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J) \to f (0) = a$
46	45	adantl	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to f (0) = a$
47	8	adantr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to a \in x$
48	46 47	eqeltrd	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to f (0) \in x$
49	22 24 25 26 42 44 48	conncn	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to f : [0, 1] ⟶ x$
50		1elunit	$⊢ 1 \in [0, 1]$
51		ffvelrn	$⊢ (f : [0, 1] ⟶ x \land 1 \in [0, 1]) \to f (1) \in x$
52	49 50 51	sylancl	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to f (1) \in x$
53	21 52	eqeltrrd	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to b \in x$
54	12	adantr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to b \in y$
55		inelcm	$⊢ (b \in x \land b \in y) \to x \cap y \neq \emptyset$
56	53 54 55	syl2anc	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to x \cap y \neq \emptyset$
57	19 56	pm2.21ddne	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land ((f \in (II Cn J) \land (f (0) = a \land f (1) = b)) \land x \cup y = ⋃ J)) \to \neg x \cup y = ⋃ J$
58	57	expr	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land (f \in (II Cn J) \land (f (0) = a \land f (1) = b))) \to (x \cup y = ⋃ J \to \neg x \cup y = ⋃ J)$
59	58	pm2.01d	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land (f \in (II Cn J) \land (f (0) = a \land f (1) = b))) \to \neg x \cup y = ⋃ J$
60	59	neqned	$⊢ (((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \land (f \in (II Cn J) \land (f (0) = a \land f (1) = b))) \to x \cup y \neq ⋃ J$
61	18 60	rexlimddv	$⊢ ((J \in PConn \land (x \in J \land y \in J)) \land ((a \in x \land b \in y) \land x \cap y = \emptyset)) \to x \cup y \neq ⋃ J$
62	61	exp32	$⊢ (J \in PConn \land (x \in J \land y \in J)) \to ((a \in x \land b \in y) \to (x \cap y = \emptyset \to x \cup y \neq ⋃ J))$
63	62	exlimdvv	$⊢ (J \in PConn \land (x \in J \land y \in J)) \to (\exists a \exists b (a \in x \land b \in y) \to (x \cap y = \emptyset \to x \cup y \neq ⋃ J))$
64	6 63	syl5bi	$⊢ (J \in PConn \land (x \in J \land y \in J)) \to ((x \neq \emptyset \land y \neq \emptyset) \to (x \cap y = \emptyset \to x \cup y \neq ⋃ J))$
65	64	impd	$⊢ (J \in PConn \land (x \in J \land y \in J)) \to (((x \neq \emptyset \land y \neq \emptyset) \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J)$
66	1 65	syl5bi	$⊢ (J \in PConn \land (x \in J \land y \in J)) \to ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J)$
67	66	ralrimivva	$⊢ J \in PConn \to \forall x \in J \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J)$
68	16	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
69	38 68	sylib	$⊢ J \in PConn \to J \in TopOn (⋃ J)$
70		dfconn2	$⊢ J \in TopOn (⋃ J) \to (J \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J))$
71	69 70	syl	$⊢ J \in PConn \to (J \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J))$
72	67 71	mpbird	$⊢ J \in PConn \to J \in Conn$

Metamath Proof Explorer

Theorem pconnconn

Proof