Theorem qtoptop

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

	Ref	Expression
Hypothesis	qtoptop.1	⊢ 𝑋 = ∪ 𝐽
Assertion	qtoptop	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		qtoptop.1	⊢ 𝑋 = ∪ 𝐽
2		simpl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → 𝐽 ∈ Top )
3		id	⊢ ( 𝐹 Fn 𝑋 → 𝐹 Fn 𝑋 )
4	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
5		fnex	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝐹 ∈ V )
6	3 4 5	syl2anr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ V )
7		fnfun	⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
8	7	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → Fun 𝐹 )
9		qtoptop2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ V ∧ Fun 𝐹 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
10	2 6 8 9	syl3anc	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )