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	syl6bi	|- ( ( 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 ) )