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	syl5eq	⊢ ( ( 𝐽 ∈ ( 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 ↾ 𝑋 ) ) = 𝐽 )