This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }