This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 qTop ( I ↾ 𝑋 ) ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 cnvresid ⊢ ◡ ( I ↾ 𝑋 ) = ( I ↾ 𝑋 )
2 1 imaeq1i ⊢ ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) = ( ( I ↾ 𝑋 ) “ 𝑥 )
3 resiima ⊢ ( 𝑥 ⊆ 𝑋 → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 )
4 3 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 )
5 2 4 eqtrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 )
6 5 eleq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ 𝑥 ∈ 𝐽 ) )
7 6 pm5.32da ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝑥 ⊆ 𝑋 ∧ ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ∈ 𝐽 ) ) )
8 f1oi ⊢ ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋
9 f1ofo ⊢ ( ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 → ( I ↾ 𝑋 ) : 𝑋 –onto→ 𝑋 )
10 8 9 mp1i ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) : 𝑋 –onto→ 𝑋 )
11 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( I ↾ 𝑋 ) : 𝑋 –onto→ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 qTop ( I ↾ 𝑋 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ) )
12 10 11 mpdan ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 qTop ( I ↾ 𝑋 ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ) )
13 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
14 13 ex ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋 ) )
15 14 pm4.71rd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ∈ 𝐽 ) ) )
16 7 12 15 3bitr4d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 qTop ( I ↾ 𝑋 ) ) ↔ 𝑥 ∈ 𝐽 ) )
17 16 eqrdv ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 qTop ( I ↾ 𝑋 ) ) = 𝐽 )