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-1 Y
Assertion qtopf1 ⊢ φ → F ∈ J Homeo J qTop F

Proof

Step Hyp Ref Expression
1 qtopf1.1 ⊢ φ → J ∈ TopOn ⁡ X
2 qtopf1.2 ⊢ φ → F : X ⟶ 1-1 Y
3 f1fn ⊢ F : X ⟶ 1-1 Y → F Fn X
4 2 3 syl ⊢ φ → F Fn X
5 qtopid ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F ∈ J Cn J qTop F
6 1 4 5 syl2anc ⊢ φ → F ∈ 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 -1 : ran ⁡ F ⟶ 1-1 onto X
9 f1of ⊢ F -1 : ran ⁡ F ⟶ 1-1 onto X → F -1 : ran ⁡ F ⟶ X
10 2 7 8 9 4syl ⊢ φ → F -1 : ran ⁡ F ⟶ X
11 imacnvcnv ⊢ F -1 -1 x = F x
12 imassrn ⊢ F x ⊆ ran ⁡ F
13 12 a1i ⊢ φ ∧ x ∈ J → F x ⊆ ran ⁡ F
14 2 adantr ⊢ φ ∧ x ∈ J → F : X ⟶ 1-1 Y
15 toponss ⊢ J ∈ TopOn ⁡ X ∧ x ∈ J → x ⊆ X
16 1 15 sylan ⊢ φ ∧ x ∈ J → x ⊆ X
17 f1imacnv ⊢ F : X ⟶ 1-1 Y ∧ x ⊆ X → F -1 F x = x
18 14 16 17 syl2anc ⊢ φ ∧ x ∈ J → F -1 F x = x
19 simpr ⊢ φ ∧ x ∈ J → x ∈ J
20 18 19 eqeltrd ⊢ φ ∧ x ∈ J → F -1 F x ∈ J
21 dffn4 ⊢ F Fn X ↔ F : X ⟶ onto ran ⁡ F
22 4 21 sylib ⊢ φ → F : X ⟶ onto ran ⁡ F
23 elqtop3 ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → F x ∈ J qTop F ↔ F x ⊆ ran ⁡ F ∧ F -1 F x ∈ J
24 1 22 23 syl2anc ⊢ φ → F x ∈ J qTop F ↔ F x ⊆ ran ⁡ F ∧ F -1 F x ∈ J
25 24 adantr ⊢ φ ∧ x ∈ J → F x ∈ J qTop F ↔ F x ⊆ ran ⁡ F ∧ F -1 F x ∈ J
26 13 20 25 mpbir2and ⊢ φ ∧ x ∈ J → F x ∈ J qTop F
27 11 26 eqeltrid ⊢ φ ∧ x ∈ J → F -1 -1 x ∈ J qTop F
28 27 ralrimiva ⊢ φ → ∀ x ∈ J F -1 -1 x ∈ J qTop F
29 qtoptopon ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → J qTop F ∈ TopOn ⁡ ran ⁡ F
30 1 22 29 syl2anc ⊢ φ → J qTop F ∈ TopOn ⁡ ran ⁡ F
31 iscn ⊢ J qTop F ∈ TopOn ⁡ ran ⁡ F ∧ J ∈ TopOn ⁡ X → F -1 ∈ J qTop F Cn J ↔ F -1 : ran ⁡ F ⟶ X ∧ ∀ x ∈ J F -1 -1 x ∈ J qTop F
32 30 1 31 syl2anc ⊢ φ → F -1 ∈ J qTop F Cn J ↔ F -1 : ran ⁡ F ⟶ X ∧ ∀ x ∈ J F -1 -1 x ∈ J qTop F
33 10 28 32 mpbir2and ⊢ φ → F -1 ∈ J qTop F Cn J
34 ishmeo ⊢ F ∈ J Homeo J qTop F ↔ F ∈ J Cn J qTop F ∧ F -1 ∈ J qTop F Cn J
35 6 33 34 sylanbrc ⊢ φ → F ∈ J Homeo J qTop F