Theorem hmphdis

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

	Ref	Expression
Hypothesis	hmphdis.1	$$⊢X=\bigcup J$$
Assertion	hmphdis	$$⊢J\simeq 𝒫A\to J=𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		hmphdis.1	$$⊢X=\bigcup J$$
2		pwuni	$$⊢J\subseteq 𝒫\bigcup J$$
3	1	pweqi	$$⊢𝒫X=𝒫\bigcup J$$
4	2 3	sseqtrri	$$⊢J\subseteq 𝒫X$$
5	4	a1i	$$⊢J\simeq 𝒫A\to J\subseteq 𝒫X$$
6		hmph	$$⊢J\simeq 𝒫A\leftrightarrow J\mathrm{Homeo}𝒫A\ne \varnothing$$
7		n0	$$⊢J\mathrm{Homeo}𝒫A\ne \varnothing \leftrightarrow \exists ff\in \left(J\mathrm{Homeo}𝒫A\right)$$
8		elpwi	$$⊢x\in 𝒫X\to x\subseteq X$$
9		imassrn	$$⊢f\left[x\right]\subseteq \mathrm{ran}f$$
10		unipw	$$⊢\bigcup 𝒫A=A$$
11	10	eqcomi	$$⊢A=\bigcup 𝒫A$$
12	1 11	hmeof1o	$$⊢f\in \left(J\mathrm{Homeo}𝒫A\right)\to f:X\underset{1-1\; onto}{⟶}A$$
13		f1of	$$⊢f:X\underset{1-1\; onto}{⟶}A\to f:X⟶A$$
14		frn	$$⊢f:X⟶A\to \mathrm{ran}f\subseteq A$$
15	12 13 14	3syl	$$⊢f\in \left(J\mathrm{Homeo}𝒫A\right)\to \mathrm{ran}f\subseteq A$$
16	15	adantr	$$⊢\left(f\in \left(J\mathrm{Homeo}𝒫A\right)\wedge x\subseteq X\right)\to \mathrm{ran}f\subseteq A$$
17	9 16	sstrid	$$⊢\left(f\in \left(J\mathrm{Homeo}𝒫A\right)\wedge x\subseteq X\right)\to f\left[x\right]\subseteq A$$
18		vex	$$⊢f\in \mathrm{V}$$
19	18	imaex	$$⊢f\left[x\right]\in \mathrm{V}$$
20	19	elpw	$$⊢f\left[x\right]\in 𝒫A\leftrightarrow f\left[x\right]\subseteq A$$
21	17 20	sylibr	$$⊢\left(f\in \left(J\mathrm{Homeo}𝒫A\right)\wedge x\subseteq X\right)\to f\left[x\right]\in 𝒫A$$
22	1	hmeoopn	$$⊢\left(f\in \left(J\mathrm{Homeo}𝒫A\right)\wedge x\subseteq X\right)\to \left(x\in J\leftrightarrow f\left[x\right]\in 𝒫A\right)$$
23	21 22	mpbird	$$⊢\left(f\in \left(J\mathrm{Homeo}𝒫A\right)\wedge x\subseteq X\right)\to x\in J$$
24	23	ex	$$⊢f\in \left(J\mathrm{Homeo}𝒫A\right)\to \left(x\subseteq X\to x\in J\right)$$
25	8 24	syl5	$$⊢f\in \left(J\mathrm{Homeo}𝒫A\right)\to \left(x\in 𝒫X\to x\in J\right)$$
26	25	ssrdv	$$⊢f\in \left(J\mathrm{Homeo}𝒫A\right)\to 𝒫X\subseteq J$$
27	26	exlimiv	$$⊢\exists ff\in \left(J\mathrm{Homeo}𝒫A\right)\to 𝒫X\subseteq J$$
28	7 27	sylbi	$$⊢J\mathrm{Homeo}𝒫A\ne \varnothing \to 𝒫X\subseteq J$$
29	6 28	sylbi	$$⊢J\simeq 𝒫A\to 𝒫X\subseteq J$$
30	5 29	eqssd	$$⊢J\simeq 𝒫A\to J=𝒫X$$