Theorem indiscld

Description: The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	indiscld	|- ( Clsd ` { (/) , A } ) = { (/) , A }

Proof

Step	Hyp	Ref	Expression
1		indistop	|- { (/) , A } e. Top
2		indisuni	|- ( _I ` A ) = U. { (/) , A }
3	2	iscld	|- ( { (/) , A } e. Top -> ( x e. ( Clsd ` { (/) , A } ) <-> ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) ) )
4	1 3	ax-mp	|- ( x e. ( Clsd ` { (/) , A } ) <-> ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) )
5		simpl	|- ( ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) -> x C_ ( _I ` A ) )
6		dfss4	|- ( x C_ ( _I ` A ) <-> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) = x )
7	5 6	sylib	|- ( ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) = x )
8		simpr	|- ( ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) -> ( ( _I ` A ) \ x ) e. { (/) , A } )
9		indislem	|- { (/) , ( _I ` A ) } = { (/) , A }
10	8 9	eleqtrrdi	|- ( ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) -> ( ( _I ` A ) \ x ) e. { (/) , ( _I ` A ) } )
11		elpri	|- ( ( ( _I ` A ) \ x ) e. { (/) , ( _I ` A ) } -> ( ( ( _I ` A ) \ x ) = (/) \/ ( ( _I ` A ) \ x ) = ( _I ` A ) ) )
12		difeq2	|- ( ( ( _I ` A ) \ x ) = (/) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) = ( ( _I ` A ) \ (/) ) )
13		dif0	|- ( ( _I ` A ) \ (/) ) = ( _I ` A )
14	12 13	eqtrdi	|- ( ( ( _I ` A ) \ x ) = (/) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) = ( _I ` A ) )
15		fvex	|- ( _I ` A ) e. _V
16	15	prid2	|- ( _I ` A ) e. { (/) , ( _I ` A ) }
17	16 9	eleqtri	|- ( _I ` A ) e. { (/) , A }
18	14 17	eqeltrdi	|- ( ( ( _I ` A ) \ x ) = (/) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) e. { (/) , A } )
19		difeq2	|- ( ( ( _I ` A ) \ x ) = ( _I ` A ) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) = ( ( _I ` A ) \ ( _I ` A ) ) )
20		difid	|- ( ( _I ` A ) \ ( _I ` A ) ) = (/)
21	19 20	eqtrdi	|- ( ( ( _I ` A ) \ x ) = ( _I ` A ) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) = (/) )
22		0ex	|- (/) e. _V
23	22	prid1	|- (/) e. { (/) , A }
24	21 23	eqeltrdi	|- ( ( ( _I ` A ) \ x ) = ( _I ` A ) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) e. { (/) , A } )
25	18 24	jaoi	|- ( ( ( ( _I ` A ) \ x ) = (/) \/ ( ( _I ` A ) \ x ) = ( _I ` A ) ) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) e. { (/) , A } )
26	10 11 25	3syl	|- ( ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) -> ( ( _I ` A ) \ ( ( _I ` A ) \ x ) ) e. { (/) , A } )
27	7 26	eqeltrrd	|- ( ( x C_ ( _I ` A ) /\ ( ( _I ` A ) \ x ) e. { (/) , A } ) -> x e. { (/) , A } )
28	4 27	sylbi	|- ( x e. ( Clsd ` { (/) , A } ) -> x e. { (/) , A } )
29	28	ssriv	|- ( Clsd ` { (/) , A } ) C_ { (/) , A }
30		0cld	|- ( { (/) , A } e. Top -> (/) e. ( Clsd ` { (/) , A } ) )
31	1 30	ax-mp	|- (/) e. ( Clsd ` { (/) , A } )
32	2	topcld	|- ( { (/) , A } e. Top -> ( _I ` A ) e. ( Clsd ` { (/) , A } ) )
33	1 32	ax-mp	|- ( _I ` A ) e. ( Clsd ` { (/) , A } )
34		prssi	|- ( ( (/) e. ( Clsd ` { (/) , A } ) /\ ( _I ` A ) e. ( Clsd ` { (/) , A } ) ) -> { (/) , ( _I ` A ) } C_ ( Clsd ` { (/) , A } ) )
35	31 33 34	mp2an	|- { (/) , ( _I ` A ) } C_ ( Clsd ` { (/) , A } )
36	9 35	eqsstrri	|- { (/) , A } C_ ( Clsd ` { (/) , A } )
37	29 36	eqssi	|- ( Clsd ` { (/) , A } ) = { (/) , A }