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 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 }