dfconn2

Description: An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Assertion	dfconn2	$⊢ J \in TopOn (X) \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 X))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		simpll	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to J \in Conn$
3		simplrl	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to x \in J$
4		simpr1	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to x \neq \emptyset$
5		simplrr	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to y \in J$
6		simpr2	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to y \neq \emptyset$
7		simpr3	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to x \cap y = \emptyset$
8	1 2 3 4 5 6 7	conndisj	$⊢ ((J \in Conn \land (x \in J \land y \in J)) \land (x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset)) \to x \cup y \neq ⋃ J$
9	8	ex	$⊢ (J \in Conn \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)$
10	9	ralrimivva	$⊢ J \in Conn \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)$
11		topontop	$⊢ J \in TopOn (X) \to J \in Top$
12	1	cldopn	$⊢ x \in Clsd (J) \to ⋃ J ∖ x \in J$
13	12	adantl	$⊢ (J \in Top \land x \in Clsd (J)) \to ⋃ J ∖ x \in J$
14		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)$
15		ineq2	$⊢ y = ⋃ J ∖ x \to x \cap y = x \cap (⋃ J ∖ x)$
16		disjdif	$⊢ x \cap (⋃ J ∖ x) = \emptyset$
17	15 16	eqtrdi	$⊢ y = ⋃ J ∖ x \to x \cap y = \emptyset$
18	17	biantrud	$⊢ y = ⋃ J ∖ x \to ((x \neq \emptyset \land y \neq \emptyset) \leftrightarrow ((x \neq \emptyset \land y \neq \emptyset) \land x \cap y = \emptyset))$
19		neeq1	$⊢ y = ⋃ J ∖ x \to (y \neq \emptyset \leftrightarrow ⋃ J ∖ x \neq \emptyset)$
20	19	anbi2d	$⊢ y = ⋃ J ∖ x \to ((x \neq \emptyset \land y \neq \emptyset) \leftrightarrow (x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset))$
21	18 20	bitr3d	$⊢ y = ⋃ J ∖ x \to (((x \neq \emptyset \land y \neq \emptyset) \land x \cap y = \emptyset) \leftrightarrow (x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset))$
22	14 21	syl5bb	$⊢ y = ⋃ J ∖ x \to ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \leftrightarrow (x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset))$
23		uneq2	$⊢ y = ⋃ J ∖ x \to x \cup y = x \cup (⋃ J ∖ x)$
24		undif2	$⊢ x \cup (⋃ J ∖ x) = x \cup ⋃ J$
25	23 24	eqtrdi	$⊢ y = ⋃ J ∖ x \to x \cup y = x \cup ⋃ J$
26	25	neeq1d	$⊢ y = ⋃ J ∖ x \to (x \cup y \neq ⋃ J \leftrightarrow x \cup ⋃ J \neq ⋃ J)$
27	22 26	imbi12d	$⊢ y = ⋃ J ∖ x \to (((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J) \leftrightarrow ((x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset) \to x \cup ⋃ J \neq ⋃ J))$
28	27	rspcv	$⊢ ⋃ J ∖ x \in J \to (\forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J) \to ((x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset) \to x \cup ⋃ J \neq ⋃ J))$
29	13 28	syl	$⊢ (J \in Top \land x \in Clsd (J)) \to (\forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J) \to ((x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset) \to x \cup ⋃ J \neq ⋃ J))$
30	1	cldss	$⊢ x \in Clsd (J) \to x \subseteq ⋃ J$
31	30	adantl	$⊢ (J \in Top \land x \in Clsd (J)) \to x \subseteq ⋃ J$
32		ssequn1	$⊢ x \subseteq ⋃ J \leftrightarrow x \cup ⋃ J = ⋃ J$
33	31 32	sylib	$⊢ (J \in Top \land x \in Clsd (J)) \to x \cup ⋃ J = ⋃ J$
34		ssdif0	$⊢ ⋃ J \subseteq x \leftrightarrow ⋃ J ∖ x = \emptyset$
35		idd	$⊢ (J \in Top \land x \in Clsd (J)) \to (⋃ J \subseteq x \to ⋃ J \subseteq x)$
36	35 31	jctild	$⊢ (J \in Top \land x \in Clsd (J)) \to (⋃ J \subseteq x \to (x \subseteq ⋃ J \land ⋃ J \subseteq x))$
37		eqss	$⊢ x = ⋃ J \leftrightarrow (x \subseteq ⋃ J \land ⋃ J \subseteq x)$
38	36 37	syl6ibr	$⊢ (J \in Top \land x \in Clsd (J)) \to (⋃ J \subseteq x \to x = ⋃ J)$
39	34 38	syl5bir	$⊢ (J \in Top \land x \in Clsd (J)) \to (⋃ J ∖ x = \emptyset \to x = ⋃ J)$
40	33 39	embantd	$⊢ (J \in Top \land x \in Clsd (J)) \to ((x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset) \to x = ⋃ J)$
41	40	orim2d	$⊢ (J \in Top \land x \in Clsd (J)) \to ((x = \emptyset \lor (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset)) \to (x = \emptyset \lor x = ⋃ J))$
42		impexp	$⊢ ((x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset) \to x \cup ⋃ J \neq ⋃ J) \leftrightarrow (x \neq \emptyset \to (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J))$
43		df-ne	$⊢ x \neq \emptyset \leftrightarrow \neg x = \emptyset$
44		id	$⊢ (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J) \to (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J)$
45	44	necon4d	$⊢ (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J) \to (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset)$
46		id	$⊢ (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset) \to (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset)$
47	46	necon3d	$⊢ (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset) \to (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J)$
48	45 47	impbii	$⊢ (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J) \leftrightarrow (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset)$
49	43 48	imbi12i	$⊢ (x \neq \emptyset \to (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J)) \leftrightarrow (\neg x = \emptyset \to (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset))$
50		pm4.64	$⊢ (\neg x = \emptyset \to (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset)) \leftrightarrow (x = \emptyset \lor (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset))$
51	49 50	bitri	$⊢ (x \neq \emptyset \to (⋃ J ∖ x \neq \emptyset \to x \cup ⋃ J \neq ⋃ J)) \leftrightarrow (x = \emptyset \lor (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset))$
52	42 51	bitri	$⊢ ((x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset) \to x \cup ⋃ J \neq ⋃ J) \leftrightarrow (x = \emptyset \lor (x \cup ⋃ J = ⋃ J \to ⋃ J ∖ x = \emptyset))$
53		vex	$⊢ x \in V$
54	53	elpr	$⊢ x \in \{\emptyset, ⋃ J\} \leftrightarrow (x = \emptyset \lor x = ⋃ J)$
55	41 52 54	3imtr4g	$⊢ (J \in Top \land x \in Clsd (J)) \to (((x \neq \emptyset \land ⋃ J ∖ x \neq \emptyset) \to x \cup ⋃ J \neq ⋃ J) \to x \in \{\emptyset, ⋃ J\})$
56	29 55	syld	$⊢ (J \in Top \land x \in Clsd (J)) \to (\forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J) \to x \in \{\emptyset, ⋃ J\})$
57	56	ex	$⊢ J \in Top \to (x \in Clsd (J) \to (\forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J) \to x \in \{\emptyset, ⋃ J\}))$
58	57	com23	$⊢ J \in Top \to (\forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J) \to (x \in Clsd (J) \to x \in \{\emptyset, ⋃ J\}))$
59	58	imim2d	$⊢ J \in Top \to ((x \in J \to \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J)) \to (x \in J \to (x \in Clsd (J) \to x \in \{\emptyset, ⋃ J\})))$
60		elin	$⊢ x \in (J \cap Clsd (J)) \leftrightarrow (x \in J \land x \in Clsd (J))$
61	60	imbi1i	$⊢ (x \in (J \cap Clsd (J)) \to x \in \{\emptyset, ⋃ J\}) \leftrightarrow ((x \in J \land x \in Clsd (J)) \to x \in \{\emptyset, ⋃ J\})$
62		impexp	$⊢ ((x \in J \land x \in Clsd (J)) \to x \in \{\emptyset, ⋃ J\}) \leftrightarrow (x \in J \to (x \in Clsd (J) \to x \in \{\emptyset, ⋃ J\}))$
63	61 62	bitri	$⊢ (x \in (J \cap Clsd (J)) \to x \in \{\emptyset, ⋃ J\}) \leftrightarrow (x \in J \to (x \in Clsd (J) \to x \in \{\emptyset, ⋃ J\}))$
64	59 63	syl6ibr	$⊢ J \in Top \to ((x \in J \to \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J)) \to (x \in (J \cap Clsd (J)) \to x \in \{\emptyset, ⋃ J\}))$
65	64	alimdv	$⊢ J \in Top \to (\forall x (x \in J \to \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J)) \to \forall x (x \in (J \cap Clsd (J)) \to x \in \{\emptyset, ⋃ J\}))$
66		df-ral	$⊢ \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) \leftrightarrow \forall x (x \in J \to \forall y \in J ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J))$
67		dfss2	$⊢ J \cap Clsd (J) \subseteq \{\emptyset, ⋃ J\} \leftrightarrow \forall x (x \in (J \cap Clsd (J)) \to x \in \{\emptyset, ⋃ J\})$
68	65 66 67	3imtr4g	$⊢ J \in Top \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) \to J \cap Clsd (J) \subseteq \{\emptyset, ⋃ J\})$
69	1	isconn2	$⊢ J \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) \subseteq \{\emptyset, ⋃ J\})$
70	69	baib	$⊢ J \in Top \to (J \in Conn \leftrightarrow J \cap Clsd (J) \subseteq \{\emptyset, ⋃ J\})$
71	68 70	sylibrd	$⊢ J \in Top \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) \to J \in Conn)$
72	11 71	syl	$⊢ J \in TopOn (X) \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) \to J \in Conn)$
73	10 72	impbid2	$⊢ J \in TopOn (X) \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))$
74		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
75	74	neeq2d	$⊢ J \in TopOn (X) \to (x \cup y \neq X \leftrightarrow x \cup y \neq ⋃ J)$
76	75	imbi2d	$⊢ J \in TopOn (X) \to (((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq X) \leftrightarrow ((x \neq \emptyset \land y \neq \emptyset \land x \cap y = \emptyset) \to x \cup y \neq ⋃ J))$
77	76	2ralbidv	$⊢ J \in TopOn (X) \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 X) \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))$
78	73 77	bitr4d	$⊢ J \in TopOn (X) \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 X))$

Metamath Proof Explorer

Theorem dfconn2

Proof