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	ffvelrnda	$⊢ (φ \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		fex	$⊢ (R : I ⟶ TopSp \land I \in W) \to R \in V$
15	4 3 14	syl2anc	$⊢ φ \to R \in V$
16		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
17	4	fdmd	$⊢ φ \to dom R = I$
18		eqid	$⊢ TopSet (Y) = TopSet (Y)$
19	1 2 15 16 17 18	prdstset	$⊢ φ \to TopSet (Y) = \prod_{𝑡} (TopOpen \circ R)$
20		topnfn	$⊢ TopOpen Fn V$
21		dffn2	$⊢ TopOpen Fn V \leftrightarrow TopOpen : V ⟶ V$
22	20 21	mpbi	$⊢ TopOpen : V ⟶ V$
23		ssv	$⊢ TopSp \subseteq V$
24		fss	$⊢ (R : I ⟶ TopSp \land TopSp \subseteq V) \to R : I ⟶ V$
25	4 23 24	sylancl	$⊢ φ \to R : I ⟶ V$
26		fcompt	$⊢ (TopOpen : V ⟶ V \land R : I ⟶ V) \to TopOpen \circ R = (x \in I ⟼ TopOpen (R (x)))$
27	22 25 26	sylancr	$⊢ φ \to TopOpen \circ R = (x \in I ⟼ TopOpen (R (x)))$
28	27	fveq2d	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x))))$
29	19 28	eqtrd	$⊢ φ \to TopSet (Y) = \prod_{𝑡} ((x \in I ⟼ TopOpen (R (x))))$
30	1 2 15 16 17	prdsbas	$⊢ φ \to {Base}_{Y} = \underset{x \in I}{⨉} {Base}_{R (x)}$
31	30	fveq2d	$⊢ φ \to TopOn ({Base}_{Y}) = TopOn (\underset{x \in I}{⨉} {Base}_{R (x)})$
32	13 29 31	3eltr4d	$⊢ φ \to TopSet (Y) \in TopOn ({Base}_{Y})$
33	16 18	tsettps	$⊢ TopSet (Y) \in TopOn ({Base}_{Y}) \to Y \in TopSp$
34	32 33	syl	$⊢ φ \to Y \in TopSp$

Metamath Proof Explorer

Theorem prdstps

Proof