Theorem hmphdis

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

	Ref	Expression
Hypothesis	hmphdis.1	⊢ 𝑋 = ∪ 𝐽
Assertion	hmphdis	⊢ ( 𝐽 ≃ 𝒫 𝐴 → 𝐽 = 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		hmphdis.1	⊢ 𝑋 = ∪ 𝐽
2		pwuni	⊢ 𝐽 ⊆ 𝒫 ∪ 𝐽
3	1	pweqi	⊢ 𝒫 𝑋 = 𝒫 ∪ 𝐽
4	2 3	sseqtrri	⊢ 𝐽 ⊆ 𝒫 𝑋
5	4	a1i	⊢ ( 𝐽 ≃ 𝒫 𝐴 → 𝐽 ⊆ 𝒫 𝑋 )
6		hmph	⊢ ( 𝐽 ≃ 𝒫 𝐴 ↔ ( 𝐽 Homeo 𝒫 𝐴 ) ≠ ∅ )
7		n0	⊢ ( ( 𝐽 Homeo 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) )
8		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
9		imassrn	⊢ ( 𝑓 “ 𝑥 ) ⊆ ran 𝑓
10		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
11	10	eqcomi	⊢ 𝐴 = ∪ 𝒫 𝐴
12	1 11	hmeof1o	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) → 𝑓 : 𝑋 –1-1-onto→ 𝐴 )
13		f1of	⊢ ( 𝑓 : 𝑋 –1-1-onto→ 𝐴 → 𝑓 : 𝑋 ⟶ 𝐴 )
14		frn	⊢ ( 𝑓 : 𝑋 ⟶ 𝐴 → ran 𝑓 ⊆ 𝐴 )
15	12 13 14	3syl	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) → ran 𝑓 ⊆ 𝐴 )
16	15	adantr	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) ∧ 𝑥 ⊆ 𝑋 ) → ran 𝑓 ⊆ 𝐴 )
17	9 16	sstrid	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑓 “ 𝑥 ) ⊆ 𝐴 )
18		vex	⊢ 𝑓 ∈ V
19	18	imaex	⊢ ( 𝑓 “ 𝑥 ) ∈ V
20	19	elpw	⊢ ( ( 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ↔ ( 𝑓 “ 𝑥 ) ⊆ 𝐴 )
21	17 20	sylibr	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 )
22	1	hmeoopn	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 ↔ ( 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ) )
23	21 22	mpbird	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ∈ 𝐽 )
24	23	ex	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) → ( 𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐽 ) )
25	8 24	syl5	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) → ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ∈ 𝐽 ) )
26	25	ssrdv	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) → 𝒫 𝑋 ⊆ 𝐽 )
27	26	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝒫 𝐴 ) → 𝒫 𝑋 ⊆ 𝐽 )
28	7 27	sylbi	⊢ ( ( 𝐽 Homeo 𝒫 𝐴 ) ≠ ∅ → 𝒫 𝑋 ⊆ 𝐽 )
29	6 28	sylbi	⊢ ( 𝐽 ≃ 𝒫 𝐴 → 𝒫 𝑋 ⊆ 𝐽 )
30	5 29	eqssd	⊢ ( 𝐽 ≃ 𝒫 𝐴 → 𝐽 = 𝒫 𝑋 )