Metamath Proof Explorer


Theorem qtopuni

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

Ref Expression
Hypothesis qtoptop.1 𝑋 = 𝐽
Assertion qtopuni ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑌 = ( 𝐽 qTop 𝐹 ) )

Proof

Step Hyp Ref Expression
1 qtoptop.1 𝑋 = 𝐽
2 ssidd ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑌𝑌 )
3 fof ( 𝐹 : 𝑋onto𝑌𝐹 : 𝑋𝑌 )
4 3 adantl ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝐹 : 𝑋𝑌 )
5 fimacnv ( 𝐹 : 𝑋𝑌 → ( 𝐹𝑌 ) = 𝑋 )
6 4 5 syl ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐹𝑌 ) = 𝑋 )
7 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
8 7 adantr ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑋𝐽 )
9 6 8 eqeltrd ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐹𝑌 ) ∈ 𝐽 )
10 1 elqtop2 ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝑌 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑌𝑌 ∧ ( 𝐹𝑌 ) ∈ 𝐽 ) ) )
11 2 9 10 mpbir2and ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑌 ∈ ( 𝐽 qTop 𝐹 ) )
12 elssuni ( 𝑌 ∈ ( 𝐽 qTop 𝐹 ) → 𝑌 ( 𝐽 qTop 𝐹 ) )
13 11 12 syl ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑌 ( 𝐽 qTop 𝐹 ) )
14 1 elqtop2 ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥𝑌 ∧ ( 𝐹𝑥 ) ∈ 𝐽 ) ) )
15 simpl ( ( 𝑥𝑌 ∧ ( 𝐹𝑥 ) ∈ 𝐽 ) → 𝑥𝑌 )
16 velpw ( 𝑥 ∈ 𝒫 𝑌𝑥𝑌 )
17 15 16 sylibr ( ( 𝑥𝑌 ∧ ( 𝐹𝑥 ) ∈ 𝐽 ) → 𝑥 ∈ 𝒫 𝑌 )
18 14 17 syl6bi ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) → 𝑥 ∈ 𝒫 𝑌 ) )
19 18 ssrdv ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 𝑌 )
20 sspwuni ( ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 𝑌 ( 𝐽 qTop 𝐹 ) ⊆ 𝑌 )
21 19 20 sylib ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐽 qTop 𝐹 ) ⊆ 𝑌 )
22 13 21 eqssd ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋onto𝑌 ) → 𝑌 = ( 𝐽 qTop 𝐹 ) )