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 ⊢φ→J∈TopOn⁡X
qtopf1.2 ⊢φ→F:X⟶1-1Y
Assertion qtopf1 ⊢φ→F∈JHomeoJqTopF

Proof

Step Hyp Ref Expression
1 qtopf1.1 ⊢φ→J∈TopOn⁡X
2 qtopf1.2 ⊢φ→F:X⟶1-1Y
3 f1fn ⊢F:X⟶1-1Y→FFnX
4 2 3 syl ⊢φ→FFnX
5 qtopid ⊢J∈TopOn⁡X∧FFnX→F∈JCnJqTopF
6 1 4 5 syl2anc ⊢φ→F∈JCnJqTopF
7 f1f1orn ⊢F:X⟶1-1Y→F:X⟶1-1 ontoran⁡F
8 f1ocnv ⊢F:X⟶1-1 ontoran⁡F→F-1:ran⁡F⟶1-1 ontoX
9 f1of ⊢F-1:ran⁡F⟶1-1 ontoX→F-1:ran⁡F⟶X
10 2 7 8 9 4syl ⊢φ→F-1:ran⁡F⟶X
11 imacnvcnv ⊢F-1-1x=Fx
12 imassrn ⊢Fx⊆ran⁡F
13 12 a1i ⊢φ∧x∈J→Fx⊆ran⁡F
14 2 adantr ⊢φ∧x∈J→F:X⟶1-1Y
15 toponss ⊢J∈TopOn⁡X∧x∈J→x⊆X
16 1 15 sylan ⊢φ∧x∈J→x⊆X
17 f1imacnv ⊢F:X⟶1-1Y∧x⊆X→F-1Fx=x
18 14 16 17 syl2anc ⊢φ∧x∈J→F-1Fx=x
19 simpr ⊢φ∧x∈J→x∈J
20 18 19 eqeltrd ⊢φ∧x∈J→F-1Fx∈J
21 dffn4 ⊢FFnX↔F:X⟶ontoran⁡F
22 4 21 sylib ⊢φ→F:X⟶ontoran⁡F
23 elqtop3 ⊢J∈TopOn⁡X∧F:X⟶ontoran⁡F→Fx∈JqTopF↔Fx⊆ran⁡F∧F-1Fx∈J
24 1 22 23 syl2anc ⊢φ→Fx∈JqTopF↔Fx⊆ran⁡F∧F-1Fx∈J
25 24 adantr ⊢φ∧x∈J→Fx∈JqTopF↔Fx⊆ran⁡F∧F-1Fx∈J
26 13 20 25 mpbir2and ⊢φ∧x∈J→Fx∈JqTopF
27 11 26 eqeltrid ⊢φ∧x∈J→F-1-1x∈JqTopF
28 27 ralrimiva ⊢φ→∀x∈JF-1-1x∈JqTopF
29 qtoptopon ⊢J∈TopOn⁡X∧F:X⟶ontoran⁡F→JqTopF∈TopOn⁡ran⁡F
30 1 22 29 syl2anc ⊢φ→JqTopF∈TopOn⁡ran⁡F
31 iscn ⊢JqTopF∈TopOn⁡ran⁡F∧J∈TopOn⁡X→F-1∈JqTopFCnJ↔F-1:ran⁡F⟶X∧∀x∈JF-1-1x∈JqTopF
32 30 1 31 syl2anc ⊢φ→F-1∈JqTopFCnJ↔F-1:ran⁡F⟶X∧∀x∈JF-1-1x∈JqTopF
33 10 28 32 mpbir2and ⊢φ→F-1∈JqTopFCnJ
34 ishmeo ⊢F∈JHomeoJqTopF↔F∈JCnJqTopF∧F-1∈JqTopFCnJ
35 6 33 34 sylanbrc ⊢φ→F∈JHomeoJqTopF