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