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