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 = U. J
	Assertion	isclo	\|- ( ( J e. Top /\ A C_ X ) -> ( A e. ( J i^i ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isclo.1	\|- X = U. J
2		elin	\|- ( A e. ( J i^i ( Clsd ` J ) ) <-> ( A e. J /\ A e. ( Clsd ` J ) ) )
3	1	iscld2	\|- ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( X \ A ) e. J ) )
4	3	anbi2d	\|- ( ( J e. Top /\ A C_ X ) -> ( ( A e. J /\ A e. ( Clsd ` J ) ) <-> ( A e. J /\ ( X \ A ) e. J ) ) )
5		eltop2	\|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )
6		dfss3	\|- ( y C_ A <-> A. z e. y z e. A )
7		pm5.501	\|- ( x e. A -> ( z e. A <-> ( x e. A <-> z e. A ) ) )
8	7	ralbidv	\|- ( x e. A -> ( A. z e. y z e. A <-> A. z e. y ( x e. A <-> z e. A ) ) )
9	6 8	syl5bb	\|- ( x e. A -> ( y C_ A <-> A. z e. y ( x e. A <-> z e. A ) ) )
10	9	anbi2d	\|- ( x e. A -> ( ( x e. y /\ y C_ A ) <-> ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
11	10	rexbidv	\|- ( x e. A -> ( E. y e. J ( x e. y /\ y C_ A ) <-> E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
12	11	ralbiia	\|- ( A. x e. A E. y e. J ( x e. y /\ y C_ A ) <-> A. x e. A E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) )
13	5 12	bitrdi	\|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
14		eltop2	\|- ( J e. Top -> ( ( X \ A ) e. J <-> A. x e. ( X \ A ) E. y e. J ( x e. y /\ y C_ ( X \ A ) ) ) )
15		dfss3	\|- ( y C_ ( X \ A ) <-> A. z e. y z e. ( X \ A ) )
16		id	\|- ( z e. y -> z e. y )
17		simpr	\|- ( ( x e. ( X \ A ) /\ y e. J ) -> y e. J )
18		elunii	\|- ( ( z e. y /\ y e. J ) -> z e. U. J )
19	16 17 18	syl2anr	\|- ( ( ( x e. ( X \ A ) /\ y e. J ) /\ z e. y ) -> z e. U. J )
20	19 1	eleqtrrdi	\|- ( ( ( x e. ( X \ A ) /\ y e. J ) /\ z e. y ) -> z e. X )
21		eldif	\|- ( z e. ( X \ A ) <-> ( z e. X /\ -. z e. A ) )
22	21	baib	\|- ( z e. X -> ( z e. ( X \ A ) <-> -. z e. A ) )
23	20 22	syl	\|- ( ( ( x e. ( X \ A ) /\ y e. J ) /\ z e. y ) -> ( z e. ( X \ A ) <-> -. z e. A ) )
24		eldifn	\|- ( x e. ( X \ A ) -> -. x e. A )
25		nbn2	\|- ( -. x e. A -> ( -. z e. A <-> ( x e. A <-> z e. A ) ) )
26	24 25	syl	\|- ( x e. ( X \ A ) -> ( -. z e. A <-> ( x e. A <-> z e. A ) ) )
27	26	ad2antrr	\|- ( ( ( x e. ( X \ A ) /\ y e. J ) /\ z e. y ) -> ( -. z e. A <-> ( x e. A <-> z e. A ) ) )
28	23 27	bitrd	\|- ( ( ( x e. ( X \ A ) /\ y e. J ) /\ z e. y ) -> ( z e. ( X \ A ) <-> ( x e. A <-> z e. A ) ) )
29	28	ralbidva	\|- ( ( x e. ( X \ A ) /\ y e. J ) -> ( A. z e. y z e. ( X \ A ) <-> A. z e. y ( x e. A <-> z e. A ) ) )
30	15 29	syl5bb	\|- ( ( x e. ( X \ A ) /\ y e. J ) -> ( y C_ ( X \ A ) <-> A. z e. y ( x e. A <-> z e. A ) ) )
31	30	anbi2d	\|- ( ( x e. ( X \ A ) /\ y e. J ) -> ( ( x e. y /\ y C_ ( X \ A ) ) <-> ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
32	31	rexbidva	\|- ( x e. ( X \ A ) -> ( E. y e. J ( x e. y /\ y C_ ( X \ A ) ) <-> E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
33	32	ralbiia	\|- ( A. x e. ( X \ A ) E. y e. J ( x e. y /\ y C_ ( X \ A ) ) <-> A. x e. ( X \ A ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) )
34	14 33	bitrdi	\|- ( J e. Top -> ( ( X \ A ) e. J <-> A. x e. ( X \ A ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
35	13 34	anbi12d	\|- ( J e. Top -> ( ( A e. J /\ ( X \ A ) e. J ) <-> ( A. x e. A E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) /\ A. x e. ( X \ A ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) ) )
36	35	adantr	\|- ( ( J e. Top /\ A C_ X ) -> ( ( A e. J /\ ( X \ A ) e. J ) <-> ( A. x e. A E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) /\ A. x e. ( X \ A ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) ) )
37		ralunb	\|- ( A. x e. ( A u. ( X \ A ) ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) <-> ( A. x e. A E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) /\ A. x e. ( X \ A ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
38		simpr	\|- ( ( J e. Top /\ A C_ X ) -> A C_ X )
39		undif	\|- ( A C_ X <-> ( A u. ( X \ A ) ) = X )
40	38 39	sylib	\|- ( ( J e. Top /\ A C_ X ) -> ( A u. ( X \ A ) ) = X )
41	40	raleqdv	\|- ( ( J e. Top /\ A C_ X ) -> ( A. x e. ( A u. ( X \ A ) ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
42	37 41	bitr3id	\|- ( ( J e. Top /\ A C_ X ) -> ( ( A. x e. A E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) /\ A. x e. ( X \ A ) E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
43	4 36 42	3bitrd	\|- ( ( J e. Top /\ A C_ X ) -> ( ( A e. J /\ A e. ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
44	2 43	syl5bb	\|- ( ( J e. Top /\ A C_ X ) -> ( A e. ( J i^i ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )

Metamath Proof Explorer

Theorem isclo

Proof