Metamath Proof Explorer


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 )