Theorem imastps

Description: The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	imastps.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
	imastps.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imastps.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imastps.r	⊢ ( 𝜑 → 𝑅 ∈ TopSp )
Assertion	imastps	⊢ ( 𝜑 → 𝑈 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		imastps.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2		imastps.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imastps.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imastps.r	⊢ ( 𝜑 → 𝑅 ∈ TopSp )
5		eqid	⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
6		eqid	⊢ ( TopOpen ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 )
7	1 2 3 4 5 6	imastopn	⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	8 5	istps	⊢ ( 𝑅 ∈ TopSp ↔ ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
10	4 9	sylib	⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
11	2	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ 𝑉 ) = ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
12	10 11	eleqtrrd	⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑉 ) )
13		qtoptopon	⊢ ( ( ( TopOpen ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑉 ) ∧ 𝐹 : 𝑉 –onto→ 𝐵 ) → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ∈ ( TopOn ‘ 𝐵 ) )
14	12 3 13	syl2anc	⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ∈ ( TopOn ‘ 𝐵 ) )
15	1 2 3 4	imasbas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ 𝐵 ) = ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
17	14 16	eleqtrd	⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ∈ ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
18	7 17	eqeltrd	⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) ∈ ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
19		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20	19 6	istps	⊢ ( 𝑈 ∈ TopSp ↔ ( TopOpen ‘ 𝑈 ) ∈ ( TopOn ‘ ( Base ‘ 𝑈 ) ) )
21	18 20	sylibr	⊢ ( 𝜑 → 𝑈 ∈ TopSp )