isclo2

Description: A set A is clopen iff for every point x in the space there is a neighborhood y of x which is either disjoint from A or contained in A . (Contributed by Mario Carneiro, 7-Jul-2015)

		Ref	Expression
	Hypothesis	isclo.1	$⊢ X = ⋃ J$
	Assertion	isclo2	$⊢ (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 (z \in A \to y \subseteq A)))$

Proof

Step	Hyp	Ref	Expression
1		isclo.1	$⊢ X = ⋃ J$
2	1	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)))$
3		eleq1w	$⊢ z = w \to (z \in A \leftrightarrow w \in A)$
4	3	bibi2d	$⊢ z = w \to ((x \in A \leftrightarrow z \in A) \leftrightarrow (x \in A \leftrightarrow w \in A))$
5	4	cbvralvw	$⊢ \forall z \in y (x \in A \leftrightarrow z \in A) \leftrightarrow \forall w \in y (x \in A \leftrightarrow w \in A)$
6	5	anbi2i	$⊢ (\forall z \in y (x \in A \leftrightarrow z \in A) \land \forall z \in y (x \in A \leftrightarrow z \in A)) \leftrightarrow (\forall z \in y (x \in A \leftrightarrow z \in A) \land \forall w \in y (x \in A \leftrightarrow w \in A))$
7		pm4.24	$⊢ \forall z \in y (x \in A \leftrightarrow z \in A) \leftrightarrow (\forall z \in y (x \in A \leftrightarrow z \in A) \land \forall z \in y (x \in A \leftrightarrow z \in A))$
8		raaanv	$⊢ \forall z \in y \forall w \in y ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \leftrightarrow (\forall z \in y (x \in A \leftrightarrow z \in A) \land \forall w \in y (x \in A \leftrightarrow w \in A))$
9	6 7 8	3bitr4i	$⊢ \forall z \in y (x \in A \leftrightarrow z \in A) \leftrightarrow \forall z \in y \forall w \in y ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A))$
10		bibi1	$⊢ (x \in A \leftrightarrow z \in A) \to ((x \in A \leftrightarrow w \in A) \leftrightarrow (z \in A \leftrightarrow w \in A))$
11	10	biimpa	$⊢ ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \to (z \in A \leftrightarrow w \in A)$
12	11	biimpcd	$⊢ z \in A \to (((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \to w \in A)$
13	12	ralimdv	$⊢ z \in A \to (\forall w \in y ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \to \forall w \in y w \in A)$
14	13	com12	$⊢ \forall w \in y ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \to (z \in A \to \forall w \in y w \in A)$
15		dfss3	$⊢ y \subseteq A \leftrightarrow \forall w \in y w \in A$
16	14 15	syl6ibr	$⊢ \forall w \in y ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \to (z \in A \to y \subseteq A)$
17	16	ralimi	$⊢ \forall z \in y \forall w \in y ((x \in A \leftrightarrow z \in A) \land (x \in A \leftrightarrow w \in A)) \to \forall z \in y (z \in A \to y \subseteq A)$
18	9 17	sylbi	$⊢ \forall z \in y (x \in A \leftrightarrow z \in A) \to \forall z \in y (z \in A \to y \subseteq A)$
19		eleq1w	$⊢ z = x \to (z \in A \leftrightarrow x \in A)$
20	19	imbi1d	$⊢ z = x \to ((z \in A \to y \subseteq A) \leftrightarrow (x \in A \to y \subseteq A))$
21	20	rspcv	$⊢ x \in y \to (\forall z \in y (z \in A \to y \subseteq A) \to (x \in A \to y \subseteq A))$
22		dfss3	$⊢ y \subseteq A \leftrightarrow \forall z \in y z \in A$
23	22	imbi2i	$⊢ (x \in A \to y \subseteq A) \leftrightarrow (x \in A \to \forall z \in y z \in A)$
24		r19.21v	$⊢ \forall z \in y (x \in A \to z \in A) \leftrightarrow (x \in A \to \forall z \in y z \in A)$
25	23 24	bitr4i	$⊢ (x \in A \to y \subseteq A) \leftrightarrow \forall z \in y (x \in A \to z \in A)$
26	21 25	syl6ib	$⊢ x \in y \to (\forall z \in y (z \in A \to y \subseteq A) \to \forall z \in y (x \in A \to z \in A))$
27		ssel	$⊢ y \subseteq A \to (x \in y \to x \in A)$
28	27	com12	$⊢ x \in y \to (y \subseteq A \to x \in A)$
29	28	imim2d	$⊢ x \in y \to ((z \in A \to y \subseteq A) \to (z \in A \to x \in A))$
30	29	ralimdv	$⊢ x \in y \to (\forall z \in y (z \in A \to y \subseteq A) \to \forall z \in y (z \in A \to x \in A))$
31	26 30	jcad	$⊢ x \in y \to (\forall z \in y (z \in A \to y \subseteq A) \to (\forall z \in y (x \in A \to z \in A) \land \forall z \in y (z \in A \to x \in A)))$
32		ralbiim	$⊢ \forall z \in y (x \in A \leftrightarrow z \in A) \leftrightarrow (\forall z \in y (x \in A \to z \in A) \land \forall z \in y (z \in A \to x \in A))$
33	31 32	syl6ibr	$⊢ x \in y \to (\forall z \in y (z \in A \to y \subseteq A) \to \forall z \in y (x \in A \leftrightarrow z \in A))$
34	18 33	impbid2	$⊢ x \in y \to (\forall z \in y (x \in A \leftrightarrow z \in A) \leftrightarrow \forall z \in y (z \in A \to y \subseteq A))$
35	34	pm5.32i	$⊢ (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \leftrightarrow (x \in y \land \forall z \in y (z \in A \to y \subseteq A))$
36	35	rexbii	$⊢ \exists y \in J (x \in y \land \forall z \in y (x \in A \leftrightarrow z \in A)) \leftrightarrow \exists y \in J (x \in y \land \forall z \in y (z \in A \to y \subseteq A))$
37	36	ralbii	$⊢ \forall x \in X \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 (z \in A \to y \subseteq A))$
38	2 37	bitrdi	$⊢ (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 (z \in A \to y \subseteq A)))$

Metamath Proof Explorer

Theorem isclo2

Proof