prdstps

Description: A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	prdstopn.y	$⊢ Y = S ⨉_{𝑠} R$
	prdstopn.s	$⊢ φ \to S \in V$
	prdstopn.i	$⊢ φ \to I \in W$
	prdstps.r	$⊢ φ \to R : I ⟶ TopSp$
Assertion	prdstps	$⊢ φ \to Y \in TopSp$

Proof

Step	Hyp	Ref	Expression
1		prdstopn.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdstopn.s	$⊢ φ \to S \in V$
3		prdstopn.i	$⊢ φ \to I \in W$
4		prdstps.r	$⊢ φ \to R : I ⟶ TopSp$
5	4	ffvelcdmda	$⊢ (φ \land x \in I) \to R (x) \in TopSp$
6		eqid	$⊢ {Base}_{R (x)} = {Base}_{R (x)}$
7		eqid	$⊢ TopOpen (R (x)) = TopOpen (R (x))$
8	6 7	istps	$⊢ R (x) \in TopSp \leftrightarrow TopOpen (R (x)) \in TopOn ({Base}_{R (x)})$
9	5 8	sylib	$⊢ (φ \land x \in I) \to TopOpen (R (x)) \in TopOn ({Base}_{R (x)})$
10	9	ralrimiva	$⊢ φ \to \forall x \in I TopOpen (R (x)) \in TopOn ({Base}_{R (x)})$
11		eqid	$⊢ \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x)))) = \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x))))$
12	11	pttopon	$⊢ (I \in W \land \forall x \in I TopOpen (R (x)) \in TopOn ({Base}_{R (x)})) \to \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x)))) \in TopOn (\underset{x \in I}{⨉} {Base}_{R (x)})$
13	3 10 12	syl2anc	$⊢ φ \to \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x)))) \in TopOn (\underset{x \in I}{⨉} {Base}_{R (x)})$
14	4 3	fexd	$⊢ φ \to R \in V$
15		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
16	4	fdmd	$⊢ φ \to dom R = I$
17		eqid	$⊢ TopSet (Y) = TopSet (Y)$
18	1 2 14 15 16 17	prdstset	$⊢ φ \to TopSet (Y) = \prod_{𝑡} (TopOpen \circ R)$
19		topnfn	$⊢ TopOpen Fn V$
20		dffn2	$⊢ TopOpen Fn V \leftrightarrow TopOpen : V ⟶ V$
21	19 20	mpbi	$⊢ TopOpen : V ⟶ V$
22		ssv	$⊢ TopSp \subseteq V$
23		fss	$⊢ (R : I ⟶ TopSp \land TopSp \subseteq V) \to R : I ⟶ V$
24	4 22 23	sylancl	$⊢ φ \to R : I ⟶ V$
25		fcompt	$⊢ (TopOpen : V ⟶ V \land R : I ⟶ V) \to TopOpen \circ R = (x \in I ⟼ TopOpen (R (x)))$
26	21 24 25	sylancr	$⊢ φ \to TopOpen \circ R = (x \in I ⟼ TopOpen (R (x)))$
27	26	fveq2d	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x))))$
28	18 27	eqtrd	$⊢ φ \to TopSet (Y) = \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x))))$
29	1 2 14 15 16	prdsbas	$⊢ φ \to {Base}_{Y} = \underset{x \in I}{⨉} {Base}_{R (x)}$
30	29	fveq2d	$⊢ φ \to TopOn ({Base}_{Y}) = TopOn (\underset{x \in I}{⨉} {Base}_{R (x)})$
31	13 28 30	3eltr4d	$⊢ φ \to TopSet (Y) \in TopOn ({Base}_{Y})$
32	15 17	tsettps	$⊢ TopSet (Y) \in TopOn ({Base}_{Y}) \to Y \in TopSp$
33	31 32	syl	$⊢ φ \to Y \in TopSp$

Metamath Proof Explorer

Theorem prdstps

Proof