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