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