isclo

Description: A set A is clopen iff for every point x in the space there is a neighborhood y such that all the points in y are in A iff x is. (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Hypothesis	isclo.1	$⊢ X = ⋃ J$
	Assertion	isclo	$⊢ (J \in Top \land A \subseteq X) \to (A \in (J \cap Clsd (J)) \leftrightarrow \forall x \in X \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$

Proof

Step	Hyp	Ref	Expression
1		isclo.1	$⊢ X = ⋃ J$
2		elin	$⊢ A \in (J \cap Clsd (J)) \leftrightarrow (A \in J \land A \in Clsd (J))$
3	1	iscld2	$⊢ (J \in Top \land A \subseteq X) \to (A \in Clsd (J) \leftrightarrow X ∖ A \in J)$
4	3	anbi2d	$⊢ (J \in Top \land A \subseteq X) \to ((A \in J \land A \in Clsd (J)) \leftrightarrow (A \in J \land X ∖ A \in J))$
5		eltop2	$⊢ J \in Top \to (A \in J \leftrightarrow \forall x \in A \exists y \in J (x \in y \land y \subseteq A))$
6		dfss3	$⊢ y \subseteq A \leftrightarrow \forall z \in y z \in A$
7		pm5.501	$⊢ x \in A \to (z \in A \leftrightarrow (x \in A \leftrightarrow z \in A))$
8	7	ralbidv	$⊢ x \in A \to (\forall z \in y z \in A \leftrightarrow \forall z \in y (x \in A \leftrightarrow z \in A))$
9	6 8	bitrid	$⊢ x \in A \to (y \subseteq A \leftrightarrow \forall z \in y (x \in A \leftrightarrow z \in A))$
10	9	anbi2d	$⊢ x \in A \to ((x \in y \land y \subseteq A) \leftrightarrow (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
11	10	rexbidv	$⊢ x \in A \to (\exists y \in J (x \in y \land y \subseteq A) \leftrightarrow \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
12	11	ralbiia	$⊢ \forall x \in A \exists y \in J (x \in y \land y \subseteq A) \leftrightarrow \forall x \in A \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A))$
13	5 12	bitrdi	$⊢ J \in Top \to (A \in J \leftrightarrow \forall x \in A \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
14		eltop2	$⊢ J \in Top \to (X ∖ A \in J \leftrightarrow \forall x \in (X ∖ A) \exists y \in J (x \in y \land y \subseteq X ∖ A))$
15		dfss3	$⊢ y \subseteq X ∖ A \leftrightarrow \forall z \in y z \in (X ∖ A)$
16		id	$⊢ z \in y \to z \in y$
17		simpr	$⊢ (x \in (X ∖ A) \land y \in J) \to y \in J$
18		elunii	$⊢ (z \in y \land y \in J) \to z \in ⋃ J$
19	16 17 18	syl2anr	$⊢ ((x \in (X ∖ A) \land y \in J) \land z \in y) \to z \in ⋃ J$
20	19 1	eleqtrrdi	$⊢ ((x \in (X ∖ A) \land y \in J) \land z \in y) \to z \in X$
21		eldif	$⊢ z \in (X ∖ A) \leftrightarrow (z \in X \land \neg z \in A)$
22	21	baib	$⊢ z \in X \to (z \in (X ∖ A) \leftrightarrow \neg z \in A)$
23	20 22	syl	$⊢ ((x \in (X ∖ A) \land y \in J) \land z \in y) \to (z \in (X ∖ A) \leftrightarrow \neg z \in A)$
24		eldifn	$⊢ x \in (X ∖ A) \to \neg x \in A$
25		nbn2	$⊢ \neg x \in A \to (\neg z \in A \leftrightarrow (x \in A \leftrightarrow z \in A))$
26	24 25	syl	$⊢ x \in (X ∖ A) \to (\neg z \in A \leftrightarrow (x \in A \leftrightarrow z \in A))$
27	26	ad2antrr	$⊢ ((x \in (X ∖ A) \land y \in J) \land z \in y) \to (\neg z \in A \leftrightarrow (x \in A \leftrightarrow z \in A))$
28	23 27	bitrd	$⊢ ((x \in (X ∖ A) \land y \in J) \land z \in y) \to (z \in (X ∖ A) \leftrightarrow (x \in A \leftrightarrow z \in A))$
29	28	ralbidva	$⊢ (x \in (X ∖ A) \land y \in J) \to (\forall z \in y z \in (X ∖ A) \leftrightarrow \forall z \in y (x \in A \leftrightarrow z \in A))$
30	15 29	bitrid	$⊢ (x \in (X ∖ A) \land y \in J) \to (y \subseteq X ∖ A \leftrightarrow \forall z \in y (x \in A \leftrightarrow z \in A))$
31	30	anbi2d	$⊢ (x \in (X ∖ A) \land y \in J) \to ((x \in y \land y \subseteq X ∖ A) \leftrightarrow (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
32	31	rexbidva	$⊢ x \in (X ∖ A) \to (\exists y \in J (x \in y \land y \subseteq X ∖ A) \leftrightarrow \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
33	32	ralbiia	$⊢ \forall x \in (X ∖ A) \exists y \in J (x \in y \land y \subseteq X ∖ A) \leftrightarrow \forall x \in (X ∖ A) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A))$
34	14 33	bitrdi	$⊢ J \in Top \to (X ∖ A \in J \leftrightarrow \forall x \in (X ∖ A) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
35	13 34	anbi12d	$⊢ J \in Top \to ((A \in J \land X ∖ A \in J) \leftrightarrow (\forall x \in A \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \land \forall x \in (X ∖ A) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A))))$
36	35	adantr	$⊢ (J \in Top \land A \subseteq X) \to ((A \in J \land X ∖ A \in J) \leftrightarrow (\forall x \in A \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \land \forall x \in (X ∖ A) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A))))$
37		ralunb	$⊢ \forall x \in (A \cup (X ∖ A)) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \leftrightarrow (\forall x \in A \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \land \forall x \in (X ∖ A) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
38		simpr	$⊢ (J \in Top \land A \subseteq X) \to A \subseteq X$
39		undif	$⊢ A \subseteq X \leftrightarrow A \cup (X ∖ A) = X$
40	38 39	sylib	$⊢ (J \in Top \land A \subseteq X) \to A \cup (X ∖ A) = X$
41	40	raleqdv	$⊢ (J \in Top \land A \subseteq X) \to (\forall x \in (A \cup (X ∖ A)) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \leftrightarrow \forall x \in X \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
42	37 41	bitr3id	$⊢ (J \in Top \land A \subseteq X) \to ((\forall x \in A \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \land \forall x \in (X ∖ A) \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A))) \leftrightarrow \forall x \in X \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
43	4 36 42	3bitrd	$⊢ (J \in Top \land A \subseteq X) \to ((A \in J \land A \in Clsd (J)) \leftrightarrow \forall x \in X \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$
44	2 43	bitrid	$⊢ (J \in Top \land A \subseteq X) \to (A \in (J \cap Clsd (J)) \leftrightarrow \forall x \in X \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)))$

Metamath Proof Explorer

Theorem isclo

Proof