Metamath Proof Explorer

Theorem qtopf1

Description: If a quotient map is injective, then it is a homeomorphism. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses qtopf1.1 
|- ( ph -> J e. ( TopOn ` X ) )
qtopf1.2 
|- ( ph -> F : X -1-1-> Y )
Assertion qtopf1 
|- ( ph -> F e. ( J Homeo ( J qTop F ) ) )

Proof

Step Hyp Ref Expression
1 qtopf1.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 qtopf1.2 
 |-  ( ph -> F : X -1-1-> Y )
3 f1fn 
 |-  ( F : X -1-1-> Y -> F Fn X )
4 2 3 syl 
 |-  ( ph -> F Fn X )
5 qtopid 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
6 1 4 5 syl2anc 
 |-  ( ph -> F e. ( J Cn ( J qTop F ) ) )
7 f1f1orn 
 |-  ( F : X -1-1-> Y -> F : X -1-1-onto-> ran F )
8 f1ocnv 
 |-  ( F : X -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> X )
9 f1of 
 |-  ( `' F : ran F -1-1-onto-> X -> `' F : ran F --> X )
10 2 7 8 9 4syl 
 |-  ( ph -> `' F : ran F --> X )
11 imacnvcnv 
 |-  ( `' `' F " x ) = ( F " x )
12 imassrn 
 |-  ( F " x ) C_ ran F
13 12 a1i 
 |-  ( ( ph /\ x e. J ) -> ( F " x ) C_ ran F )
14 2 adantr 
 |-  ( ( ph /\ x e. J ) -> F : X -1-1-> Y )
15 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
16 1 15 sylan 
 |-  ( ( ph /\ x e. J ) -> x C_ X )
17 f1imacnv 
 |-  ( ( F : X -1-1-> Y /\ x C_ X ) -> ( `' F " ( F " x ) ) = x )
18 14 16 17 syl2anc 
 |-  ( ( ph /\ x e. J ) -> ( `' F " ( F " x ) ) = x )
19 simpr 
 |-  ( ( ph /\ x e. J ) -> x e. J )
20 18 19 eqeltrd 
 |-  ( ( ph /\ x e. J ) -> ( `' F " ( F " x ) ) e. J )
21 dffn4 
 |-  ( F Fn X <-> F : X -onto-> ran F )
22 4 21 sylib 
 |-  ( ph -> F : X -onto-> ran F )
23 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( ( F " x ) e. ( J qTop F ) <-> ( ( F " x ) C_ ran F /\ ( `' F " ( F " x ) ) e. J ) ) )
24 1 22 23 syl2anc 
 |-  ( ph -> ( ( F " x ) e. ( J qTop F ) <-> ( ( F " x ) C_ ran F /\ ( `' F " ( F " x ) ) e. J ) ) )
25 24 adantr 
 |-  ( ( ph /\ x e. J ) -> ( ( F " x ) e. ( J qTop F ) <-> ( ( F " x ) C_ ran F /\ ( `' F " ( F " x ) ) e. J ) ) )
26 13 20 25 mpbir2and 
 |-  ( ( ph /\ x e. J ) -> ( F " x ) e. ( J qTop F ) )
27 11 26 eqeltrid 
 |-  ( ( ph /\ x e. J ) -> ( `' `' F " x ) e. ( J qTop F ) )
28 27 ralrimiva 
 |-  ( ph -> A. x e. J ( `' `' F " x ) e. ( J qTop F ) )
29 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( J qTop F ) e. ( TopOn ` ran F ) )
30 1 22 29 syl2anc 
 |-  ( ph -> ( J qTop F ) e. ( TopOn ` ran F ) )
31 iscn 
 |-  ( ( ( J qTop F ) e. ( TopOn ` ran F ) /\ J e. ( TopOn ` X ) ) -> ( `' F e. ( ( J qTop F ) Cn J ) <-> ( `' F : ran F --> X /\ A. x e. J ( `' `' F " x ) e. ( J qTop F ) ) ) )
32 30 1 31 syl2anc 
 |-  ( ph -> ( `' F e. ( ( J qTop F ) Cn J ) <-> ( `' F : ran F --> X /\ A. x e. J ( `' `' F " x ) e. ( J qTop F ) ) ) )
33 10 28 32 mpbir2and 
 |-  ( ph -> `' F e. ( ( J qTop F ) Cn J ) )
34 ishmeo 
 |-  ( F e. ( J Homeo ( J qTop F ) ) <-> ( F e. ( J Cn ( J qTop F ) ) /\ `' F e. ( ( J qTop F ) Cn J ) ) )
35 6 33 34 sylanbrc 
 |-  ( ph -> F e. ( J Homeo ( J qTop F ) ) )