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 e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )

Proof

Step Hyp Ref Expression
1 dffn4 
 |-  ( F Fn X <-> F : X -onto-> ran F )
2 1 bilani 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F : X -onto-> ran F )
3 fof 
 |-  ( F : X -onto-> ran F -> F : X --> ran F )
4 2 3 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F : X --> ran F )
5 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( x e. ( J qTop F ) <-> ( x C_ ran F /\ ( `' F " x ) e. J ) ) )
6 2 5 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> ( x e. ( J qTop F ) <-> ( x C_ ran F /\ ( `' F " x ) e. J ) ) )
7 6 simplbda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F Fn X ) /\ x e. ( J qTop F ) ) -> ( `' F " x ) e. J )
8 7 ralrimiva 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> A. x e. ( J qTop F ) ( `' F " x ) e. J )
9 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( J qTop F ) e. ( TopOn ` ran F ) )
10 2 9 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> ( J qTop F ) e. ( TopOn ` ran F ) )
11 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ ( J qTop F ) e. ( TopOn ` ran F ) ) -> ( F e. ( J Cn ( J qTop F ) ) <-> ( F : X --> ran F /\ A. x e. ( J qTop F ) ( `' F " x ) e. J ) ) )
12 10 11 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> ( F e. ( J Cn ( J qTop F ) ) <-> ( F : X --> ran F /\ A. x e. ( J qTop F ) ( `' F " x ) e. J ) ) )
13 4 8 12 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )