clsconn

Description: The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	clsconn	$⊢ (J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \to J ↾_{𝑡} cls (J) (A) \in Conn$

Proof

Step	Hyp	Ref	Expression
1		simpll3	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land (x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A))) \to J ↾_{𝑡} A \in Conn$
2		simpll1	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to J \in TopOn (X)$
3		simpll2	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to A \subseteq X$
4		simplrl	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to x \in J$
5		simplrr	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to y \in J$
6		simprl1	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to x \cap cls (J) (A) \neq \emptyset$
7		n0	$⊢ x \cap cls (J) (A) \neq \emptyset \leftrightarrow \exists z z \in (x \cap cls (J) (A))$
8	6 7	sylib	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to \exists z z \in (x \cap cls (J) (A))$
9	2	adantr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to J \in TopOn (X)$
10		topontop	$⊢ J \in TopOn (X) \to J \in Top$
11	9 10	syl	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to J \in Top$
12	3	adantr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to A \subseteq X$
13		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
14	9 13	syl	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to X = ⋃ J$
15	12 14	sseqtrd	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to A \subseteq ⋃ J$
16		simpr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to z \in (x \cap cls (J) (A))$
17	16	elin2d	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to z \in cls (J) (A)$
18	4	adantr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to x \in J$
19	16	elin1d	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to z \in x$
20		eqid	$⊢ ⋃ J = ⋃ J$
21	20	clsndisj	$⊢ ((J \in Top \land A \subseteq ⋃ J \land z \in cls (J) (A)) \land (x \in J \land z \in x)) \to x \cap A \neq \emptyset$
22	11 15 17 18 19 21	syl32anc	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (x \cap cls (J) (A))) \to x \cap A \neq \emptyset$
23	8 22	exlimddv	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to x \cap A \neq \emptyset$
24		simprl2	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to y \cap cls (J) (A) \neq \emptyset$
25		n0	$⊢ y \cap cls (J) (A) \neq \emptyset \leftrightarrow \exists z z \in (y \cap cls (J) (A))$
26	24 25	sylib	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to \exists z z \in (y \cap cls (J) (A))$
27	2	adantr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to J \in TopOn (X)$
28	27 10	syl	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to J \in Top$
29	3	adantr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to A \subseteq X$
30	27 13	syl	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to X = ⋃ J$
31	29 30	sseqtrd	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to A \subseteq ⋃ J$
32		simpr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to z \in (y \cap cls (J) (A))$
33	32	elin2d	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to z \in cls (J) (A)$
34	5	adantr	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to y \in J$
35	32	elin1d	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to z \in y$
36	20	clsndisj	$⊢ ((J \in Top \land A \subseteq ⋃ J \land z \in cls (J) (A)) \land (y \in J \land z \in y)) \to y \cap A \neq \emptyset$
37	28 31 33 34 35 36	syl32anc	$⊢ ((((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \land z \in (y \cap cls (J) (A))) \to y \cap A \neq \emptyset$
38	26 37	exlimddv	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to y \cap A \neq \emptyset$
39		simprl3	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to x \cap y \subseteq X ∖ cls (J) (A)$
40	2 10	syl	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to J \in Top$
41	2 13	syl	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to X = ⋃ J$
42	3 41	sseqtrd	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to A \subseteq ⋃ J$
43	20	sscls	$⊢ (J \in Top \land A \subseteq ⋃ J) \to A \subseteq cls (J) (A)$
44	40 42 43	syl2anc	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to A \subseteq cls (J) (A)$
45	44	sscond	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to X ∖ cls (J) (A) \subseteq X ∖ A$
46	39 45	sstrd	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to x \cap y \subseteq X ∖ A$
47		ssv	$⊢ X \subseteq V$
48		ssdif	$⊢ X \subseteq V \to X ∖ A \subseteq V ∖ A$
49	47 48	ax-mp	$⊢ X ∖ A \subseteq V ∖ A$
50	46 49	sstrdi	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to x \cap y \subseteq V ∖ A$
51		disj2	$⊢ (x \cap y) \cap A = \emptyset \leftrightarrow x \cap y \subseteq V ∖ A$
52	50 51	sylibr	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to (x \cap y) \cap A = \emptyset$
53		simprr	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to cls (J) (A) \subseteq x \cup y$
54	44 53	sstrd	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to A \subseteq x \cup y$
55	2 3 4 5 23 38 52 54	nconnsubb	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \land cls (J) (A) \subseteq x \cup y)) \to \neg J ↾_{𝑡} A \in Conn$
56	55	expr	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land (x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A))) \to (cls (J) (A) \subseteq x \cup y \to \neg J ↾_{𝑡} A \in Conn)$
57	1 56	mt2d	$⊢ (((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \land (x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A))) \to \neg cls (J) (A) \subseteq x \cup y$
58	57	ex	$⊢ ((J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \land (x \in J \land y \in J)) \to ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \to \neg cls (J) (A) \subseteq x \cup y)$
59	58	ralrimivva	$⊢ (J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \to \forall x \in J \forall y \in J ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \to \neg cls (J) (A) \subseteq x \cup y)$
60		simp1	$⊢ (J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \to J \in TopOn (X)$
61	13	sseq2d	$⊢ J \in TopOn (X) \to (A \subseteq X \leftrightarrow A \subseteq ⋃ J)$
62	61	biimpa	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \subseteq ⋃ J$
63	20	clsss3	$⊢ (J \in Top \land A \subseteq ⋃ J) \to cls (J) (A) \subseteq ⋃ J$
64	10 62 63	syl2an2r	$⊢ (J \in TopOn (X) \land A \subseteq X) \to cls (J) (A) \subseteq ⋃ J$
65	13	adantr	$⊢ (J \in TopOn (X) \land A \subseteq X) \to X = ⋃ J$
66	64 65	sseqtrrd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to cls (J) (A) \subseteq X$
67	66	3adant3	$⊢ (J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \to cls (J) (A) \subseteq X$
68		connsub	$⊢ (J \in TopOn (X) \land cls (J) (A) \subseteq X) \to (J ↾_{𝑡} cls (J) (A) \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \to \neg cls (J) (A) \subseteq x \cup y))$
69	60 67 68	syl2anc	$⊢ (J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \to (J ↾_{𝑡} cls (J) (A) \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \cap cls (J) (A) \neq \emptyset \land y \cap cls (J) (A) \neq \emptyset \land x \cap y \subseteq X ∖ cls (J) (A)) \to \neg cls (J) (A) \subseteq x \cup y))$
70	59 69	mpbird	$⊢ (J \in TopOn (X) \land A \subseteq X \land J ↾_{𝑡} A \in Conn) \to J ↾_{𝑡} cls (J) (A) \in Conn$

Metamath Proof Explorer

Theorem clsconn

Proof