Theorem qtoptop

Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		qtoptop.1	|- X = U. J
2		simpl	|- ( ( J e. Top /\ F Fn X ) -> J e. Top )
3		id	|- ( F Fn X -> F Fn X )
4	1	topopn	|- ( J e. Top -> X e. J )
5		fnex	|- ( ( F Fn X /\ X e. J ) -> F e. _V )
6	3 4 5	syl2anr	|- ( ( J e. Top /\ F Fn X ) -> F e. _V )
7		fnfun	|- ( F Fn X -> Fun F )
8	7	adantl	|- ( ( J e. Top /\ F Fn X ) -> Fun F )
9		qtoptop2	|- ( ( J e. Top /\ F e. _V /\ Fun F ) -> ( J qTop F ) e. Top )
10	2 6 8 9	syl3anc	|- ( ( J e. Top /\ F Fn X ) -> ( J qTop F ) e. Top )