# Metamath Proof Explorer

## Theorem hmphdis

Description: Homeomorphisms preserve topological discretion. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis hmphdis.1
|- X = U. J
Assertion hmphdis
|- ( J ~= ~P A -> J = ~P X )

### Proof

Step Hyp Ref Expression
1 hmphdis.1
|-  X = U. J
2 pwuni
|-  J C_ ~P U. J
3 1 pweqi
|-  ~P X = ~P U. J
4 2 3 sseqtrri
|-  J C_ ~P X
5 4 a1i
|-  ( J ~= ~P A -> J C_ ~P X )
6 hmph
|-  ( J ~= ~P A <-> ( J Homeo ~P A ) =/= (/) )
7 n0
|-  ( ( J Homeo ~P A ) =/= (/) <-> E. f f e. ( J Homeo ~P A ) )
8 elpwi
|-  ( x e. ~P X -> x C_ X )
9 imassrn
|-  ( f " x ) C_ ran f
10 unipw
|-  U. ~P A = A
11 10 eqcomi
|-  A = U. ~P A
12 1 11 hmeof1o
|-  ( f e. ( J Homeo ~P A ) -> f : X -1-1-onto-> A )
13 f1of
|-  ( f : X -1-1-onto-> A -> f : X --> A )
14 frn
|-  ( f : X --> A -> ran f C_ A )
15 12 13 14 3syl
|-  ( f e. ( J Homeo ~P A ) -> ran f C_ A )
|-  ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) -> ran f C_ A )
17 9 16 sstrid
|-  ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) -> ( f " x ) C_ A )
18 vex
|-  f e. _V
19 18 imaex
|-  ( f " x ) e. _V
20 19 elpw
|-  ( ( f " x ) e. ~P A <-> ( f " x ) C_ A )
21 17 20 sylibr
|-  ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) -> ( f " x ) e. ~P A )
22 1 hmeoopn
|-  ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) -> ( x e. J <-> ( f " x ) e. ~P A ) )
23 21 22 mpbird
|-  ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) -> x e. J )
24 23 ex
|-  ( f e. ( J Homeo ~P A ) -> ( x C_ X -> x e. J ) )
25 8 24 syl5
|-  ( f e. ( J Homeo ~P A ) -> ( x e. ~P X -> x e. J ) )
26 25 ssrdv
|-  ( f e. ( J Homeo ~P A ) -> ~P X C_ J )
27 26 exlimiv
|-  ( E. f f e. ( J Homeo ~P A ) -> ~P X C_ J )
28 7 27 sylbi
|-  ( ( J Homeo ~P A ) =/= (/) -> ~P X C_ J )
29 6 28 sylbi
|-  ( J ~= ~P A -> ~P X C_ J )
30 5 29 eqssd
|-  ( J ~= ~P A -> J = ~P X )