Metamath Proof Explorer

Theorem qtoptopon

Description: The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion qtoptopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
3 foeq2 ⊢ ( 𝑋 = ∪ 𝐽 → ( 𝐹 : 𝑋 –onto→ 𝑌 ↔ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) )
4 2 3 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐹 : 𝑋 –onto→ 𝑌 ↔ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) )
5 4 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
6 fofn ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 → 𝐹 Fn ∪ 𝐽 )
7 5 6 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝐹 Fn ∪ 𝐽 )
8 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
9 8 qtoptop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn ∪ 𝐽 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
10 1 7 9 syl2an2r ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
11 8 qtopuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
12 1 5 11 syl2an2r ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
13 istopon ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ↔ ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) ) )
14 10 12 13 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )