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 e. ( TopOn ` X ) -> ( J qTop ( _I |` X ) ) = J )

Proof

Step Hyp Ref Expression
1 cnvresid 
 |-  `' ( _I |` X ) = ( _I |` X )
2 1 imaeq1i 
 |-  ( `' ( _I |` X ) " x ) = ( ( _I |` X ) " x )
3 resiima 
 |-  ( x C_ X -> ( ( _I |` X ) " x ) = x )
4 3 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ X ) -> ( ( _I |` X ) " x ) = x )
5 2 4 syl5eq 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ X ) -> ( `' ( _I |` X ) " x ) = x )
6 5 eleq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ X ) -> ( ( `' ( _I |` X ) " x ) e. J <-> x e. J ) )
7 6 pm5.32da 
 |-  ( J e. ( TopOn ` X ) -> ( ( x C_ X /\ ( `' ( _I |` X ) " x ) e. J ) <-> ( x C_ X /\ x e. 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 e. ( TopOn ` X ) -> ( _I |` X ) : X -onto-> X )
11 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ ( _I |` X ) : X -onto-> X ) -> ( x e. ( J qTop ( _I |` X ) ) <-> ( x C_ X /\ ( `' ( _I |` X ) " x ) e. J ) ) )
12 10 11 mpdan 
 |-  ( J e. ( TopOn ` X ) -> ( x e. ( J qTop ( _I |` X ) ) <-> ( x C_ X /\ ( `' ( _I |` X ) " x ) e. J ) ) )
13 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
14 13 ex 
 |-  ( J e. ( TopOn ` X ) -> ( x e. J -> x C_ X ) )
15 14 pm4.71rd 
 |-  ( J e. ( TopOn ` X ) -> ( x e. J <-> ( x C_ X /\ x e. J ) ) )
16 7 12 15 3bitr4d 
 |-  ( J e. ( TopOn ` X ) -> ( x e. ( J qTop ( _I |` X ) ) <-> x e. J ) )
17 16 eqrdv 
 |-  ( J e. ( TopOn ` X ) -> ( J qTop ( _I |` X ) ) = J )