This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝐽 ∈ 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 𝐹 ) )