# Metamath Proof Explorer

## Theorem hmphindis

Description: Homeomorphisms preserve topological indiscretion. (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 syl5eqr
` |-  ( ( _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 pr2nelem
` |-  ( ( (/) 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 } )`