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

Metamath Proof Explorer

Theorem hmphdis

Description: Homeomorphisms preserve topological discreteness. (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 )
16 15 adantr 
 |-  ( ( 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 )