Metamath Proof Explorer

Theorem idqtop

Description: The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion idqtop ⊢ J ∈ TopOn ⁡ X → J qTop I ↾ X = J

Proof

Step Hyp Ref Expression
1 cnvresid ⊢ I ↾ X -1 = I ↾ X
2 1 imaeq1i ⊢ I ↾ X -1 x = I ↾ X x
3 resiima ⊢ x ⊆ X → I ↾ X x = x
4 3 adantl ⊢ J ∈ TopOn ⁡ X ∧ x ⊆ X → I ↾ X x = x
5 2 4 syl5eq ⊢ J ∈ TopOn ⁡ X ∧ x ⊆ X → I ↾ X -1 x = x
6 5 eleq1d ⊢ J ∈ TopOn ⁡ X ∧ x ⊆ X → I ↾ X -1 x ∈ J ↔ x ∈ J
7 6 pm5.32da ⊢ J ∈ TopOn ⁡ X → x ⊆ X ∧ I ↾ X -1 x ∈ J ↔ x ⊆ X ∧ x ∈ J
8 f1oi ⊢ I ↾ X : X ⟶ 1-1 onto X
9 f1ofo ⊢ I ↾ X : X ⟶ 1-1 onto X → I ↾ X : X ⟶ onto X
10 8 9 mp1i ⊢ J ∈ TopOn ⁡ X → I ↾ X : X ⟶ onto X
11 elqtop3 ⊢ J ∈ TopOn ⁡ X ∧ I ↾ X : X ⟶ onto X → x ∈ J qTop I ↾ X ↔ x ⊆ X ∧ I ↾ X -1 x ∈ J
12 10 11 mpdan ⊢ J ∈ TopOn ⁡ X → x ∈ J qTop I ↾ X ↔ x ⊆ X ∧ I ↾ X -1 x ∈ J
13 toponss ⊢ J ∈ TopOn ⁡ X ∧ x ∈ J → x ⊆ X
14 13 ex ⊢ J ∈ TopOn ⁡ X → x ∈ J → x ⊆ X
15 14 pm4.71rd ⊢ J ∈ TopOn ⁡ X → x ∈ J ↔ x ⊆ X ∧ x ∈ J
16 7 12 15 3bitr4d ⊢ J ∈ TopOn ⁡ X → x ∈ J qTop I ↾ X ↔ x ∈ J
17 16 eqrdv ⊢ J ∈ TopOn ⁡ X → J qTop I ↾ X = J