Metamath Proof Explorer

Theorem qtopid

Description: A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion qtopid ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F ∈ J Cn J qTop F

Proof

Step Hyp Ref Expression
1 dffn4 ⊢ F Fn X ↔ F : X ⟶ onto ran ⁡ F
2 1 bilani ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F : X ⟶ onto ran ⁡ F
3 fof ⊢ F : X ⟶ onto ran ⁡ F → F : X ⟶ ran ⁡ F
4 2 3 syl ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F : X ⟶ ran ⁡ F
5 elqtop3 ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → x ∈ J qTop F ↔ x ⊆ ran ⁡ F ∧ F -1 x ∈ J
6 2 5 syldan ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → x ∈ J qTop F ↔ x ⊆ ran ⁡ F ∧ F -1 x ∈ J
7 6 simplbda ⊢ J ∈ TopOn ⁡ X ∧ F Fn X ∧ x ∈ J qTop F → F -1 x ∈ J
8 7 ralrimiva ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → ∀ x ∈ J qTop F F -1 x ∈ J
9 qtoptopon ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → J qTop F ∈ TopOn ⁡ ran ⁡ F
10 2 9 syldan ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → J qTop F ∈ TopOn ⁡ ran ⁡ F
11 iscn ⊢ J ∈ TopOn ⁡ X ∧ J qTop F ∈ TopOn ⁡ ran ⁡ F → F ∈ J Cn J qTop F ↔ F : X ⟶ ran ⁡ F ∧ ∀ x ∈ J qTop F F -1 x ∈ J
12 10 11 syldan ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F ∈ J Cn J qTop F ↔ F : X ⟶ ran ⁡ F ∧ ∀ x ∈ J qTop F F -1 x ∈ J
13 4 8 12 mpbir2and ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F ∈ J Cn J qTop F