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 simpr ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F Fn X
2 dffn4 ⊢ F Fn X ↔ F : X ⟶ onto ran ⁡ F
3 1 2 sylib ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F : X ⟶ onto ran ⁡ F
4 fof ⊢ F : X ⟶ onto ran ⁡ F → F : X ⟶ ran ⁡ F
5 3 4 syl ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F : X ⟶ ran ⁡ F
6 elqtop3 ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → x ∈ J qTop F ↔ x ⊆ ran ⁡ F ∧ F -1 x ∈ J
7 3 6 syldan ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → x ∈ J qTop F ↔ x ⊆ ran ⁡ F ∧ F -1 x ∈ J
8 7 simplbda ⊢ J ∈ TopOn ⁡ X ∧ F Fn X ∧ x ∈ J qTop F → F -1 x ∈ J
9 8 ralrimiva ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → ∀ x ∈ J qTop F F -1 x ∈ J
10 qtoptopon ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → J qTop F ∈ TopOn ⁡ ran ⁡ F
11 3 10 syldan ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → J qTop F ∈ TopOn ⁡ ran ⁡ F
12 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
13 11 12 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
14 5 9 13 mpbir2and ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F ∈ J Cn J qTop F