Metamath Proof Explorer

Theorem elqtop3

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion elqtop3 
|- ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )

Proof

Step Hyp Ref Expression
1 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
2 eqimss 
 |-  ( X = U. J -> X C_ U. J )
3 1 2 syl 
 |-  ( J e. ( TopOn ` X ) -> X C_ U. J )
4 3 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> X C_ U. J )
5 eqid 
 |-  U. J = U. J
6 5 elqtop 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y /\ X C_ U. J ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )
7 4 6 mpd3an3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )