Metamath Proof Explorer

Theorem qtoptopon

Description: The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion qtoptopon 
|- ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
3 foeq2 
 |-  ( X = U. J -> ( F : X -onto-> Y <-> F : U. J -onto-> Y ) )
4 2 3 syl 
 |-  ( J e. ( TopOn ` X ) -> ( F : X -onto-> Y <-> F : U. J -onto-> Y ) )
5 4 biimpa 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> F : U. J -onto-> Y )
6 fofn 
 |-  ( F : U. J -onto-> Y -> F Fn U. J )
7 5 6 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> F Fn U. J )
8 eqid 
 |-  U. J = U. J
9 8 qtoptop 
 |-  ( ( J e. Top /\ F Fn U. J ) -> ( J qTop F ) e. Top )
10 1 7 9 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. Top )
11 8 qtopuni 
 |-  ( ( J e. Top /\ F : U. J -onto-> Y ) -> Y = U. ( J qTop F ) )
12 1 5 11 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )
13 istopon 
 |-  ( ( J qTop F ) e. ( TopOn ` Y ) <-> ( ( J qTop F ) e. Top /\ Y = U. ( J qTop F ) ) )
14 10 12 13 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )