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

Metamath Proof Explorer

Theorem hmphindis

Description: Homeomorphisms preserve topological indiscreteness. (Contributed by FL, 18-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis hmphdis.1 
|- X = U. J
Assertion hmphindis 
|- ( J ~= { (/) , A } -> J = { (/) , X } )

Proof

Step Hyp Ref Expression
1 hmphdis.1 
 |-  X = U. J
2 dfsn2 
 |-  { (/) } = { (/) , (/) }
3 indislem 
 |-  { (/) , ( _I ` A ) } = { (/) , A }
4 preq2 
 |-  ( ( _I ` A ) = (/) -> { (/) , ( _I ` A ) } = { (/) , (/) } )
5 4 2 eqtr4di 
 |-  ( ( _I ` A ) = (/) -> { (/) , ( _I ` A ) } = { (/) } )
6 3 5 eqtr3id 
 |-  ( ( _I ` A ) = (/) -> { (/) , A } = { (/) } )
7 6 breq2d 
 |-  ( ( _I ` A ) = (/) -> ( J ~= { (/) , A } <-> J ~= { (/) } ) )
8 7 biimpac 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> J ~= { (/) } )
9 hmph0 
 |-  ( J ~= { (/) } <-> J = { (/) } )
10 8 9 sylib 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> J = { (/) } )
11 10 unieqd 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> U. J = U. { (/) } )
12 0ex 
 |-  (/) e. _V
13 12 unisn 
 |-  U. { (/) } = (/)
14 13 eqcomi 
 |-  (/) = U. { (/) }
15 11 1 14 3eqtr4g 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> X = (/) )
16 15 preq2d 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> { (/) , X } = { (/) , (/) } )
17 2 10 16 3eqtr4a 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> J = { (/) , X } )
18 hmphen 
 |-  ( J ~= { (/) , A } -> J ~~ { (/) , A } )
19 necom 
 |-  ( ( _I ` A ) =/= (/) <-> (/) =/= ( _I ` A ) )
20 fvex 
 |-  ( _I ` A ) e. _V
21 enpr2 
 |-  ( ( (/) e. _V /\ ( _I ` A ) e. _V /\ (/) =/= ( _I ` A ) ) -> { (/) , ( _I ` A ) } ~~ 2o )
22 12 20 21 mp3an12 
 |-  ( (/) =/= ( _I ` A ) -> { (/) , ( _I ` A ) } ~~ 2o )
23 19 22 sylbi 
 |-  ( ( _I ` A ) =/= (/) -> { (/) , ( _I ` A ) } ~~ 2o )
24 23 adantl 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> { (/) , ( _I ` A ) } ~~ 2o )
25 3 24 eqbrtrrid 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> { (/) , A } ~~ 2o )
26 entr 
 |-  ( ( J ~~ { (/) , A } /\ { (/) , A } ~~ 2o ) -> J ~~ 2o )
27 18 25 26 syl2an2r 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J ~~ 2o )
28 hmphtop1 
 |-  ( J ~= { (/) , A } -> J e. Top )
29 28 adantr 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J e. Top )
30 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
31 29 30 sylib 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J e. ( TopOn ` X ) )
32 en2top 
 |-  ( J e. ( TopOn ` X ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )
33 31 32 syl 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )
34 27 33 mpbid 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> ( J = { (/) , X } /\ X =/= (/) ) )
35 34 simpld 
 |-  ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J = { (/) , X } )
36 17 35 pm2.61dane 
 |-  ( J ~= { (/) , A } -> J = { (/) , X } )