# 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`