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 )
9 8 ad2antll 
 |-  ( ( ( 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 )
14 13 adantr 
 |-  ( ( ( 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 )
17 16 ad2antll 
 |-  ( ( ( 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 )
23 22 adantr 
 |-  ( ( ( 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 ) ) )
34 7 33 jcad 
 |-  ( ( 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 imbitrrdi 
 |-  ( ( 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 ) )