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