imastps

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

Step	Hyp	Ref	Expression
1		imastps.u	$⊢ φ \to U = F “_{𝑠} R$
2		imastps.v	$⊢ φ \to V = {Base}_{R}$
3		imastps.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
4		imastps.r	$⊢ φ \to R \in TopSp$
5		eqid	$⊢ TopOpen (R) = TopOpen (R)$
6		eqid	$⊢ TopOpen (U) = TopOpen (U)$
7	1 2 3 4 5 6	imastopn	$⊢ φ \to TopOpen (U) = TopOpen (R) qTop F$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8 5	istps	$⊢ R \in TopSp \leftrightarrow TopOpen (R) \in TopOn ({Base}_{R})$
10	4 9	sylib	$⊢ φ \to TopOpen (R) \in TopOn ({Base}_{R})$
11	2	fveq2d	$⊢ φ \to TopOn (V) = TopOn ({Base}_{R})$
12	10 11	eleqtrrd	$⊢ φ \to TopOpen (R) \in TopOn (V)$
13		qtoptopon	$⊢ (TopOpen (R) \in TopOn (V) \land F : V \underset{onto}{⟶} B) \to TopOpen (R) qTop F \in TopOn (B)$
14	12 3 13	syl2anc	$⊢ φ \to TopOpen (R) qTop F \in TopOn (B)$
15	1 2 3 4	imasbas	$⊢ φ \to B = {Base}_{U}$
16	15	fveq2d	$⊢ φ \to TopOn (B) = TopOn ({Base}_{U})$
17	14 16	eleqtrd	$⊢ φ \to TopOpen (R) qTop F \in TopOn ({Base}_{U})$
18	7 17	eqeltrd	$⊢ φ \to TopOpen (U) \in TopOn ({Base}_{U})$
19		eqid	$⊢ {Base}_{U} = {Base}_{U}$
20	19 6	istps	$⊢ U \in TopSp \leftrightarrow TopOpen (U) \in TopOn ({Base}_{U})$
21	18 20	sylibr	$⊢ φ \to U \in TopSp$

Metamath Proof Explorer