Metamath Proof Explorer

Theorem cmphaushmeo

Description: A continuous bijection from a compact space to a Hausdorff space is a homeomorphism. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Hypotheses cmphaushmeo.1 ⊢ 𝑋 = ∪ 𝐽
cmphaushmeo.2 ⊢ 𝑌 = ∪ 𝐾
Assertion cmphaushmeo ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 cmphaushmeo.1 ⊢ 𝑋 = ∪ 𝐽
2 cmphaushmeo.2 ⊢ 𝑌 = ∪ 𝐾
3 1 2 hmeof1o ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
4 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
5 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
6 4 5 syl ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
7 6 a1i ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 ) )
8 f1orel ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → Rel 𝐹 )
9 8 ad2antll ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → Rel 𝐹 )
10 dfrel2 ⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
11 9 10 sylib ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ◡ ◡ 𝐹 = 𝐹 )
12 11 imaeq1d ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ( ◡ ◡ 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑥 ) )
13 simp2 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Haus )
14 13 adantr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → 𝐾 ∈ Haus )
15 imassrn ⊢ ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹
16 f1ofo ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 )
17 16 ad2antll ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
18 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
19 17 18 syl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ran 𝐹 = 𝑌 )
20 15 19 sseqtrid ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑌 )
21 simpl3 ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
22 simp1 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Comp )
23 22 adantr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → 𝐽 ∈ Comp )
24 simprl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
25 cmpcld ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝑥 ) ∈ Comp )
26 23 24 25 syl2anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ( 𝐽 ↾t 𝑥 ) ∈ Comp )
27 imacmp ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽 ↾t 𝑥 ) ∈ Comp ) → ( 𝐾 ↾t ( 𝐹 “ 𝑥 ) ) ∈ Comp )
28 21 26 27 syl2anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ( 𝐾 ↾t ( 𝐹 “ 𝑥 ) ) ∈ Comp )
29 2 hauscmp ⊢ ( ( 𝐾 ∈ Haus ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑌 ∧ ( 𝐾 ↾t ( 𝐹 “ 𝑥 ) ) ∈ Comp ) → ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
30 14 20 28 29 syl3anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
31 12 30 eqeltrd ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) → ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
32 31 expr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) )
33 32 ralrimdva ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) )
34 7 33 jcad ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) ) )
35 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
36 13 35 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
37 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
38 36 37 sylib ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
39 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
40 22 39 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
41 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
42 40 41 sylib ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
43 iscncl ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) ) )
44 38 42 43 syl2anc ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ) ) )
45 34 44 sylibrd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) )
46 simp3 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
47 45 46 jctild ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) ) )
48 ishmeo ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ↔ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) )
49 47 48 syl6ibr ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) )
50 3 49 impbid2 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )