# 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
`|- X = U. J`
cmphaushmeo.2
`|- Y = U. K`
Assertion cmphaushmeo
`|- ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F e. ( J Homeo K ) <-> F : X -1-1-onto-> Y ) )`

### Proof

Step Hyp Ref Expression
1 cmphaushmeo.1
` |-  X = U. J`
2 cmphaushmeo.2
` |-  Y = U. K`
3 1 2 hmeof1o
` |-  ( F e. ( J Homeo K ) -> F : X -1-1-onto-> Y )`
4 f1ocnv
` |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )`
5 f1of
` |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )`
6 4 5 syl
` |-  ( F : X -1-1-onto-> Y -> `' F : Y --> X )`
7 6 a1i
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F : X -1-1-onto-> Y -> `' F : Y --> X ) )`
8 f1orel
` |-  ( F : X -1-1-onto-> Y -> Rel F )`
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> Rel F )`
10 dfrel2
` |-  ( Rel F <-> `' `' F = F )`
11 9 10 sylib
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> `' `' F = F )`
12 11 imaeq1d
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ( `' `' F " x ) = ( F " x ) )`
13 simp2
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> K e. Haus )`
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> K e. Haus )`
15 imassrn
` |-  ( F " x ) C_ ran F`
16 f1ofo
` |-  ( F : X -1-1-onto-> Y -> F : X -onto-> Y )`
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> F : X -onto-> Y )`
18 forn
` |-  ( F : X -onto-> Y -> ran F = Y )`
19 17 18 syl
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ran F = Y )`
20 15 19 sseqtrid
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ( F " x ) C_ Y )`
21 simpl3
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> F e. ( J Cn K ) )`
22 simp1
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> J e. Comp )`
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> J e. Comp )`
24 simprl
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> x e. ( Clsd ` J ) )`
25 cmpcld
` |-  ( ( J e. Comp /\ x e. ( Clsd ` J ) ) -> ( J |`t x ) e. Comp )`
26 23 24 25 syl2anc
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ( J |`t x ) e. Comp )`
27 imacmp
` |-  ( ( F e. ( J Cn K ) /\ ( J |`t x ) e. Comp ) -> ( K |`t ( F " x ) ) e. Comp )`
28 21 26 27 syl2anc
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ( K |`t ( F " x ) ) e. Comp )`
29 2 hauscmp
` |-  ( ( K e. Haus /\ ( F " x ) C_ Y /\ ( K |`t ( F " x ) ) e. Comp ) -> ( F " x ) e. ( Clsd ` K ) )`
30 14 20 28 29 syl3anc
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ( F " x ) e. ( Clsd ` K ) )`
31 12 30 eqeltrd
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ ( x e. ( Clsd ` J ) /\ F : X -1-1-onto-> Y ) ) -> ( `' `' F " x ) e. ( Clsd ` K ) )`
32 31 expr
` |-  ( ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) /\ x e. ( Clsd ` J ) ) -> ( F : X -1-1-onto-> Y -> ( `' `' F " x ) e. ( Clsd ` K ) ) )`
33 32 ralrimdva
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F : X -1-1-onto-> Y -> A. x e. ( Clsd ` J ) ( `' `' F " x ) e. ( Clsd ` K ) ) )`
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F : X -1-1-onto-> Y -> ( `' F : Y --> X /\ A. x e. ( Clsd ` J ) ( `' `' F " x ) e. ( Clsd ` K ) ) ) )`
35 haustop
` |-  ( K e. Haus -> K e. Top )`
36 13 35 syl
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> K e. Top )`
37 2 toptopon
` |-  ( K e. Top <-> K e. ( TopOn ` Y ) )`
38 36 37 sylib
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> K e. ( TopOn ` Y ) )`
39 cmptop
` |-  ( J e. Comp -> J e. Top )`
40 22 39 syl
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> J e. Top )`
41 1 toptopon
` |-  ( J e. Top <-> J e. ( TopOn ` X ) )`
42 40 41 sylib
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> J e. ( TopOn ` X ) )`
43 iscncl
` |-  ( ( K e. ( TopOn ` Y ) /\ J e. ( TopOn ` X ) ) -> ( `' F e. ( K Cn J ) <-> ( `' F : Y --> X /\ A. x e. ( Clsd ` J ) ( `' `' F " x ) e. ( Clsd ` K ) ) ) )`
44 38 42 43 syl2anc
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( `' F e. ( K Cn J ) <-> ( `' F : Y --> X /\ A. x e. ( Clsd ` J ) ( `' `' F " x ) e. ( Clsd ` K ) ) ) )`
45 34 44 sylibrd
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F : X -1-1-onto-> Y -> `' F e. ( K Cn J ) ) )`
46 simp3
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> F e. ( J Cn K ) )`
47 45 46 jctild
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F : X -1-1-onto-> Y -> ( F e. ( J Cn K ) /\ `' F e. ( K Cn J ) ) ) )`
48 ishmeo
` |-  ( F e. ( J Homeo K ) <-> ( F e. ( J Cn K ) /\ `' F e. ( K Cn J ) ) )`
49 47 48 syl6ibr
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F : X -1-1-onto-> Y -> F e. ( J Homeo K ) ) )`
50 3 49 impbid2
` |-  ( ( J e. Comp /\ K e. Haus /\ F e. ( J Cn K ) ) -> ( F e. ( J Homeo K ) <-> F : X -1-1-onto-> Y ) )`