This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qtopuni

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

Ref Expression
Hypothesis qtoptop.1 
|- X = U. J
Assertion qtopuni 
|- ( ( J e. Top /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )

Proof

Step Hyp Ref Expression
1 qtoptop.1 
 |-  X = U. J
2 ssidd 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> Y C_ Y )
3 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
4 3 adantl 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> F : X --> Y )
5 fimacnv 
 |-  ( F : X --> Y -> ( `' F " Y ) = X )
6 4 5 syl 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> ( `' F " Y ) = X )
7 1 topopn 
 |-  ( J e. Top -> X e. J )
8 7 adantr 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> X e. J )
9 6 8 eqeltrd 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> ( `' F " Y ) e. J )
10 1 elqtop2 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> ( Y e. ( J qTop F ) <-> ( Y C_ Y /\ ( `' F " Y ) e. J ) ) )
11 2 9 10 mpbir2and 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> Y e. ( J qTop F ) )
12 elssuni 
 |-  ( Y e. ( J qTop F ) -> Y C_ U. ( J qTop F ) )
13 11 12 syl 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> Y C_ U. ( J qTop F ) )
14 1 elqtop2 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) )
15 simpl 
 |-  ( ( x C_ Y /\ ( `' F " x ) e. J ) -> x C_ Y )
16 velpw 
 |-  ( x e. ~P Y <-> x C_ Y )
17 15 16 sylibr 
 |-  ( ( x C_ Y /\ ( `' F " x ) e. J ) -> x e. ~P Y )
18 14 17 biimtrdi 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> ( x e. ( J qTop F ) -> x e. ~P Y ) )
19 18 ssrdv 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> ( J qTop F ) C_ ~P Y )
20 sspwuni 
 |-  ( ( J qTop F ) C_ ~P Y <-> U. ( J qTop F ) C_ Y )
21 19 20 sylib 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> U. ( J qTop F ) C_ Y )
22 13 21 eqssd 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )