hmphdis

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

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

Proof

Step	Hyp	Ref	Expression
1		hmphdis.1	$⊢ X = ⋃ J$
2		pwuni	$⊢ J \subseteq 𝒫 ⋃ J$
3	1	pweqi	$⊢ 𝒫 X = 𝒫 ⋃ J$
4	2 3	sseqtrri	$⊢ J \subseteq 𝒫 X$
5	4	a1i	$⊢ J ≃ 𝒫 A \to J \subseteq 𝒫 X$
6		hmph	$⊢ J ≃ 𝒫 A \leftrightarrow J Homeo 𝒫 A \neq \emptyset$
7		n0	$⊢ J Homeo 𝒫 A \neq \emptyset \leftrightarrow \exists f f \in (J Homeo 𝒫 A)$
8		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
9		imassrn	$⊢ f [x] \subseteq ran f$
10		unipw	$⊢ ⋃ 𝒫 A = A$
11	10	eqcomi	$⊢ A = ⋃ 𝒫 A$
12	1 11	hmeof1o	$⊢ f \in (J Homeo 𝒫 A) \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 ran f \subseteq A$
15	12 13 14	3syl	$⊢ f \in (J Homeo 𝒫 A) \to ran f \subseteq A$
16	15	adantr	$⊢ (f \in (J Homeo 𝒫 A) \land x \subseteq X) \to ran f \subseteq A$
17	9 16	sstrid	$⊢ (f \in (J Homeo 𝒫 A) \land x \subseteq X) \to f [x] \subseteq A$
18		vex	$⊢ f \in V$
19	18	imaex	$⊢ f [x] \in V$
20	19	elpw	$⊢ f [x] \in 𝒫 A \leftrightarrow f [x] \subseteq A$
21	17 20	sylibr	$⊢ (f \in (J Homeo 𝒫 A) \land x \subseteq X) \to f [x] \in 𝒫 A$
22	1	hmeoopn	$⊢ (f \in (J Homeo 𝒫 A) \land x \subseteq X) \to (x \in J \leftrightarrow f [x] \in 𝒫 A)$
23	21 22	mpbird	$⊢ (f \in (J Homeo 𝒫 A) \land x \subseteq X) \to x \in J$
24	23	ex	$⊢ f \in (J Homeo 𝒫 A) \to (x \subseteq X \to x \in J)$
25	8 24	syl5	$⊢ f \in (J Homeo 𝒫 A) \to (x \in 𝒫 X \to x \in J)$
26	25	ssrdv	$⊢ f \in (J Homeo 𝒫 A) \to 𝒫 X \subseteq J$
27	26	exlimiv	$⊢ \exists f f \in (J Homeo 𝒫 A) \to 𝒫 X \subseteq J$
28	7 27	sylbi	$⊢ J Homeo 𝒫 A \neq \emptyset \to 𝒫 X \subseteq J$
29	6 28	sylbi	$⊢ J ≃ 𝒫 A \to 𝒫 X \subseteq J$
30	5 29	eqssd	$⊢ J ≃ 𝒫 A \to J = 𝒫 X$

Metamath Proof Explorer

Theorem hmphdis

Proof